pith. sign in

arxiv: 2605.19237 · v1 · pith:7X2RDTVRnew · submitted 2026-05-19 · 💻 cs.DC

Generalized Compare-and-Swap and Space-Efficient Universal Constructions for the Infinite-Arrival Model

Vassos Hadzilacos , Myles Thiessen , Sam Toueg This is my paper

Pith reviewed 2026-05-20 03:13 UTC · model grok-4.3

classification 💻 cs.DC
keywords generalized compare-and-swapuniversal constructionwait-freeinfinite-arrival modelspace complexitymemory recyclingpoint contentiondistributed computing
0
0 comments X

The pith

Generalized compare-and-swap supports the first wait-free universal constructions with space linear in participated processes or point contention for the infinite-arrival model.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces GCAS as a natural extension of compare-and-swap that replaces the fixed equality test with a comparator chosen from the set {<, =, >}. It then deploys this object to construct two wait-free universal objects for the infinite-arrival model, where the set of participating processes is unknown in advance and may grow without bound. The first construction uses space linear in the total number of processes observed so far; the second achieves space linear in instantaneous point contention by means of a new memory-recycling technique, but only under the added premise of bounded concurrency. A reader would care because unbounded memory growth has been a standing obstacle to practical wait-free synchronization when process participation cannot be bounded in advance. The authors present both constructions as the first to reach these space bounds in the infinite-arrival setting.

Core claim

By generalizing the equality test of CAS to a parametrized comparator drawn from {<, =, >}, GCAS permits two space-efficient wait-free universal constructions in the infinite-arrival model: one whose space is linear in the number of processes that have participated so far, and a second whose space is linear in point contention (via a novel memory-recycling scheme) when concurrency is bounded. These are claimed to be the first such wait-free constructions achieving the stated space complexities in the infinite-arrival model.

What carries the argument

GCAS, a compare-and-swap object whose equality test is replaced by a user-chosen comparator from the set {<, =, >}.

If this is right

  • Universal constructions become feasible with space linear in the number of processes observed so far, without a priori knowledge of the process set.
  • Under bounded concurrency, space can be reduced further to linear in instantaneous point contention through explicit memory reuse.
  • The recycling scheme itself operates correctly in the infinite-arrival model provided concurrency remains bounded.
  • Both constructions remain wait-free while respecting the stated space bounds.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same recycling technique might be adapted to other linearizable objects that must tolerate unbounded process arrivals.
  • Space bounds linear in point contention could become a target for additional synchronization primitives once bounded concurrency is assumed.
  • Implementations could test whether GCAS itself admits a constant-space wait-free realization under the same model restrictions.

Load-bearing premise

The second construction relies on the assumption of bounded concurrency to keep space linear in point contention while employing the memory-recycling scheme.

What would settle it

An execution in the infinite-arrival model with unbounded concurrency in which any wait-free universal construction that uses the described recycling scheme is forced to allocate more than a constant number of words per point-contention value.

Figures

Figures reproduced from arXiv: 2605.19237 by Myles Thiessen, Sam Toueg, Vassos Hadzilacos.

Figure 1
Figure 1. Figure 1: CAS and GCAS operations. 1 Introduction We propose a natural generalization of compare-and-swap (CAS), a fundamental object in shared memory systems, and show how it enables space-efficient, wait-free universal constructions in systems where the number of participating processes is unknown and may be infinite (this is the infinite-arrival model introduced by Merrit and Taubenfeld [18]). This model encourag… view at source ↗
read the original abstract

