PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Nisansala P. Yatapanage

arXiv:2609.27392v1cs.LO

TL;DR

Concurrent interference makes it difficult to specify rely and guarantee conditions for the Ben-Ari garbage collector, where memory in use can appear reclaimable. The paper verifies the components using a property proved for all variables in a set and instantiated to the local variable needed by the Collector; the proof establishes conditions under which marking proceeds despite Mutator steps.

  • Problem

    For the Ben-Ari collector, Mutator–Collector interference can make memory in use appear to be garbage, while the reason the algorithm prevents incorrect reclamation is unclear.

    Source: §3.1 · p. 5

  • Method

    The proof establishes a property over all variables in a set, then instantiates it for the local variable needed by the Collector, without cross-component references to local variables.

    Source: §1 · p. 2

  • Results

    Mutator steps either preserve can-be-marked or increase the number of marked nodes, satisfying the Collector’s rely requirements and ensuring another marking round when needed.

    Source: §5.1 · p. 11, §5.2 · p. 12

  • Takeaways & Limitations

    The abstract predicate identifies a core property required by the Collector, clarifying why the algorithm works.

    Source: §1 · p. 3

    Rely conditions cannot express the required order of steps in the middle of an environment block, while the proposed temporal-logic alternative requires reasoning over entire traces rather than single steps or blocks.

    Source: §3.1 · p. 6

Abstract

from arXiv · show

Rely/Guarantee is a well-known verification technique for reasoning about concurrent programs. However, for some algorithms, devising suitable rely and guarantee conditions is challenging, due to the strong interference exhibited in these algorithms. The Ben-Ari concurrent garbage collector is an algorithm where the complex interactions between the components prevent the construction of compositional rely and guarantee conditions. This paper investigates an approach for verifying the Ben-Ari algorithm, which enables reasoning to be performed in a more compositional manner in cases where compositional reasoning would not otherwise be possible. 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. As well as providing a reasoning approach which is more compositional, the result is the identification of the core property required of a component, thus enabling a deeper understanding about the reasons why the algorithm works correctly. This helps to reveal the reasons why the rely/guarantee approach does not work directly for some problems.

1 Introduction

The Ben-Ari collector exposes a rely/guarantee challenge: Mutator–Collector interference can make in-use memory appear reclaimable, while the reason the algorithm prevents this is unclear. The paper uses a general property instantiated to another component’s local variable to reason more compositionally and identify a core correctness property.

1 Introduction

  • Rely/guarantee specifies environmental interference with a rely predicate and process behaviour with a guarantee, requiring each process’s guarantee to satisfy the other’s rely.It works well for many concurrent algorithms, but suitable conditions are difficult to devise for some classes.Source: §1 · p. 1
  • RGSep combines rely/guarantee for shared memory with separation logic for local memory, making it suitable for problems with a separable aspect.Classic rely/guarantee examples include inherently parallel searches with only minor interference.Source: §1 · pp. 1–2
  • Prior work on non-blocking algorithms reports that rely and guarantee conditions can be difficult to devise; possible values were used to describe a variable’s history in the Simpson and Ben-Ari cases [JH16].The cited work also covers concurrent stacks and queues [Yat24].Source: §1 · p. 2
  • In Ben-Ari’s collector, interference can make memory still in use appear to be garbage, although the algorithm prevents incorrect reclamation for reasons that are not obvious.Prior work concluded that suitable rely and guarantee conditions could not be devised without breaking compositionality.Source: §1 · p. 2
  • The proof avoids cross-component references to local variables by proving that a property holds for all variables in a set, then instantiating it for the Collector’s rely.The property bridges the Mutator’s guarantee and the Collector’s rely.Source: §1 · p. 2
  • The abstract predicate identifies a core property required by the Collector and offers insight into why the algorithm works.The approach also separates strongly intertwined behaviour without ghost variables.Source: §1 · p. 3

2 Rely/Guarantee Reasoning

Rely/guarantee reasoning extends Hoare-style reasoning with conditions for environmental interference and process behaviour. Concurrent compatibility requires each process’s guarantee to satisfy the other’s rely, with those conditions holding transitively over environment and program steps.

2 Rely/Guarantee Reasoning

  • Each process’s rely condition specifies what it can handle from the environment, while its guarantee describes what it ensures to do.Figure 1 is identified as an overview of rely/guarantee reasoning.Source: §2 · p. 3, Figure 1 · p. 3
  • Concurrent processes are compatible when each process’s guarantee satisfies the other’s rely condition.Source: §2 · p. 3
  • Rely and guarantee conditions must hold transitively across all environment and program steps, respectively.Source: §2 · p. 3

3 Ben-Ari Concurrent Garbage Collector

The Ben-Ari collector runs mark-and-sweep concurrently with a Mutator, but their interference can cause an in-use node to be reclaimed. The section explains this risk and the algorithm’s core definitions.

