subfigwrapmmO #1

# Declarative Linearizability Proofs for Descriptor-Based Concurrent Helping
Algorithms

Jesús Domínguez  IMDEA Software Institute, Spain  Universidad Politécnica de
Madrid, Spain  Aleksandar Nanevski  IMDEA Software Institute, Spain

###### Abstract

Linearizability is a standard correctness criterion for concurrent algorithms,
typically proved by establishing the algorithms’ linearization points.
However, relying on linearization points leads to proofs that are
implementation-dependent, and thus hinder abstraction and reuse. In this paper
we show that one can develop more declarative proofs by foregoing
linearization points and instead relying on a technique of axiomatization of
visibility relations. While visibility relations have been considered before,
ours is the first study where the challenge is to formalize the helping nature
of the algorithms. In particular, we show that by axiomatizing the properties
of separation between events that contain bunches of help requests, we can
extract what is common for high-level understanding of several descriptor-
based helping algorithms of Harris et al. (RDCSS, MCAS, and optimizations),
and produce novel proofs of their linearizability that share significant
components.

##  1 Introduction

_Helping_ is a design principle for concurrent algorithms in which a process
carries out work for other processes. Helping is useful for achieving lock-
free and wait-free implementations, because whenever a process $p$ becomes
stuck, other processes can help $p$ make progress, or $p$ itself can help the
process that is in its way, so that $p$ can continue [5, 4, 2]. Helping
algorithms are often equipped with _descriptors_ , which are structures that a
process uses to signal that it requests help with its task. Whenever a process
$p$ finds a descriptor in some pointer $x$, it means that some other process
$q$ has requested help with computing the value of $x$. Process $p$ then
extracts $q$’s task information from the descriptor and $p$ _fully_ helps
until $q$’s task terminates; only then, $p$ attempts its own task.

In this paper, we focus on proving correct two descriptor-based helping
algorithms: RDCSS and MCAS [11]. _Restricted Double-Compare Single Swap
(RDCSS)_ is a generalization of the compare-and-swap operation CAS. Whereas
$\textit{CAS}\,(pt_{2},exp_{2},new_{2})$ updates $pt_{2}$ with $new_{2}$ if
the old value of $pt_{2}$ is $exp_{2}$, RDCSS adds another pointer $pt_{1}$
and value $exp_{1}$ into the decision. More precisely, RDCSS receives as input
a descriptor that is a record with five pieces of data: two pointers $pt_{1}$,
$pt_{2}$ and three values $exp_{1}$, $exp_{2}$, $new_{2}$. To the invoking
client, RDCSS gives the impression that it _atomically_ carries out the
following update: if $pt_{1}$ has expected value $exp_{1}$ and $pt_{2}$ has
expected value $exp_{2}$, then $pt_{2}$ is updated to $new_{2}$. _Multiple
Compare-And-Swap (MCAS)_ also generalizes CAS, but it updates an arbitrary
number of pointers at once. More precisely, MCAS receives a list of update
entries, each being a record with three pieces of data: a pointer pt and two
values exp, new. To a client, MCAS gives the impression that it atomically
carries out the following conditional multiple update: if for every update
entry $i$, the pointer ${\textit{pt}}_{i}$ has expected value
${\textit{exp}}_{i}$, then for every update entry $j$, the pointer
${\textit{pt}}_{j}$ is updated to the new value ${\textit{new}}_{j}$.

These algorithms have recently become somewhat of a verification benchmark
[21, 15, 18] due to their tricky _linearizability_ 111A structure is
_linearizable_ [14] if in every concurrent execution history of the
structure’s exportable methods, the method invocations can be ordered linearly
just by permuting overlapping invocations, so that the obtained history is
_sequentially sound_ ; that is, executing the methods sequentially in the
linear order produces the same outputs that the methods had in the concurrent
history. In other words, every concurrent history is equivalent to a
sequential one where methods execute without interference, i.e., _atomically_.
The linear order must include all terminated methods, but may also include
selected non-terminated ones, if their partial execution influenced (i.e., was
_visible_ to) others. proofs. The existing linearizability proofs of RDCSS and
MCAS all employ the _linearization point_ (LP) approach. Given a method
(henceforth, _event_), its LP is the moment in the event’s duration at which
the event’s effect can be considered to have occurred _abstractly_ , in the
sense that the linearization order of the events is determined by the real-
time order of the chosen LPs. The LPs are always described _operationally_ ,
by indicating a line in the code together with a run-time condition under
which the line applies (thus, the code line chosen as the LP may vary). The
linearizability proof then shows that the effect of the invocation abstractly
occurs at the declared line. The operational nature of the LP description
leads to proofs that are implementation-dependent. Concretely, RDCSS and MCAS
are operationally tricky because, in addition to helping, they exhibit so
called “future-dependent LPs”. These are LPs whose position depends on a run-
time condition in the future, potentially even after the considered event has
terminated.

In this paper, we develop a novel approach to proving linearizability of RDCSS
and MCAS (and optimizations) that elides LPs altogether. Our approach is
_declarative_ in nature, rather than operational. In particular, we show that
RDCSS and MCAS can be explained in an implementation-independent manner that
_brings to light the key high-level abstract design principles that they both
share_. This in turn leads to abstract proofs of linearizability that reuse
significant portions of the formal development.

More specifically, our first contribution is proposing that the kind of
helping employed by RDCSS and MCAS induces two natural notions that can be
used to capture the essence of both algorithms. The first notion is that of
_separation_ between events. Since an event that finds a descriptor carries
out its task only after completing the task of the event that requested help,
there is a _gap_ in real time between tasks carried out by the two events.
This behavior also induces the effect that help requests on the same pointer
are _disjoint_ in time, since a process must help first (hence, cannot make a
help request) if there is a descriptor present. In addition, RDCSS and MCAS
collect their help requests into “bunches” so that the bunched help requests
of one event can easily be separated from the bunched help requests of another
event. The second notion is that of _observation_. It arises because RDCSS and
MCAS modules contain procedures that modify the state, and procedures that
read the state. Thus, a reader event $A$ may observe a value written by writer
event $B$, leading to a dependence of $A$’s result on $B$. In a sequentially
sound reordering of events, no event sequenced between $B$ and $A$ may
overwrite $B$’s write.

Our second contribution is _axiomatizing_ separation and observation, which
formally exposes the common semantic structure behind RDCSS and MCAS and makes
it possible to decompose their proofs into independent components. As common
in axiomatic systems, a proof of a property developed out of axioms applies
without change to any algorithm that satisfies the axioms. We thus proceed to
prove linearizability of RDCSS and MCAS out of the axioms about separation and
observation alone. The axioms are much easier to establish and understand than
attempting the linearizability proof for either of the algorithms from scratch
and in its totality. Certain aspects of the abstract linearizability proof
(e.g., existence of a linear order) are common to MCAS and RDCSS, while other
aspects (e.g., sequential soundness) are unique to each data structure, but
are still abstract in the sense that the proof can be reused by other
implementations.

To state our axioms, we encode the notions of separation and observation as
binary relations between events. Each relation describes a different notion of
dependence between events. The axioms then state properties or behaviors
expected to hold whenever these order dependences are present. A prior event
on which a latter event may depend, is said to be “visible” to the latter
event, lending the name of _visibility relations_ [22] to our notions of
separation and observation. Visibility relations are clearly relevant to
linearizability, where a notion of one event influencing others is crucial, as
evident from our description of linearizability in Footnote 1.

Axiomatizing the visibility between events via binary relations was first
proposed as an alternative to the LP approach by Henzinger et al. [13], who
applied visibility to axiomatize concurrent queues, and termed “aspects” the
various properties that implied the axiomatization. Subsequently, axioms for
event visibility were developed for the concurrent timestamped stack [7], for
sophisticated concurrent snapshot algorithms [19], and to formalize
relaxations of linearizability and of memory consistency [8, 20]. Our paper,
however, is the first to apply visibility relations to a study of helping
algorithms, which poses very different challenges. In particular, whereas
axioms for concurrent queues, stacks, and snapshots mostly capture how the
contents of the structure evolve extensionally (e.g., queues are FIFO, stacks
are LIFO, etc.), with RDCSS and MCAS the challenge is in describing
intensional aspects of event interaction, such as temporal bunching of help
requests and the resulting separation of events. In summary, our contributions
are:

  * •

We propose separation and observation as foundational notions to formalize the
properties of RDCSS and MCAS algorithms in a declarative style.

  * •

We provide the first axiomatization of these two algorithms (or of any helping
algorithm) in the style of visibility relations (Section 3.2). The
axiomatization captures the common semantic structure underpinning the two
algorithms, and substantiates that visibility relations are a powerful method
for verification of concurrent algorithms. We show that separation and
observation axioms (henceforth, visibility axioms) imply linearizability
(Section 4).

  * •

To relate separation, observation and descriptors, we formulate another set of
axioms, called span axioms (Section 5.2). These mathematically describe, in
implementation-independent way, how descriptors in RDCSS and MCAS collect the
help requests into disjoint bunches. We prove that the span axioms imply the
visibility axioms (Section 5.2). Thus, linearizability is further reduced to
establishing the span axioms, allowing for even more proof reuse.

  * •

We show that RDCSS and MCAS satisfy the span axioms, concluding that both
algorithms are linearizable (Section 5.3 for MCAS, Appendix C.1 for RDCSS).

  * •

We also show that separation and observation generalize beyond helping. In
particular, we consider (Section 2.2.1) an optimization of the read procedure
in MCAS, introduced by Harris et al. [11], which we call “opportunistic
reading”. Opportunistic readers do not help on a descriptor; they merely
determine their return value from the descriptor, but improve their own
efficiency by leaving the actual helping to others (proofs in Appendix D).

Figure 1 summarizes the structure of our linearizability proof and of our
paper. Solid boxes and lines indicate what we discuss in the main body of the
paper; these include common considerations, and detailed treatment of the
proof of MCAS. Dashed boxes and lines indicate the material about RDCSS, MCAS
with opportunistic readers, and the generalization of the span axioms that
deal with opportunism, found in the appendices.

Figure 1: Steps in the linearizability proof for the RDCSS and MCAS
implementations. (1) and (2) represent distinct proofs of sequential soundness
for RDCSS and MCAS, respectively, which share the construction of the
linearization order. Dashed lines indicate the material in the appendices.

##  2 Algorithm Description

###  2.1 RDCSS

1:record rdesc:

2: $pt_{1}$ : cptr

3: $pt_{2}$ : dptr

4: $exp_{1}$, $exp_{2}$, $new_{2}$ : Val

5:

6:proc rdcss ($desc:\textsc{rdesc}$)

7: $d\leftarrow\textit{Alloc}\,(\textit{desc})$ as dptr

8: return $\textit{rdcss}^{\prime}\,(d,\textit{desc})$

9:

10:proc $\textit{rdcss}^{\prime}$ ($d:\textsc{dptr}$,
$\textit{desc}:\textsc{rdesc}$)

11: $\textit{old}\leftarrow\textit{CAS}\,({desc}.pt_{2},{desc}.exp_{2},d)$

12: if $\textit{is\\_rdesc}\,(\textit{old})$ then

13: $\textit{complete}\,(\textit{old})$

14: return $\textit{rdcss}^{\prime}\,(d,\textit{desc})$

15: else

16: if $\textit{old}=\textit{desc}.\textit{exp}_{2}$ then

17: $\textit{complete}\,(d)$

18: return old

19:

20:proc complete ($d:\textsc{dptr}$)

21: $\textit{desc}\leftarrow\,!d$

22: $x\leftarrow\,!{\textit{desc}}.pt_{1}$

23: if $x={\textit{desc}}.exp_{1}$ then

24: $\textit{CAS}\,({\textit{desc}}.pt_{2},d,{\textit{desc}}.new_{2})$

25: else

26: $\textit{CAS}\,({\textit{desc}}.pt_{2},d,{\textit{desc}}.exp_{2})$

27:proc rread ($\textit{pt}:\textsc{dptr}$)

28: $\textit{old}\leftarrow\,!\textit{pt}$

29: if $\textit{is\\_rdesc}\,(\textit{old})$ then

30: $\textit{complete}\,(\textit{old})$

31: return $\textit{rread}\,(\textit{pt})$

32: else

33: return old

34:

35:proc rCAS ($\textit{pt}:\textsc{dptr}$, $exp$, $new:\textsc{Val}$)

36:
$\textit{old}\leftarrow\textit{CAS}\,(\textit{pt},\textit{exp},\textit{new})$

37: if $\textit{is\\_rdesc}\,(\textit{old})$ then

38: $\textit{complete}\,(\textit{old})$

39: return $\textit{rCAS}\,(\textit{pt},\textit{exp},\textit{new})$

40: else

41: return old

42:

43:proc rwrite ($\textit{pt}:\textsc{dptr}$, $v:\textsc{Val}$)

44: $\textit{old}\leftarrow\,!\textit{pt}$

45: if $\textit{is\\_rdesc}\,(\textit{old})$ then

46: $\textit{complete}\,(\textit{old})$

47: $\textit{rwrite}\,(\textit{pt},v)$

48: else

49: $x\leftarrow\textit{CAS}\,(\textit{pt},\textit{old},v)$

50: if $x\neq\textit{old}$ then

51: $\textit{rwrite}\,(\textit{pt},v)$

52:

Figure 2: C-like pseudo code of the RDCSS implementation (essential fragment).
$!$, Alloc and CAS are the system calls for memory dereference, allocation,
and compare-and-swap.

Figure 2 shows the implementation of the RDCSS data structure (rdcss and
associated methods, and the descriptor type rdesc). Val denotes the set of all
possible input values; it excludes descriptors and descriptor-storing
pointers. Every pointer exposed to the clients is classified as a control
(cptr) or data (dptr) pointer. Data pointers may store Val values,
descriptors, and pointers, while control pointers only store Val values. Along
with the rdcss method, the implementation exports data pointer methods rread,
rwrite, and rCAS. The latter replace the system calls for pointer dereference,
update, and CAS, which they adapt to the presence of control and data
pointers. Not shown, but also exported, are the methods for dereference,
update and CAS over control pointers, implemented simply as respective system
calls. Methods $\textit{rdcss}^{\prime}$ and complete are internal, and not
exported. The implementation further assumes: (1) an exported method
$\textit{ralloc}\,(v,t)$ for allocating a pointer of type
$t\in\\{\textsc{cptr},\textsc{dptr}\\}$ with initial value $v$, which replaces
the system operation Alloc, and (2) an internal Boolean predicate
$\textit{is\\_rdesc}\,(p)$ that returns true iff pointer $p$ stores an RDCSS
descriptor. We show their implementation in Appendix C.1, but elide here as it
is not essential for understanding.

We next give a high-level description of rdcss. Any thread $T$ invoking rdcss
allocates a fresh address $d$ for the input descriptor desc (line 7); $d$ will
serve as a unique identifier for the rdcss invocation. Next, $T$ calls the
recursive procedure $\textit{rdcss}^{\prime}$. This first CASs on
${\textit{desc}}.pt_{2}$ to read the old value and write $d$ if the old value
is the expected ${\textit{desc}}.exp_{2}$ (line 11). By this write, $T$
essentially requests help with $d$, and signals to other threads that:

  * •

Descriptor desc (which is stored in $d$) is currently active in
${\textit{desc}}.pt_{2}$.

  * •

$T$ is invoking rdcss in which pointer ${\textit{desc}}.pt_{1}$ still needs to
be read.

  * •

While $desc$ remains active in ${\textit{desc}}.pt_{2}$, value
${\textit{desc}}.exp_{2}$ is stored in ${\textit{desc}}.pt_{2}$ _indirectly_ ,
as it can be reached by following the descriptor.

After the CAS in line 11, if old is a descriptor, then $T$ first _helps_ by
invoking $\textit{complete}{(\textit{old})}$ (line 13), and then $T$ recurses
to reattempt its task. If old is a value not matching
${\textit{desc}}.exp_{2}$, then no modification to ${\textit{desc}}.pt_{2}$ is
performed and $T$ returns old. If old is the expected value (i.e., the CAS
succeeded), then $T$ invokes $\textit{complete}{(d)}$ to help itself (line
17).

We describe complete from the point of view of another thread $T^{\prime}$
that reads ${\textit{desc}}.pt_{2}$ and finds $d$ (lines 12, 29, 37, 45).
Before doing anything else, $T^{\prime}$ helps on $d$ by invoking complete as
follows (lines 13, 30, 38, 46). $T^{\prime}$ first reads pointer
${\textit{desc}}.pt_{1}$ (line 22). If it finds the expected value
${\textit{desc}}.exp_{1}$, and since pointer ${\textit{desc}}.pt_{2}$
indirectly stores the expected value, then rdcss can succeed; thus,
$T^{\prime}$ attempts to replace the descriptor in ${\textit{desc}}.pt_{2}$
with the new value ${\textit{desc}}.new_{2}$ (line 24). The replacement in
line 24 is performed by CAS, which may fail if some other thread managed to
help $T$ before $T^{\prime}$. Either way, $T$ has been helped after the call
to complete. Otherwise, if $T^{\prime}$ does not find the expected value
${\textit{desc}}.exp_{1}$, it attempts to undo $T$’s modification to
${\textit{desc}}.pt_{2}$ (line 26) by replacing $d$ in
${\textit{desc}}.pt_{2}$ back to ${\textit{desc}}.exp_{2}$, via CAS. This
undoing may fail if some other thread managed to help $T$ before $T^{\prime}$.
Either way, $T$ has again been helped after the call to complete.

