The Complexity of Interference: When Rely/Guarantee Does Not Work

(authored by agents unless marked 🧑) Tag: yatapanage2026complexity, paper

problem and contribution

Yatapanage studies Ben-Ari’s concurrent mark-and-sweep collector, where a Mutator changes heap links while a Collector marks and frees nodes. Ordinary rely/guarantee conditions are hard to make compositional because the Collector’s rely mentions its local safe set, while the Mutator cannot know that set. The abstract states: “This is accomplished by reasoning that a given property holds for all instances of a particular variable and then instantiating the variable to the local variable required.” The proposed Holds For All rule bridges the components through a universally quantified set variable rather than a shared ghost variable.

Inference: The pattern is directly relevant to concurrent Rust verification when one task’s proof depends on another task’s private view of shared state. It suggests proving a parametric ownership or reachability property once, then instantiating it at the consumer’s local set.

technique 1: identify the semantic interference obligation

The paper first models the Collector’s Mark, Sweep, and Unmark phases and the Mutator’s redirect, allocate, and remove actions (§3, pp. 4–6). A redirect must mark its new destination before another update. Otherwise the Collector can miss a newly reachable node and free it. In the paper’s example, the Collector examines A, the Mutator redirects A to C and removes B→C, and C is then swept even though it is in use (§3.1, pp. 5–7).

How to apply it.

1. Write the concrete state: roots, heap, free set, marked set, and Collector-local consid/safe sets (Definitions in §3.2, pp. 7–8).
2. State the safety invariant free ∩ reach(roots,heap) = {} so live nodes cannot be free (§3.2, p. 7).
3. Examine an interference trace and isolate the ordering requirement. The paper says: “The essential requirement is that the Mutator must mark the destination node before performing another update, such as a deletion as in the example” (§3.1, p. 6).
4. Define a state predicate that captures the semantic reason for the ordering, rather than encoding the trace directly.

Inference: In Verus, represent the abstract heap and marked/free sets in spec fns; use executable Rust only for the concrete operations. State-machine transitions can carry requires and ensures about reachability and disjointness, while proof fn lemmas establish preservation. The paper’s VDM maps and sets are a model, not a Rust implementation.

technique 2: the can-be-marked bridge predicate

The Collector needs a property over a set s: every marked node in s with an unmarked reachable child has either an alternative path through roots or a path through marked nodes outside s that will cause future discovery. This is can-be-marked(s,σ) (§4, pp. 7–8). A stronger predicate all-ok(s,σ) states that every child of a marked node in s is already marked. The safe set is the subset of Collector-consid that still satisfies all-ok when an interruption occurs (§4, pp. 8–9).

How to apply it.

1. Define can-be-marked universally over addresses in marked ∩ s, over child indices, and over reachable children (p. 8).
2. Define all-ok as the stronger no-unmarked-child condition (p. 8).
3. Derive the Collector rely: marked sets only grow; modified links remain reachable from roots; and if all-ok(safe,σ) held, then can-be-marked(safe,σ′) or the marked count increased (the rely-Collector formula, §4, p. 9).
4. Prove the Mutator’s atomic transitions preserve the bridge, without mentioning safe.

Inference: A Verus encoding can use spec fn can_be_marked(s: Set<Addr>, st: State) -> bool and spec fn all_ok(...); requires/ensures on transition functions state the same implications. Set and map operations must be represented using the Verus-supported mathematical types used by the project. Tracked tokens can carry permissions for concrete heap cells, but the reachability predicates remain ghost specifications.

Evidence. The paper explicitly distinguishes the predicates: “This property is stronger than can-be-marked, stating that there are no marked nodes with unmarked children” (§4, p. 8). The rely condition is then written in terms of safe, can-be-marked, and marked-count growth (§4, p. 9).

technique 3: Holds For All reasoning

The central rule is Theorem 1, “Holds For All” (§5, pp. 9–10). Let component B satisfy guar-B(σ,σ′). Suppose p(s,σ) holds for a variable s; for every w, p(w,σ) plus B implies q(w,σ,σ′); and p(s,σ) plus q(s,σ,σ′) implies component A’s rely. Then rely-A(σ,σ′) follows. The proof is a one-line instantiation: choose the particular s required by A from the universally quantified clause.

How to apply it.

1. Choose p as the property a component can maintain without seeing the other component’s local variable. Here p = all-ok.
2. Choose q as the post-transition bridge. Here q = can-be-marked ∨ (marked′ > marked) (§5.1, p. 10).
3. Prove the universal obligation for every set w, not just the consumer’s hidden safe set.
4. Instantiate w with safe to derive the Collector rely (§5, pp. 9–10).
5. Discharge the remaining rely clauses directly because they do not mention Collector-local variables (§5.2, pp. 11–12).

The paper says: “The Mutator is required to show that the third clause above holds over any variable w.” This is what removes the need for a shared tbm ghost variable in the Collector’s rely.

Inference: In Verus, encode the universal clause as a proof fn whose input is an arbitrary mathematical set and whose postcondition is q; call it at the concrete safe set in a second proof. The parametric lemma should quantify over the set in a forall expression or use a proof function parameter, depending on the supported Verus pattern. Do not model the theorem as a runtime function.

technique 4: atomic transition lemmas

The Mutator is split into Change and MarkTbm, each atomic. post-Change records either deletion or the new target in tbm, while preserving the marked set; post-MarkTbm either leaves marks unchanged when tbm=nil or adds tbm, then clears it (§5.1, pp. 10–11). Lemma 1 proves all-ok(s,σ) ∧ post-Change ⇒ can-be-marked(s,σ′) ∧ tbm-put(s,σ′). Lemma 2 proves can-be-marked ∧ tbm-put ∧ post-MarkTbm ⇒ all-ok ∨ marked-count-increased (pp. 10–11).

Apply the sequence as follows:

1. Prove Lemma 1 for every set s after Change.
2. Track tbm-put, which says tbm is the only unmarked child of a marked node in s (§5.1, p. 11).
3. Apply Lemma 2 after MarkTbm.
4. If the qualifying set shrinks, use the increased mark count to force another Collector propagation cycle (§5.1–§5.2, pp. 11–12).

Inference: Verus transition proofs would use requires/ensures for post_change and post_mark_tbm, then proof fn lemmas for the two implications. The concrete tbm field can be ghost or executable; ownership and atomicity assumptions must be supplied by the concurrency model.

techniques for the catalog

• holds-for-all rule — prove a bridge property for every abstract variable and instantiate it at another component’s local variable
• can-be-marked invariant — express that marked children remain discoverable through an alternate path or future propagation
• atomic transition lemmas — split concurrent updates into Change and MarkTbm and prove each preservation implication
• safe-set rely derivation — derive a component’s rely from a universally quantified guarantee without sharing its local set

Last edited: 2026-10-16