3.1 Interference in the Algorithm

  • The Collector’s Mark, Sweep, and Unmark phases run alongside Mutator updates, creating an interleaving in which an in-use node can be swept.After the Mutator redirects A to C and removes B’s link to C, the Collector misses C during marking and later frees it as unmarked.Source: §3 · p. 4, §3.1 · p. 5
  • The Mutator must mark a redirected-to node before another update, so the Collector detects increased marking and runs another cycle.In the example, marking C causes a further cycle that can find C through A’s link.Source: §3.1 · pp. 5–6
  • Rely conditions struggle to express the required redirect–mark–delete order because they relate block start and end states, while temporal logic requires whole-trace reasoning.A shared ghost variable can represent a pending mark, but then the Collector must know which node the Mutator modified.Source: §3.1 · pp. 5–6

3.2 Required Definitions From [JY19]

  • The concrete state uses roots, a heap mapping address-index pairs to addresses, and free addresses; reach follows child links transitively, and the invariant separates free from in-use addresses.These definitions are taken from [JY19].Source: §3.2 · p. 7

4 Rely of the Collector

The Collector’s rely is grounded in a property that can be checked for any set of nodes. A safe subset captures which already-considered nodes may not be revisited, while the Mutator’s actions must preserve a route to eventual marking.

4 Rely of the Collector

  • can-be-marked generalizes the Collector’s requirement to an abstract set: each marked node in that set with an unmarked child must have another route by which the child can eventually be marked.The alternative route is through the roots or a marked node outside the set that remains eligible for marking.Source: §4 · pp. 7–8
  • The safe subset contains considered nodes that still satisfy all-ok when the Mutator interrupts and that the Collector may not necessarily revisit.A newly marked child may already be considered; increased marked-node count makes Propagate run again, but safe identifies nodes that still satisfy all-ok at interruption.Source: §4 · p. 8
  • The rely requires a changed heap target to remain reachable and, when all-ok held, either can-be-marked to hold afterward or the marked-node count to increase.The count increase causes another Propagate cycle.Source: §4 · pp. 7, 9

5 Holds For All Reasoning

Holds For All reasoning lets one component establish another’s rely condition without reasoning about its local variables. Applied to the Mutator, it shows how changes in a set of addresses preserve the Collector’s requirements or trigger another marking round.

5 Holds For All Reasoning

  • Holds For All proves a component’s rely by showing its guarantee preserves a property for every variable, then instantiating the required local variable.The Mutator need not know which addresses are in the Collector’s safe set.Source: §5 · pp. 9–10

5.1 The Mutator Proof Obligations

  • For Mutator steps, all-ok(s) leads to can-be-marked(s) or an increase in marked nodes, satisfying the Collector’s rely across a sequence.MarkTbm uses tbm-put to track a pending node; if the set must shrink to restore all-ok, marked-node growth ensures another round.Source: §5.1 · pp. 10–11

5.2 Showing that rely-Collector holds

  • The Mutator satisfies the remaining Collector-rely clauses directly, while a reduced set is paired with increased marking so another round finds required nodes.The Collector preserves all-ok or can-be-marked; MarkTbm need not increase the marked count when its target is already marked.Source: §5.2 · pp. 11–12

6 Related Work and Conclusion

The paper proposes Holds For All reasoning to verify two-component algorithms without shared auxiliary variables, and identifies can-be-marked as the Collector’s core requirement. It relates this approach to earlier Ben-Ari proofs and notes that mechanisation remains future work.

6 Related Work and Conclusion

  • Holds For All reasons about another component’s local variables without shared auxiliary variables, but its proofs remain to be mechanised.The paper presents it as an approach for algorithms with two components.Source: §6 · p. 12
  • Identifying can-be-marked exposes the Collector’s actual requirement and clarifies why Ben-Ari’s algorithm works.The paper suggests this core property could inform more efficient algorithms, although the proposed alternative of consulting consid would break compositionality.Source: §6 · p. 12
  • Havelund’s PVS and Murφ proofs use 55 lemmas and are non-compositional, while the Owicki-Gries proof uses two auxiliary variables and does not identify can-be-marked.The paper says these examples illustrate difficulties in understanding the required properties and verification details.Source: §6 · p. 12

7 Appendix

The appendix gives the proof of Lemma 1 by considering how a Mutator change affects can-be-marked and tbm-put. Its cases establish vacuous preservation or an alternative path for the relevant node.

7 Appendix

  • If c becomes unreachable after the link change while x is in s and marked, the proof finds a marked ancestor with an unmarked child to preserve an alternative route for c.The argument then uses all-ok and the increased marked set to establish can-be-marked.Source: §7 · p. 14
  • When c lies in s or marked, hp(x,k) is marked and can-be-marked holds vacuously; otherwise c satisfies can-be-marked and provides an alternative path.These are the two cases described for the proof branch involving c.Source: §7 · p. 15
  • The proof derives tbm-put from all-ok and post-Change because the new destination is tbm and no other node in s and marked has unmarked children.Source: §7 · p. 15
Loading 2609.27392v1…