Procedures rread, rCAS and rwrite follow the same helping strategy, i.e.,
whenever they find a descriptor in their input pointer, they invoke complete
to help the pending rdcss before recursing to reattempt their own task.

###  2.2 MCAS

1:record update_entry:

2: pt : dptr

3: exp, new : Val

4:enum status: Undec, Succ, Fail

5:record mdesc:

6: status : cptr status

7: entries : list update_entry

8:

9:proc $\textit{mcas}^{\prime}$ ($d:\textsc{dptr}$)

10: $\textit{desc}\leftarrow\textit{rread}\,(d)$

11: $\textit{phase}_{1}\leftarrow\,!{\textit{desc}}.\textit{status}$

12: if $\textit{phase}_{1}=\textsc{Undec}$ then

13: $s\leftarrow\textit{writeall}\,(d,\textit{desc})$

14: $\textit{CAS}\,({\textit{desc}}.\textit{status},\textsc{Undec},s)$

15: $\textit{phase}_{2}\leftarrow\,!{\textit{desc}}.\textit{status}$

16: $b\leftarrow(\textit{phase}_{2}=\textsc{Succ})$

17: for each $e$ in ${\textit{desc}}.\textit{entries}$:

18: $\textit{rCAS}\,({e}.pt,d,b\ ?\ {e}.new:{e}.exp)$

19: return $b$

20:

21:proc mcas ($\overline{u}:\textsc{list}\,\textsc{update\\_entry}$)

22: $s\leftarrow\textit{ralloc}\,(\textsc{Undec},\textsc{cptr})$

23: $\textit{desc}\leftarrow\textsc{mdesc}\ (s,\overline{u})$

24: $d\leftarrow\textit{ralloc}\,(\textit{desc},\textsc{dptr})$

25: return $\textit{mcas}^{\prime}\,(d)$

26:

27:proc writeall ($d:\textsc{dptr},\textit{desc}:\textsc{mdesc}$)

28: for each $e$ in ${\textit{desc}}.\textit{entries}$:

29: $\textit{rd}\leftarrow\textsc{rdesc}\ ({\textit{desc}}.\textit{status},$

30: $\phantom{\textit{rd}\leftarrow\quad}{e}.pt,\textsc{Undec},{e}.exp,d)$

31: $\textit{old}\leftarrow\textit{rdcss}\,(\textit{rd})$

32: if $\textit{is\\_mdesc}\,(\textit{old})$ then

33: if $\textit{old}\neq d$ then

34: $\textit{mcas}^{\prime}\,(\textit{old})$

35: return $\textit{writeall}\,(d,\textit{desc})$

36: else if $\textit{old}\neq{e}.exp$ then

37: return Fail

38: return Succ

Figure 3: C-like pseudo code of the MCAS implementation (essential fragment).
The command return finishes the procedure execution where it is used.

Figure 3 shows the implementation of the MCAS data structure (mcas and
associated methods, and the descriptor type mdesc) atop RDCSS. Procedures
$\textit{mcas}^{\prime}$ and writeall are internal. The figure elides the
exported procedures mread, mwrite, and malloc, which can be found in Appendix
C.2. Again, Val is the set of input values that excludes descriptors and
descriptor-storing pointers. We use the notation ${pt}_{i}$, ${exp}_{i}$, and
${new}_{i}$ to refer to the components of an update_entry $i$.

High-level description of mcas is as follows. Thread $T$ invoking mcas first
creates an MCAS descriptor desc containing the non-empty list of update
entries and a status pointer (line 23). The status pointer starts in an
undecided state (Undec) and evolves into either a success (Succ) or failed
(Fail) state. Succ indicates that the descriptor was written into all input
pointers, while Fail indicates the failure of at least one such write. Next,
$T$ allocates a fresh address $d$ for desc (line 24), which serves as the
unique identifier for the mcas invocation. Eventually, through a call to
$\textit{mcas}^{\prime}$, $T$ invokes writeall (line 13) to attempt storing
$d$ into each input pointer, via rdcss. If any individual rdcss of writeall
fails, then $T$ attempts to mark the status pointer of $desc$ as failed (line
14). In general, $T$ writing $d$ into pointer ${pt}_{i}$ of entry $i$ signals
that writing $d$ into previous entries has succeeded and:

  * •

Descriptor desc (stored in $d$) is currently active in ${pt}_{j}$ for every
$j\leq i$.

  * •

$T$ has an ongoing mcas in which pointers ${pt}_{j}$ for $j>i$ still need to
be updated with $d$.

  * •

Pointers ${pt}_{j}$ for $j\leq i$ indirectly have their expected values.

If another thread $T^{\prime}$ attempts to access ${pt}_{i}$ and finds $d$, it
will _help_ $T$ complete mcas before doing anything else, by invoking
$\textit{mcas}^{\prime}$ as follows. $T^{\prime}$ first attempts to write the
descriptor into all remaining pointers (line 13). If $T^{\prime}$ succeeds,
then all pointers had the expected values. The variable $s$ in line 13 is set
to Succ, and $T^{\prime}$ attempts changing the status field of $desc$
accordingly (line 14) and replacing all the descriptors with the new values
(line 18). These attempts utilize CAS which may fail if some other thread
already helped $T$ to either succeed or fail in its mcas. Alternatively, if
$T^{\prime}$ fails to write $d$ into some pointer, it means that not all
pointers had the expected values. The variable $s$ in line 13 is bound to
Fail, $T^{\prime}$ attempts to change the status field of $desc$ accordingly
(line 14), and to undo $T$’s writing of $d$ (line 18). As before, the CAS’s in
these attempts may fail if some other thread already helped $T$ to either
succeed or fail in its mcas.

Notice that $\textit{mcas}^{\prime}$ and writeall are mutually recursive. This
is necessary, because while a thread $T$ is writing the descriptor into all
the input pointers using writeall, $T$ may encounter other descriptors that
force it to help by invoking $\textit{mcas}^{\prime}$ (lines 32-34), after
which $T$ must reattempt writing the descriptor again (line 35).

####  2.2.1 Helping reading vs. opportunistic reading

Helping readingfig::sub::standard-mcas-read-impl[0.5]

1:proc mread ($pt:\textsc{dptr}$)

2: $old\leftarrow\textit{rread}(pt)$

3: if $\textit{is\\_mdesc}(old)$ then

4: $\textit{mcas}^{\prime}(old)$

5: return $\textit{mread}(pt)$

6: else

7: return $old$

Opportunistic readingfig::sub::optimal-mcas-read-impl[0.5]

1:proc mread ($pt:\textsc{dptr}$)

2: $old\leftarrow\textit{rread}(pt)$

3: if $\textit{is\\_mdesc}(old)$ then

4: $d\leftarrow\textit{rread}(old)$

5: $s\leftarrow!({d}.\textit{status})$

6: $e\leftarrow$ entry for $pt$ in ${d}.\textit{entries}$

7: if $s=\textsc{Succ}$ then

8: return ${e}.new$

9: else

10: return ${e}.exp$

11: else

12: return $old$

Figure 4: Different implementations for mread.

Figure 4 shows two possible implementations of the mread procedure, realizing
two different reading strategies: _helping reading_ (Figure
LABEL:fig::sub::standard-mcas-read-impl), and its optimization _opportunistic
reading_ (Figure LABEL:fig::sub::optimal-mcas-read-impl). Both have been
introduced by Harris et al. [11]; the second one informally. In the rest of
the paper, we assume helping reading, delegating opportunistic reading to
Appendix D. Nevertheless, we show both implementations here, to emphasize that
our approach applies to both implementations.

The helping reader works as follows. After reading the input pointer (line 2),
if an MCAS descriptor is found, it helps the ongoing mcas by invoking
$\textit{mcas}^{\prime}$ (line 4). Then, it starts again (line 5). In
contrast, an opportunistic reader optimizes by using the following strategy.
If an MCAS descriptor is found (line 3), instead of helping, mread reads the
descriptor’s status (line 5). If the status is Succ, the descriptor was
successfully written into all input pointers in the ongoing mcas (including
pointer $pt$, i.e. the input pointer to mread). In this case, mread returns
the new value for $pt$ (as found in the descriptor) because this is the value
mcas will write eventually anyway. If the status is Fail, mread returns the
expected value for $pt$ because mcas will leave $pt$ unmodified, and the
presence of the descriptor means that $pt$ indirectly has the expected value.
If the status is Undec, mread also returns the expected value for $pt$ because
mread can pretend that the read to $pt$ occurred before any modification to
$pt$, since mcas is still attempting to write the descriptor into all the
input pointers. We say that the optimized implementation is an _opportunistic_
reader because instead of helping, it takes advantage of what helpers have
registered in the descriptor. Opportunistic reading is an optimization over
helping reading because it avoids the need to wait for a value to return, as
such a wait increases the response time in the common case when the number of
mread’s is greater than the number of mcas invocations.

##  3 Introducing and Axiomatizing Visibility

State-based sequential specification.
${H}[{{{pt}_{i}}\mapsto{{new}_{i}}}]_{i\in\overline{u}}$ is the heap (i.e.,
memory) obtained when pointers ${pt}_{i}$ ($i\in\overline{u}$) in the heap $H$
are mutated into ${new}_{i}$, while leaving the rest of $H$
unchanged.subfig:atomic-spec-state  $(A_{1})$ Successful mcas
$H\xrightarrow{\textit{mcas}(\overline{u})\ \langle
true\rangle}{H}[{{{pt}_{i}}\mapsto{{new}_{i}}}]_{i\in\overline{u}}$ if
$\forall i\in\overline{u}.\ H({pt}_{i})={exp}_{i}$ $(A_{2})$ Failing mcas
$H\xrightarrow{\textit{mcas}(\overline{u})\ \langle false\rangle}H$ if
$\exists i\in\overline{u}.\ H({pt}_{i})\neq{exp}_{i}$

History-based sequential specification. Relation
$\mathrel{\lessdot}_{{p}}:\textsc{Ev}\times\textsc{Ev}$ is
abstract.subfig:atomic-spec-history  $(B_{1})$ No in-between
$({w}\mathrel{\lessdot}_{{p}}{r}\wedge
w^{\prime}\in\mathcal{W}_{{p}})\implies({w^{\prime}}\sqsubseteq{w}\vee{r}\sqsubseteq{w^{\prime}})$
$(B_{2})$ Observed events are writes ${w}\mathrel{\lessdot}_{{p}}{\\_}\implies
w\in\mathcal{W}_{{p}}$ $(B_{3})$ Dependences occur in the past
${w}\mathrel{\lessdot}_{{p}}{r}\implies{w}\sqsubset{r}$ $(B_{4.1})$ Successful
mcas $r=\textit{mcas}(\overline{u})\left<true\right>\implies\forall
i\in\overline{u}.\ \exists w.\
{w}\mathrel{\lessdot}_{{{pt}_{i}}}{r}\wedge\textsc{writer}\ {w}\ {{pt}_{i}}\
{{exp}_{i}}$ $(B_{4.2})$ Failing mcas
$r=\textit{mcas}(\overline{u})\left<false\right>\implies\exists
i\in\overline{u}.\ \exists w.\ \exists v^{\prime}.\
{w}\mathrel{\lessdot}_{{{pt}_{i}}}{r}\wedge{}\textsc{writer}\ {w}\ {{pt}_{i}}\
{v^{\prime}}\wedge v^{\prime}\neq{exp}_{i}$ $\begin{aligned} {\textsc{writer}\
{x}\ {p}\ {v}}\mathrel{\>\widehat{=}\>}&\ x=\textit{mcas}([\ldots,\\{{pt}:p,\
{exp}:\\_,\ {new}:v\\},\ldots])\left<\\_\right>\vee{}\\\ &\
x=\textit{mwrite}(p,v)\left<\\_\right>\vee
x=\textit{malloc}(v)\left<p\right>\\\ \end{aligned}$ $\begin{aligned}
x\in\mathcal{W}_{p}\Longleftrightarrow&\ x=\textit{mcas}([\ldots,\\{{pt}:p,\
\ldots\\},\ldots])\left<true\right>\vee
x=\textit{mwrite}(p,\\_)\left<\\_\right>\vee
x=\textit{malloc}(\\_)\left<p\right>\\\ \end{aligned}$

Figure 5: State-based and history-based sequential specifications for mcas.

###  3.1 Sequential History Specifications and Observation Relations

Following Henzinger et al. [13], we start the development of visibility
relations by introducing _history-based specifications_ for our data
structures. The idea is that a history-based specification in terms of
visibility relations will be more concrete—and thus more direct to prove—than
merely asserting linearizability of the involved structures. At the same time,
the specification will still be sufficiently abstract and high-level that: (1)
it is largely _shared_ by RDCSS and MCAS, thus providing a unifying
explanation of both (and of the opportunistic reading optimization), and (2)
it generically implies linearizability. We next illustrate the intuition
behind history-based specifications, focusing on the mcas procedure.

History-based specifications describe relationships between the data
structure’s procedures in an execution history. They are significantly
different (and more involved) from the perhaps more customary state-based
specifications that describe the actions of a procedure in terms of input and
output state. However, history-based specifications scale better to the
concurrent setting, which is why concurrent consistency criteria such as
linearizability are invariably defined in terms of execution histories (e.g.,
see Footnote 1 of Introduction).

In this section we focus on _sequential_ histories in order to introduce the
idea of _observation relation_ in a simple way, before generalizing to
concurrent histories in Section 3.2. A sequential history is a sequence of the
form $[proc(in_{1})\langle out_{1}\rangle,\ \ldots,\ proc(in_{n})\langle
out_{n}\rangle]$, where $proc(in_{i})\langle out_{i}\rangle$ means that
$proc(in_{i})$ executed _atomically_ and produced output $out_{i}$. We term
_event_ each element in a sequential history $h$, and Ev denotes the set of
all events in $h$.

Figure 5 illustrates the distinction between sequential state-based and
history-based specifications for mcas. The state-based specification in Figure
LABEL:subfig:atomic-spec-state says in axiom $A_{1}$ that a successful mcas
occurs when all input pointers contain the expected values; the pointers are
then mutated to their new values. Axiom $A_{2}$ says that a failing mcas
occurs when some input pointer does not have the expected value, leaving the
heap unchanged.

Figure LABEL:subfig:atomic-spec-history shows the history sequential
specification for mcas. The specification utilizes the _observation relation_
$\mathrel{\lessdot}_{{p}}$ to capture a read-write causal dependence between
events. In particular, ${w}\mathrel{\lessdot}_{{p}}{r}$ means that “event $r$
reads a value that event $w$ wrote into pointer $p$”. Under this
interpretation, axioms $B_{1},...,B_{4.2}$ state the following expected
properties.222Our paper will make heavy use of several different relations. To
help the reader keep track of them, we shall denote the relations by symbols
that graphically associate to the relation’s meaning. For example, we use
$\lessdot$ for the observation relation, because the symbol graphically
resembles an eye.

Axiom $B_{1}$ (No in-between) says that if $r$ reads from $w$ in $p$, then no
other successful $p$-write can occur between $w$ and $r$ (otherwise, such a
write would overwrite $w$). Relation $\sqsubset$ is the _returns-before_
relation (with $\sqsubseteq$ its reflexive closure), where ${x}\sqsubset{y}$
means that $x$ terminated before $y$ started. Note that $\sqsubset$ is a total
order on events, as in a sequential setting the executions of different events
cannot overlap. Set $\mathcal{W}_{p}$ collects the successful $p$-writes,
e.g., writes of the form $\textit{mwrite}(p,\\_)$, malloc events returning
$p$, and $\textit{mcas}(\overline{u})$ events returning $true$ and having $p$
in $\overline{u}$.

Axiom $B_{2}$ (Observed events are writes) says that any observed event at $p$
must be a successful $p$-write, i.e., if $r$ reads from $w$ in $p$, then $w$
must have actually written into $p$. Axiom $B_{3}$ (Dependences occur in the
past) says that if a read depends on a write, then the write executes before
the read.

Axioms $B_{4.1}$ (Successful mcas) and $B_{4.2}$ (Failing mcas) essentially
encode the state-based sequential specification for mcas. For example, axiom
$B_{4.1}$ directly says that a successful
$\textit{mcas}(\overline{u})\left<true\right>$ event $r$ observes—for each of
its input entries $\overline{u}$—a successful write event (mcas, mwrite or
malloc, as per axiom $B_{2}$) that wrote the expected value into the
appropriate pointer. Because the write events are _observed_ by $r$, axiom
$B_{3}$ ensures that they execute before $r$, while axiom $B_{1}$ guarantees
the none of them is overwritten before $r$ executes. Thus, diagrammatically,
for each entry $i\in\overline{u}$, the execution looks as follows, where the
write into pointer ${pt}_{i}$ persists until the heap $H_{n}$ at which $r$
executes.

