TL;DR: Stale snapshots from non-garbage actors can prevent actual garbage actors from being detected. I propose a fix. Until this is fixed, it's more important than ever to (a) remove snapshots from QD's state for actors that have self-terminated, and (b) make sure all live actors regularly take snapshots.
In the CONCUR paper, we defined the notion of a "finalized" set of snapshots. It means that the set is "closed" with respect to the potential inverse acquaintance relation, and every actor "appears blocked". We presented an algorithm for finding the maximum finalized subset of a collection of snapshots. We then showed that every actor in a finalized set of snapshots is garbage. This gave us a safe algorithm for finding garbage based on a set of snapshots. We've implemented that algorithm in QuiescenceDetector.scala.
We also gave a liveness property: If every garbage actor in a configuration takes a snapshot, then the resulting set of snapshots is finalized.
But there is a subtle problem in the specification of our maximal finalized set detection algorithm: Given a set S, it finds the largest subset S' that is finalized with respect to S, rather than with respect to S'. It turns out that this subset S' is indeed finalized, but it's not the largest finalized subset of S.
Here's an example. Suppose actors A and B have references to each other and actor C has references to A and another actor D.
C sends D a reference to A. That reference is in now C's "created" set.
C takes a snapshot.
C and D deactivate their references to A.
A receives the Release messages and becomes idle. Now A and B are garbage.
A and B both take snapshots.
If we look only at A and B's snapshots, they form a finalized set. However, if we include C's snapshot, then there appears to be an extra reference from D to A -- so the set {A,B} is no longer closed, and no longer finalized, with respect to the set {A,B,C}.
How do we deal with this problem? By finding the smallest finalized set containing each actor. Finalized sets are closed under union, so we can then merge all these sets and return the result. For A and B, this set is {A,B}. For C and D, there is no such set.
In order to find the smallest finalized set containing an actor A, we trace a path from A to all of its potential inverse acquaintances: If A has an unreleased consistent refob x: B -o A in its owners set, then the set must include B. If B's snapshot includes unreleased consistent y: C -o A in its created set, then the set must also include C; and so on. Notice that in the example above, there's no way to trace a path from the garbage actor A to its old inverse acquaintance C.
TL;DR: Stale snapshots from non-garbage actors can prevent actual garbage actors from being detected. I propose a fix. Until this is fixed, it's more important than ever to (a) remove snapshots from QD's state for actors that have self-terminated, and (b) make sure all live actors regularly take snapshots.
In the CONCUR paper, we defined the notion of a "finalized" set of snapshots. It means that the set is "closed" with respect to the potential inverse acquaintance relation, and every actor "appears blocked". We presented an algorithm for finding the maximum finalized subset of a collection of snapshots. We then showed that every actor in a finalized set of snapshots is garbage. This gave us a safe algorithm for finding garbage based on a set of snapshots. We've implemented that algorithm in
QuiescenceDetector.scala.We also gave a liveness property: If every garbage actor in a configuration takes a snapshot, then the resulting set of snapshots is finalized.
But there is a subtle problem in the specification of our maximal finalized set detection algorithm: Given a set S, it finds the largest subset S' that is finalized with respect to S, rather than with respect to S'. It turns out that this subset S' is indeed finalized, but it's not the largest finalized subset of S.
Here's an example. Suppose actors A and B have references to each other and actor C has references to A and another actor D.
How do we deal with this problem? By finding the smallest finalized set containing each actor. Finalized sets are closed under union, so we can then merge all these sets and return the result. For A and B, this set is {A,B}. For C and D, there is no such set.
In order to find the smallest finalized set containing an actor A, we trace a path from A to all of its potential inverse acquaintances: If A has an unreleased consistent refob
x: B -o Ain its owners set, then the set must include B. If B's snapshot includes unreleased consistenty: C -o Ain its created set, then the set must also include C; and so on. Notice that in the example above, there's no way to trace a path from the garbage actor A to its old inverse acquaintance C.