We introduce GCAS, a natural generalization of the well-known compare-and-swap (CAS) object. Intuitively, GCAS just replaces the fixed equality test of CAS with a parametrized comparator chosen from $\{<, =, >\}$. To showcase the utility of GCAS, we present two space-efficient wait-free universal constructions for systems where the number of participating processes is unknown and may be infinite (the infinite-arrival model). The first has space-complexity linear in the number of processes that have participated so far, while the second has space-complexity linear in the point contention but assumes bounded concurrency. To the best of our knowledge, these are the first wait-free universal constructions that achieve this space complexity in the infinite-arrival model. To achieve space complexity linear in the point contention, our second universal construction uses a novel memory recycling scheme that works in the infinite-arrival model with bounded concurrency. The ideas behind this recycling scheme could be of more general use.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The paper introduces GCAS, a generalization of compare-and-swap that replaces the fixed equality test with a parametrized comparator chosen from {<, =, >}. It then presents two wait-free universal constructions for the infinite-arrival model (unknown and possibly infinite number of processes). The first construction has space complexity linear in the number of processes that have participated so far. The second achieves space linear in point contention under a bounded-concurrency assumption, using a novel memory recycling scheme. The authors claim these are the first wait-free universal constructions with these space bounds in the infinite-arrival model.

Significance. If the constructions and their proofs are correct, the results would be significant for distributed computing: they provide the first space-efficient wait-free universal constructions in the infinite-arrival model, addressing a key challenge when the number of participants is unbounded. The memory recycling scheme for the second construction could have broader applicability beyond universal constructions. The work strengthens the toolkit for designing efficient concurrent objects in dynamic systems.

major comments (2)
  1. [§4.2, Theorem 2] §4.2, Theorem 2: the proof of wait-freedom for the second construction relies on the bounded-concurrency assumption to bound the recycling scheme; it is unclear whether the linear-in-point-contention bound holds if concurrency is unbounded even for finite periods, as the recycling may then require unbounded space in the worst case.
  2. [§3.1, Definition 1] §3.1, Definition 1: the GCAS specification is given in terms of a linearizable object with the parametrized comparator, but the paper does not explicitly state whether the implementation of GCAS itself is wait-free or only lock-free; this affects the overall wait-freedom claim of the universal constructions that build on it.
minor comments (3)
  1. [Abstract and §1] The abstract and introduction should clarify whether the first construction requires any additional assumptions beyond the infinite-arrival model.
  2. [Figure 1] Figure 1 (pseudocode for GCAS) uses notation for the comparator that is not defined until §3.2; move the definition earlier for readability.
  3. [§1] Missing reference to prior work on universal constructions in the infinite-arrival model (e.g., the 2018 PODC paper on wait-free objects with unknown participants).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment of our work and for the constructive comments. We address each major comment below.

read point-by-point responses

  1. Referee: [§4.2, Theorem 2] the proof of wait-freedom for the second construction relies on the bounded-concurrency assumption to bound the recycling scheme; it is unclear whether the linear-in-point-contention bound holds if concurrency is unbounded even for finite periods, as the recycling may then require unbounded space in the worst case.

    Authors: We thank the referee for this observation. The second construction is explicitly presented under the bounded-concurrency assumption, as stated in the abstract and Section 4.2. The memory recycling scheme is designed to keep space linear in point contention precisely because the assumption bounds the number of concurrently active processes at any time, which in turn bounds the memory allocated before recycling completes. The wait-freedom argument in Theorem 2 relies on this bound. We agree that the linear space claim would not hold in general without the assumption, since temporary unbounded concurrency could cause unbounded allocation. In the revision we will add a clarifying sentence in Section 4.2 stating that the linear-in-point-contention bound requires bounded concurrency. revision: yes

  2. Referee: [§3.1, Definition 1] the GCAS specification is given in terms of a linearizable object with the parametrized comparator, but the paper does not explicitly state whether the implementation of GCAS itself is wait-free or only lock-free; this affects the overall wait-freedom claim of the universal constructions that build on it.

    Authors: We appreciate the referee pointing out this lack of explicitness. The GCAS implementation in Section 3.1 is wait-free: each operation performs a bounded number of steps using the underlying wait-free CAS primitive, independent of the number of processes. The two universal constructions then compose this wait-free GCAS to obtain wait-freedom for arbitrary objects. We will revise Section 3.1 to state explicitly that the GCAS implementation is wait-free, thereby clarifying the source of wait-freedom for the constructions. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper directly defines GCAS as a parametrized generalization of CAS with comparator chosen from {<, =, >} and then describes two explicit algorithmic universal constructions for the infinite-arrival model, with the second construction's space bound qualified by an explicit bounded-concurrency assumption and a novel recycling scheme. No load-bearing step reduces a claimed result to a fitted parameter, self-referential definition, or unverified self-citation chain; the constructions are presented as self-contained algorithms whose correctness rests on standard wait-free techniques rather than equations that loop back to their own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Review based on abstract only; no explicit free parameters, invented entities, or non-standard axioms are mentioned. Standard distributed-computing assumptions such as asynchronous shared memory and wait-freedom are implicitly used.