${\ldots}$${H_{k}}$${H_{k+1}}$${\ldots}$${H_{n}}$${\ldots}$$\scriptstyle{w_{i}}$$\scriptstyle{\textit{mcas}(\overline{u})\left<true\right>}$$\scriptstyle{{pt}_{i}\mapsto{exp}_{i}\text{
persists}}$$\scriptstyle{\mathrel{\lessdot}_{{{pt}_{i}}}}$

Concurrent specification. Relations
$\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}}:\textsc{Ev}\times\textsc{Ev}$
are existentially quantified.subfig:concurrent-spec-history  ($C_{1}$) No in-
between $({w}\mathrel{\lessdot}_{{p}}{r}\wedge
w^{\prime}\in\mathcal{W}_{{p}})\implies({w^{\prime}}\mathrel{\mathrel{\vbox{\offinterlineskip\hbox{\phantom{$\ltimes$}}\vskip-1.50696pt\hbox{$\ltimes$}\vskip-1.50696pt\hbox{$-$}}}}_{{p}}{w}\vee{r}\mathrel{\mathrel{\vbox{\offinterlineskip\hbox{\phantom{$\ltimes$}}\vskip-1.50696pt\hbox{$\ltimes$}\vskip-1.50696pt\hbox{$-$}}}}_{{p}}{w^{\prime}})$
($C_{2}$) Observed events are writes ${w}\mathrel{\lessdot}_{{p}}{\\_}\implies
w\in\mathcal{W}_{{p}}$ ($C_{3}$) No future dependences
$x\mathrel{{\prec}^{+}}y\implies{y}\not\sqsubseteq{x}$ ($C_{4}$) Return value
completion $\exists v.\ \mathcal{Q}_{{x},{v}}\wedge(x\in T\implies
v={x}.\textit{out})$

Defined notions.subfig:defined-notions-concurrent-spec-history  General
visibility relation
${\prec}\mathrel{\>\widehat{=}\>}\bigcup_{p}(\mathrel{\lessdot}_{{p}}\cup\mathrel{\ltimes}_{{p}})$
Returns-before relation
${e}\sqsubset{e^{\prime}}\mathrel{\>\widehat{=}\>}{e}.\textit{end}<_{\mathbb{N}}{e^{\prime}}.\textit{start}$
Set of terminated events
$T\mathrel{\>\widehat{=}\>}\\{e\mid{e}.\textit{end}\neq\bot\\}$ Closure of
terminated events $\overline{T}\mathrel{\>\widehat{=}\>}\\{e\mid\exists t\in
T.\ e\mathrel{{\prec}^{*}}t\\}$
$\mathcal{Q}_{{\textit{mcas}(\overline{u})},{v}}\mathrel{\>\widehat{=}\>}v\in\textsc{Bool}\wedge\begin{cases}\forall
i\in\overline{u}.\ \exists w.\
{w}\mathrel{\lessdot}_{{{pt}_{i}}}{\textit{mcas}(\overline{u})}\wedge\textsc{writer}\
{w}\ {{pt}_{i}}\ {{exp}_{i}}&\text{if $v=true$}\\\ \exists i\in\overline{u}.\
\exists w.\ \exists v^{\prime}.\
{w}\mathrel{\lessdot}_{{{pt}_{i}}}{\textit{mcas}(\overline{u})}\wedge{}&\text{if
$v=false$}\\\ \hskip 30.0pt\textsc{writer}\ {w}\ {{pt}_{i}}\
{v^{\prime}}\wedge v^{\prime}\neq{exp}_{i}&\\\ \end{cases}$ $\begin{aligned}
\textit{mcas}(\overline{u})\in\mathcal{W}_{p}\Longleftrightarrow(\exists
j\in\overline{u}.\ p={pt}_{j})\wedge\forall i\in\overline{u}.\ \exists w.\
{w}\mathrel{\lessdot}_{{{pt}_{i}}}{\textit{mcas}(\overline{u})}\wedge\textsc{writer}\
{w}\ {{pt}_{i}}\ {{exp}_{i}}\end{aligned}$

Figure 6: Concurrent history-based specification (fragment) for mcas.
Variables $w$, $w^{\prime}$, $r$, $x$, $y$ range over $\overline{T}$.
Variables $e$, $e^{\prime}$ range over Ev. Full definitions of $\mathcal{Q}$,
$\mathcal{W}_{p}$, and writer for the MCAS module are found in Appendix A.3.
Two more axioms involving allocs are elided (also elided from Figure
LABEL:subfig:atomic-spec-history). The full list of axioms is shown in Figure
11 of Appendix A.

###  3.2 Concurrent Specifications and Separable-Before Relations

Concurrent execution histories do not satisfy the sequential axioms in Figure
LABEL:subfig:atomic-spec-history for two main reasons. First, concurrent
events can _overlap_ in real time. As a consequence, the axioms $B_{1}$ (No
in-between) and $B_{3}$ (Dependencies occur in the past) are too restrictive,
as they force events to be disjoint, due to the use of the returns-before
relation $\sqsubset$. Second, events can no longer be treated as atomic; thus
event’s start and end times (if the event is terminated) must be taken into
account. As a consequence, axioms $B_{4.1}$ and $B_{4.2}$ and set
$\mathcal{W}_{p}$ must be modified to account for the output of an unfinished
event not being available yet. We continue using Ev for the set of events in
the concurrent history. We denote by ${e}.\textit{start}$, ${e}.\textit{end}$,
the start and end time of event $e$, respectively. We use the standard order
relation on natural numbers $<_{\mathbb{N}}$ to compare start and end times.

Figure 6 shows the concurrent specification that addresses the above issues.
Importantly, in addition to the observation relation, the specification
utilizes the _separable-before relation_ $\mathrel{\ltimes}_{{p}}$ to capture
an ordering dependence between events. In particular,
${x}\mathrel{\ltimes}_{{p}}{y}$ means that “event $x$ is separable before $y$
because of some logical gap when using shared pointer $p$”. We now explain how
the concurrent specification of Figure 6 is obtained from the sequential one
in Figure LABEL:subfig:atomic-spec-history.

Axiom $C_{\ref{vis-ax::cc-no-in-between}}$ is obtained from $B_{1}$ by
replacing $\sqsubset$ with $\mathrel{\ltimes}_{p}$. The intuition is that we
want to relax the real-time strong separation imposed by $\sqsubset$ into a
more permissive separation $\mathrel{\ltimes}_{p}$. The latter captures that a
gap can be viewed as existing between possibly overlapping events, forcing one
event to be ordered before another.333The symbol $\ltimes$ twists $\sqsubset$,
suggesting that the separable-before relation $\ltimes$ relaxes (i.e., is a
twist on) returns-before relation $\sqsubset$. The definition of
$\mathrel{\ltimes}_{p}$ is different for different implementations (thus, the
gap is described by logically different properties in different
implementations), but they all satisfy axiom $C_{\ref{vis-ax::cc-no-in-
between}}$. We shall see in Section 3.3 the concrete definition of
$\mathrel{\ltimes}_{p}$ (i.e., the description of the logical gap) for the
mcas implementation of Figure 3.

Axiom $C_{\ref{vis-ax::cc-observed-are-writes}}$ is unchanged compared to
$B_{2}$.

Axiom $C_{\ref{vis-ax::cc-no-future-dependence}}$ is obtained from $B_{3}$ as
follows. In the sequential specification, $\mathrel{\lessdot}_{p}$ was the
only relation encoding dependences between events, but now we have two
relations encoding dependences, $\mathrel{\lessdot}_{p}$ and
$\mathrel{\ltimes}_{p}$. The relation
${\prec}\mathrel{\>\widehat{=}\>}{\cup_{p}{(\mathrel{\lessdot}_{p}\cup\mathrel{\ltimes}_{p})}}$
thus collects all the dependences, and we call $\prec$ the _general_
visibility relation.444The symbol $\prec$ reminds us of an eye without an
iris, suggesting that the general visibility relation is “blinder” than
$\lessdot$, since $\prec$ also contains $\ltimes$. We can consider modifying
Axiom $B_{3}$ into ${x}\prec{y}\implies{x}\sqsubset{y}$ to say that any
dependence $x$ of $y$ must terminate before $y$ starts. However, such a
modification of $B_{3}$ is too stringent, as it does not allow $x$ to overlap
with $y$. Instead, we relax the conclusion to say that an event cannot depend
on itself or events from the future, i.e.,
${x}\prec{y}\implies{y}\not\sqsubseteq{x}$. Finally, we get axiom
$C_{\ref{vis-ax::cc-no-future-dependence}}$ by replacing $\prec$ with its
transitive closure $\mathrel{{\prec}^{+}}$ to account for _indirect_
dependences of $y$; e.g., in $x_{1}\prec x_{2}\prec y$, event $x_{1}$ is an
indirect dependence of $y$. Hence, $C_{\ref{vis-ax::cc-no-future-dependence}}$
reads “any direct or indirect dependence does not execute in the future, and
events do not depend on themselves”.

To understand Axiom $C_{\ref{vis-ax::cc-return-completion}}$, we need to
consider the set $T$ of all _terminated_ events and its closure under the
general visibility relation
$\overline{T}\mathrel{\>\widehat{=}\>}\\{e\in\textsc{Ev}\mid\exists t\in T.\
e\mathrel{{\prec}^{*}}t\\}$. As usual, $\mathrel{{\prec}^{*}}$ is the
reflexive-transitive closure of $\prec$. The idea here is that $\overline{T}$
contains all the events that have contributed to producing values in the
execution history, either by being terminated (and thus directly returning a
value), or by being an event on which some terminated event depends. The
dependence may be indirect, and the depended event may be unterminated. For
example, a terminated mcas $r$ may observe an unterminated mcas $w$, i.e.,
${w}\mathrel{\lessdot}_{p}{r}$ as follows: $w$ mutates $p$ but is preempted
just before termination, thus allowing $r$ to read. At any rate,
$\overline{T}$ contains all the events required to “explain” the values
obtained in the concurrent execution, and thus establish that the linearized
execution is _sequentially sound_ , as per Footnote 1. In our example with $r$
and $w$, we must consider $w$ if we want to explain the return value of $r$,
which is why $w$ is included in $\overline{T}$.

Axiom $C_{\ref{vis-ax::cc-return-completion}}$ first coalesces axioms
$B_{4.1}$ and $B_{4.2}$ into the postcondition predicate $\mathcal{Q}$, as
shown in Figure LABEL:subfig:defined-notions-concurrent-spec-history. Then
$C_{\ref{vis-ax::cc-return-completion}}$ requires that every event
$x\in\overline{T}$ satisfies $\mathcal{Q}$. In case $x$ is a terminated mcas
event, it is easy to see that this requirement, along with the requirement
that $v$ equals the output of $x$, directly corresponds to the sequential
axioms $B_{4.1}$ and $B_{4.2}$. In case $x$ is an unterminated mcas event, the
axiom posits that some value $v$ can be found to make $x$ appear as if it has
terminated in a manner coherent with the other events. The latter “completion”
of $x$ with $v$ is a common pattern that we inherit from the work on
linearizability.

We further emphasize that in the concurrent setting we also need to redefine
the set $\mathcal{W}_{p}$ of successful writes into pointer $p$. It does not
suffice to consider an mcas as a successful write if it returns $true$; we
need a criterion when an unfinished mcas is a successful write as well. Thus,
we define in Figure LABEL:subfig:defined-notions-concurrent-spec-history that
an $\textit{mcas}(\overline{u})$ is a successful $p$-write if $p$ is a pointer
in $\overline{u}$, and $\textit{mcas}(\overline{u})$ observes events writing
the expected values for each entry in $\overline{u}$.

$\mathcal{Q}_{{\textit{rdcss}(d)},{v}}\mathrel{\>\widehat{=}\>}\begin{aligned}
\exists
w_{2}.\,{w_{2}}\mathrel{\lessdot}_{{{d}.pt_{2}}}{\textit{rdcss}(d)}\wedge\textsc{writer}\
{w_{2}}\ {{d}.pt_{2}}\ {v}\wedge{}\\\ (v={d}.exp_{2}\implies\exists
w_{1}.\,{w_{1}}\mathrel{\lessdot}_{{{d}.pt_{1}}}{\textit{rdcss}(d)})\end{aligned}$
---
$\textit{rdcss}(d)\in\mathcal{W}_{p}\Longleftrightarrow\begin{aligned}
p={d}.pt_{2}\wedge\exists w_{1},w_{2}.\
{w_{1}}\mathrel{\lessdot}_{{{d}.pt_{1}}}{\textit{rdcss}(d)}\wedge{w_{2}}\mathrel{\lessdot}_{{{d}.pt_{2}}}{\textit{rdcss}(d)}\wedge{}\\\
\textsc{writer}\ {w_{1}}\ {{d}.pt_{1}}\ {{d}.exp_{1}}\wedge\textsc{writer}\
{w_{2}}\ {{d}.pt_{2}}\ {{d}.exp_{2}}\end{aligned}$
Figure 7: Together with axioms in Figure LABEL:subfig:concurrent-spec-history,
this is a (fragment of) concurrent specification for rdcss. Full definitions
of $\mathcal{Q}$, $\mathcal{W}_{p}$, and writer for the RDCSS module are in
Appendix A.2.

Section 4 will show that the axioms in Figure LABEL:subfig:concurrent-spec-
history, henceforth called _visibility axioms_ , suffice to prove the
existence of a sequentially sound total order. Thus, proving linearizability
for an MCAS implementation reduces to finding $\mathrel{\lessdot}_{p}$ and
$\mathrel{\ltimes}_{p}$ that satisfy the visibility axioms.

One can repeat the steps for rdcss, and obtain again the axioms in Figure
LABEL:subfig:concurrent-spec-history, but with $\mathcal{W}_{p}$ and
$\mathcal{Q}$ defined as in Figure 7. The postcondition for
$\textit{rdcss}(d)$ states that $\textit{rdcss}(d)$ must observe an event that
wrote $\textit{rdcss}(d)$’s output $v$ into ${d}.pt_{2}$, and in case $v$ is
the expected value, $\textit{rdcss}(d)$ must have read pointer ${d}.pt_{1}$
also. An $\textit{rdcss}(d)$ successfully writes if it observes two events
that wrote the expected values into pointers ${d}.pt_{1}$ and ${d}.pt_{2}$.

Figure 8: An execution of mcas events $A$ and $B$. Each event encircles the
spans belonging to it (i.e., helping it). The intersection of spans for each
event are shown as gray columns. Spans $a$ and $b$, both accessing pointer
$p$, are named for later reference.

###  3.3 Visibility Relations for MCAS

####  3.3.1 Definitions of Visibility Relations

We now proceed to explain how relations $\mathrel{\lessdot}_{p}$ and
$\mathrel{\ltimes}_{p}$ are defined for the implementation of mcas in Figure
3. The key idea is to analyze the behavior of the descriptors during the
execution. Figure 8 shows the execution of two overlapping invocations of
mcas, which we refer to as events $A$ and $B$, respectively.555We focus on the
successful mcas case. Section 5 will explain the failing mcas case. During the
execution of mcas, threads write the descriptor into a pointer (line 31 in
Figure 3), and then remove it (line 18). We term _span_ the time interval
between writing the descriptor and removing it. We also say that the removed
descriptor is _resolved_. Figure 8 depicts spans as bounded line segments.

There are two key invariants of mcas that give rise to its visibility
relations. The first key invariant is that all the spans of an event _must
overlap_ (we call this the _bunching invariant_). Concretely for mcas events,
any descriptor write must occur before any descriptor removal. This is so
because of the following two properties related to how control flows through
mcas. First, threads can reach line 18 (descriptor removal) only if some
thread changed the descriptor status at line 14.666Recall that all descriptors
are Undec initially, and can evolve to Succ or Fail only. This holds because
line 18 (descriptor removal) is in the $\mathit{false}$ branch of the
conditional at line 12 that checks if the descriptor status is Undec.
Therefore, if no thread has changed the descriptor status at line 14, threads
starting the $\textit{mcas}^{\prime}$ procedure will keep entering the
$\mathsf{true}$ branch at line 12. The second property is that any descriptor
write at line 31 must occur before some thread changes the descriptor status
at line 14. This holds because the rdcss at line 31 (descriptor write attempt)
fails if the descriptor status is no longer Undec. These two properties imply
that any descriptor write must occur before the status change, and any
descriptor removal must occur after the status change, i.e., any span starts
before any span finishes in the event; hence, span intersection is non-empty.
Figure 8 depicts the spans’ intersection for each event as gray columns. Since
the presence of a descriptor signals that a pointer indirectly has the
expected value, inside the gray column all the event’s pointers simultaneously
have the expected values. Therefore, the event can be considered as abstractly
occurring (i.e., having its LP) anywhere inside the gray column.

The second key invariant is that spans writing into _the same pointer_ (e.g.,
spans $a$ and $b$ in Figure 8) _must be disjoint_ (we call this the
_disjointness invariant_). This is so because mcas uses helping; thus an event
writes into a pointer only if there is no descriptor currently present. More
specifically, the rdcss at line 31 in Figure 3 writes the descriptor only if
the expected value is present directly (i.e., not via a descriptor). Since
spans start by writing a descriptor, no span can start while there is a
descriptor present, or equivalently, when another span is already active in
the pointer. The span can start only after the currently present descriptor is
removed.

These two invariants imply, as also apparent from Figure 8, that gray columns
of different events $A$ and $B$ accessing a common pointer must be disjoint.
Thus, we can _separate_ event $A$ before event $B$ in time, because $A$’s gray
column executes before $B$’s. In the figure, we can describe the separation
(i.e., the gap between the gray columns) by saying that there is a span in $A$
(namely $a$) and a span in $B$ (namely $b$), both accessing a common pointer,
and $a$ completes before $b$ starts. Spans $a$ and $b$, being disjoint, induce
a gap in the gray columns.

We define the separable-before relation $\mathrel{\ltimes}_{{p}}$ so that it
directly formalizes the above description of the separation between $A$ and
$B$,

$\displaystyle{A}\mathrel{\ltimes}_{{p}}{B}\mathrel{\>\widehat{=}\>}\exists
x\in\mathcal{S}_{p}(A),y\in\mathcal{S}_{p}(B).\ {x}\sqsubset^{S}{y}$ (1)

In the definition, $x\in\mathcal{S}_{p}(A)$ means that $x$ is a span accessing
pointer $p$ in event $A$ (similarly for $y\in\mathcal{S}_{p}(B)$), and
${x}\sqsubset^{S}{y}$ means that span $x$ terminates before $y$ starts.
Relation $\sqsubset^{S}$ is a partial order on spans that totally orders spans
accessing the same pointer due to span disjointness. $\sqsubseteq^{S}$ denotes
its reflexive closure.

We now focus on the observation relation $\mathrel{\lessdot}_{{p}}$. We
previously informally explained that ${A}\mathrel{\lessdot}_{{p}}{B}$
intuitively captures that event $B$ reads a value written by the $p$-write
$A$, with no other intervening writes between. To illustrate how this
intuition can be expressed using spans, consider the span $b$ in Figure 8.
When this span starts, it reads the input pointer (this is so because the
rdcss at line 31 in Figure 3 obtains the pointer’s value, writes the
descriptor and returns the read value). This obtained value must have been
written by the most recent span that successfully wrote into the pointer,
which, in Figure 8 is span $a$.

To formally capture the described situation, we say that event $A$ is
_observed_ by $B$ at pointer $p$ if there are spans $x$ and $y$ in $A$ and
$B$, respectively, such that $x$ is the most recent span that terminated
before $y$ started, and that successfully wrote into $p$,

$\displaystyle{A}\mathrel{\lessdot}_{{p}}{B}\mathrel{\>\widehat{=}\>}\exists
x\in\mathcal{S}_{p}(A),y\in\mathcal{S}_{p}(B).\
x=\max_{\sqsubseteq^{S}}\\{z\in\mathcal{S}^{W}_{p}\mid{z}\sqsubset^{S}{y}\\}$
(2)

In the definition, the maximum is taken under $\sqsubseteq^{S}$, and set
$\mathcal{S}^{W}_{p}$ collects the spans that _successfully_ write into $p$.
We differentiate successful writes because some spans do not carry out
changes. For example, line 18 in Figure 3 produces a span that writes the new
value only if the descriptor’s status was set to Succ, but produces a span
that undoes changes (as if the descriptor was not written) if the status was
set to Fail. Notice that it makes sense to take the maximum under
$\sqsubseteq^{S}$ because spans accessing the same pointer are disjoint,
hence, linearly ordered under $\sqsubseteq^{S}$.

####  3.3.2 Spans and Visibility Axioms

Section 5 will substantiate more how definitions (1) and (2) satisfy the
visibility axioms of Figure LABEL:subfig:concurrent-spec-history. Here, we
briefly illustrate how the definitions satisfy the no in-between axiom
$C_{\ref{vis-ax::cc-no-in-between}}$ using Figure 8. In Figure 8, assertion
${A}\mathrel{\lessdot}_{{p}}{B}$ means that span $b$ reads a value written by
span $a$ in pointer $p$. Since $a$ is the most recent $p$-writing span before
$b$ in real-time, and due to span disjointness, any other $p$-writing span $c$
must execute either completely before $a$ or completely after $b$. Therefore,
if $c$ belongs to some $p$-write $C$, there will be a gap between the gray
columns of either $C$ and $A$ or $B$ and $C$, depending on whether $c$
executes before $a$ or after $b$.

####  3.3.3 Alternative Span Definitions

As we just saw, the definitions (1) and (2) satisfy axiom $C_{\ref{vis-ax::cc-
no-in-between}}$. Notice, however, that the argument relied solely on the span
disjointness invariant, and not on a specific definition of spans. This is
actually an overarching property that we shall utilize when proving each of
the visibility axioms from Figure LABEL:subfig:concurrent-spec-history.
Neither proof will depend on the particular definition of spans, but only on
high-level abstract span invariants such as bunching, disjointness and a small
number of additional structural ones that we shall introduce in Section 5.

This abstraction affords some freedom to deviate from the operational
definition of spans as the time intervals between writing the descriptor and
resolving it, so long as the high-level span invariants remain satisfied by
the programs.

To illustrate, bunching and disjointness remain satisfied if the successful
CAS at line 14 is chosen as the ending point of a span, instead of line 18
that we previously considered. Recall that while explaining the bunching
invariant in Section 3.3.1, we stated that any descriptor write must occur
before the status change at line 14. Therefore, the successful CAS at line 14
is perfectly fine to end spans, because any span must start before it, i.e.,
bunching holds because any span starts before the CAS, which is the ending
point for all the spans. Disjointness still holds because of the same reason
as in Section 3.3.1: no descriptor can be written if there is currently a
descriptor present. Therefore, if we end the span prematurely at line 14,
still no span can start until the descriptor is removed at line 18 much later.

Additionally, single reads that return a Val value can be treated as spans
that write a descriptor and instantaneously resolve it (i.e. a “collapsed
span”). For example, the read at line 2 of Figure LABEL:fig::sub::standard-
mcas-read-impl. It is essential that we treat as spans only those reads that
return Val values to ensure the span disjointness invariant: if we treat reads
that return descriptors as spans, then the read will occur while a descriptor
is present, i.e., inside another span, violating disjointness.

####  3.3.4 Visibility Relations for RDCSS and Opportunistic Readers

Perhaps surprisingly, definitions (1) and (2) apply without change not only to
mcas, but to all events using helping in RDCSS and MCAS implementations such
as mcas, mwrite, mread, rdcss, rread, etc.

For example, rdcss events can be seen as a special case of Figure 8, in which
each rdcss event executes at most two spans. The first span of rdcss is
generated by writing the descriptor at line 11 in Figure 2, and resolved at
either line 24 or line 26. The second span consists of a single read of the
control pointer at line 22 (thus, it is a “collapsed” span). Trivially, rdcss
satisfies the bunching invariant because the thread that resolves the
descriptor at either line 24 or line 26, must have also previously read the
control pointer at line 22 while the descriptor was present. In other words,
the collapsed span overlaps the first span. Also, rdcss satisfies span
disjointness: an rdcss invocation cannot write a new descriptor into a pointer
if there is currently another descriptor present.

On the other hand, opportunistic reading requires definitions different from
(1) and (2) (see Definition D.5 in Appendix D). Nevertheless, the concepts of
separable-before and observation relations satisfying the axioms in Figure
LABEL:subfig:concurrent-spec-history, are general high-level characteristics
of all these algorithms.

###  3.4 Comparing Visibility Relations and Linearization Points

The standard way of proving a concurrent algorithm linearizable is to exhibit
the algorithm’s LPs. For example, the LPs for rdcss from Figure 2 have been
described operationally in previous work [11, 21, 15]: one LP occurs at line
11 whenever the CAS in line 11 fails and the value returned by the CAS is not
a descriptor; another LP occurs at line 22, as long as the thread that
executes this line can successfully execute one of the CASs at lines 24 and
26, _later on_. While a proof that this is a correct description of the LPs of
rdcss exists (e.g., in Jung et. al. [15]), the LP assignment alone does not
really provide much intuition as to the underlying principles behind rdcss, or
how these principles are shared with mcas.

For comparison, we can recover the LP approach by defining the visibility
relations in terms of LPs. For example, defining the separable-before relation
as,

$\displaystyle{x}\mathrel{\ltimes}_{{p}}{y}\mathrel{\>\widehat{=}\>}LP(x)\sqsubset
LP(y)$ (3)

where $LP(x)$ and $LP(y)$ are the linearization points of $x$ and $y$,
respectively. However, (3) leads to a less abstract and less modular proof
than ours. Regarding abstraction, (3) does not bring out that span bunching
and disjointness are the two high-level invariants that rdcss and mcas share,
and that suffice to describe separation between events for both algorithms.
Regarding modularity, (3) defines a total order on events _right away_. But
notice that the specification in Figure LABEL:subfig:concurrent-spec-history
does not require the relation $\mathrel{\ltimes}_{{p}}$ to be total, not even
over events sharing pointer $p$; it _only_ requires to somehow separate the
events that share $p$. In particular, (1) is not a total order over events
sharing pointer $p$. Instead, the visibility approach divides the burden of
proving linearizability into two stages that are easier to conquer than
directly proving linearizability. In the first stage, we define the visibility
relations and prove the visibility axioms. In the second stage, the (total)
linearization order is constructed out of the visibility relations.
Importantly, the second stage is generic and independent of the first, as it
can be developed out of the visibility axioms alone, without having the
definitions of the visibility relations in hand.

Where the LP approach very concretely and operationally locates the LP of each
event, the visibility approach is more concerned with capturing the semantic
structure of the algorithms, such as, in the example of RDCSS and MCAS,
recognizing that each event is characterized by the disjoint bunches of its
spans. In fact, this semantic structure appears to capture how Harris et al.
[11] themselves thought about these algorithms, as they reveal in this quote
from their Section 4.2:

> Each invocation of RDCSS can be considered separately. This surprising
> observation follows by examining the memory accesses. […] Different RDCSS
> operations acting on the same location are thereby serialized by the order
> of their active periods, so we can consider them individually.

Clearly, “active periods” corresponds to spans, and “serialization by the
order of active periods” corresponds to the separable-before relation. On the
other hand, Harris et al. [11] do not pursue axiomatization, which is why no
concept analogous to the observation relation appears for them. Be it as it
may, the quote already contrasts with the (arguably, not very intuitive)
description of the LPs of rdcss we gave at the beginning of this section. That
visibility relations can formalize this (shared) intuition behind algorithms
such as RDCSS and MCAS, is the point of our paper.

##  4 Proving Linearizability out of Visibility Axioms

Having provided a high-level overview, we now proceed with the technical
development of the proofs of linearizability that are _abstract_ , i.e., they
proceed from the visibility axioms, and apply to arbitrary implementations of
RDCSS and MCAS (the gray box in Figure 1). In this section we exhibit the
abstract proof for MCAS. The one for RDCSS is in Appendix A.2. Later on, we
shall instantiate the abstract proofs to conclude that the _concrete_
implementations are linearizable. In particular, the helping MCAS
implementation is shown linearizable in Section 5, the RDCSS implementation in
Appendix C.1, and the opportunistic MCAS implementation in Appendix D.

######  Definition 4.1 (Linearizability).

We say that a data structure’s implementation $D$ is _linearizable_ if for any
set of events Ev generated from an arbitrary execution history in $D$, there
is a binary relation ${\prec}\subseteq{\textsc{Ev}\times\textsc{Ev}}$
(_general visibility relation_) and a linear order
${\leq}\subseteq{\overline{T}\times\overline{T}}$
(_linearization_)777$\overline{T}$ is the closure of the terminated events $T$
under $\prec$, as in Figure LABEL:subfig:defined-notions-concurrent-spec-
history. s.t.,

  * •

$\leq$ respects the real-time ordering of events, i.e., $\sqsubset$ restricted
to $\overline{T}$ is contained in $\leq$.

  * •

$\leq$ respects the ordering constraints in $\prec$, i.e., $\prec$ restricted
to $\overline{T}$ is contained in $\leq$.

  * •

$\leq$ is _sequentially sound_ , i.e., when events are executed in the order
determined by $\leq$, the execution output $o_{i}$ of the $i$-th event $x_{i}$
matches ${x_{i}}.\textit{out}$ if $x_{i}\in T$ or it is consistent to define
${x_{i}}.\textit{out}$ as $o_{i}$ if $x_{i}\notin T$. The operational
semantics of executing events in the order of $\leq$ is data-structure
specific.

Our definition of linearizability differs slightly from the usual formulation
[14] in that it emphasizes working with visibility relations, as follows. When
judging a history $h$ linearizable, the standard definition starts by
requiring an _arbitrary_ completion $\hat{h}$, which closes up some non-
terminated events in $h$. For us, the completion is not arbitrary, but is
generated by the specific visibility relation that we work with, as captured
by the set $\overline{T}$. It is thus easy to see that our definition implies
the standard one. Our definition is justified, because in practice of proving
linearizability, the choice of the completion is always guided by an implicit
notion of dependence between events; we merely make this notion explicit by
means of $\prec$.

###  4.1 Constructing the linearization order

Given arbitrary $\mathrel{\lessdot}_{{p}}$, $\mathrel{\ltimes}_{{p}}$, we
denote by $V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$
the specification for MCAS in Figure 6. We first give an overview of the
structure of the proof.

The proof is divided into two steps. The first step constructs a linear order
$\leq$ containing both $\prec$ and $\sqsubset$ (the first two requirements in
Definition 4.1) and satisfying:

$\displaystyle{x}\mathrel{\lessdot}_{{p}}{y}\implies\neg\exists
z\in\mathcal{W}_{p}\cap\overline{T}.\ x<z<y$ (4)

i.e., there are no $p$-writes in between a $p$-observation in the linear
order. The second step consists in proving that $\leq$ is sequentially sound
(the third requirement in Definition 4.1) by using (4), which ensures that the
order of any mutation performed by $x$ remains unchanged in $\leq$ up to the
point where $y$ reads. We assume throughout that the visibility axioms of
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ hold.

The first step of the proof is independent of the particular definitions for
the postcondition predicate $\mathcal{Q}$ and the successful writes set
$\mathcal{W}_{p}$ in
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$. Hence, to
generalize the first step, we introduce the following definition. Given
$\mathrel{\lessdot}_{p},\mathrel{\ltimes}_{p}$, we say that a _specification_
, denoted $V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$, is a pair
$(\mathcal{Q},\mathcal{W}_{p})$.888This definition is extended in Definition
A.1 of Appendix A.1 to include allocation events. We elide such events here,
as they do not modify the intuition behind the presentation. A _valid_
specification $V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ satisfies
the axioms in Figure LABEL:subfig:concurrent-spec-history.

We now focus on the first step, i.e., showing the existence of the linear
order, for a valid specification. We sketch the construction here, with the
full proof in Appendix A.1.

######  Lemma 4.1.

Given relations $\mathrel{\lessdot}_{{p}}$, $\mathrel{\ltimes}_{{p}}$ and
_valid_ specification $V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$,
there is a linear order $\leq$ over $\overline{T}$, such that
${({\prec}\cup{\sqsubset})}\subseteq{\leq}$ and property (4) holds.

###### Proof sketch.

Define relation
${\vartriangleleft}\mathrel{\>\widehat{=}\>}{(\sqsubset\cup\prec)^{+}}$, i.e.,
the transitive closure of the union of the general visibility and returns-
before relations. Let $\trianglelefteq$ be its reflexive closure. We show that
$\trianglelefteq$ is a partial order and can be extended into a linear order.

First, axiom $C_{\ref{vis-ax::cc-no-future-dependence}}$ ensures that
$\trianglelefteq$ is a partial order over $\overline{T}$ (Lemma A.5 in
Appendix A.1). Intuitively, $C_{\ref{vis-ax::cc-no-future-dependence}}$ states
that events do not look for dependencies into their real-time future, so that
cycles will not be inserted when $\prec$ is combined with $\sqsubset$,
ensuring irreflexivity of $\vartriangleleft$.

Second, given an _arbitrary_ partial order extension $\leq$ of
$\trianglelefteq$ (over domain $\overline{T}$), axiom $C_{\ref{vis-ax::cc-no-
in-between}}$ ensures property (4). Indeed, if there is such write $z$, then
axiom $C_{\ref{vis-ax::cc-no-in-between}}$ says that $z$ is separable before
$x$ or after $y$. But $\leq$ contains $\trianglelefteq$ (hence the separable-
before relation as well), which means that $z$ must also occur in $\leq$
before $x$ or after $y$ (Contradiction).

Third, since any partial order can be extended to a linear order,999See
topological sorting algorithms [16]. choose some linear order $\leq$ extending
$\trianglelefteq$. Notice that $\leq$ will satisfy (4) because it is a partial
order extension of $\trianglelefteq$. Also, $\leq$ contains ${\prec}$ and
${\sqsubset}$, since $\leq$ contains $\trianglelefteq$ by construction. ∎

Now that we have a linear order $\leq$ that respects both $\prec$ and
$\sqsubset$, for the second step in the linearizability proof we show that
$\leq$ is sequentially sound.