axioms (1)
  • domain assumption Standard model assumptions for wait-free algorithms in asynchronous shared-memory systems with infinite arrivals.
    Typical background for the subfield; invoked implicitly by the problem statement.

pith-pipeline@v0.9.0 · 5705 in / 1114 out tokens · 33040 ms · 2026-05-20T03:13:48.741338+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

77 extracted references · 77 canonical work pages

  1. [1]

    Common2 extended to stacks and unbounded concurrency

    Yehuda Afek, Eli Gafni, and Adam Morrison. “Common2 extended to stacks and unbounded concurrency”. In: Proceedings of the twenty-fifth annual ACM symposium on Principles of distributed computing. 2006, pp. 218–227

    work page 2006

  2. [2]

    A pleasant stroll through the land of infinitely many creatures

    Marcos K Aguilera. “A pleasant stroll through the land of infinitely many creatures”. In: ACM Sigact News 35.2 (2004), pp. 36–59

    work page 2004

  3. [3]

    Concurrent deferred reference counting with constant-time overhead

    Daniel Anderson, Guy E Blelloch, and Yuanhao Wei. “Concurrent deferred reference counting with constant-time overhead”. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation . 2021, pp. 526–541

    work page 2021

  4. [4]

    Wait-free consensus with infinite arrivals

    James Aspnes, Gauri Shah, and Jatin Shah. “Wait-free consensus with infinite arrivals”. In: Proceedings of the thiry-fourth annual ACM symposium on Theory of computing . 2002, pp. 524–533

    work page 2002

  5. [5]

    Wait-free Algorithms: the Burden of the Past

    Denis B´ edin et al. “Wait-free Algorithms: the Burden of the Past”. In: (2024). url: https: //doi.org/10.21203/rs.3.rs-4125819/v1

    work page doi:10.21203/rs.3.rs-4125819/v1 2024

  6. [6]

    Wait-Free CAS-Based Algorithms: The Burden of the Past

    Denis B´ edin et al. “Wait-Free CAS-Based Algorithms: The Burden of the Past”. In: 35th International Symposium on Distributed Computing (DISC 2021) . Schloss-Dagstuhl-Leibniz Zentrum f¨ ur Informatik. 2021

    work page 2021

  7. [7]

    Reclaiming memory for lock-free data structures: There has to be a better way

    Trevor Alexander Brown. “Reclaiming memory for lock-free data structures: There has to be a better way”. In: Proceedings of the 2015 ACM Symposium on Principles of Distributed Computing. 2015, pp. 261–270

    work page 2015

  8. [8]

    Differentiated nonblocking: a new progress condition and a matching queue algorithm

    David YC Chan et al. “Differentiated nonblocking: a new progress condition and a matching queue algorithm”. In: arXiv preprint arXiv:2103.11926 (2021)

    work page arXiv 2021

  9. [9]

    Lock-free reference counting

    David L Detlefs et al. “Lock-free reference counting”. In: Proceedings of the twentieth annual ACM symposium on Principles of distributed computing . 2001, pp. 190–199

    work page 2001

  10. [10]

    The concurrency hierarchy, and algorithms for unbounded concurrency

    Eli Gafni, Michael Merritt, and Gadi Taubenfeld. “The concurrency hierarchy, and algorithms for unbounded concurrency”. In: Proceedings of the twentieth annual ACM symposium on Principles of distributed computing . 2001, pp. 161–169

    work page 2001

  11. [11]

    Generalized Compare and Swap

    Vassos Hadzilacos, Myles Thiessen, and Sam Toueg. “Generalized Compare and Swap”. In: arXiv preprint arXiv:2410.19102 (2024)

    work page arXiv 2024

  12. [12]

    Wait-free synchronization

    Maurice Herlihy. “Wait-free synchronization”. In: ACM Transactions on Programming Lan- guages and Systems (TOPLAS) 13.1 (1991), pp. 124–149

    work page 1991

  13. [13]

    The repeat offender problem: A mech- anism for supporting dynamic-sized, lock-free data structures

    Maurice Herlihy, Victor Luchangco, and Mark Moir. “The repeat offender problem: A mech- anism for supporting dynamic-sized, lock-free data structures”. In: International Symposium on Distributed Computing . Springer. 2002, pp. 339–353

    work page 2002

  14. [14]

    Nonblocking memory management support for dynamic-sized data structures

    Maurice Herlihy et al. “Nonblocking memory management support for dynamic-sized data structures”. In: ACM Transactions on Computer Systems (TOCS) 23.2 (2005), pp. 146–196. 16

    work page 2005

  15. [15]

    Linearizability: A correctness condition for con- current objects

    Maurice P Herlihy and Jeannette M Wing. “Linearizability: A correctness condition for con- current objects”. In: ACM Transactions on Programming Languages and Systems (TOPLAS) 12.3 (1990), pp. 463–492

    work page 1990

  16. [16]

    Efficiently implementing a large number of LL/SC objects

    Prasad Jayanti and Srdjan Petrovic. “Efficiently implementing a large number of LL/SC objects”. In: International Conference On Principles Of Distributed Systems . Springer. 2005, pp. 17–31

    work page 2005

  17. [17]

    Efficiently implementing LL/SC objects shared by an unknown number of processes

    Prasad Jayanti and Srdjan Petrovic. “Efficiently implementing LL/SC objects shared by an unknown number of processes”. In: International Workshop on Distributed Computing . Springer. 2005, pp. 45–56

    work page 2005

  18. [18]

    Computing with infinitely many processes

    Michael Merritt and Gadi Taubenfeld. “Computing with infinitely many processes”. In: In- formation and Computation 233 (2013), pp. 12–31

    work page 2013

  19. [19]

    Hazard pointers: Safe memory reclamation for lock-free objects

    Maged M Michael. “Hazard pointers: Safe memory reclamation for lock-free objects”. In: IEEE Transactions on Parallel and Distributed Systems 15.6 (2004), pp. 491–504

    work page 2004

  20. [20]

    Safe memory reclamation for dynamic lock-free objects using atomic reads and writes

    Maged M Michael. “Safe memory reclamation for dynamic lock-free objects using atomic reads and writes”. In: Proceedings of the twenty-first annual symposium on Principles of distributed computing. 2002, pp. 21–30

    work page 2002

  21. [21]

    Hyaline: fast and transparent lock-free memory recla- mation

    Ruslan Nikolaev and Binoy Ravindran. “Hyaline: fast and transparent lock-free memory recla- mation”. In: Proceedings of the 2019 ACM Symposium on Principles of Distributed Comput- ing. 2019, pp. 419–421

    work page 2019

  22. [22]

    Snapshot-free, transparent, and robust memory reclamation for lock-free data structures

    Ruslan Nikolaev and Binoy Ravindran. “Snapshot-free, transparent, and robust memory reclamation for lock-free data structures”. In: Proceedings of the 42nd ACM SIGPLAN Inter- national Conference on Programming Language Design and Implementation . 2021, pp. 987– 1002

    work page 2021

  23. [23]

    Extending the wait-free hier- archy to multi-threaded systems

    Matthieu Perrin, Achour Mostefaoui, and Gr´ egoire Bonin. “Extending the wait-free hier- archy to multi-threaded systems”. In: Proceedings of the 39th Symposium on Principles of Distributed Computing. 2020, pp. 21–30

    work page 2020

  24. [24]

    Lock-free linked lists using compare-and-swap

    John D Valois. “Lock-free linked lists using compare-and-swap”. In: Proceedings of the four- teenth annual ACM symposium on Principles of distributed computing . 1995, pp. 214–222. 17 Appendix Contents A Model 19 B Proof of Algorithm 1 20 B.1 Basic Facts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 B.2 Step Complexi...

    work page 1995

  25. [25]

    There is an operation o′ ∈ S(o) that is done at some time T1 during P . 26

    work page

  26. [26]

    o′ is stored in A at some time T2 during P

    work page

  27. [27]

    correctness- preserving mapping

    Some operation o∗ ̸= o′ is stored in A at some time T3 during P such that T3 > max(T1, T2). The bulk of the work is to prove that every non-initial period is useful. The next two lemmas motivate why we consider non-initial periods instead of periods. Roughly speaking, by discarding the first iteration of the loop within an operation o, we don’t need to wo...

    work page

  28. [28]

    If during this step p performs an AllocateCell operation on the memory manager whose response is ptr, then the state assigned to each object of the cell pointed to by ptr in C′ is the initial state specified in Algorithm 2

    work page

  29. [29]

    for every implemen- tation history I B of B

    If during this step p performs an operation o on an object of a cell whose pointer is not in the state assigned to the memory manager in C, then the response of o is arbitrary. Definition C.0.2 (B). Algorithm B is Algorithm 2 using the “lazy” memory manager given in Algorithm 4. 9 In contrast to algorithm A, AllocateCell operations do not change the state...

    work page

  30. [30]

    Every list-add attempt for some ptr after some curr ptr in I B is preceded by a unique L-add event for ptr; furthermore, if I is the prefix of I B up to but excluding that L-add event, curr ptr is the second last pointer in List(I) — i.e., the one preceding Null

    work page

  31. [31]

    Invariant R(I B): All of the following are true for any two successive L-events e and e′ in I B:

    Every list-remove attempt for some ptr between some prev ptr and some next ptr in I B is preceded by a unique L-remove event for ptr; furthermore, if I is the prefix of I B up to but excluding that L-remove event, ptr is in List(I) exactly once and prev ptr and next ptr are the pointers preceding and succeeding ptr in List(I). Invariant R(I B): All of the...

    work page

  32. [32]

    If e is an L-add event for ptr, then the interval betweene and e′ contains one successfullist-add attempt for ptr and no other successful list-add or list-remove attempt for any pointer. 40

    work page

  33. [33]

    If e is an L-apply event, then the interval between e and e′ contains no successful list-add or list-remove attempts for any pointer

    work page

  34. [34]

    If e is an L-remove event for ptr, the interval between e and e′ contains one successful list- remove attempt for ptr and no other successful list-remove or list-add attempt for any pointer. Invariant O(I B): All of the following are true for any two successive L-events e and e′ in I B: • If e is an L-add or L-remove event, then the interval between e and...

    work page

  35. [35]

    a is an add-response-set attempt if and only if I was invoked during an invocation of the DoAddCell procedure

    work page

  36. [36]

    a is a remove-response-set attempt if and only if I was invoked during an invocation of the DoRemoveCell procedure

    work page

  37. [37]

    C.1.2 A-events, L-events, S-attempts, and list-attempts We start with some facts about A-events

    a is an apply-response-set attempt if and only if I was invoked during an invocation of the DoApply&CopyResponse procedure. C.1.2 A-events, L-events, S-attempts, and list-attempts We start with some facts about A-events. Proposition C.1.13. Every A-event in I B is for a timestamp larger than 0. Proof. Consider any A-event e for some timestamp t executed b...

    work page

  38. [38]

    for every implementation history I B of B

    is an L-add event for curr ptr (resp. ptr), by Definition C.1.7, curr ptr and ptr are successive elements of List(I2), and so curr ptr appears immediately before ptr in List(I2) as required. Lemma C.1.115 Lemma C.1.116. Suppose P (I B) holds. For every finite prefix I of I B if ptr ∈ List(I), then there are no L-remove events for ptr in I and there are no...

    work page

  39. [39]

    if I has at least one L-event, the last L-event in I denoted by e is a L-add or L-remove event, and from e onwards in I there are no successful list-add or list-remove attempts, then the list of cells conforms to List(I exclude e ) in I where I exclude e is the prefix of I up to but excluding e

    work page

  40. [40]

    otherwise, the list of cells conforms to List(I) in I. Proof. Let P(n) be the predicate: for every implementation history I of B of n steps, if P (I), Q(I), and R(I) hold, then the list of cells conforms to either one of two sequences in I as described in the statement of the lemma. We prove P(n) by induction on n. Base Case. P(0). Let I0 be an implementa...

    work page

  41. [41]

    In has at least one L-event

    work page

  42. [42]

    e is the last L-event in In and it is an L-add or L-remove event

    work page

  43. [43]

    From e onwards in In there are no successful list-add or list-remove attempts

    work page

  44. [44]

    The list of cells conforms to List(I exclude e ) in In where I exclude e is the prefix of In up to but excluding e. Proof. First 1. Since e is the corresponding L-event of s, by Corollary C.1.37, e < s . Hence, since s is the only step in In+1 not in In, we have that e is in In. Therefore, In has at least one L-event. Now 2. Since by 1 e is in In, by Clai...

    work page

  45. [45]

    if (∗curr ptr).next.ptr = Null at T 104, then I’s response is (NotFound, ∗); otherwise

    work page

  46. [46]

    I’s response is (Found, next ptr) where (∗curr ptr).next.ptr = next ptr at T 104. Proof. Since L.ullo = ulloL at T 105, it follows that p finds the condition on line 105 to be false at T 105. Hence, since p exits I, p executes line 107 after T 105 during I. Let T 107 be the time of p’s next execution of line 107 after T 105. By definition T 104 < T 105 < ...

    work page

  47. [47]

    if target ptr ∈ List(I), then status = Found; and

    work page

  48. [48]

    traverses

    if target ptr ̸∈ List(I), then status = NotFound. Proof. We start by showing that our first assumption implies the following claim. As we will see, this claim is useful for satisfying the conditions of Lemma C.2.11 and our second assumption. Claim C.2.12.1. Consider any invocation I ∗ of the AcquireNext procedure on line 95 during I. Note that since I exi...

    work page

  49. [50]

    99 Proof

    T 104 I ∗ ∈ (e, T exit]. 99 Proof. First 1. Since I ∗ began and exited during the loop on line 46 in I, all steps during the loop on line 46 during I are during ( e, T exit], and by (*) L.ullo = ulloL throughout (e, T exit], we have that L.ullo = ulloL throughout I ∗. Hence, since T 105 I ∗ is the time of a step during I ∗, we have that L.ullo = ulloL at ...

    work page

  50. [51]

    if ptr ∈ List(I), then status = Found; and

    work page

  51. [52]

    if ptr /∈ List(I), then status = NotFound. Proof. Suppose p read ulloL from L.ullo on line 14 during I; say at time T 14. Let I ′ be the invocation of the Acquire procedure on line 80 during I. We satisfy the conditions of Lemma C.2.12 for I ′. Since p read ulloL from L.ullo on line 14 during I and p read (∗, ptr) from A on line 22 during I, we have that ...

    work page

  52. [53]

    by Claim C.2.19.1 L.ullo = ulloL at the end of I ∗ and 2. by Claim C.2.19.2 the list of cells conforms to List(I) in I ∗, and so by Lemma C.2.12, if ptr ∈ List(I), then status = Found, and if ptr /∈ List(I), then status = NotFound as wanted. Lemma C.2.19 We now prove that the IsDone procedure has the intended effect for each type of low-level operation th...

    work page

  53. [54]

    If p received NotDone on line 23 during I, then there is no L-add event for ptr in I; and

    work page

  54. [55]

    If p received Done on line 23 during I, then there is a L-add event for ptr in I. Proof. Since p read ((∗, AddCell), ptr) from A during I, and A is initially ((0, Noop), (0, Null)), we have that A was set to (( ∗, AddCell), ptr), and so by Observation C.1.6 some A-event a 109 set A = (( ∗, AddCell), ptr). Hence, by Definition C.1.5, this is an A-add event...

    work page

  55. [56]

    If p received NotDone on line 23 during I, then there is no L-apply event for ptr in I; and

    work page

  56. [57]

    If p received Done on line 23 during I, then there is a L-apply event for ptr in I B. Proof. Since p read (( ∗, ⟨Apply&CopyResponse, ∗⟩), ptr) from A during I, and A is initially ((0, Noop), (0, Null)), we have that A was set to (( ∗, ⟨Apply&CopyResponse, ∗⟩), ptr), and so by Observation C.1.6 some A-event a set A = ((∗, ⟨Apply&CopyResponse, ∗⟩), ptr). He...

    work page

  57. [58]

    If p received NotDone on line 23 during I, then there is no L-remove event for ptr in I; and

    work page

  58. [59]

    I”, and I is plugged in for “ I B

    If p received Done on line 23 during I, then there is a L-remove event for ptr in I. Proof. Since p read (( ∗, RemoveCell), ptr) from A on line 22 during I, and the value of A is initially (( ∗, Noop), (∗, Null)), we have that A was set to (( ∗, RemoveCell), ptr). Hence, by Observation C.1.6, there is an A-event eremove that sets A = ((∗, RemoveCell), ptr...

    work page

  59. [60]

    L.ullo = ulloL at T 105 I ∗ ; and

    work page

  60. [61]

    traverses

    T 104 I ∗ ∈ (e, T 35]. Proof. Since I ∗ began and exited during I, and all steps during I are after e, we have that all steps during I ∗ are after e. Furthermore, since T 35 is the only time p executes line 35 during I, it follows that I ∗ exited before T 35, and so all steps during I ∗ are during ( e, T 35]. Now 1. Since e set L.ullo = ulloL and by Claim...

    work page

  61. [62]

    L.ullo = ulloL at T 105 I ∗ ; and 119

    work page

  62. [63]

    moreover

    T 104 I ∗ ∈ (e, T 59]. Proof. Since I ∗ began and exited during I, and all steps during I are after e, we have that all steps during I ∗ are after e. Furthermore, since T 59 is the last time p executes line 59 during I, it follows that I ∗ exited before T 59, and so all steps during I ∗ are during ( e, T 59]. Now 1. Since e set L.ullo = ulloL and by Claim...

    work page

  63. [66]

    Theorem (B is Space-Efficient)

    Every operation on an object of the cell pointed to by ptr in I B is after an AllocateCell operation whose response is ptr, and is before any FreeCell (ptr) operation. Theorem (B is Space-Efficient). Suppose I B is finite. Let Allocate(I B) be the set of pointers which have been allocated in I B, i.e., ptr ∈ Allocate(I B) if and only if there is an Alloca...

    work page

  64. [67]

    If the process that executed opx executed line 2 during opx with response ptropx, then for every ptr ̸= ptropx R(I B, opx, ptr) ≥ 0, and R(I B, opx, ptropx) ≥ −1

    work page

  65. [68]

    Otherwise, R(I B, opx, ptr) ≥ 0 for every ptr. We now prove the second property of this section, which is, roughly speaking, that the process that executed opx only performs an operation on an object of the cell when it has the right to use it. We start with a few observations regarding R at the beginning of every iteration of the loops on lines 30, 46, a...

    work page

  66. [69]

    if the last step of I B is on line 5, 12, 13, or 113 during an invocation of the Relinquish procedure invoked on line 7, then R(I −, opx, ptr) ≥ 0

    work page

  67. [70]

    clean up

    otherwise, R(I −, opx, ptr) ≥ 1 where I − is the prefix of I B excluding the last step. Proof. Let p be the process that executed opx. Observe that the last step of I B is either on line 5, 12, 13, 34, 36, 53, 54, 55, 56, 58, 61, 62, 77, 88, 104, 109, and 113. The proof is by cases. Case 1. The last step of I B is either on line 5, 12, or 13. Hence, p exe...

    work page

  68. [72]

    if I is the prefix of I B up to and including e then A(I, ptr) = A(I B, ptr). Since by Lemma C.5.4 there is at most one acquire-copy event for ptr, (1) of this lemma states that the process that performs an acquire-copy event e for ptr “knows” the total number of successful list-acquire-next attempts that will ever happen for ptr, and (2) states that all ...

    work page

  69. [73]

    e = F&A((∗ptr).revocations, −(A(I B, ptr) + 1)); and

    work page

  70. [74]

    if I is the prefix of I B up to and including e then A(I, ptr) = A(I B, ptr). Proof. Let p be the process that executed e and let I be the invocation of the DoRemoveCell procedure that e was executed during. Hence, by Lemma C.1.96 ptr ∈ C and by Definition C.1.5 the second parameter of I is ptr. Furthermore, by Lemma C.1.95, p performed a successful list-...

    work page

  71. [75]

    There is at most one AllocateCell operation whose response isptr, and at most one FreeCell(ptr) operation in I B

    work page

  72. [76]

    If there is a FreeCell (ptr) operation in I B, then it is after an AllocateCell operation whose response is ptr

    work page

  73. [77]

    tracking

    Every operation on an object of the cell pointed to by ptr in I B is after an AllocateCell operation whose response is ptr, and is before any FreeCell (ptr) operation. Proof. Algorithm 4 and Lemma C.5.6 imply 1, Lemma C.5.7 implies 2, and Propositions C.5.47 and C.5.50 imply 3. Theorem C.5.51 194 C.5.5 B is space-efficient This section proves the B is spa...

    work page

  74. [78]

    If pi does not set the jth index of O during the ith step of I A, then Wi(O, j) = Wi−1(O, j).17

    work page

  75. [79]

    If O is a local variable of pi other than its program counter, then: (a) If O is the local variable ptr of pi on line 2, and pi sets the jth index of O to vj during the ith step of I A because pi performs an AllocateCell operation whose response is vj, then Wi(O, j) = i. (b) If pi sets the jth index of O to vj during the ith step of I A because pi perform...

    work page

  76. [80]

    rename” pointers in A to “fresh

    If O is a base object, and pi sets the jth index of O to vj during the ith step of I A because the kth index of one of pi’s local variables O′ in CA i−1 is vj, then Wi(O, j) = Wi−1(O′, k). In all other cases Wi(O, j) = ⊥. So, by definition, Wi(O, j) ∈ N ∪ {⊥}. 17Note that this is not equivalent to saying that the jth index of O is the same in C A i−1 and ...

    work page

  77. [81]

    externally

    Thus, on+1 is a write operation for a value Sn(ullo, 1), Sn(ullo, 2), Null. Therefore, since Sn+1(O) = Sn(ullo, 1), Sn(ullo, 2), Null and on+1 is an operation on O∗, we have that CB n+1 assigns state Sn+1(O) to O∗. Furthermore, since oA n+1 and on+1 are both write operations, their responses are both Done. Case 3. oA n+1 is a F&A operation. Observe that o...

    work page