We need to show that executing the events in the order of $\leq$ produces
outputs that match the outputs registered in each event. To define the notion
of execution of events in MCAS, we introduce a state-based sequential
operational semantics. States for MCAS are memory heaps. Let us denote by
$H\xrightarrow{proc(in)\ \langle out\rangle}H^{\prime}$ the statement that
procedure $proc$ with input $in$ executes atomically on heap $H$, produces
output $out$ and modifies the heap into $H^{\prime}$. We can then define the
effect of the mcas procedure on a heap by the following operational semantics
(we will focus only on mcas, for the rest of procedures in MCAS, see
Definition A.13 in Appendix A.3),

  * •

$H\xrightarrow{\textit{mcas}(\overline{u})\ \langle false\rangle}H$, if for
some $j\in\overline{u}$, $H({pt}_{j})\neq{exp}_{j}$.

  * •

$H\xrightarrow{\textit{mcas}(\overline{u})\ \langle
true\rangle}{H}[{{{pt}_{j}}\mapsto{{new}_{j}}}]_{j\in\overline{u}}$, if for
every $j\in\overline{u}$, $H({pt}_{j})={exp}_{j}$.

The first case corresponds to a failing execution in which some input pointer
does not have the expected value, while the second case corresponds to a
successful execution in which all input pointers have their expected values
and the pointers mutate into their new values.

Executing $\leq$ then translates to proving the existence of a path in the
operational semantics such that the $i$-th event $x_{i}$ in $\leq$ matches the
$i$-th procedure in the path, and if $x_{i}\in T$, then ${x_{i}}.\textit{out}$
matches the $i$-th output in the path. Notice that the existence of the path
implicitly assigns an output to those events in $\overline{T}\setminus T$.

The hypothesis of validity of the specification $V^{\textsc{M}}$ for MCAS,
will ensure the existence of such a path, as the following lemma shows (the
full proof is in Appendix A.3).

######  Lemma 4.2.

Given relations $\mathrel{\lessdot}_{{p}}$, $\mathrel{\ltimes}_{{p}}$ such
that $V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is
valid, the linear order $\leq$ of Lemma 4.1 is sequentially sound.

###### Proof sketch.

We prove by induction on $n$ the following claim, so that sequential soundness
follows by applying the claim with $n=\lvert\overline{T}\rvert$.

######  Claim.

For any $1\leq_{\mathbb{N}}n\leq_{\mathbb{N}}\lvert\overline{T}\rvert$, there
is a path of length $n$ starting from the empty heap that matches $\leq$ from
the $1$-th event to the $n$-th event.

We focus on the inductive case, as the base case $n=1$ must have an alloc as
first event in $\leq$ (see Lemma A.17 in Appendix A.3 for details). The
inductive hypothesis provides a path of length $n$ that matches $\leq$ up to
the $n$-th event,

$\displaystyle H_{0}=\emptyset\xrightarrow{proc_{1}(in_{1})\
\left<out_{1}\right>}H_{1}\xrightarrow{proc_{2}(in_{2})\
\left<out_{2}\right>}H_{2}\ldots\xrightarrow{proc_{n}(in_{n})\
\left<out_{n}\right>}H_{n}$ (5)

We need to show that we can extend the path with a $(n+1)-st$ step that
matches the $(n+1)-st$ event in $\leq$. We case analyze the $(n+1)-st$ event.
Let us focus on the $\textit{mcas}(\overline{u})$ case (see Lemma A.17 in
Appendix A.3 for the other cases).

From Axiom $C_{\ref{vis-ax::cc-return-completion}}$ and the definition of
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$, we have
that event $\textit{mcas}(\overline{u})$ must satisfy for some
$v\in\textsc{Bool}$,

$\displaystyle\begin{cases}\forall i\in\overline{u}.\ \exists z.\
{z}\mathrel{\lessdot}_{{{pt}_{i}}}{\textit{mcas}(\overline{u})}\wedge\textsc{writer}\
{z}\ {{pt}_{i}}\ {{exp}_{i}}&\text{ if }v=true\\\ \exists
i\in\overline{u},v^{\prime}\in\textsc{Val}.\ \exists z.\
{z}\mathrel{\lessdot}_{{{pt}_{i}}}{\textit{mcas}(\overline{u})}\wedge\textsc{writer}\
{z}\ {{pt}_{i}}\ {v^{\prime}}\wedge v^{\prime}\neq{{exp}_{i}}&\text{ if
}v=false\end{cases}$

Focusing on the $v=true$ case, event $\textit{mcas}(\overline{u})$ must be
observing at every input pointer ${pt}_{i}$ an event $z$ that wrote the
expected value ${exp}_{i}$ into ${pt}_{i}$. Notice that $z$ must be a write
thanks to Axiom $C_{\ref{vis-ax::cc-observed-are-writes}}$. Since path (5)
matches $\leq$ and $z$ is an event occurring before
$\textit{mcas}(\overline{u})$ (i.e.,
${z}\mathrel{\lessdot}_{{{pt}_{i}}}{\textit{mcas}(\overline{u})}$ implies
$z<\textit{mcas}(\overline{u})$), $z$ must be one of the $proc_{k}$’s in the
path, which means that $H_{k}({pt}_{i})={exp}_{i}$. In addition, property (4)
ensures that there is no other write to pointer ${pt}_{i}$ between $z$ and
$\textit{mcas}(\overline{u})$, which means that there is no ${pt}_{i}$-write
in path (5) from $proc_{k}$ up to $proc_{n}$, having as consequence that
$H_{n}({pt}_{i})={exp}_{i}$ (see Lemma A.15 in Appendix A.3). Since this
happens with every input pointer, heap $H_{n}$ contains the expected values in
the input pointers, so that we can augment path (5) with the step
$H_{n}\xrightarrow{\textit{mcas}(\overline{u})\ \langle
true\rangle}{H_{n}}[{{{pt}_{i}}\mapsto{{new}_{i}}}]_{i\in\overline{u}}$. In
case $\textit{mcas}(\overline{u})\in T$, Axiom $C_{\ref{vis-ax::cc-return-
completion}}$ also ensures that
$true=v={\textit{mcas}(\overline{u})}.\textit{out}$, so that the new step
matches $\leq$. The case $v=false$ is similar. ∎

Together, Lemmas 4.1 and 4.2 imply the following theorem.

######  Theorem 4.1.

Given an implementation of MCAS, suppose that for any set of events Ev
generated from an arbitrary execution history in the implementation, there are
relations $\mathrel{\lessdot}_{{p}}$, $\mathrel{\ltimes}_{{p}}$ such that
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},{\mathrel{\ltimes}_{{p}}})$ is valid.
Then, the implementation is linearizable.

###### Proof.

Let Ev be a set of events generated from an arbitrary execution history in the
implementation. From the hypothesis,
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},{\mathrel{\ltimes}_{{p}}})$ is valid
for some $\mathrel{\lessdot}_{{p}}$ and $\mathrel{\ltimes}_{{p}}$. Let $\leq$
be the linear order of Lemma 4.1. Then, we take $\prec$ and $\leq$ to be the
relations required by Definition 4.1. By construction, $\leq$ respects both
$\prec$ and $\sqsubset$. Also, $\leq$ is sequentially sound by Lemma 4.2. ∎

##  5 Axiomatizing Spans and Proving Visibility

This section fills the remaining gap in our proofs of linearizability and
concludes the technical development. Again, we illustrate with the helping
MCAS implementation, relegating RDCSS and opportunistic MCAS to Appendices C.1
and D, respectively.

To prove that the implementation in Figure 3 is linearizable, Theorem 4.1
requires exhibiting two relations $\mathrel{\lessdot}_{{p}}$,
$\mathrel{\ltimes}_{{p}}$ that make the MCAS specification
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ valid. We
will show that the separable-before (1) and observation (2) relations from
Section 3.3 suffice. In this section, $\mathrel{\ltimes}_{{p}}$ and
$\mathrel{\lessdot}_{{p}}$ refer to (1) and (2), respectively. As apparent,
$\mathrel{\ltimes}_{{p}}$ and $\mathrel{\lessdot}_{{p}}$ are defined in terms
of spans. While Section 3.3 describes spans informally, here we make the
definitions formal and abstract, via a notion of _span structure_.

We shall postulate a number of axioms that a span structure must satisfy. Our
proof obligations for validity of
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ then split
into two parts. First, we show that if the span structure we define for MCAS
satisfies the axioms, then
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is valid,
and thus, by Theorem 4.1, MCAS is linearizable. Second, we show that the span
structure for MCAS satisfies the axioms. We remark that the first part of the
proof is actually more general, as it also applies to RDCSS; indeed, it only
uses the span axioms and definitions (1) and (2), which are shared with RDCSS
(see Appendix B).

###  5.1 Intuition

Successful execution. subfig:successful-execution[0.47]  Failing execution.
subfig:failing-execution[0.47]

Figure 9: Spans of $\textit{mcas}(\overline{u})$. Full spans represent
successful help attempts, and are shown as line segments. Collapsed spans
represent failed help attempts, and are represented as dots. Encircled spans
are the ones chosen to formally denote the execution of the
$\textit{mcas}(\overline{u})$ event. All spans write into the same descriptor.
All full spans share the same ending rep event—the successful CAS at line 14
that changes the descriptor status—represented as a vertical line on the
right. The span with $\checkmark$ indicates that the thread that started the
span, successfully executed the CAS at line 14.

As mentioned in Section 3.3.3, we can use many different definitions of spans,
as long as they satisfy the span invariants (i.e., span axioms, to be
presented in Section 5.2). In particular, we shall use two different kinds of
spans: full and collapsed spans, illustrated in Figure 9 as line segments and
dots, respectively. A _full span_ starts when the successful rdcss at line 31
in Figure 3 writes the descriptor, and finishes when the descriptor status is
updated at line 14, as explained in Section 3.3.3. A _collapsed span_ is any
failing rdcss at line 31 that returns the non-expected Val value; thus, a
collapsed span corresponds to a failed help attempt. Figure 9 shows how full
and collapsed spans interact in two kinds of executions of
$\textit{mcas}(\overline{u})$.

Successful execution of $\textit{mcas}(\overline{u})$ (Figure
LABEL:subfig:successful-execution) occurs when a descriptor $d$ is created at
line 24 containing the entries in $\overline{u}$, each full span writes the
descriptor $d$ into each entry pointer of $\overline{u}$, and the thread that
executed the last full span sets the descriptor status to Succ (indicated in
the figure with a $\checkmark$).

While the actual successful execution of $\textit{mcas}(\overline{u})$ may
witness both kinds of spans (as evident in Figure LABEL:subfig:successful-
execution), it is only the full spans writing $d$ that explain the successful
outcome. Indeed, a collapsed span may arise if the considered pointer did not
contain the expected value when help was attempted. However, such a failed
help attempt must be followed by a full span at the same pointer, or else the
execution of $\textit{mcas}(\overline{u})$ would not be successful. Such a
full span overrides any prior collapsed span at the same pointer, and, along
with other full spans, ultimately explains the overall outcome of the
$\textit{mcas}(\overline{u})$.

This is why we use the set of full spans as the semantic abstraction (i.e.,
_denotation_) of the successful execution of $\textit{mcas}(\overline{u})$,
and represent this in Figure LABEL:subfig:successful-execution by encircling
the full spans only. It is this denotation that our span axioms apply to. For
example, we introduced the bunching invariant in Section 3.3.1 to hold of a
number of spans if they share a common subinterval. As evident from Figure
LABEL:subfig:successful-execution, bunching holds of the encircled spans.
However, it would fail if, for example, the collapsed span (dot) on $p_{2}$
were to be encircled as well, since this dot does not overlap with the segment
on $p_{n}$.

Failing execution of $\textit{mcas}(\overline{u})$ (Figure
LABEL:subfig:failing-execution) occurs when a descriptor $d$ is created at
line 24 containing the entries $\overline{u}$, and:

  * •

there is an entry $j\in\overline{u}$ such that some collapsed span failed to
write descriptor $d$ into the $j$-th pointer,

  * •

there are full spans that write descriptor $d$ into each pointer of entries
$i<j$, and

  * •

the thread that executed the collapsed span for the $j$-th entry managed to
set the descriptor status to Fail using the CAS in line 14 (the collapsed span
for the $j$-th entry is indicated in the figure with a $\checkmark$).

As encircled in Figure LABEL:subfig:failing-execution, the full spans writing
$d$ for entries $i<j$, along with the $\checkmark$-ed collapsed span, explain
the failed outcome of $\textit{mcas}(\overline{u})$, and thus we use this set
of spans as the denotation for the failed $\textit{mcas}(\overline{u})$ event.

The collapsed spans for entries $i<j$, the full spans following the
$\checkmark$-ed collapsed span, and the full and collapsed spans for entries
$i>j$, do not influence the Fail outcome of $\textit{mcas}(\overline{u})$,
because the $\checkmark$-ed collapsed span is the one responsible for setting
the status to Fail. In other words, the thread executing the $\checkmark$-ed
span ultimately confirms the failure by setting the descriptor status to Fail
at the CAS.

As in the successful case, we apply our span axioms to the denotation of a
failing $\textit{mcas}(\overline{u})$. For example, while bunching holds for
the encircled spans in Figure LABEL:subfig:failing-execution, it would fail if
we additionally encircled the full span on $p_{j}$.

###  5.2 Axiomatizing Spans

We now formalize spans via the notion of span structure, so that invariants
(now called span axioms), like bunching and disjointness, are stated
independently of the span definitions (e.g., as in Section 3.3.2, where the
argument for $C_{\ref{vis-ax::cc-no-in-between}}$ depended solely on the
disjointness invariant, and not on the span definition). We first need a
helper notion of rep events.

##### Rep events.

_Rep events_ are generated by the invocation of a code line inside a
procedure. For example, invoking line 14 in Figure 3 produces a rep event. We
do not assume that rep events are atomic, because events in Ev may become rep
events from the point of view of another implementation; for example, the
exportable procedures in the RDCSS implementation are used as primitive
procedures in MCAS. If $x$ is a rep event, ${x}.\textit{start}$,
${x}.\textit{end}$, and ${x}.\textit{out}$ denotes its start time, ending
time, and output, respectively. Since rep events are not atomic, we assume
that we are given a linearization $\leq^{R}$ on rep events, and use
$[\leq^{R}]$ to denote the domain of this relation. The set of all rep events
in an execution history is denoted as Rep. The distinction between events (Ev)
and rep events is standard in the theory of linearizability [14].

##### Span Structure.

A _span structure_
$(\mathcal{S}_{p},\mathcal{S}^{W}_{p},\left\llbracket{\cdot}\right\rrbracket)$
consists of:

  * •

For every pointer $p$, a set
$\mathcal{S}_{p}\subseteq\textsc{Rep}\times\textsc{Rep}$, called the _spans_
accessing $p$.

  * •

For every pointer $p$, a set $\mathcal{S}^{W}_{p}\subseteq\mathcal{S}_{p}$,
called the _successful write spans_ into $p$.

  * •

A function
$\left\llbracket{\cdot}\right\rrbracket:\textsc{Ev}\rightarrow(\mathcal{P}(\bigcup_{p}\mathcal{S}_{p})\times(\textsc{Val}\cup\\{\bot\\}))$,
called _event denotation_ , written $\left\llbracket{x}\right\rrbracket$ for
event $x$. Here, $\mathcal{P}(\bigcup_{p}\mathcal{S}_{p})$ denotes the power
set of $\bigcup_{p}\mathcal{S}_{p}$.

Each span in $\mathcal{S}_{p}$ is a pair of rep events, encoding the end
points of the span. We denote as $f$ (“first”) and $l$ (“last”) the standard
pair projection functions. A collapsed span has coinciding end-points $(a,a)$,
and is abbreviated as $(a)$.

Set $\mathcal{S}^{W}_{p}$ collects spans that mutate state, for example, those
full spans in Figure LABEL:subfig:successful-execution that set their
descriptor status to Succ.

The denotation $\left\llbracket{x}\right\rrbracket$ for event
$x\in\textsc{Ev}$ returns a pair, whose first component is the set of spans
belonging to $x$, and whose second component is the output associated with the
denotation ($\bot$ if no output is defined). Intuitively, the denotation
models the closed path encircling the spans in Figure 9, together with its
associated output.

We define
$\mathcal{S}(x)\mathrel{\>\widehat{=}\>}\pi_{1}({\left\llbracket{x}\right\rrbracket})$
to be the set of spans in the denotation of $x$;
$\mathcal{S}_{p}(x)\mathrel{\>\widehat{=}\>}\mathcal{S}(x)\cap\mathcal{S}_{p}$
to be the set of $p$-accessing spans in the denotation of $x$.101010This is
the notation we already used in Section 3.3 and in definitions (1) and (2).
Also, we define
$o({x})\mathrel{\>\widehat{=}\>}\pi_{2}({\left\llbracket{x}\right\rrbracket})$
to be the denotation output of event $x$.111111It is essential to not confuse
$o({x})$ with the event’s output ${x}.\textit{out}$. An event $x$ may have
${x}.\textit{out}$ undefined because $x$ has not terminated, but still have
$o({x})$ defined because $x$ executed the corresponding spans and is ready to
terminate. For terminated events, the two values coincide.

##### Span returns-before relation.

Relation ${b}\sqsubset^{S}{c}\mathrel{\>\widehat{=}\>}{l({b})}<^{R}{f({c})}$
states that span $b$ terminates before $c$ starts in the linearization of rep
events. ${b}\sqsubset^{S}{c}$ can be interpreted as “$b$ resolves its
descriptor before $c$ writes its own”.

##### Implementation by a span structure.

Given arbitrary relations $\mathrel{\lessdot}_{{p}}$,
$\mathrel{\ltimes}_{{p}}$, we say that
$V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ (which is a pair
$(\mathcal{W}_{p},\mathcal{Q})$) is _implemented by span structure_
$(\mathcal{S}_{p},\mathcal{S}^{W}_{p},\left\llbracket{\cdot}\right\rrbracket)$
if all the span axioms in Figure 10 are satisfied. We also say that
$V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is _implemented by
spans_ if there exists some span structure that implements it. The idea is
that the span axioms imply the validity of
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$, as per the
following theorem, which thus, together with Theorem 4.1, reduces
linearizability to proving the span axioms.

######  Theorem 5.1.

If $V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is
implemented by spans, then
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is
valid.121212This is theorem B.1 stated in a more general form in Appendix B,
here instantiated with $\mu=\textsc{M}$.

Defined notions for span axioms.fig::sub::span-defined-spans  Span returns-
before relation
${b}\sqsubset^{S}{c}\mathrel{\>\widehat{=}\>}{l({b})}<^{R}{f({c})}$ Set of
spans in denotation
$\mathcal{S}(x)\mathrel{\>\widehat{=}\>}\pi_{1}({\left\llbracket{x}\right\rrbracket})$
Denotation output
$o({x})\mathrel{\>\widehat{=}\>}\pi_{2}({\left\llbracket{x}\right\rrbracket})$

Key Axiomsfig::sub::span-spans-key-axioms  ($S_{1}$) Disjointness ($S_{2}$)
Bunching
$b,c\in\mathcal{S}_{p}\implies({{b}\sqsubset^{S}{c}}\vee{{c}\sqsubset^{S}{b}}\vee{b=c})$
$b,c\in\mathcal{S}(x)\implies{f({b})}\leq^{R}{l({c})}$ ($S_{3}$) Adequacy
$x\in T\implies o({x})={x}.\textit{out}\wedge\mathcal{S}(x)\neq\emptyset$

Structural Axiomsfig::sub::span-spans-structural-axioms  ($S_{4}$)
${f({b})}\leq^{R}{l({b})}$ ($S_{5}$)
$\mathcal{S}(x)\cap\mathcal{S}(y)\neq\emptyset\implies x=y$ ($S_{6}$)
$b\in\mathcal{S}^{W}_{p}\implies\exists x.\ b\in\mathcal{S}(x)$ ($S_{7}$)
$\mathcal{S}(x)\neq\emptyset\implies
o({x})\neq\bot\wedge\mathcal{Q}_{{x},{o({x})}}$ ($S_{8}$)
$\mathcal{S}(x)\neq\emptyset\implies(x\in\mathcal{W}_{p}\Leftrightarrow\mathcal{S}(x)\cap\mathcal{S}^{W}_{p}\neq\emptyset)$
($S_{9}$) (i)
$b\in\mathcal{S}(x)\implies{x}.\textit{start}\leq_{\mathbb{N}}{f({b})}.\textit{start}$
(ii) $(b\in\mathcal{S}(x)\wedge x\in T)\implies{}$ $\exists i\in[\leq^{R}].\
{i}.\textit{end}\leq_{\mathbb{N}}{x}.\textit{end}\wedge{l({b})}\leq^{R}{i}$

Figure 10: Span axioms for span structure
$(\mathcal{S}_{p},\mathcal{S}^{W}_{p},\left\llbracket{\cdot}\right\rrbracket)$
implementing
$V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})=(\mathcal{W}_{p},\mathcal{Q})$.
Variables $x$, $y$ range over Ev. Variables $b$, $c$ over
$\bigcup_{p}\mathcal{S}_{p}$. Variable $p$ over pts. The list omits three
axioms involving allocs, which are shown in Figure 12 of Appendix B.

We now explain the span axioms. The first two axioms formalize the
disjointness and bunching invariants from Section 3.3. The remaining axioms
relate the code to the span structure and formalize book-keeping invariants
required for the proofs.

##### Key Axioms.

_Disjointness Axiom $S_{\ref{span::descriptors-do-not-interfere}}$_ states
that spans accessing the same pointer $p$ do not overlap, i.e., any descriptor
in $p$ must be resolved before another one is written in $p$. _Bunching Axiom
$S_{\ref{span::all-descriptors-are-written-before-any-resolution}}$_ states
that any two spans executed by the same event must overlap. In other words, no
descriptor can be resolved unless all descriptors pertinent to the event have
been written first (i.e., $f({b})\leq^{R}l({c})$, pairwise, for all spans $b$,
$c$ in the event’s denotation). _Adequacy Axiom $S_{\ref{span::finished-
operations-have-a-run}}$_ states that for terminated events, the denotation
output coincides with the event’s output, and the event contains at least one
span. This axiom is proved by showing that executing the actual code produces
the denotation. For example, proving adequacy for an mcas event amounts to
showing that the code does produce the spans encircled in Figures
LABEL:subfig:successful-execution and LABEL:subfig:failing-execution, as shown
in Theorem 5.2 of Section 5.3.

##### Structural Axioms.

_Axiom $S_{\ref{span::descriptor-write-precedes-resolution}}$_ justifies
calling functions $f$, $l$ the first and last rep events in a span. The axiom
states that writing a descriptor precedes its resolution. _Axiom
$S_{\ref{span::runs-are-injective}}$_ states that denotations of different
events do not share spans. _Axiom $S_{\ref{span::writer-blocks-belong-to-
runs}}$_ states that successful writer spans must belong to the denotation of
some event (i.e. mutations do not occur “out of thin air”). Although it is
possible to strengthen the axiom to _all_ spans, this is not required for
correctness since non-writer spans can spuriously occur in the execution
history as they do not have an effect that could be discovered by other spans.
_Axiom $S_{\ref{span::postcondition-predicate-holds}}$_ considers an event
$x$, which has completed its execution, though it need not have terminated
yet. We identify the completion of the execution with the set of spans in
$x$’s denotation being nonempty (i.e. $\mathcal{S}(x)\neq\emptyset$). The
axiom then says that $x$ produced a denotation output and $x$’s postcondition
predicate must hold at $x$’s denotation output, as if $x$ has terminated.
_Axiom $S_{\ref{span::writers-have-writer-blocks}}$_ states that successful
$p$-write events must contain a successful $p$-writer span in their
denotation. _Axiom $S_{\ref{span::blocks-contained-in-abstract-time-
interval}}$_ describes the relation between an event’s duration and the spans
in its denotation. The first part of Axiom $S_{\ref{span::blocks-contained-in-
abstract-time-interval}}$ says that spans in a denotation start (in real time)
after the event starts. The second part of Axiom $S_{\ref{span::blocks-
contained-in-abstract-time-interval}}$ says that spans in a denotation finish
(according to the rep linearization) before some rep event $i$ that witnesses
the event’s end in real-time. For the second part, we cannot require the
stronger property ${l({b})}.\textit{end}\leq_{\mathbb{N}}{x}.\textit{end}$
because spans may be ended by threads different from the one invoking $x$,
which means that $l({b})$ could still be executing by the time $x$
finishes.131313Recall that rep events are not required to be atomic.

###  5.3 Proving the Span Axioms for MCAS

By Theorem 5.1, the problem of proving linearizability of MCAS reduces to
defining a span structure $S^{\textsc{M}}$ that implements the MCAS
specification
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$. Here we
define $S^{\textsc{M}}$ by using the code for mcas in Figure 3. Appendix C.2
gives the full definition of $S^{\textsc{M}}$ using the full code in Figure
14, which contains procedures elided from Figure 3. Then, we show that
$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is
implemented by span structure $S^{\textsc{M}}$, i.e, that mcas satisfies the
span axioms.

Intuitively, structure $S^{\textsc{M}}$ encodes the ideas presented in Section
5.1. Set $\mathcal{S}_{p}$ contains all full and collapsed spans accessing
pointer $p$, defined as follows,

  * •

A _full_ span at pointer $p$ is a tuple $(a,b)$ of rep events $a$, $b$, where
$a$ is the successful rdcss at line 31 writing some descriptor $d$ in $p$, and
$b$ is the successful CAS at line 14 updating $d$’s status to either Succ or
Fail.

  * •

A _collapsed_ span at pointer $p$ is $(c)$, where rep event $c$ is an rdcss at
line 31 that fails to write a descriptor into $p$ (i.e., $c$ returns a Val
value different from the expected value).

Set $\mathcal{S}^{W}_{p}$ contains all spans $(a,b)\in\mathcal{S}_{p}$ where
$b$ updates the status to Succ. The denotation
$\left\llbracket{x}\right\rrbracket$ for $x=\textit{mcas}(\overline{u})$ is
defined by cases, encoding the two kinds of executions discussed in Section
5.1,

  * •

(Successful execution)
$\left\llbracket{x}\right\rrbracket\mathrel{\>\widehat{=}\>}(\\{(a_{i},b)\in\mathcal{S}_{{pt}_{i}}\mid
i\in\overline{u}\\},\textit{true})$, where each $a_{i}$ wrote in ${pt}_{i}$
the same descriptor $d$ (created at line 24) containing the entries
$\overline{u}$, and $b$ is the unique CAS at line 14 that successfully updated
$d$’s status to Succ.

  * •

(Failing execution)
$\left\llbracket{x}\right\rrbracket\mathrel{\>\widehat{=}\>}(\\{(a_{i},b)\in\mathcal{S}_{{pt}_{i}}\mid
i<j\\}\cup\\{(c)\\},\textit{false})$, where each $a_{i}$ wrote in ${pt}_{i}$
the same descriptor $d$ (created at line 24) containing the entries
$\overline{u}$; $b$ is the unique CAS at line 14 that successfully updated
$d$’s status to Fail; $b$ and $c$ are executed by some thread $T$ such that
$c$ is the failed rdcss at line 31 that attempted to write $d$ and is the most
recent such rdcss preceding $b$ in the control flow of $T$; and $j$ is the
entry in which $c$ failed to write $d$ (i.e., $c$ failed to write in pointer
${pt}_{j}$).

  * •

$\left\llbracket{x}\right\rrbracket\mathrel{\>\widehat{=}\>}(\emptyset,\bot)$,
if the history does not satisfy the previous two cases.

In both non-empty cases of the definition of
$\left\llbracket{x}\right\rrbracket$, full spans are uniquely determined,
because the descriptor $d$ is unique to the mcas invocation. Moreover, once
$b$ changes $d$’s status, $d$ cannot be written nor its status be changed,
since both the rdcss and CAS at lines 31, 14 expect the Undec status. Hence,
for each $i$, $\mathcal{S}_{{pt}_{i}}$ contains at most one full span writing
$d$. Additionally, in the failing execution, $(c)$ is uniquely determined
because it is executed by the same thread $T$ that executed $b$. More
specifically, when $T$ executes $c$ at line 31 (descriptor write attempt),
immediately after $c$ fails, $T$ exits the writeall procedure at line 13 and
executes $b$ (descriptor status change), meaning that $c$ is the instruction
immediately preceding $b$ in the control flow of $T$.

The empty case of the definition of $\left\llbracket{x}\right\rrbracket$ is
when the denotation is undefined. It is the role of the adequacy axiom
$S_{\ref{span::finished-operations-have-a-run}}$ to ensure that this case does
not arise for terminated events, and therefore that the denotation correctly
captures the spans that are executed by the code of a terminated mcas.

With this definition for $S^{\textsc{M}}$, we have the following theorem,
which together with theorems 4.1 and 5.1 implies that mcas is linearizable.

######  Theorem 5.2.

$V^{\textsc{M}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is
implemented by span structure $S^{\textsc{M}}$.

###### Proof sketch.

We consider only the case of the mcas procedure in Figure 3, focusing on the
proof of the adequacy axiom, in the case when mcas returns $\mathit{true}$.
The proof of the $\mathit{false}$ case and the other span axioms are found in
their respective lemmas in Appendix C.2, which uses the full code in Figure
14.

Since $\textit{mcas}(\overline{u})$ returned $true$, line 15 in Figure 3 must
have read the status pointer of descriptor $d$ to be Succ (where $d$ was
created at line 24). This implies that some thread $T^{\prime}$ (which could
be $T$ as well) must have set $d$’s status pointer to Succ at line 14, and
$T^{\prime}$ must have finished the execution of writeall with a Succ at line
13. Since writeall is a recursive method which only recurses when it needs to
try again, and we know that $T^{\prime}$ finished executing writeall,
$T^{\prime}$ must have reached an invocation of writeall that did not recurse,
i.e., an invocation of writeall where lines 34-35 were not executed. So, we
can assume we are on such execution.

Since writeall returned Succ, thread $T^{\prime}$ must have tried all the
entries inside the loop. For each entry $i\in\overline{u}$, $T^{\prime}$ must
have tried to write $d$ using the rdcss at line 31. The rdcss must have
returned either $d$ or the expected value ${exp}_{i}$ (it cannot return a
descriptor different from $d$, because lines 34-35 would be executed). If the
returned value was the expected value ${exp}_{i}$, then the rdcss succeeded
(since we already know that $d$’s status was set to Succ by $T^{\prime}$
later, and $d$’s status is Undec previous to the change). If the rdcss at line
31 returned $d$, then some other thread (or $T^{\prime}$ in a previous
recursive writeall invocation) already wrote the descriptor. In other words,
in both cases, the descriptor was written. Since $d$ was written for each
entry and its status pointer was set to Succ later, this corresponds to the
successful case in
$\left\llbracket{\textit{mcas}(\overline{u})}\right\rrbracket$, which has as
output $true$ and the denotation is not empty. ∎

##  6 Related and Future Work

##### Proofs of RDCSS and MCAS

A number of papers have considered linearizability of MCAS and RDCSS using
LPs. For MCAS, the PhD thesis of Vafeiadis [21] and the original paper of
Harris et al. [11] are the main sources for the LP proof. For RDCSS,
Vafeiadis’ PhD thesis proposed the use of _prophecy variables_ [1] to model
that the LPs of RDCSS depend on future events. The argument was later
mechanized in Coq by Liang and Feng [18] using _speculations_ (related to
prophecy variables, but less general), and eventually using prophecy variables
in Iris [15]. Both speculations and prophecies lead to operational proofs, as
they essentially codify the LPs of the methods. Our proofs, being declarative,
do not rely on speculations or prophecies, but use spans and visibility as the
common abstractions that unify RDCSS and MCAS. That said, we have not
mechanized our proofs yet.

##### Visibility relations in other contexts

Our approach uses visibility relations to model the ordering dependencies
between events, by axiomatizing the notions of observation and separation. A
general survey of the use of visibility relations in concurrency and
distributed systems is given by Viotti and Vukolić [22]. Visibility relations
and declarative proofs have also been utilized to specify consistency criteria
weaker than linearizability (Emmi and Enea [8]), to introduce a specification
framework for weak memory models (Raad et al. [20]), and to specify the RC11
memory model (Lahav et al. [17]). In particular, for the RC11 model [17], our
observation relation is reminiscent of the reads-from relation, and there may
be a potential connection between our separable-before and the (extended)
coherence order in RC11. However, the extended coherence order in RC11 is
defined in terms of reads-from, while in our approach, observation and
separable-before are independent abstract relations linked by the visibility
axioms.

In contrast to the above papers that focus on the semantics of consistency
criteria, our use of visibility relations focuses on verifying specific
algorithms and data structures, and is thus closer to the following work where
visibility relations are applied to concurrent queues (Henzinger et al. [13,
6]), concurrent stacks (Dodds et al. [7]), and memory snapshot algorithms
(Öhman and Nanevski [19]). We differ from these in the addressed structures,
RDCSS and MCAS, which, unlike the related work, further utilize helping.

##### Alternative RDCSS and MCAS implementations

The implementations of RDCSS and MCAS that we used here were originally
developed by Harris et al. [11]. However, there are alternative
implementations as well. For example, Arbel-Raviv and Brown [3] present a
variant of RDCSS where pointers to descriptors are reused instead of being
created at each RDCSS invocation. Guerraoui et al. [10] present an MCAS
implementation that does not use RDCSS as a subroutine, and that uses a
minimal amount of CAS calls. Guerraoui et al. also survey a number of other
MCAS implementations. Feldman et al. [9] present a wait-free implementation of
MCAS (the implementation we used here is only lock-free).

In the future, we will consider how our axioms apply to these alternative
implementations. For example, our span axioms are agnostic in that they impose
no restriction on how many times a pointer to a descriptor can be used across
spans. Thus, we expect that our axiomatization will be able to handle
implementations with descriptor reuse, such as those of Arbel-Raviv and Brown
[3]. Similarly, we expect that we could handle MCAS of Guerraoui et al. [10],
as it too should satisfy the span axioms. Indeed, this implementation follows
the general outline of MCAS by writing the descriptor into all input pointers
before any descriptor resolution is attempted.

##### Observation and separation as a general methodology

The pattern suggested by Sections 3.1 and 3.2, where one starts with a
history-based sequential specification and transforms it into a concurrent
specification by replacing the returns-before relation $\sqsubset$ with a
separable-before relation $\mathrel{\ltimes}_{{p}}$ defined in terms of gaps
between events, points towards a general methodology for obtaining visibility
relations for a given data structure. We have also attempted the pattern on
queues, and found that it does derive a variant of the queue axioms of
Henzinger et al. [13, 6] and applies to the queue of Herlihy and Wing [14]. In
the future, we plan to study if this pattern applies to other concurrent data
structures (e.g., memory snapshots, trees, lists, sets, etc.) and if the
induced notions of observation and separation are usable in more general
settings (e.g., to address other flavors of helping [12]).

##  7 Conclusions

In this paper, we show that axiomatization of visibility relations are a
powerful alternative to linearization points, when it comes to verifying
linearizability of a number of helping algorithms with common semantic
structure. In particular, we applied the technique to the descriptor-based
algorithms RDCSS and MCAS, identifying and axiomatizing the relations of
separation and observation between events. We achieved further abstraction by
axiomatizing the notion of spans to model how help requests bunch together in
these algorithms, and to allow expressing the separation and disjointness of
the bunches.

## References

  * [1] Martín Abadi and Leslie Lamport.  The existence of refinement mappings.  Theoretical Computer Science (TCS), 82(2):253–284, 1991.  doi:10.1016/0304-3975(91)90224-P.
  * [2] Vitaly Aksenov, Petr Kuznetsov, and Anatoly Shalyto.  On helping and stacks.  In International Conference on Networked Systems (NETYS), pages 107–121, 2019.  doi:10.1007/978-3-030-05529-5_8.
  * [3] Maya Arbel-Raviv and Trevor Brown.  Reuse, don’t recycle: transforming lock-free algorithms that throw away descriptors.  In International Symposium on Distributed Computing (DISC), pages 4:1–4:16, 2017.  doi:10.4230/LIPIcs.DISC.2017.4.
  * [4] Hagit Attiya, Armando Castañeda, and Danny Hendler.  Nontrivial and universal helping for wait-free queues and stacks.  Journal of Parallel and Distributed Computing, 121:1–14, 2018.  doi:10.1016/j.jpdc.2018.06.004.
  * [5] Keren Censor-Hillel, Erez Petrank, and Shahar Timnat.  Help!  In ACM Symposium on Principles of Distributed Computing (PODC), pages 241–250, 2015.  doi:10.1145/2767386.2767415.
  * [6] Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis.  Aspect-oriented linearizability proofs.  Logical Methods in Computer Science (LMCS), 11(1), 2015.  doi:10.2168/LMCS-11(1:20)2015.
  * [7] Mike Dodds, Andreas Haas, and Christoph M. Kirsch.  A scalable, correct time-stamped stack.  In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, pages 233–246, 2015.  URL: http://doi.acm.org/10.1145/2676726.2676963, doi:10.1145/2676726.2676963.
  * [8] Michael Emmi and Constantin Enea.  Weak-consistency specification via visibility relaxation.  Proc. ACM Program. Lang., 3(POPL):60:1–60:28, 2019.  doi:10.1145/3290373.
  * [9] Steven Feldman, Pierre Laborde, and Damian Dechev.  A wait-free multi-word compare-and-swap operation.  International Journal of Parallel Programming, 43(4):572–596, 2015\.  doi:10.1007/s10766-014-0308-7.
  * [10] Rachid Guerraoui, Alex Kogan, Virendra J. Marathe, and Igor Zablotchi.  Efficient multi-word compare and swap.  In International Symposium on Distributed Computing (DISC), pages 4:1–4:19, 2020.  doi:10.4230/LIPIcs.DISC.2020.4.
  * [11] Timothy L. Harris, Keir Fraser, and Ian A. Pratt.  A practical multi-word compare-and-swap operation.  In International Symposium on Distributed Computing (DISC), pages 265–279, 2002.  doi:10.1007/3-540-36108-1_18.
  * [12] Danny Hendler, Itai Incze, Nir Shavit, and Moran Tzafrir.  Flat combining and the synchronization-parallelism tradeoff.  In ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 355–364, 2010.  doi:10.1145/1810479.1810540.
  * [13] Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis.  Aspect-oriented linearizability proofs.  In International Conference on Concurrency Theory (CONCUR), pages 242–256, 2013.  doi:10.1007/978-3-642-40184-8_18.
  * [14] Maurice P. Herlihy and Jeannette M. Wing.  Linearizability: a correctness condition for concurrent objects.  ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3):463–492, 1990.  doi:10.1145/78969.78972.
  * [15] Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs.  The future is ours: prophecy variables in separation logic.  Proc. ACM Program. Lang., 4(POPL):45:1–45:32, 2020.  doi:10.1145/3371113.
  * [16] A. B. Kahn.  Topological sorting of large networks.  Commun. ACM, 5(11):558–562, 1962.  doi:10.1145/368996.369025.
  * [17] Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer.  Repairing sequential consistency in c/c++11.  In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, page 618–632, New York, NY, USA, 2017. Association for Computing Machinery.  doi:10.1145/3062341.3062352.
  * [18] Hongjin Liang and Xinyu Feng.  Modular verification of linearizability with non-fixed linearization points.  SIGPLAN Not., 48(6):459–470, 2013.  doi:10.1145/2499370.2462189.
  * [19] Joakim Öhman and Aleksandar Nanevski.  Visibility reasoning for concurrent snapshot algorithms.  Proc. ACM Program. Lang., 6(POPL):33:1–33:30, 2022.  doi:10.1145/3498694.
  * [20] Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis.  On library correctness under weak memory consistency: Specifying and verifying concurrent libraries under declarative consistency models.  Proc. ACM Program. Lang., 3(POPL), jan 2019.  doi:10.1145/3290381.
  * [21] Viktor Vafeiadis.  Modular fine-grained concurrency verification.  PhD thesis, University of Cambridge, Computer Laboratory, 2008.  URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-726.pdf, doi:10.48456/tr-726.
  * [22] Paolo Viotti and Marko Vukolić.  Consistency in non-transactional distributed storage systems.  ACM Comput. Surv., 49(1):19:1–19:34, 2016.  doi:10.1145/2926965.

##  Appendix A Proof of Linearizability for RDCSS and MCAS

###  A.1 Common definitions and results

This section has results that apply to both the RDCSS and MCAS data
structures. In particular, the section focuses on the first step of the
linearization proof (see gray box in Figure 1), which is proving the existence
of the linear order. Sections A.2 and A.3 then prove sequential soundness of
the linear order for RDCSS and MCAS, respectively.

######  Definition A.1 (Specification).

Given two pointer-indexed relations
${\mathrel{\lessdot}_{{p}}}\subseteq\textsc{Ev}\times\textsc{Ev}$
(_observation relation_) and
${\mathrel{\ltimes}_{{p}}}\subseteq\textsc{Ev}\times\textsc{Ev}$ (_separable-
before relation_), a _specification_ , denoted
$V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$, is a triple
$(\mathcal{W}_{p},\mathcal{A}_{p},\mathcal{Q})$ consisting of:

  * •

A pointer-indexed set ${\mathcal{W}_{p}}\subseteq\textsc{Ev}$ (called
_successful write events_).

  * •

A pointer-indexed set ${\mathcal{A}_{p}}\subseteq\textsc{Ev}$ (called _alloc
events_).

  * •

A predicate
${\mathcal{Q}}:\textsc{Ev}\times\textsc{Val}\rightarrow\textsc{Bool}$ (called
_postcondition predicate_). We denote by $\mathcal{Q}_{{x},{v}}$ the
application of $\mathcal{Q}$ to $x\in\textsc{Ev}$ and $v\in\textsc{Val}$.

Given relations $\mathrel{\lessdot}_{{p}}$, $\mathrel{\ltimes}_{{p}}$, we say
that
$V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})=(\mathcal{W}_{p},\mathcal{A}_{p},\mathcal{Q})$
is _valid_ if all the _visibility axioms_ from Figure LABEL:fig:helpingstruct
are satisfied.

Defined notions for visibility axioms.fig:defined-notions-axioms  General
visibility relation
${\prec}\mathrel{\>\widehat{=}\>}\bigcup_{p}(\mathrel{\lessdot}_{{p}}\cup\mathrel{\ltimes}_{{p}})$
Returns-before relation
${e}\sqsubset{e^{\prime}}\mathrel{\>\widehat{=}\>}{e}.\textit{end}<_{\mathbb{N}}{e^{\prime}}.\textit{start}$
Set of terminated events
$T\mathrel{\>\widehat{=}\>}\\{e\mid{e}.\textit{end}\neq\bot\\}$ Closure of
terminated events $\overline{T}\mathrel{\>\widehat{=}\>}\\{e\mid\exists t\in
T.\ e\mathrel{{\prec}^{*}}t\\}$

Visibility axioms for the validity of
$V(\mathrel{\lessdot}_{{p}},{\mathrel{\ltimes}_{{p}}})=(\mathcal{W}_{p},\mathcal{A}_{p},\mathcal{Q})$.fig:helpingstruct
($C_{1}$) No in-between $({w}\mathrel{\lessdot}_{{p}}{r}\wedge
w^{\prime}\in\mathcal{W}_{p})\implies({w^{\prime}}\mathrel{\mathrel{\vbox{\offinterlineskip\hbox{\phantom{$\ltimes$}}\vskip-1.50696pt\hbox{$\ltimes$}\vskip-1.50696pt\hbox{$-$}}}}_{{p}}{w}\vee{r}\mathrel{\mathrel{\vbox{\offinterlineskip\hbox{\phantom{$\ltimes$}}\vskip-1.50696pt\hbox{$\ltimes$}\vskip-1.50696pt\hbox{$-$}}}}_{{p}}{w^{\prime}})$
($C_{2}$) Observed events are writes ${w}\mathrel{\lessdot}_{{p}}{-}\implies
w\in\mathcal{W}_{p}$ ($C_{3}$) No future dependences
${x}\prec^{+}{y}\implies{y}\not\sqsubseteq{x}$ ($C_{4}$) Return value
completion $\exists v.\ \mathcal{Q}_{{x},{v}}\wedge(x\in T\implies
v={x}.\textit{out})$ ($C_{5}$) Allocation uniqueness
$w,w^{\prime}\in\mathcal{A}_{p}\implies w=w^{\prime}$ ($C_{6}$) Written
pointers are allocated $w\in\mathcal{W}_{p}\implies\exists
w^{\prime}\in\mathcal{A}_{p}.\
{w^{\prime}}\mathrel{\mathrel{\vbox{\offinterlineskip\hbox{\phantom{$\ltimes$}}\vskip-1.50696pt\hbox{$\ltimes$}\vskip-1.50696pt\hbox{$-$}}}}_{{p}}{w}$

Figure 11: Visibility Axioms. Variables $w$, $w^{\prime}$, $r$, $x$, $y$ range
over $\overline{T}$. Variables $e$, $e^{\prime}$ range over Ev. Variables $p$
and $v$ over pts and Val, respectively.

Section 3.2 already explained axioms $C_{\ref{help-focused::non-helpers}}$
through $C_{\ref{help-focused::fin-predicate}}$. Here, we quickly mention the
rest. Axiom $C_{\ref{help-focused::allocs}}$ states that pointers are created
by at most one alloc. Axiom $C_{\ref{help-focused::all-writers-are-willing-
helpers}}$ states that for any successful $p$-write, there must exist a
$p$-alloc separable before the write. Intuitively, this just expresses that
input pointers must have been created by previous allocs.

######  Definition A.2 (Section Hypotheses).

To shorten the statements of the lemmas and theorems, we will assume the
following hypotheses along this entire section,

  * •

Ev is an arbitrary set of events.

  * •

$\mathrel{\lessdot}_{{p}}$ and $\mathrel{\ltimes}_{{p}}$ are two arbitrary
pointer-indexed binary relations over Ev.

  * •

$V(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$ is an arbitrary valid
specification.

######  Lemma A.1.

Suppose hypotheses A.2. Relation $\prec$ is acyclic on $\overline{T}$.

###### Proof.

Suppose there is a cycle for some $x\in\overline{T}$. Hence, ${x}\prec^{+}{x}$
holds. But, by Axiom $C_{\ref{help-focused::vis-acyclic}}$,
${x}\not\sqsubseteq{x}$ must hold, which means $x\neq x$ (Contradiction). ∎

######  Lemma A.2.

Suppose hypotheses A.2. Relation $\sqsubseteq$ is a partial order on Ev. In
addition, $\sqsubset$ satisfies the interval order property,

$\forall w,x,y,z\in\textsc{Ev}.\
({w}\sqsubset{x}\wedge{y}\sqsubset{z})\rightarrow({w}\sqsubset{z}\vee{y}\sqsubset{x})$

###### Proof.

To show that $\sqsubseteq$ is a partial order, it is enough to show that
$\sqsubset$ is irreflexive and transitive, because it is a standard result
that the reflexive closure of an irreflexive and transitive relation is a
partial order.

  * •

Irreflexivity. If ${x}\sqsubset{x}$, then we would have
${x}.\textit{end}<_{\mathbb{N}}{x}.\textit{start}\leq_{\mathbb{N}}{x}.\textit{end}$,
which is a contradiction.

  * •

Transitivity. If ${x}\sqsubset{y}$ and ${y}\sqsubset{z}$, then
${x}.\textit{end}<_{\mathbb{N}}{y}.\textit{start}\leq_{\mathbb{N}}{y}.\textit{end}<_{\mathbb{N}}{z}.\textit{start}$,
which means ${x}.\textit{end}<_{\mathbb{N}}{z}.\textit{start}$. Hence,
${x}\sqsubset{z}$.

We now show that $\sqsubset$ satisfies the interval order property.

Let ${w}\sqsubset{x}$ and ${y}\sqsubset{z}$. Hence,
${w}.\textit{end}<_{\mathbb{N}}{x}.\textit{start}$ and
${y}.\textit{end}<_{\mathbb{N}}{z}.\textit{start}$.

Either ${w}.\textit{end}<_{\mathbb{N}}{z}.\textit{start}$ or
${z}.\textit{start}\leq_{\mathbb{N}}{w}.\textit{end}$. The first case leads to
${w}\sqsubset{z}$.

For the second case, by using the hypotheses, we have
${y}.\textit{end}<_{\mathbb{N}}{z}.\textit{start}\leq_{\mathbb{N}}{w}.\textit{end}<_{\mathbb{N}}{x}.\textit{start}$.
Therefore, ${y}\sqsubset{x}$. ∎

######  Lemma A.3.

Suppose hypotheses A.2. Let $n>_{\mathbb{N}}0$. If $a_{0}R_{1}a_{1}R_{2}\ldots
R_{n-1}a_{n-1}R_{n}a_{n}$ is a sequence of $n$ steps where each $R_{i}$ is
either $\prec$ or $\sqsubset$, and each $a_{i}\in\overline{T}$, then
${a_{n}}\not\sqsubseteq{a_{0}}$.

###### Proof.

By strong induction on $n$.

  * •

Case $n=1$. So, we have $a_{0}R_{1}a_{1}$.

If $R_{1}={\prec}$, then from ${a_{0}}\prec{a_{1}}$ and Axiom $C_{\ref{help-
focused::vis-acyclic}}$, we get ${a_{1}}\not\sqsubseteq{a_{0}}$.

If $R_{1}={\sqsubset}$, then from ${a_{0}}\sqsubset{a_{1}}$, we cannot have
${a_{1}}\sqsubseteq{a_{0}}$, because we would get $a_{0}\sqsubset
a_{1}\sqsubseteq a_{0}$ (Contradiction by Lemma A.2).

  * •

Inductive case. Let $a_{0}R_{1}a_{1}R_{2}\ldots R_{n}a_{n}R_{n+1}a_{n+1}$ be a
sequence of $n+1$ steps.

If all $R_{i}$ are $\prec$, then ${a_{n+1}}\not\sqsubseteq{a_{0}}$ follows by
Axiom $C_{\ref{help-focused::vis-acyclic}}$.

Therefore, we can assume that for some
$1\leq_{\mathbb{N}}i\leq_{\mathbb{N}}n+1$, we have $R_{i}={\sqsubset}$, i.e.,

$\displaystyle\overbrace{a_{0}R_{1}\ldots R_{i-1}a_{i-1}}^{i-1\text{
steps}}\sqsubset\overbrace{a_{i}R_{i+1}\ldots R_{n+1}a_{n+1}}^{n-i+1\text{
steps}}$ (6)

Suppose for a contradiction that ${a_{n+1}}\sqsubseteq{a_{0}}$.

If $a_{n+1}=a_{0}$. Then,

$a_{i}R_{i+1}\ldots R_{n}a_{n}R_{n+1}a_{0}R_{1}\ldots R_{i-1}a_{i-1}$

is a sequence of $(n-i+1)+(i-1)=n$ steps. Therefore, by the inductive
hypothesis, ${a_{i-1}}\not\sqsubseteq{a_{i}}$, which contradicts (6).

It remains to check the case ${a_{n+1}}\sqsubset{a_{0}}$.

    * –

Subcase $i=1$. Hence, ${a_{n+1}}\sqsubset{a_{0}}\sqsubset a_{1}$.

But ${a_{1}}R_{2}\ldots R_{n+1}{a_{n+1}}$ is a sequence of $n$ steps.
Therefore, by the inductive hypothesis, ${a_{n+1}}\not\sqsubseteq{a_{1}}$
(Contradiction).

    * –

Subcase $i=n+1$. Hence, ${a_{n}}\sqsubset{a_{n+1}}\sqsubset a_{0}$.

But ${a_{0}}R_{1}\ldots R_{n}{a_{n}}$ is a sequence of $n$ steps. Therefore,
by the inductive hypothesis, ${a_{n}}\not\sqsubseteq{a_{0}}$ (Contradiction).

    * –

Subcase $1<_{\mathbb{N}}i<_{\mathbb{N}}n+1$.

Since ${a_{i-1}}\sqsubset{a_{i}}$ and ${a_{n+1}}\sqsubset{a_{0}}$, by Lemma
A.2, either ${a_{i-1}}\sqsubset{a_{0}}$ or ${a_{n+1}}\sqsubset{a_{i}}$.

But $a_{0}R_{1}\ldots R_{i-1}a_{i-1}$ is a sequence with
$0<_{\mathbb{N}}i-1<_{\mathbb{N}}n$ steps and $a_{i}R_{i+1}\ldots
R_{n+1}a_{n+1}$ is a sequence with $0<_{\mathbb{N}}n-i+1<_{\mathbb{N}}n$
steps. Therefore, by the inductive hypothesis,
${a_{i-1}}\not\sqsubseteq{a_{0}}$ and ${a_{n+1}}\not\sqsubseteq{a_{i}}$
(Contradiction).

∎

######  Definition A.3.

Define the _happens-before_ relation
${\vartriangleleft}\mathrel{\>\widehat{=}\>}{(\prec\cup\sqsubset)^{+}}$, i.e.,
the transitive closure of the union of the general visibility and returns-
before relations.

######  Lemma A.4.

Suppose hypotheses A.2. The relation $\vartriangleleft$ is irreflexive on
$\overline{T}$.

###### Proof.

If ${x}\vartriangleleft{x}$, then for some $n>_{\mathbb{N}}0$, there is a
sequence $a_{0}R_{1}\ldots R_{n}a_{n}$ of $n$ steps, where each $R_{i}$ is
either $\prec$ or $\sqsubset$, each $a_{i}\in\overline{T}$ and $a_{0}=x$, and
$a_{n}=x$.

But by Lemma A.3, we would have ${x}\not\sqsubseteq{x}$ which is a
contradiction. ∎

######  Lemma A.5.

Suppose hypotheses A.2. The relation $\trianglelefteq$ is a partial order on
$\overline{T}$.

###### Proof.

It is a standard result that the reflexive closure of an irreflexive and
transitive relation is a partial order. Hence, $\trianglelefteq$ is a partial
order on $\overline{T}$ by Lemma A.4 and the fact that $\vartriangleleft$ is
transitive by definition. ∎

######  Lemma A.6.

Suppose hypotheses A.2. Set $\overline{T}$ is $\prec$-downward closed. In
other words, if $x\in\overline{T}$ and ${y}\prec{x}$, then $y\in\overline{T}$.

###### Proof.

Since $x\in\overline{T}$, there is $z\in T$ such that
$x\mathrel{{\prec}^{*}}z$. So $y\prec x\mathrel{{\prec}^{*}}z$ which means
$y\in\overline{T}$. ∎

######  Lemma A.7.

Suppose hypotheses A.2. Given a partial order $\leq$ over $\overline{T}$ such
that ${\trianglelefteq}\subseteq{\leq}$, the following holds,

$\displaystyle\forall x,y\in\overline{T}.\
{x}\mathrel{\lessdot}_{{p}}{y}\implies\neg\exists
z\in\mathcal{W}_{p}\cap\overline{T}.\ x<z<y$ (7)

###### Proof.

Let ${x}\mathrel{\lessdot}_{{p}}{y}$. Suppose for a contradiction that $x<z<y$
for some $z\in\mathcal{W}_{p}\cap\overline{T}$.

By Axiom $C_{\ref{help-focused::non-helpers}}$, either
${y}\mathrel{\ltimes}_{{p}}{z}$ or ${z}\mathrel{\ltimes}_{{p}}{x}$ or $y=z$ or
$x=z$.

  * •

Case ${y}\mathrel{\ltimes}_{{p}}{z}$. Since
${\trianglelefteq}\subseteq{\leq}$, we have $y<z$. But by hypothesis $z<y$
(Contradiction).

  * •

Case ${z}\mathrel{\ltimes}_{{p}}{x}$. Since
${\trianglelefteq}\subseteq{\leq}$, we have $z<x$. But by hypothesis $x<z$
(Contradiction).

  * •

Case $y=z$. This contradicts hypothesis $z<y$.

  * •

Case $x=z$. This contradicts hypothesis $x<z$.

∎

######  Lemma A.8.

Suppose hypotheses A.2. There is a linear order $\leq$ over $\overline{T}$
containing $\prec$ and $\sqsubset$, such that property (7) holds.

###### Proof.

Any finite partial order is contained in a linear order [16]. Pick some linear
order $\leq$ containing the partial order $\trianglelefteq$ over
$\overline{T}$.

By Lemma A.7, property (7) holds. ∎

###  A.2 Linearizability Proof for the RDCSS Data Structure

This section focuses on proving, for the RDCSS data structure, sequential
soundness of the linear order built in Lemma A.8. This section makes use of
Definition A.1.

######  Definition A.4 (Exportable Procedures in the RDCSS Data Structure).

The following are the exportable procedures in the RDCSS Data Structure,

$\textit{rdcss}(d:\textsc{rdesc})$ | (RDCSS for descriptor $d$)
---|---
$\textit{ralloc}(v:\textsc{Val},\ k:\textsc{ptKind})$ | (Allocation of pointer kind $k\in\\{\textsc{cptr},\textsc{dptr}\\}$)
$\textit{rCAS}(p:\textsc{dptr},\ e:\textsc{Val},\ n:\textsc{Val})$ | (CAS for data pointers)
$\textit{rwrite}(p:\textsc{dptr},\ v:\textsc{Val})$ | (Write for data pointers)
$\textit{rread}(p:\textsc{dptr})$ | (Read for data pointers)
$\textit{rCAS-c}(p:\textsc{cptr},\ e:\textsc{Val},\ n:\textsc{Val})$ | (CAS for control pointers)
$\textit{rwrite-c}(p:\textsc{cptr},\ v:\textsc{Val})$ | (Write for control pointers)
$\textit{rread-c}(p:\textsc{cptr})$ | (Read for control pointers)

For each $x\in\textsc{Ev}$ and pointer $p$, we define the _writer predicate_
$\textsc{writer}\ {x}\ {p}\ {v}$.

######  Definition A.5 (Writer Predicate for the RDCSS Data Structure).

The _writer predicate_
$\textsc{writer}\subseteq\textsc{Ev}\times\textsc{pts}\times\textsc{Val}$,
denoted $\textsc{writer}\ {x}\ {p}\ {v}$, is defined by cases,

$\displaystyle\textsc{writer}\ {x}\ {p}\ {v}\mathrel{\>\widehat{=}\>}$
$\displaystyle(\exists d.\ x=\textit{rdcss}(d)\wedge p={d}.pt_{2}\wedge
v={d}.new_{2})\vee{}$
$\displaystyle(x=\textit{ralloc}(v,\\_)\wedge{x}.\textit{end}\neq\bot\wedge
p={x}.\textit{out})\vee{}$ $\displaystyle x=\textit{rCAS}(p,\\_,v)\vee
x=\textit{rwrite}(p,v)\vee{}$ $\displaystyle x=\textit{rCAS-c}(p,\\_,v)\vee
x=\textit{rwrite-c}(p,v)$

Predicate $\textsc{writer}\ {x}\ {p}\ {v}$ denotes the value $v$ in
${x}.\textit{in}$ that $x$ will attempt to write into pointer $p$.

Notice that for the case of allocs, writer is defined only after the alloc has
finished, since writer depends on the pointer generated by the alloc. We only
need to consider terminated allocs because any procedure $x$ requires in its
input the pointers produced by allocs at the moment $x$ is invoked.

We now define the specification for the RDCSS data structure.

######  Definition A.6 (Specification for the RDCSS Data Structure).

Given relations $\mathrel{\lessdot}_{{p}}$, $\mathrel{\ltimes}_{{p}}$, we
define the specification for the RDCSS data structure, denoted
$V^{\textsc{R}}(\mathrel{\lessdot}_{{p}},\mathrel{\ltimes}_{{p}})$, as
follows,

$\displaystyle x\in\mathcal{A}_{p}$
$\displaystyle\mathrel{\>\widehat{=}\>}x=\textit{ralloc}(\\_,\\_)\wedge{x}.\textit{end}\neq\bot\wedge
p={x}.\textit{out}$ $\displaystyle x\in\mathcal{W}_{p}$
$\displaystyle\mathrel{\>\widehat{=}\>}\begin{cases}p={d}.pt_{2}\wedge\exists
z_{1},z_{2}.\
{z_{1}}\mathrel{\lessdot}_{{{d}.pt_{1}}}{x}\wedge{z_{2}}\mathrel{\lessdot}_{{{d}.pt_{2}}}{x}\wedge{}&\text{if
}x=\textit{rdcss}(d)\\\ \quad\textsc{writer}\ {z_{1}}\ {{d}.pt_{1}}\
{{d}.exp_{1}}\wedge\textsc{writer}\ {z_{2}}\ {{d}.pt_{2}}\ {{d}.exp_{2}}&\\\
{x}.\textit{end}\neq\bot\wedge p={x}.\textit{out}&\text{if
}x=\textit{ralloc}(\\_,\\_)\\\ p=q\wedge\exists z.\
{z}\mathrel{\lessdot}_{{q}}{x}\wedge\textsc{writer}\ {z}\ {q}\ {e}&\text{if
}x=\textit{rCAS}(q,e,\\_)\\\ p=q&\text{if }x=\textit{rwrite}(q,\\_)\\\
p=q\wedge\exists z.\ {z}\mathrel{\lessdot}_{{q}}{x}\wedge\textsc{writer}\ {z}\
{q}\ {e}&\text{if }x=\textit{rCAS-c}(q,e,\\_)\\\ p=q&\text{if
}x=\textit{rwrite-c}(q,\\_)\\\ \end{cases}$
$\displaystyle\mathcal{Q}_{{x},{v}}$
$\displaystyle\mathrel{\>\widehat{=}\>}\begin{cases}\exists z_{2}.\
{z_{2}}\mathrel{\lessdot}_{{{d}.pt_{2}}}{x}\wedge\textsc{writer}\ {z_{2}}\
{{d}.pt_{2}}\ {v}\wedge{}&\text{if }x=\textit{rdcss}(d)\\\
\quad(v={d}.exp_{2}\implies\exists z_{1}.\
{z_{1}}\mathrel{\lessdot}_{{{d}.pt_{1}}}{x})&\\\
{x}.\textit{end}\neq\bot\wedge v={x}.\textit{out}&\text{if
}x=\textit{ralloc}(\\_,\\_)\\\ \exists z.\
{z}\mathrel{\lessdot}_{{q}}{x}\wedge\textsc{writer}\ {z}\ {q}\ {v}&\text{if
}x=\textit{rCAS}(q,\\_,\\_)\\\ v=tt&\text{if }x=\textit{rwrite}(\\_,\\_)\\\
\exists z.\ {z}\mathrel{\lessdot}_{{q}}{x}\wedge\textsc{writer}\ {z}\ {q}\
{v}&\text{if }x=\textit{rread}(q)\\\ \exists z.\
{z}\mathrel{\lessdot}_{{q}}{x}\wedge\textsc{writer}\ {z}\ {q}\ {v}&\text{if
}x=\textit{rCAS-c}(q,\\_,\\_)\\\ v=tt&\text{if
}x=\textit{rwrite-c}(\\_,\\_)\\\ \exists z.\
{z}\mathrel{\lessdot}_{{q}}{x}\wedge\textsc{writer}\ {z}\ {q}\ {v}&\text{if
}x=\textit{rread-c}(q)\\\ \end{cases}$

We have the following immediate lemma,

######  Lemma A.9.

If $x\in\mathcal{W}_{p}$, then there is $v\in\textsc{Val}$ such that
$\textsc{writer}\ {x}\ {p}\ {v}$.

###### Proof.

By cases on $x$.

  * •

Case $x=\textit{rdcss}(d)$. We have $p={d}.pt_{2}$ and $\textsc{writer}\ {x}\
{p}\ {{d}.new_{2}}$ follows by definition of writer.

  * •

Case $x=\textit{ralloc}(v,\\_)$. We have $p={x}.\textit{out}$ and
$\textsc{writer}\ {x}\ {p}\ {v}$ follows by definition of writer.

  * •

Case $x=\textit{rCAS}(q,\\_,n)$. We have $p=q$ and $\textsc{writer}\ {x}\ {p}\
{n}$ follows by definition of writer.

  * •

Case $x=\textit{rwrite}(q,v)$. We have $p=q$ and $\textsc{writer}\ {x}\ {p}\
{v}$ follows by definition of writer.

  * •

Cases when $x$ is one of $\textit{rCAS-c}(q,\\_,n)$ or
$\textit{rwrite-c}(q,v)$ are similar.

∎

Towards defining the notion of sequential soundness for a linear order over
events in RDCSS, we need to describe what it means for events to execute. For
that matter, we define the following state-based operational semantics, so
that intuitively, events execute by building a path in the operational
semantics.

######  Definition A.7 (Operational semantics for events in the RDCSS Data
Structure).

Let $Op^{R}$ denote the operational semantics generated by the following base
steps, where states are heaps and labels are of the form “$proc(in)\ \langle
out\rangle$” where $proc$ is the procedure name, $in$ the procedure’s input,
and $out$ the procedure’s output.

  * •

$H\xrightarrow{\textit{rdcss}(d)\ \langle v\rangle}H$, if $H({d}.pt_{2})=v$
and $v\neq{d}.exp_{2}$.

  * •

$H\xrightarrow{\textit{rdcss}(d)\ \langle{d}.exp_{2}\rangle}H$, if
$H({d}.pt_{2})={d}.exp_{2}$ and $H({d}.pt_{1})\neq{d}.exp_{1}$.

  * •

$H\xrightarrow{\textit{rdcss}(d)\
\langle{{d}.exp_{2}}\rangle}{H}[{{{d}.pt_{2}}\mapsto{{d}.new_{2}}}]$, if
$H({d}.pt_{2})={d}.exp_{2}$ and $H({d}.pt_{1})={d}.exp_{1}$.

  * •

$H\xrightarrow{\textit{ralloc}(v,\\_)\ \langle p\rangle}{H}[{{p}\mapsto{v}}]$,
if $p\notin dom(H)$.

  * •

$H\xrightarrow{\textit{rCAS}(p,e,\\_)\ \langle v\rangle}H$, if $H(p)=v$ and
$v\neq e$.

  * •

$H\xrightarrow{\textit{rCAS}(p,e,n)\ \langle e\rangle}{H}[{{p}\mapsto{n}}]$,
if $H(p)=e$.

  * •

$H\xrightarrow{\textit{rwrite}(p,v)\ \langle tt\rangle}{H}[{{p}\mapsto{v}}]$,
if $p\in dom(H)$.

  * •

$H\xrightarrow{\textit{rread}(p)\ \langle v\rangle}H$, if $H(p)=v$.

  * •

$H\xrightarrow{\textit{rCAS-c}(p,e,\\_)\ \langle v\rangle}H$, if $H(p)=v$ and
$v\neq e$.

  * •

$H\xrightarrow{\textit{rCAS-c}(p,e,n)\ \langle e\rangle}{H}[{{p}\mapsto{n}}]$,
if $H(p)=e$.

  * •

$H\xrightarrow{\textit{rwrite-c}(p,v)\ \langle
tt\rangle}{H}[{{p}\mapsto{v}}]$, if $p\in dom(H)$.

  * •

$H\xrightarrow{\textit{rread-c}(p)\ \langle v\rangle}H$, if $H(p)=v$.

We now define the notion of sequential soundness of a linear order $\leq$.

######  Definition A.8 (Sequential soundness of a linear order).

Given a linear order $\leq$ over a set of events, and a path $P$ in the
operational semantics $Op^{R}$, we say that $P$ _matches_ $\leq$ if for every
step $i$ in $P$,

  * •

The $i$-th procedure’s name in $P$ equals the procedure’s name of the $i$-th
event in $\leq$.

  * •

The $i$-th procedure’s input in $P$ equals the procedure’s input of the $i$-th
event in $\leq$.

  * •

If the $i$-th event in $\leq$ is terminated, then the $i$-th procedure’s
output in $P$ equals the $i$-th event output in $\leq$.

We say that $\leq$ is _sequentially sound_ if there is a matching path in
$Op^{R}$, starting from the empty heap and having as many steps as the number
of events in the domain of $\leq$.

######  Notation.

If path $P$ matches $\leq$, and $H\xrightarrow{proc(in)\ \langle
out\rangle}H^{\prime}$ is a step in $P$, we denote by
$\left\llbracket{proc}\right\rrbracket$ the corresponding event in $\leq$.