Proving linearizability using forward simulations

TL;DR

This paper demonstrates that many complex concurrent data structure implementations can be proven linearizable using only forward simulation, simplifying correctness proofs and enabling automation.

Contribution

It shows that forward simulation alone suffices for proving linearizability of complex implementations, challenging the belief that backward reasoning is necessary.

Findings

Many complex implementations can be proved correct with forward simulation.

Forward simulation proofs are simpler and more natural.

These proofs are suitable for automation.

Abstract

Linearizability is the standard correctness criterion concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation.Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy&Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to conceptually simple and natural correctness proofs for these implementations that are amenable to automation.

Equations

$$C=\{inv(m,d,k):m\in \text{<}Methods>,d\in \text{<}Vals>,k\in \text{<}Ops>\}\text{ and }R=\{ret(m,d,k):m\in \text{<}Methods>,d\in \text{<}Vals>,k\in \text{<}Ops>\}$$

$$\frac{\text{vbox}k\notin dom(cp)d\ne \mathtt{EMPTY}\text{vbox}}{\text{vbox}\text{vbox}O,<,\ell ,rv,cp\stackrel{inv(enq,d,k)}{\to }O\cup \{k\},<\cup \mathtt{COMP}(O)\times \{k\},\ell [k\mapsto (d,\mathtt{PEND})],rv,cp[k\mapsto A_1]}$$

$$\mathtt{x}(k_d)=\mathtt{null}\wedge \mathtt{i}(k^{\prime })\le \mathtt{range}(k_d)\wedge \mathtt{i}(k)\le \mathtt{i}(k_d)\le \mathtt{i}(k^{\prime })\wedge (\mathtt{i}(k)=\mathtt{i}(k_d)=>k_d@\mathtt{if}\text{-}\mathtt{inc})$$

$$\frac{\text{vbox}k\notin dom(cp)d\ne \mathtt{EMPTY}\forall k^{\prime }.o{v}^{\prime }(k^{\prime })=ov(k^{\prime })\cup \{k\}\text{vbox}}{\text{vbox}\text{vbox}O,<,\ell ,rv,cp,be,ov\stackrel{inv(push,d,k)}{\to }O\cup \{k\},<\cup \mathtt{COMP}(O)\times \{k\},\ell [k\mapsto (d,\mathtt{PEND})],rv,cp[k\mapsto A_1],be,o{v}^{\prime }}$$

$$C=\{inv(m,d,k):m\in \text{<}Methods>,d\in \text{<}Vals>,k\in \text{<}Ops>\}\text{, and }$$

$$R=\{ret(m,d,k):m\in \text{<}Methods>,d\in \text{<}Vals>,k\in \text{<}Ops>\}$$

$$\frac{\text{vbox}k\notin dom(c{p}^0)d\ne \mathtt{EMPTY}\text{vbox}}{\text{vbox}\text{vbox}\sigma ,i{n}^0,r{v}^0,c{p}^0\stackrel{inv(enq,d,k)}{\to }\sigma ,i{n}^0[k\mapsto d],r{v}^0,c{p}^0[k\mapsto A_1]}$$

$$k\in O\wedge \ell (k)=(d,\mathtt{PEND})\text{mbox}iff$$

$$(c{p}^0(k)=A_1\wedge i{n}^0(k)=d)\vee (\exists i.{\sigma }_i=d\wedge c{p}^0(k)=A\wedge i{n}^0(k)=d)$$

$$k\in O\wedge \ell (k)=(d,\mathtt{COMP})\text{mbox}iff\exists i.{\sigma }_i=d\wedge c{p}^0(k)=A_2\wedge i{n}^0(k)=d$$

$$\frac{\text{vbox}k\notin dom(c{p}^0)d\ne \mathtt{EMPTY}\text{vbox}}{\text{vbox}\text{vbox}\sigma ,i{n}^0,r{v}^0,c{p}^0\stackrel{inv(push,d,k)}{\to }\sigma ,i{n}^0[k\mapsto d],r{v}^0,c{p}^0[k\mapsto A_1]}$$

$$\text{displaystyle@t}=inv(push,d,k),lin(push,d,k),lin(push,d_{i+1},k_{i+1}),\dots ,lin(push,d_{n-1},k_{n-1})$$

$$t\stackrel{inv(push,d,k),lin(push,d,k)lin(pop,d,k^{\prime })}{\to }{t}^{\prime }$$

$$\text{displaystyle@t}=inv(pop,k),lin(pop,d,k),lin(push,d_{i+1},k_{i+1}),\dots ,lin(push,d_{n-1},k_{n-1})$$

$$\frac{\text{vbox}k\notin dom(cp)d\ne \mathtt{null}\text{vbox}}{\text{vbox}\text{vbox}...,O_a,x,cp,...\stackrel{inv(push,d,k)}{\to }...,O_a\cup \{k\},x[k\mapsto d],cp[k\mapsto A_1],...}$$

$$\frac{\text{vbox}k\notin dom(cp)\text{vbox}}{\text{vbox}\text{vbox}...,O_r,cp,...\stackrel{inv(pop,k)}{\to }...,O_r\cup \{k\},cp[k\mapsto R_1],...}$$

Full text

1 Introduction

Programming efficient concurrent implementations of atomic collections, e.g., stacks and queues, is error prone. To minimize synchronization overhead between concurrent method invocations, implementors avoid blocking operations like lock acquisition, allowing methods to execute concurrently. However, concurrency risks unintended inter-operation interference, and risks conformance to atomic reference implementations. Conformance is formally captured by (observational) refinement, which assures that all behaviors of programs using these efficient implementations would also be possible were the atomic reference implementations used instead.

Observational refinement can be formalized as a trace inclusion problem, and the latter can itself be reduced to an invariant checking problem, but this requires in general introducing history and prophecy variables [1]. Alternatively, verifying refinement requires in general establishing a forward simulation and a backward simulation [20]. While simulations are natural concepts, backward reasoning, corresponding to the use of prophecy variables, is in general hard and complex for programs manipulating data structures. Therefore, a crucial issue is to understand the limits of forward reasoning in establishing refinement. More precisely, an important question is to determine for which concurrent abstract data structures, and for which classes of implementations, it is possible to carry out a refinement proof using only forward simulations.

To get rid of backward simulations (or prophecy variables) while preserving completeness w.r.t. refinement, it is necessary to have reference implementations that are deterministic. Interestingly, determinism allows also to simplify the forward simulation checking problem. Indeed, in this case, this problem can be reduced to an invariant checking problem. Basically, the simulation relation can be seen as an invariant of the system composed of the two compared programs. Therefore, existing methods and tools for invariant checking can be leveraged in this context.

But, in order to determine precisely what is meant by determinism, an important point is to fix the alphabet of observable events along computations. Typically, to reason about refinement between two library implementations, the only observable events are the calls and returns corresponding to the method invocations along computations. This means that only the external interface of the library is considered to compare behaviors, and nothing else from the implementations is exposed. Unfortunately, it can be shown that in this case, it is impossible to have deterministic atomic reference implementations for common data structures such as stacks and queues (see, e.g., [24]). Then, an important question is what is the necessary amount of information that should be exposed by the implementations to overcome this problem ?

One approach addressing this question is based on linearizability [17] and its correspondence with refinement [11, 7]. Linearizability of a computation (of some implementation) means that each of the method invocations can be seen as happening at some point, called linearization point, occurring somewhere between the call and return events of that invocation. The obtained sequence of linearization points along the computation should define a sequence of operations that is possible in the atomic reference implementation. Proving the existence of such sequences of linearization points, for all the computations of a concurrent library, is a complex problem [3, 5, 13]. However, proving linearizability becomes less complex when linearization points are fixed for each method, i.e., associated with the execution of a designated statement in its source code [5]. In this case, we can consider that libraries expose in addition to calls and returns, events signaling linearization points. By extending this way the alphabet of observable events, it becomes straightforward to define deterministic atomic reference implementations. Therefore, proving linearizability can be carried out using forward simulations when linearization points are fixed, e.g., [28, 4, 27, 2]. Unfortunately, this approach is not applicable to efficient implementations such as the LCRQ queue [21] (based on the principle of the Herlihy&Wing queue [17]), and the Time-Stamped Stack [9]. The proofs of linearizability of these implementations are highly nontrivial, very involved, and hard to read, understand and automatize. Therefore, the crucial question we address is what is precisely the kind of information that is necessary to expose in order to obtain deterministic atomic reference implementations for such data structures, allowing to derive simple and natural linearizability proofs for such complex implementations, based on forward simulations, that are amenable to automation ?

We observe that the main difficulty in reasoning about these implementations is that, linearization points of enqueue/push operations occurring along some given computation, depend in general on the linearization points of dequeue/pop operations that occur arbitrarily far in the future. Therefore, since linearization points for enqueue/push operations cannot be determined in advance, the information that could be fixed and exposed can concern only the dequeue/pop operations.

One first idea is to consider that linearization points are fixed for dequeue/pop methods and only for these methods. We show that under the assumption that implementations expose linearizations points for these methods, it is possible to define deterministic atomic reference implementations for both queues and stacks. We show that this is indeed useful by providing a simple proof of the Herlihy&Wing queue (based on establishing a forward simulation) that can be carried out as an invariant checking proof.

However, in the case of Time-Stamped Stack, fixing linearization points of pop operations is actually too restrictive. Nevertheless, we show that our approach can be generalized to handle this case. The key idea is to reason about what we call commit points, and that correspond roughly speaking to the last point a method accesses to the shared data structure during its execution. We prove that by exposing commit points (instead of linearization points) for pop methods, we can still provide deterministic reference implementations. We show that using this approach leads to a quite simple proof of the Time-Stamped Stack, based on forward simulations.

2 Preliminaries

We formalize several abstraction relations between libraries using a simple yet universal model of computation, namely labeled transition systems (LTS). This model captures shared-memory programs with an arbitrary number of threads, abstracting away the details of any particular programming system irrelevant to our development.

A labeled transition system (LTS) $A=(Q,\Sigma,s_{0},\delta)$ over the possibly-infinite alphabet $\Sigma$ is a possibly-infinite set $Q$ of states with initial state $s_{0}\in Q$, and a transition relation $\delta\subseteq Q\times@S\times Q$. The $i$th symbol of a sequence $@t\in@S^{*}$ is denoted $@t_{i}$, and the empty sequence is denoted by $\epsilon$. An execution of $A$ is an alternating sequence of states and transition labels (called also actions) $\rho=s_{0},e_{0},s_{1}\ldots e_{k-1},s_{k}$ for some $k>0$ such that $\delta(s_{i},e_{i},s_{i+1})$ for each $i$ such that $0\leq i<k$. We write $s_{i}\xrightarrow{e_{i}\ldots e_{j-1}}_{A}s_{j}$ as shorthand for the subsequence $s_{i},e_{i},...,s_{j-1},e_{j-1},s_{j}$ of $\rho$, for any $0\leq i\leq j<k$ (in particular $s_{i}\xrightarrow{\epsilon}s_{i}$). The projection $@t|\Gamma$ of a sequence $@t$ is the maximum subsequence of $@t$ over alphabet $\Gamma$. This notation is extended to sets of sequences as usual. A trace of $A$ is the projection $\rho|\Sigma$ of an execution $\rho$ of $A$. The set of executions, resp., traces, of an LTS $A$ is denoted by $E(A)$, resp., $Tr(A)$. An LTS is deterministic if for any state $s$ and any sequence $@t\in\Sigma^{*}$, there is at most one state $s^{\prime}$ such that $s\xrightarrow{@t}s^{\prime}$. More generally, for an alphabet $\Gamma\subseteq\Sigma$, an LTS is $\Gamma$-deterministic if for any state s and any sequence $@t\in\Gamma^{*}$, there is at most one state $s^{\prime}$ such that $s\xrightarrow{@t^{\prime}}s^{\prime}$ and $@t$ is a subsequence of $@t^{\prime}$.

2.1 Libraries

Programs interact with libraries by calling named library methods, which receive parameter values and yield return values upon completion. We fix arbitrary sets $\<Methods>$ and $\<Vals>$ of method names and parameter/return values. We fix an arbitrary set $\<Ops>$ of operation identifiers, and for given sets $\<Methods>$ and $\<Vals>$ of methods and values, we fix the sets

[TABLE]

of call actions and return actions; each call action $inv(m,d,k)$ combines a method $m\in\<Methods>$ and value $d\in\<Vals>$ with an operation identifier $k\in\<Ops>$. Operation identifiers are used to pair call and return actions. We may omit the second field from a call/return action $a$ for methods that have no inputs or return values. For notational convenience, we take $\<Ops>=\<Nats>$ for the rest of the paper.

A library is an LTS over alphabet $\Sigma$ such that $C\cup R\subseteq\Sigma$. We assume that the traces of a library satisfy standard well-formedness properties, e.g., return actions correspond to previous call actions, which for lack of space are delegated to Appendix 0.A. An operation $k$ is called completed in a trace $\tau$ when $ret(m,d,k)$ occurs in $\tau$, for some $m$ and $d$. Otherwise, it is called pending.

The projection of a library trace over $C\cup R$ is called a history. The set of histories of a library $L$ is denoted by $H(L)$. Since libraries only dictate methods’ executions between their respective calls and returns, for any history they admit, they must also admit histories with weaker inter-operation ordering, in which calls may happen earlier, and/or returns later. A history $h_{1}$ is weaker than a history $h_{2}$, written $h_{1}\sqsubseteq h_{2}$, iff there exists a history $h_{1}^{\prime}$ obtained from $h_{1}$ by appending return actions, and deleting call actions, s.t.: $h_{2}$ is a permutation of $h_{1}^{\prime}$ that preserves the order between return and call actions, i.e., if a given return action occurs before a given call action in $h_{1}^{\prime}$, then the same holds in $h_{2}$.

A library $L$ is called atomic when there exists a set $S$ of sequential histories such that $H(L)$ contains every weakening of a history in $S$. Atomic libraries are often considered as specifications for concurrent objects. Libraries can be made atomic by guarding their methods bodies with global lock acquisitions.

A library $L$ is called a queue implementation when $\<Methods>=\{enq,deq\}$ ($enq$ is the method that enqueues a value and $deq$ is the method removing a value) and $\<Vals>=\<Nats>\cup\{{\tt EMPTY}\}$ where EMPTY is the value returned by $deq$ when the queue is empty. Similarly, a library $L$ is called a stack implementation when $\<Methods>=\{push,pop\}$ and $\<Vals>=\<Nats>\cup\{{\tt EMPTY}\}$. For queue and stack implementations, we assume that the same value is never added twice, i.e., for every trace $@t$ of such a library and every two call actions $inv(m,d_{1},k_{1})$ and $inv(m,d_{2},k_{2})$ where $m\in\{enq,push\}$ we have that $d_{1}\neq d_{2}$. As shown in several works [2, 6], this assumption is without loss of generality for libraries that are data independent, i.e., their behaviors are not influenced by the values added to the collection, which is always the case in practice. On a technical note, this assumption is used to define ($\Gamma$-)deterministic abstract implementations of stacks and queues in Section 4 and Section 5.

2.2 Refinement and Linearizability

Conformance of a library $L_{1}$ to a specification given as an “abstract” library $L_{2}$ is formally captured by (observational) refinement. Informally, we say $L_{1}$ refines $L_{2}$ iff every computation of every program using $L_{1}$ would also be possible were $L_{2}$ used instead. We assume that a program can interact with the library only through call and return actions, and thus refinement can be defined as history set inclusion. Refinement is equivalent to the linearizability criterion [17] when $L_{2}$ is an atomic library [11, 7].

Definition 1

A library $L_{1}$ refines another library $L_{2}$ iff $H(L_{1})\subseteq H(L_{2})$.

Linearizability [17] requires that every history of a concurrent library $L_{1}$ can be “linearized” to a sequential history admitted by a library $L_{2}$ used as a specification. Formally, a sequential history $h_{2}$ with only complete operations is called a linearization of a history $h_{1}$ when $h_{1}\sqsubseteq h_{2}$. A history $h_{1}$ is linearizable w.r.t. a library $L_{2}$ iff there exists a linearization $h_{2}$ of $h_{1}$ such that $h_{2}\in H(L_{2})$. A library $L_{1}$ is linearizable w.r.t. $L_{2}$, written $L_{1}\sqsubseteq L_{2}$, iff each history $h_{1}\in H(L_{1})$ is linearizable w.r.t. $L_{2}$.

Theorem 2.1 ([11, 7])

$L_{1}\sqsubseteq L_{2}$* iff $L_{1}$ refines $L_{2}$, if $L_{2}$ is atomic.*

In the rest of the paper, we discuss methods for proving refinement (and thus, linearizability) focusing mainly on queue and stack implementations.

3 Refinement Proofs

Library refinement is the instance of a more general notion of refinement between LTSs which for some alphabet $\Gamma$ of observable actions is defined as the inclusion of sets of traces projected on $\Gamma$. Library refinement corresponds to the case $\Gamma=C\cup R$. Typically, $\Gamma$-refinement between two LTSs $A$ and $B$ is proved using simulation relations which roughly, require that $B$ can mimic every step of $A$ using a (possibly empty) sequence of steps. Mainly, there are two kinds of simulation relations, forward or backward, depending on whether the preservation of steps is proved starting from a similar state forward or backward. It has been shown that $\Gamma$-refinement is equivalent to the existence of backward simulations, modulo the addition of history variables that record events in the implementation, and to the existence of forward simulations provided that the right-hand side LTS $B$ is $\Gamma$-deterministic [1, 20]. We focus on proofs based on forward simulations because they are easier to automatize.

In general, forward simulations are not a complete proof method for library refinement because libraries are not $C\cup R$-deterministic (the same sequence of call/return actions can lead to different states depending on the interleaving of the internal actions). However, there are classes of atomic libraries, e.g., libraries with “fixed linearization points” (defined later in this section), for which it is possible to identify a larger alphabet $\Gamma$ of observable actions (including call/return actions), and implementations that are $\Gamma$-deterministic. For queues and stacks, Section 4 and Section 5 define other such classes of implementations that cover all the implementations that we are aware of.

Let $L_{1}=(Q_{1},\Sigma,s_{0}^{1},\delta_{1})$ and $L_{2}=(Q_{2},\Sigma,s_{0}^{2},\delta_{2})$ be two libraries over $\Sigma_{1}$ and $\Sigma_{2}$, resp., such that $C\cup R\subseteq\Sigma_{1}\cap\Sigma_{2}$. Also, let $\Gamma$ be a set of actions s.t. $C\cup R\subseteq\Gamma\subseteq\Sigma_{1}\cap\Sigma_{2}$.

Definition 2

The library $L_{1}$ $\Gamma$-refines $L_{2}$ iff $Tr(L_{1})|\Gamma\subseteq Tr(L_{2})|\Gamma$.

Notice that $\Gamma$-refinement implies refinement for any $\Gamma$ as in Definition 2.

We define a notion of forward simulation that can be used to prove $\Gamma$-refinement (a dual notion of backward simulation is defined in Appendix 0.B). For a relation $R\subseteq A\times B$, $R[X]$ is the set of elements related by $R$ to elements of $X$, i.e., $R[X]={\{y:\exists x\in X.\ R(x,y)\}}$.

Definition 3

A relation $\mathit{fs}\subseteq Q_{1}\times Q_{2}$ is called a $\Gamma$-forward simulation from $L_{1}$ to $L_{2}$ iff $\mathit{fs}[s_{0}^{1}]=\{s_{0}^{2}\}$ and:

• •

If $(s,\gamma,s^{\prime})\in\delta_{1}$, for some $\gamma\in\Gamma$, and $u\in\mathit{fs}[s]$, then there exists $u^{\prime}\in\mathit{fs}[s^{\prime}]$ such that $u\xrightarrow{@s}u^{\prime}$, $@s_{i}=\gamma$, for some $i$, and $@s_{j}\in\Sigma_{2}\setminus\Gamma$, for each $j\neq i$.

• •

If $(s,e,s^{\prime})\in\delta_{1}$, for some $e\in\Sigma_{1}\setminus\Gamma$ and $u\in\mathit{fs}[s]$, then there exists $u^{\prime}\in\mathit{fs}[s^{\prime}]$ such that $u\xrightarrow{\sigma}u^{\prime}$ and $\sigma\in(\Sigma_{2}\setminus\Gamma)^{*}$.

A $\Gamma$-forward simulation requires that every step of $L_{1}$ corresponds to a sequence of steps of $L_{2}$. To imply $\Gamma$-refinement, every step of $L_{1}$ labeled by an observable action $\gamma\in\Gamma$ should be simulated by a sequence of steps of $L_{2}$ where exactly one transition is labeled by $\gamma$ and all the other transitions are labeled by non-observable actions.

The following shows the soundness and the completeness of $\Gamma$-forward simulations (when $L_{2}$ is $\Gamma$-deterministic). It is an instantiation of previous results  [1, 20].

Theorem 3.1

$L_{1}$* $\Gamma$-refines $L_{2}$ when there is a $\Gamma$-forward simulation from $L_{1}$ to $L_{2}$. Moreover, if $L_{1}$ $\Gamma$-refines $L_{2}$ and $L_{2}$ is $\Gamma$-deterministic, then there is a $\Gamma$-forward simulation from $L_{1}$ to $L_{2}$.*

The linearization of a concurrent history can be also defined in terms of linearization points. Informally, a linearization point of an operation in an execution is a point in time where the operation is conceptually effectuated; given the linearization points of each operation, the linearization of a concurrent history is the sequential history which takes operations in order of their linearization points. For some libraries, the linearization points correspond to a fixed set of actions. For instance, in the case of atomic libraries where method bodies are guarded with a global-lock acquisition, the linearization point of every method invocation corresponds to the execution of the body. When the linearization points are fixed, we assume that the library is an LTS over an alphabet that includes actions $lin(m,d,k)$ with $m\in\<Methods>$, $d\in\<Vals>$ and $k\in\<Ops>$. The action $lin(m,d,k)$ represents the linearization point of the operation $k$ returning value $d$. Let $Lin$ denote the set of such actions. The projection of a library trace over $C\cup R\cup Lin$ is called an extended history. A trace or extended history is called $Lin$-complete when every completed operation has a linearization point, i.e., each return action $ret(m,d,k)$ is preceded by an action $lin(m,d,k)$. A library $L$ over alphabet $\Sigma$ is called with fixed linearization points iff $C\cup R\cup Lin\subseteq\Sigma$ and every trace $@t\in Tr(L)$ is $Lin$-complete.

Proving the correctness of an implementation $L_{1}$ of a concurrent object such as a queue or a stack with fixed linearization points reduces to proving that $L_{1}$ is a $(C\cup R\cup Lin)$-refinement of an abstract implementation $L_{2}$ of the same object where method bodies are guarded with a global-lock acquisition. Since the abstract implementation is usually $(C\cup R\cup Lin)$-deterministic, by Theorem 3.1, proving $(C\cup R\cup Lin)$-refinement is equivalent to finding a $(C\cup R\cup Lin)$-forward simulation from $L_{1}$ to $L_{2}$.

Section 4 and Section 5 extend this result to queue and stack implementations where the linearization point of the methods adding values to the collection is not fixed.

4 Queues With Fixed Dequeue Linearization Points

The typical abstract implementation of a concurrent queue, denoted as $AbsQ_{0}$, maintains a sequence of values, the enqueue adds a value atomically to the beginning of the sequence, and the dequeue removes a value from the end of the sequence (if any, otherwise it returns EMPTY). Both methods have a fixed linearization point when the update of the sequence happens. For some queue implementations, e.g., the Herlihy&Wing Queue [17] ($\mathit{HWQ}$ for short), there exists no forward simulation to $AbsQ_{0}$ although they are a refinement of $AbsQ_{0}$. The main reason is that the enqueue methods don’t have a fixed linearization point. In this section, we propose a new abstract implementation for queues, denoted as $AbsQ$, which roughly maintains a partially-ordered set of values instead of a sequence. We show that there exists a forward simulation from any correct queue implementation where only the dequeue methods have fixed linearization points (the enqueue methods are unconstrained) to $AbsQ$. This covers all the queue implementations that we are aware of, in particular $\mathit{HWQ}$, Baskets Queue [18], LCRQ [21], or Time-Stamped Queue [9] (where the enqueues don’t have fixed linearization points). We also describe a forward simulation from $\mathit{HWQ}$ to $AbsQ$.

4.1 Enqueue Methods With Non-Fixed Linearization Points

We describe $\mathit{HWQ}$ where the linearization points of the enqueue methods are not fixed. The shared state consists of an array items storing the values in the queue and a counter back storing the index of the first unused position in items. Initially, all the positions in the array are null and back is 0. An enqueue method starts by reserving a position in items (i stores the index of this position and back is incremented so the same position can’t be used by other enqueues) and then, stores the input value x at this position. The dequeue method traverses the array items starting from the beginning and atomically swaps null with the encountered value. If the value is not null, then the dequeue returns that value. If it reaches the end of the array, then it restarts.

The linearization points of the enqueues are not fixed, they depend on dequeues executing in the future. Consider the following trace with two concurrent enqueues (${\tt i}(k)$ represents the value of i in operation $k$): $inv(enq,x,1)$, $inv(enq,y,2)$, ${\tt i}(1)=\mbox{{\tt bck++}}$, ${\tt i}(2)=\mbox{{\tt bck++}}$, ${\tt items[i(}2{\tt)]}=y$. Assuming that the linearization point corresponds to the assignment of i, the history of this trace should be linearized to $inv(enq,x,1)$, $ret(enq,1)$, $inv(enq,y,2)$, $ret(enq,2)$. However, a dequeue executing until completion after this trace will return $y$ (only position $1$ is filled in the array items) which is not consistent with this linearization. On the other hand, assuming that enqueues should be linearized at the assignment of items[i] and extending the trace with ${\tt items[i(}1{\tt)]}=x$ and a completed dequeue that in this case returns $x$, leads to the incorrect linearization: $inv(enq,y,2)$, $ret(enq,2)$, $inv(enq,x,1)$, $ret(enq,1)$, $inv(deq,3)$, $ret(deq,x,3)$.

The dequeue method has a fixed linearization point which corresponds to an execution of swap returning a non-null value. This action alone contributes to the effect of that value being removed from the queue. Every concurrent history can be linearized to a sequential history where dequeues occur in the order of their linearization points in the concurrent history. This claim is formally proved in Section 4.3.

Since the linearization points of the enqueues are not fixed, there exists no forward simulation from $\mathit{HWQ}$ to $AbsQ_{0}$. In the following, we describe the abstract implementation $AbsQ$ for which such a forward simulation does exist.

4.2 Abstract Queue Implementation

Informally, $AbsQ$ records the happens-before order between enqueue operations for which the added value has not been removed by a dequeue operation. The linearization point of a dequeue operation with return value $d\neq{\tt EMPTY}$ is enabled only if the happens-before stored in the current state contains a minimal enqueue that adds the value $d$. The effect of the linearization point is that the minimal enqueue is removed from the current state and the return value is recorded in the library state. When the return value is EMPTY, the linearization point of a dequeue is enabled only if the current state stores only pending enqueues (the dequeue overlaps with all the enqueue operations stored in the current state and it can be linearized before all of them). The return of a dequeue is enabled only if the returned value matches the one fixed at the linearization point.

Figure 2 pictures two executions of $AbsQ$ for two extended histories (that include dequeue linearization points). The state of $AbsQ$ after each action is pictured as a graph below the action. The nodes of this graph represent enqueue operations and the edges happens-before constraints. Each node is labeled by a value (the input of the enqueue) and a flag PEND or COMP showing whether the operation is pending or completed. For instance, in the case of the first history, the dequeue linearization point $lin(deq,y,3)$ is enabled because the current happens-before contains a minimal enqueue operation with input $y$. Note that a linearization point $lin(deq,x,3)$ is also enabled at this state.

Formally, the states of $AbsQ$ are tuples $\langle{O,<,\ell,rv,cp}\rangle$ where $O\subseteq\<Ops>$ is a set of operation identifiers, $<\subseteq O\times O$ is a strict partial order, $\ell:O->\<Vals>\times\{\tt{PEND,\tt{COMP}}\}$ labels every identifier with a value and a pending/completed flag (the flag is used to track the happens-before order), $rv:\<Ops>~{}>\<Vals>$ records the return value of a dequeue fixed at its linearization point ($~{}>$ denotes a partial function), and $cp:\<Ops>~{}>\{A_{1},A_{2},R_{1},R_{2},R_{3}\}$ records the control point of every enqueue ($A_{1},A_{2}$) or dequeue operation ($R_{1},R_{2},R_{3}$). All the components are $\emptyset$ in the initial state, and the transition relation $->$ is defined in Fig. 3. The alphabet of $AbsQ$ contains call/return actions and dequeue linearization points, denoted by $lin(deq,d,k)$. $Lin(deq)$ is the set of all actions $lin(deq,d,k)$.

Concerning enqueue operations, the rule call-enq orders the invoked operation after all the completed enqueues in the current state, and the rules ret-enq1/ret-enq2 flip the corresponding flag from PEND to COMP provided that the operation is still present in the current state. For dequeue operations, call-deq only increments the control point and ret-deq checks whether the return value is the same as the one fixed at the linearization point. The linearization point rule lin-deq1 corresponds to the case of a non-empty queue, showing that $lin(deq,d,k)$ is enabled only if $d$ has been added by an enqueue which is minimal in the current happens-before. When enabled, it removes the enqueue adding $d$ from the state. The linearization point rule lin-deq2 corresponds to the case of dequeue operations linearized with an EMPTY return value.

The following result states that the library $AbsQ$ has exactly the same set of histories as the standard abstract library $AbsQ_{0}$ (see Appendix 0.C for a proof).

Theorem 4.1

$AbsQ$* is a refinement of $AbsQ_{0}$ and vice-versa.*

A trace of a queue implementation is called $Lin(deq)$-complete when every completed dequeue has a linearization point, i.e., each return action $ret(deq,d,k)$ is preceded by an action $lin(deq,d,k)$. A queue implementation $L$ over alphabet $\Sigma$, such that $C\cup R\cup Lin(deq)\subseteq\Sigma$, is called with fixed dequeue linearization points when every trace $@t\in Tr(L)$ is $Lin(deq)$-complete.

The following result shows that $C\cup R\cup Lin(deq)$-forward simulations are a sound and complete proof method for showing the correctness of a queue implementation with fixed dequeue linearization points (up to the correctness of the linearization points). It is obtained from Theorem 4.1 and Theorem 3.1 using the fact that the alphabet of $AbsQ$ is exactly $C\cup R\cup Lin(deq)$ and $AbsQ$ is deterministic.

Corollary 1

A queue implementation $L$ with fixed dequeue linearization points is a $C\cup R\cup Lin(deq)$-refinement of $AbsQ_{0}$ iff there exists a $C\cup R\cup Lin(deq)$-forward simulation from $L$ to $AbsQ$.

4.3 A Correctness Proof For Herlihy&Wing Queue

We describe a forward simulation $\mathit{fs}_{1}$ from $\mathit{HWQ}$ to $AbsQ$. A $\mathit{HWQ}$ state is related by $\mathit{fs}_{1}$ to an $AbsQ$ state that consists of all the enqueue operations for which the input is still present in the array items and all the pending enqueue operations that have at most reserved an array position, ordered by a relation $<$ satisfying the following:

• (a)

pending enqueues are maximal, i.e., for every two enqueues $k$ and $k^{\prime}$ such that $k^{\prime}$ is pending, we have that $k^{\prime}\not<k$,

• (b)

$<$ is consistent with the order in which positions of items have been reserved, i.e., for every two enqueues $k$ and $k^{\prime}$ such that ${\tt i}(k)<{\tt i}(k^{\prime})$, we have that $k^{\prime}\not<k$,

• (c)

an enqueue which has reserved a position $i$ can’t be ordered before another enqueue that has reserved a position $j\geq i$ when the position $i$ has been “observed” by a non-linearized dequeue that may “observe” $j$ in the current array traversal, i.e., for every two enqueues $k$ and $k^{\prime}$, and a dequeue $k_{d}$, such that

[TABLE]

we have that $k\not<k^{\prime}$. The predicate $k_{d}@{\tt if}\text{-}{\tt inc}$ holds when the dequeue $k_{d}$ is at a control point after a swap returning null and before the increment of i.

An enqueue is labeled by $(d,{\tt PEND})$ where $d$ is the input value if it’s pending and by $(d,{\tt COMP})$, otherwise. Also, for every dequeue operation $k$ such that ${\tt x}(k)=d\neq{\tt null}$, we have that $rv(k)=d$.

We show that $\mathit{fs}_{1}$ is indeed a $C\cup R\cup Lin(deq)$-forward simulation. Let $s$ and $t$ be states of $\mathit{HWQ}$ and $AbsQ$, respectively, such that $(s,t)\in\mathit{fs}_{1}$. We omit discussing the trivial case of transitions labeled by call and return actions which are simulated by similar transitions of $AbsQ$ (for the return a dequeue operation $k$, we use the equality between the local variable ${\tt x}(k)$ in $s$ and the component $rv(k)$ in $t$).

We show that each internal step of an enqueue or dequeue, except the execution of swap returning a non-null value in dequeue (which represents its linearization point), is simulated by an empty sequence of $AbsQ$ transitions, i.e., for every state $s^{\prime}$ obtained through one of these steps, if $(s,t)\in\mathit{fs}_{1}$, then $(s^{\prime},t)\in\mathit{fs}_{1}$ for each $AbsQ$ state $t$. Essentially, this consists in proving the following property, called monotonicity: the set of possible orders $<$ associated by $\mathit{fs}_{1}$ to $s^{\prime}$ doesn’t exclude any order $<$ associated to $s$.

Concerning enqueues, let $s^{\prime}$ be the state obtained from $s$ when a pending enqueue $k$ reserves an array position. This enqueue must be maximal in both $t$ and any state $t^{\prime}$ related to $s^{\prime}$ (since it’s pending). Moreover, there is no dequeue that can “observe” this position before restarting the array traversal. Therefore, item (c) in the definition of $<$ doesn’t constrain the order between $k$ and some other enqueue neither in $s$ nor in $s^{\prime}$. Since this transition doesn’t affect the constraints on the order between enqueues different from $k$ (their local variables remain unchanged), monotonicity holds. This property is trivially satisfied by the second step of enqueue which doesn’t affect i.

To prove monotonicity in the case of dequeue internal steps different from its linearization point, it is important to track the non-trivial instantiations of item (c) in the definition of $<$ over the two states $s$ and $s^{\prime}$, i.e., the triples $(k,k^{\prime},k_{d})$ for which (1) holds. Instantiations that are enabled only in $s^{\prime}$ may in principle lead to a violation of monotonicity (since they restrict the orders $<$ associated to $s^{\prime}$). For the two steps that begin an array traversal, i.e., reading the index of the last used position and setting i to [math], there exist no such new instantiations in $s^{\prime}$ because the value of i is either not set or [math]. The same is true for the increment of i in a dequeue $k_{d}$ since the predicate $k_{d}@{\tt if}\text{-}{\tt inc}$ holds in state $s$. The execution of swap returning null in a dequeue $k_{d}$ enables new instantiations $(k,k^{\prime},k_{d})$ in $s^{\prime}$, thus adding potentially new constraints $k\not<k^{\prime}$. We show that these instantiations are however vacuous because $k$ must be pending in $s$ and thus maximal in every order $<$ associated by $\mathit{fs}_{1}$ to $s$. Let $k$ and $k^{\prime}$ be two enqueues such that together with the dequeue $k_{d}$ they satisfy the property (1) in $s^{\prime}$ but not in $s$. We write ${\tt i}_{s}(k)$ for the value of the variable i of operation $k$ in state $s$. We have that ${\tt i}_{s^{\prime}}(k)={\tt i}_{s^{\prime}}(k_{d})\leq{\tt i}_{s^{\prime}}(k^{\prime})$ and ${\tt items}[{\tt i}_{s^{\prime}}(k_{d})]={\tt null}$. The latter implies that the enqueue $k$ didn’t executed the second statement (since the position it reserved is still null) and it is pending in $s$. The step that checks that the value returned by swap is null doesn’t modify the variables in property (1) and also, it doesn’t change the valuation of the predicate $@{\tt if}\text{-}{\tt inc}$.

Finally, we show that the linearization point of a dequeue $k$ of $\mathit{HWQ}$, i.e., an execution of swap returning a non-null value $d$, from state $s$ and leading to a state $s^{\prime}$ is simulated by a transition labeled by $lin(deq,d,k)$ of $AbsQ$ from state $t$. By the definition of $\mathit{HWQ}$, there is a unique enqueue $k_{e}$ which filled the position updated by $k$, i.e., ${\tt i}_{s}(k_{e})=i_{s}(k)$ and ${\tt x}_{s^{\prime}}(k)={\tt x}_{s}(k_{e})$. We show that $k_{e}$ is minimal in the order $<$ of $t$ which implies that $lin(deq,d,k)$ is enabled in $t$. Thus, instantiating item (c) in the definition of $<$ with $k^{\prime}=k_{e}$ and $k_{d}=k$ we get that every enqueue that reserved a position smaller than the one of $k_{e}$ can’t be ordered before $k_{e}$ in the order $<$. Also, applying item (b) with $k=k_{e}$ we get the same for every enqueue that reserved a bigger position. An enqueue that didn’t reserved a position is by definition maximal in $<$ and therefore, not a predecessor of $k_{e}$. Then, the state $t^{\prime}$ obtained from $t$ through a $lin(deq,d,k)$ transition is related to $s^{\prime}$ because (1) the value added by $k_{e}$ is not anymore present in items which implies that $k_{e}$ doesn’t occur in any $AbsQ$ state related to $s^{\prime}$, and (2) the value of ${\tt x}(k)$ is set to $d\neq{\tt null}$ which implies that $rv(k)$ is set to $d$ in every $AbsQ$ state related to $s^{\prime}$.

5 Stacks With Fixed Pop Commit Points

While the abstract queue in Section 4 can be adapted to stacks (the linearization point $lin(pop,d,k)$ with $d\neq{\tt EMPTY}$ is enabled when $k$ is added by a push which is maximal in the happens-before order stored in the state), it can’t simulate (through forward simulations) existing stack implementations like the Time-Stamped Stack [9] ($\mathit{TSS}$, for short) where the linearization points of the pop operations are not fixed. Exploiting particular properties of the stack semantics, we refine the ideas used in $AbsQ$ and define a new abstract implementation for stacks, denoted as $AbsQ$, which is able to simulate such implementations. Forward simulations to $AbsS$ are complete for proving the correctness of stack implementations provided that the point in time where the return value of a pop operation is determined, called commit point, corresponds to a fixed action.

5.1 Pop Methods With Fixed Commit Points

We explain the meaning of the commit points on a simplified version of the Time-Stamped Stack [9] ($\mathit{TSS}$, for short) given in Figure 4. This implementation maintains an array of singly-linked lists, one for each thread, where list nodes contain a data value (field data), a timestamp (field ts), the next pointer (field next), and a boolean flag indicating whether the node represents a value removed from the stack (field taken). Initially, each list contains a sentinel dummy node pointing to itself with timestamp $-1$ and the flag taken set to false.

Pushing a value to the stack proceeds in several steps: adding a node with maximal timestamp in the list associated to the thread executing the push (given by the special variable myTID), asking for a new timestamp (given by the shared variable TS), and updating the timestamp of the added node. Popping a value from the stack consists in traversing all the lists, finding the first element which doesn’t represent a removed value (i.e., taken is false) in each list, and selecting the element with the maximal timestamp. A compare-and-swap (CAS) is used to set the taken flag of this element to true. The procedure restarts if the CAS fails.

The push operations don’t have a fixed linearization point because adding a node to a list and updating its timestamp are not executed in a single atomic step. The nodes can be added in an order which is not consistent with the order between the timestamps assigned later in the execution. Also, the value added by a push that just added an element to a list can be popped before the value added by a completed push (since it has a maximal timestamp). The same holds for pop operations: The only reasonable choice for a linearization point is a successful CAS (that results in updating the field taken). Fig. 5 pictures an execution showing that this action doesn’t correspond to a linearization point, i.e., an execution for which the pop operations in every correct linearization are not ordered according to the order between successful CASs. In every correct linearization of that execution, the pop operation removing $x$ is ordered before the one removing $z$ although they perform a successful CAS in the opposite order.

An interesting property of the successful CASs in pop operations is that they fix the return value, i.e., the return value is youngest->data where youngest is the node updated by the CAS. We call such actions commit points. More generally, commit points are actions that access shared variables, from which every control-flow path leads to the return control point and contains no more accesses to the shared memory (i.e., after a commit point, the return value is computed using only local variables).

When the commit points of pop operations are fixed to particular implementation actions (e.g., a successful CAS) we assume that the library is an LTS over an alphabet that contains actions $com(pop,d,k)$ with $d\in\<Vals>$ and $k\in\<Ops>$ (denoting the commit point of the pop with identifier $k$ and returning $d$). Let $Com(pop)$ be the set of such actions.

5.2 Abstract stack implementation

We define an abstract stack $AbsS$ over alphabet $C\cup R\cup Com(pop)$ that essentially, similarly to $AbsQ$, maintains the happens-before order of the pushes whose value has not been yet removed. Pops are treated differently since the commit points are not necessarily linearization points, intuitively, a pop can be linearized before its commit. Each pop operation starts by taking a snapshot of the greatest completed push operations in the happens-before order, and continuously tracks the push operations which are overlapping with it. The commit point $com(pop,d,k)$ with $d\neq{\tt EMPTY}$ is enabled only if $d$ was added by one of the push operations in the initial snapshot, or by a push happening earlier when all the values from the initial snapshot have been removed, or by one of the push operations that overlaps with pop $k$. The commit point $com(pop,{\tt EMPTY},k)$ is enabled only if all the values added by push operations ending before $k$ started have been removed. The effect of the commit points is explained below through examples.

Figure 6 pictures two executions of $AbsS$ for two extended histories (that include pop commit points). For readability, we give the state of $AbsS$ only after several execution prefixes delimited at the right by a dotted line. We focus on pop operations – the effect of push calls and returns is similar to enqueue calls and returns in $AbsQ$. Let us first consider the history on the top part. The first state we give is reached after the call of pop with identifier $3$. This shows the effect of a pop invocation: the greatest completed pushes according to the current happens-before (here, the push with identifier $1$) are marked as $be(3)$ (from “before” operation 3), and the pending pushes are marked as $ov(3)$ (from “overlapping” with operation 3). As a side remark, any other push operation that starts after pop $3$ would be also marked as $ov(3)$. The commit point $com(pop,x,3)$ (pictured with a red circle) is enabled because $x$ was added by a push marked as $be(3)$. The effect of the commit point is that push $1$ is removed from the state (the execution on the bottom shows a more complicated case). For the second pop, the commit point $com(pop,y,4)$ is enabled because $y$ was added by a push marked as $ov(4)$. The execution on the bottom shows an example where the marking $be(k)$ for some pop $k$ is updated at commit points. The pushes $3$ and $4$ are marked as $be(5)$ and $be(6)$ when the pops $5$ and $6$ start. Then, $com(pop,t,5)$ is enabled since $t$ was added by $push(t,4)$ which is marked as $be(5)$. Besides removing $push(t,4)$, the commit point produces a state where a pop committing later, e.g., pop $6$, can remove $y$ which was added by a predecessor of $push(t,4)$ in the happens-before ($y$ could become the top of the stack when $t$ is removed). This history is valid because $push(y,2)$ can be linearized after $push(x,1)$ and $push(z,3)$. Thus, push 2, a predecessor of the push which is removed, is marked as $be(6)$. Push $1$ which is also a predecessor of the removed push is not marked as $be(6)$ because it happens before another push, i.e., push 3, which is already marked as $be(6)$ (the value added by push 3 should be removed before the value added by push 1 could become the top of the stack).

Formally, the states of $AbsS$ are tuples $\langle{O,<,\ell,rv,cp,be,ov}\rangle$ where $<$ is a strict partial order over the set $O$ of operation identifiers, $\ell:O->\<Vals>\times\{\tt{PEND,\tt{COMP}}\}$ labels every identifier in $O$ with a value and a pending/completed flag, $rv:\<Ops>~{}>\<Vals>$ records the return value of a pending pop fixed at its commit point, $cp:\<Ops>~{}>\{A_{1},A_{2},R_{1},R_{2},R_{3}\}$ records the control point of every push ($A_{1},A_{2}$) or pop operation ($R_{1},R_{2},R_{3}$), $be:\<Ops>~{}>2^{O}$ records the greatest completed push operations before a pop started or happening earlier provided that the values of all the push happening later have been removed, and $ov:\<Ops>~{}>2^{O}$ records push operations overlapping with a pop. All the components are $\emptyset$ in the initial state, and the transition relation $->$ is defined in Fig. 7.

The transition rules which don’t correspond to commit point actions are similar to those for $AbsQ$. The rule com-pop1 for $com(pop,d,k)$ is enabled only if there exists a push $k^{\prime}$ which added value $d$ and which belongs to $be(k)$ or $ov(k)$. When enabled, the push $k^{\prime}$ is removed from the set $O$ (and the order $<$) and for every other pop $k_{1}$ such that $k^{\prime}$ belongs to $be(k_{1})$, $k^{\prime}$ is replaced in $be(k_{1})$ by its predecessors which are followed exclusively by pushes overlapping with $k_{1}$ (these predecessors become maximal closed pushes once $k^{\prime}$ is removed). Also, $rv(k)$ is set to $d$. The rule com-pop1 for $com(pop,{\tt EMPTY},k)$ is enabled only if $be(k)$ is empty (i.e., all the values added by pushes ending before $k$, if any, have been removed). Then, $rv(k)$ is set to ${\tt EMPTY}$.

Let $AbsS_{0}$ be the standard abstract implementation of a stack (where elements are stored in a sequence; push, resp., pop operations add, resp., remove, an element from the beginning of the sequence in one atomic step). For $\<Methods>=\{push,pop\}$, the alphabet of $AbsS_{0}$ is $C\cup R\cup Lin$. The following result states that the library $AbsS$ has exactly the same set of histories as $AbsS_{0}$ (see Appendix 0.D for a proof).

Theorem 5.1

$AbsS$* is a refinement of $AbsS_{0}$ and vice-versa.*

A trace of a stack implementation is called $Com(pop)$-complete when every completed pop has a commit point, i.e., each return $ret(pop,d,k)$ is preceded by an action $com(pop,d,k)$. A stack implementation $L$ over $\Sigma$, such that $C\cup R\cup Com(pop)\subseteq\Sigma$, is called with fixed pop commit points when every trace $@t\in Tr(L)$ is $Com(pop)$-complete.

As a consequence of Theorem 3.1, $C\cup R\cup Com(pop)$-forward simulations are a sound and complete proof method for showing the correctness of a stack implementation with fixed pop commit points (up to the correctness of the commit points).

Corollary 2

A stack $L$ with fixed pop commit points is a $C\cup R\cup Com(pop)$-refinement of $AbsS$ iff there is a $C\cup R\cup Com(pop)$-forward simulation from $L$ to $AbsS$.

Linearization points can also be seen as commit points and thus the following holds.

Corollary 3

A stack implementation $L$ with fixed pop linearization points where transition labels $lin(pop,d,k)$ are substituted with $com(pop,d,k)$ is a $C\cup R\cup Com(pop)$-refinement of $AbsS_{0}$ iff there is a $C\cup R\cup Com(pop)$-forward simulation from $L$ to $AbsS$.

5.3 A Correctness Proof For Time-Stamped Stack

We describe a forward simulation $\mathit{fs}_{2}$ from $\mathit{TSS}$ to $AbsS$. Except for the constraints on the components $be$ and $ov$ of a $AbsS$ state, it is similar to the simulation $\mathit{fs}_{1}$ from $\mathit{HWQ}$ to $AbsQ$. Thus, the $AbsS$ states $t=\langle{O,<,\ell,rv,cp,be,ov}\rangle$ associated by $\mathit{fs}_{2}$ to a $\mathit{TSS}$ state $s$ satisfy the following. The set $O$ consists of all the identifiers of pushes in $s$ which didn’t added yet a node to pools or for which the input is still present in pools (i.e., the node created by the push has taken set to false). A push $k$ is labeled by $(d,{\tt PEND})$ where $d$ is the input value if it’s pending and by $(d,{\tt COMP})$, otherwise.

To describe the order relation $<$ we consider the following notations: ${\tt ts}_{s}(k)$, resp., ${\tt TID}_{s}(k)$, denotes the timestamp of the node created by the push $k$ in state $s$ (the ts field of this node), resp., the id of the thread executing $k$. By an abuse of terminology, we call ${\tt ts}_{s}(k)$ the timestamp of $k$ in state $s$. Also, $k\leadsto_{s}k^{\prime}$ when intuitively, a traversal of pools would encounter the node created by $k$ before the one created by $k^{\prime}$. More precisely, $k\leadsto_{s}k^{\prime}$ when ${\tt TID}_{s}(k)<{\tt TID}_{s}(k^{\prime})$, or ${\tt TID}_{s}(k)={\tt TID}_{s}(k^{\prime})$ and the node created by $k^{\prime}$ is reachable from the one created by $k$ in the list pointed to by ${\tt pools}[{\tt TID}_{s}(k)]$. The order relation $<$ satisfies the following: (1) pending pushes are maximal, (2) $<$ is consistent with the order between node timestamps, i.e., ${\tt ts}_{s}(k)\leq{\tt ts}_{s}(k^{\prime})$ implies $k^{\prime}\not<k$, and (3) $<$ includes the order between pushes executed in the same thread, i.e., ${\tt TID}_{s}(k)={\tt TID}_{s}(k^{\prime})$ and ${\tt ts}_{s}(k)<{\tt ts}_{s}(k^{\prime})$ implies $k<k^{\prime}$.

The components $be$ and $ov$ satisfy the following constraints (their domain is the set of identifiers of pending pops):

• •

a pop $k$ with ${\tt youngest}\neq{\tt null}$ that reached a node with timestamp $\tau$ (its variable n points to this node) overlaps with every push that created a node with a timestamp bigger than $\tau$ and which occurs in pools before the node reached by $k$, i.e., ${\tt youngest}_{s}(k)\neq{\tt null}$, ${\tt n}_{s}(k)={\tt n}_{s}(k_{1})$, $k_{2}\leadsto_{s}k_{1}$, ${\tt n}_{s}(k_{2})\text{\tt->taken}={\tt false}$, and ${\tt ts}_{s}(k_{2})\geq{\tt ts}_{s}(k_{1})$ implies $k_{2}\in ov(k)$, for each $k,k_{1},k_{2}$

• •

a pop $k$ with ${\tt youngest}={\tt null}$ overlaps with every push that created a node which occurs in pools before the node reached by $k$, i.e., ${\tt youngest}_{s}(k)={\tt null}$, ${\tt n}_{s}(k)={\tt n}_{s}(k_{1})$, $k_{2}\leadsto_{s}k_{1}$, and ${\tt n}_{s}(k_{2})\text{\tt->taken}={\tt false}$ implies $k_{2}\in ov(k)$, for each $k,k_{1},k_{2}$

• •

if the variable youngest of a pop $k$ points to a node which is not taken, then this node was created by a push in $be(k)\cup ov(k)$ or the node currently reached by $k$ is followed in pools by another node which was created by a push in $be(k)\cup ov(k)$, i.e., ${\tt youngest}_{s}(k)={\tt n}_{s}(k_{1})$, ${\tt n}_{s}(k_{1})\text{{\tt->taken}}={\tt false}$, and ${\tt n}_{s}(k)={\tt n}_{s}(k_{2})$ implies $k_{1}\in be(k)\cup ov(k)$ or that there exists $k_{3}\in O$ such that ${\tt ts}_{s}(k_{3})>{\tt ts}_{s}(k_{1})$, $k_{3}\in be(k)\cup ov(k)$, and either $k_{2}\leadsto_{s}k_{3}$ or ${\tt n}_{s}(k_{2})={\tt n}_{s}(k_{3})$ and TODO $k$ is traversing the last list in the array pools, for each $k,k_{1},k_{2}$

There are some more constraints on $be$ and $ov$ that can be seen as invariants of $AbsS$, i.e., $be(k)$ and $ov(k)$ don’t contain predecessors of pushes from $be(k)$ (for each $k,k_{1},k_{2}$, $k_{1}<k_{2}$ and $k_{2}\in be(k)$ implies $k_{1}\not\in be(k)\cup ov(k)$). They can be found in Appendix 0.E.

Finally, for every pop operation $k$ such that ${\tt success}(k)={\tt true}$, we have that $rv(k)={\tt youngest}(k)\text{\tt->data}$.

The proof that $\mathit{fs}_{2}$ is indeed a forward simulation from $\mathit{TSS}$ to $AbsS$ follows the same lines as the one given for the Herlihy&Wing Queue. It can be found in Appendix 0.E.

6 Related Work

Many techniques for linearizability verification, e.g., [28, 4, 27, 2], are based on forward simulation arguments, and typically only work for libraries where the linearization point of every invocation of a method $m$ is fixed to a particular statement in the code of $m$. The works in [25, 8, 10, 29] deal with external linearization points where the action of an operation $k$ can be the linearization point of a concurrently executing operation $k^{\prime}$. We say that the linearization point of $k^{\prime}$ is external. This situation arises in read-only methods like the contains method of an optimistic set [22], libraries based on the elimination back-off scheme, e.g., [14], or flat combining [15, 12]. In these implementations, an operation can do an update on the shared state that becomes the linearization point of a concurrent read-only method (e.g., a contains returning true may be linearized when an add method adds a new value to the shared state) or an operation may update the data structure on behalf of other concurrently executing operations (whose updates are published in the shared state). In all these cases, every linearization point can still be associated syntactically to a statement in the code of a method and doesn’t depend on operations executed in the future (unlike $\mathit{HWQ}$ and $\mathit{TSS}$). However, identifying the set of operations for which such a statement is a linearization point can only be done by looking at the whole program state (the local states of all the active operations). This poses a problem in the context of compositional reasoning (where auxiliary variables are required), but still admits a forward simulation argument. For manual proofs, such implementations with external linearization points can still be defined as LTSs that produce $Lin$-complete traces and thus still fall in the class of implementations for which forward simulations are enough for proving refinement. These proof methods are not complete and they are not able to deal with implementations like $\mathit{HWQ}$ or $\mathit{TSS}$.

There also exist linearizability proof techniques based on backward simulations or alternatively, prophecy variables, e.g., [26, 24, 19]. These works can deal with implementations where the linearization points are not fixed, but the proofs are conceptually more complex and less amenable to automation.

The works in [16, 6] propose reductions of linearizability to assertion checking where the idea is to define finite-state automata that recognize violations of concurrent queues and stacks. These automata are simple enough in the case of queues and there is a proof of $\mathit{HWQ}$ based on this reduction [16]. However, in the case of stacks, the automata become much more complicated and we are not aware of a proof for an implementation such as $\mathit{TSS}$ which is based on this reduction.

Appendix 0.A Libraries

Programs interact with libraries by calling named library methods, which receive parameter values and yield return values upon completion. We fix arbitrary sets $\<Methods>$ and $\<Vals>$ of method names and parameter/return values.

We fix an arbitrary set $\<Ops>$ of operation identifiers, and for given sets $\<Methods>$ and $\<Vals>$ of methods and values, we fix the sets

[TABLE]

of call actions and return actions; each call action $inv(m,d,k)$ combines a method $m\in\<Methods>$ and value $d\in\<Vals>$ with an operation identifier $k\in\<Ops>$. Operation identifiers are used to pair call and return actions. We assume every set of words is closed under isomorphic renaming of operation identifiers. We denote the operation identifier of a call/return action $a$ by $\<op>(a)$. Call and return actions $c\in C$ and $r\in R$ are matching, written $c\mathbin{\mapstochar\relbar\mapsfromchar}r$, when $\<op>(c)=\<op>(r)$. We may omit the second field from a call/return action $a$ for methods that have no inputs (e.g., the pop method of a stack) or return values (e.g., the push method of a stack). A word $\tau\in@S^{*}$ over alphabet $@S$, such that $(C\cup R)\subseteq@S$, is well formed when:

• •

Each return is preceded by a matching call:

$\tau_{j}\in R$ implies $\tau_{i}\mathbin{\mapstochar\relbar\mapsfromchar}\tau_{j}$ for some $i<j$.

• •

Each operation identifier is used in at most one call/return:

$\<op>(\tau_{i})=\<op>(\tau_{j})$ and $i<j$ implies $\tau_{i}\mathbin{\mapstochar\relbar\mapsfromchar}\tau_{j}$.

We say that the well-formed word $\tau\in@S^{*}$ is sequential when

• •

Operations do not overlap:

$\tau_{i},\tau_{k}\in C$ and $i<k$ implies $\tau_{i}\mathbin{\mapstochar\relbar\mapsfromchar}\tau_{j}$ for some $i<j<k$.

Well-formed words represent traces of a library. We assume every set of well-formed words is closed under isomorphic renaming of operation identifiers. For notational convenience, we take $\<Ops>=\<Nats>$ for the rest of the paper. When the value of a certain field in a call/return action is not important we use the placeholder $\_$, e.g., $inv(m,\_,k)$ instead of $inv(m,d,k)$ when the input $d$ can take any value.

An operation $k$ is called completed in a well-formed trace $\tau$ when $ret(m,d,k)$ occurs in $\tau$, for some $m$ and $d$. Otherwise, it is called pending.

Libraries dictate the execution of methods between their call and return points. Accordingly, a library cannot prevent a method from being called, though it can decide not to return. Furthermore, any library action performed in the interval between call and return points can also be performed should the call have been made earlier, and/or the return made later. A library thus allows any sequence of invocations to its methods made by some program.

Definition 4

A library $L$ is an LTS over alphabet $\Sigma$ such that $C\cup R\subseteq\Sigma$ and each trace $\tau\in Tr(L)$ is well formed, and

• •

Call actions $c\in C$ cannot be disabled:

$\tau\cdot\tau^{\prime}\in Tr(L)$ implies $\tau\cdot c\cdot\tau^{\prime}\in Tr(L)$ if $\tau\cdot c\cdot\tau^{\prime}$ is well formed.

• •

Call actions $c\in C$ cannot disable other actions:

$\tau\cdot a\cdot c\cdot\tau^{\prime}\in Tr(L)$ implies $\tau\cdot c\cdot a\cdot\tau^{\prime}\in Tr(L)$.

• •

Return actions $r\in R$ cannot enable other actions:

$\tau\cdot r\cdot a\cdot\tau^{\prime}\in Tr(L)$ implies $\tau\cdot a\cdot r\cdot\tau^{\prime}\in Tr(L)$.

Note that even a library that implements atomic methods, e.g., by guarding method bodies with a global-lock acquisition, admits executions in which method calls and returns overlap. For simplicity, Definition 4 assumes that every thread performs a single operation. The extension to multiple operations per thread is straightforward, e.g. the closure rules must assume that the actions $a$ and $c$ belong to different threads

Appendix 0.B Normal Forward/Backward Simulations

We define a class of forward/backward simulations, called normal simulations, that are used in the proofs in Appendix 0.C and Appendix 0.D.

Definition 5

Let $L_{1}=(Q_{1},\Sigma,s_{0}^{1},\delta_{1})$ and $L_{2}=(Q_{2},\Sigma,s_{0}^{2},\delta_{2})$ be two libraries over alphabets $\Sigma_{1}$ and $\Sigma_{2}$, respectively, such that $C\cup R\subseteq\Sigma_{1}\cap\Sigma_{2}$, and $\Gamma$ a set of actions such that $C\cup R\subseteq\Gamma\subseteq\Sigma_{1}\cap\Sigma_{2}$. A relation $\mathit{fs}\subseteq Q_{1}\times Q_{2}$ is called a normal $\Gamma$-forward simulation from $L_{1}$ to $L_{2}$ iff the following holds:

• (i)

$\mathit{fs}[s_{0}^{1}]=\{s_{0}^{2}\}$

• (ii-a)

If $(s,c,s^{\prime})\in\delta_{1}$, for some $c\in C$, and $u\in\mathit{fs}[s]$, then there exists $u^{\prime}\in\mathit{fs}[s^{\prime}]$ such that $u\xrightarrow{@s}u^{\prime}$, $@s_{0}=c$, and $@s_{i}\in\Sigma_{2}\setminus\Gamma$, for each $0<i<|@s|$.

• (ii-b)

If $(s,r,s^{\prime})\in\delta_{1}$, for some $r\in R$, and $u\in\mathit{fs}[s]$, then there exists $u^{\prime}\in\mathit{fs}[s^{\prime}]$ such that $u\xrightarrow{@s}u^{\prime}$, $@s_{|@s|-1}=r$, and $@s_{i}\in\Sigma_{2}\setminus\Gamma$, for each $0\leq i<|@s|-1$.

• (ii-c)

If $(s,\gamma,s^{\prime})\in\delta_{1}$, for some $\gamma\in\Gamma\setminus(C\cup R)$, and $u\in fs[s]$, then there exists $u^{\prime}\in fs[s^{\prime}]$ such that $\delta_{2}(u,\gamma,u^{\prime})$.

• (ii-d)

If $(s,e,s^{\prime})\in\delta_{1}$, for some $e\in\Sigma_{1}\setminus\Gamma$ and $u\in\mathit{fs}[s]$, then there exists $u^{\prime}\in\mathit{fs}[s^{\prime}]$ such that $u\xrightarrow{\sigma}u^{\prime}$ and $\sigma\in(\Sigma_{2}\setminus\Gamma)^{*}$.

With normal $\Gamma$-forward simulations, a step of $L_{1}$ labeled by a call, resp., return, action is simulated by a sequence of steps of $L_{2}$ that start, resp., end, with the same action, and a step of $L_{1}$ labeled by another observable action should be matched by a step of $L_{2}$ labeled by the same action. The rest of the transitions in $L_{1}$ are matched to a possibly empty sequence of transitions of $L_{2}$ with arbitrary labels.

A dual notion of forward simulation is the backward simulation:

Definition 6

Let $L_{1}=(Q_{1},\Sigma,s_{0}^{1},\delta_{1})$ and $L_{2}=(Q_{2},\Sigma,s_{0}^{2},\delta_{2})$ be two libraries over a common alphabet $\Sigma$, and $\Gamma\subseteq\Sigma$ a set of actions such that $(C\cup R)\subseteq\Gamma$. A relation $bs\subseteq Q_{1}\times Q_{2}$ is called a normal $\Gamma$-backward simulation from $L_{1}$ to $L_{2}$ iff the following holds:

• (i)

$bs[s_{0}^{1}]=\{s_{0}^{2}\}$

• (ii-a)

If $(s,c,s^{\prime})\in\delta_{1}$, for some $c\in C$, and $u^{\prime}\in bs[s^{\prime}]$, then there exists $u\in bs[s]$ such that $u\xrightarrow{@s}u^{\prime}$, $@s_{0}=c$, and $@s_{i}\in\Sigma\setminus\Gamma$, for each $0<i<|@s|$.

• (ii-b)

If $(s,r,s^{\prime})\in\delta_{1}$, for some $r\in R$, and $u^{\prime}\in bs[s^{\prime}]$, then there exists $u\in bs[s]$ such that $u\xrightarrow{@s}u^{\prime}$, $@s_{|@s|-1}=r$, and $@s_{i}\in\Sigma\setminus\Gamma$, for each $0\leq i<|@s|-1$.

• (ii-c)

If $(s,\gamma,s^{\prime})\in\delta_{1}$, for some $\gamma\in\Gamma\setminus(C\cup R)$, and $u^{\prime}\in bs[s^{\prime}]$, then there exists $u\in bs[s]$ such that $\delta_{2}(u,\gamma,u^{\prime})$

• (ii-d)

If $(s,e,s^{\prime})\in\delta_{1}$ for some $e\in\Sigma\setminus\Gamma$ and $u^{\prime}\in bs[s^{\prime}]$, then there exists $u\in bs[s]$ such that $u\xrightarrow{@s}u^{\prime}$ and $\sigma\in(\Sigma_{2}\setminus\Gamma)^{*}$.

Appendix 0.C Proof of Theorem 4.1

We show that $AbsQ$ and $AbsQ_{0}$ refine each other. We start by giving a formal definition of the standard reference implementation $AbsQ_{0}$. Thus, the states of $AbsQ_{0}$ are tuples $\langle{\sigma,in^{0},rv^{0},cp^{0}}\rangle$ where $\sigma\in\<Vals>^{*}$ is a sequence of values, $in^{0}:\<Ops>~{}>\<Vals>$ records the input value of an enqueue, $rv^{0}:\<Ops>~{}>\<Vals>$ records the return value of a dequeue fixed at its linearization point ($~{}>$ denotes a partial function), and $cp^{0}:\<Ops>~{}>\{A_{1},A,A_{2},R_{1},R_{2},R_{3}\}$ records the control point of every enqueue ($A_{1},A,A_{2}$) or dequeue operation ($R_{1},R_{2},R_{3}$). All the components are $\emptyset$ in the initial state, and the transition relation $->$ is defined in Fig. 8. The alphabet of $AbsQ$ contains call/return actions and enqueue/dequeue linearization points.

To prove that $AbsQ$ is a refinement of $AbsQ_{0}$ we define a normal $C\cup R\cup Lin(deq)$-backward simulation (i.e, a backward simulation as in Definition 6) from $AbsQ$ to $AbsQ_{0}$. The reverse is shown using a normal $C\cup R\cup Lin(deq)$-forward simulation (i.e, a forward simulation as in Definition 5).

Lemma 1

$AbsQ$* is a refinement of $AbsQ_{0}$.*

Proof

We define a normal $C\cup R\cup Lin(deq)$-backward simulation $bs$ from $AbsQ$ to $AbsQ_{0}$ as follows. Given an $AbsQ$ state $s=\langle{O,<,\ell,rv,cp}\rangle$ and an $AbsQ_{0}$ state $t=\langle{\sigma,in^{0},rv^{0},cp^{0}}\rangle$ we have that $(s,t)\in bs$ iff the following hold:

• •

the sequence $\sigma$ is a linearization of a partial order $(D,\prec)$ where $D$ contains values labeling elements of $O$ and all the values corresponding to completed enqueues, i.e., $\ell_{1}({\tt COMP}(O))\subseteq D\subseteq\ell_{1}(O)$ ordered according to the happens-before order between the enqueues that added them, i.e., $d_{1}\prec d_{2}$ iff there exists $k_{1},k_{2}$ such that $\ell_{1}(k_{1})=d_{1}$, $\ell_{1}(k_{2})=d_{2}$, and $k_{1}<k_{2}$.

• •

the return values fixed at dequeue linearization points are the same, i.e., for every $k$, $rv(k)=rv^{0}(k)$,

• •

every dequeue is at the same control point in both $s$ and $t$, i.e., for every $k$ and $i\in\{1,2,3\}$, $cp(k)=R_{i}$ iff $cp^{0}(k)=R_{i}$,

• •

every pending enqueue has the same input value in both $s$ and $t$, i.e., for every $k$, $\ell_{1}(k)=in^{0}(k)$,

• •

a pending enqueue from $O$ has been linearized whenever its value is contained in $\sigma$, i.e., for every $k$, $cp^{0}(k)=A$ if $\ell_{1}(k)\in D$ and $\ell_{2}(k)={\tt PEND}$,

• •

a pending enqueue from $O$ hasn’t been linearized whenever its value is not in $\sigma$, i.e., for every $k$, $cp^{0}(k)=A_{1}$ iff $\ell_{1}(k)\not\in D$ and $\ell_{2}(k)={\tt PEND}$,

• •

a pending enqueue which is not in $O$ has been linearized, i.e., for every $k$, $cp^{0}(k)=A$ if $k\not\in O$ and $cp(k)=A_{1}$,

• •

an enqueue is completed in $s$ whenever it is completed in $t$, i.e., for every $k$, $cp(k)=A_{2}$ iff $cp^{0}(k)=A_{2}$,

For the conditions described above, if we fix the set $D$ and $\sigma_{t}$, then the state $t$ related to $s$ becomes unique. We use this fact in the proof. In some places, we only give $D$, $\sigma_{t}$ and $s$ without explicitly defining $t$ or show that there exists $t$ with the given $\sigma_{t}$ that is related to $s$ by just finding a $D$ such that $\sigma_{t}$ is a linearization of $(D,\prec)$ where $\prec$ is induced from $<_{s}$.

or $\sigma_{t}$ and not describing $t$ explicitly.

In the following, we show that indeed $bs$ is a normal $C\cup R\cup Lin(deq)$-backward simulation from $AbsQ$ to $AbsQ_{0}$.

• $\langle i\rangle$

$bs[s^{AbsQ}_{0}]=\{s^{AbsQ_{0}}_{0}\}$.

• call-enq

Let $s\xrightarrow{inv(enq,d,k)}_{AbsQ}s^{\prime}$ and $t^{\prime}\in bs[s^{\prime}]$. Either $k\in D_{t^{\prime}}$ or not.

First consider the former case. We know that $\ell_{s^{\prime}}(k)=(d,\texttt{PEND})$ and $k$ is maximal in $s^{\prime}$. Hence $\sigma_{t^{\prime}}=\rho\circ\langle d\rangle\circ\pi$ where $\pi$ contains linearization of pending elements in $O_{s^{\prime}}$. Then, pick $\sigma_{t}=\rho$. We can find such a $t\in bs[s]$ with $\sigma_{t}$. Let $(D,\prec)$ be the partial order that is used while constructing $\sigma_{t^{\prime}}$ from $O_{s}$ and $<_{s}$. We can find $(D^{\prime},\prec^{\prime})$ for relating $s$ to $t$ such that $D^{\prime}$ does not contain the values of pending elements that formed $\pi$ suffix of $s_{t^{\prime}}$ and $d$ coming from linearization of $k\in O_{s^{\prime}}$.

One can also see that $t\xrightarrow{\alpha}_{AbsQ_{0}}t^{\prime}$ where $\alpha=inv(enq,d,k),lin(enq,d,k),\\ lin(enq,d_{1},k_{1}),...,lin(enq,d_{j},k_{j})$ such that $\pi=d_{1},...,d_{j}$ and $k_{1},...,k_{j}\in O_{s^{\prime}}$ are the pending elements that are linearized to form $\pi$. Note that $\alpha$ obeys the definition of normal backward simulation definition.

For the second case, pick $t$ such that $\sigma_{t}=\sigma_{t^{\prime}}$. We can find a $t$ with $\sigma_{t}$ related to $s$ by $bs$ using the same $(D,\prec)$ partial order that is used while relating $s^{\prime}$ to $t^{\prime}$. $\ell_{1}(\texttt{COMP}(O_{s}))\subseteq D$ holds because $\texttt{COMP}(O_{s})=\texttt{COMP}(O_{s^{\prime}})$.

• call-deq

Let $s\xrightarrow{inv(deq,d,k)}_{AbsQ}s^{\prime}$ and $t^{\prime}\in bs[s^{\prime}]$. Pick $t$ such that it is equal to $t^{\prime}$ in every field except that $k\notin dom(cp^{0}_{t})$. Then, $t\in bs[s]$ and $t\xrightarrow{inv(deq,d,k)_{AbsQ_{0}}}t^{\prime}$.

• lin-deq1

Let $s\xrightarrow{lin(deq,d,k)}_{AbsQ}s^{\prime}$, $t^{\prime}\in bs[s^{\prime}]$ and $d\neq\texttt{EMPTY}$. We pick $t$ such that $\sigma_{t}=\langle d\rangle\circ\sigma_{t^{\prime}}$. We first show that $t\in bs[s]$. Let $(D,\prec)$ be the partial order that is linearized to obtain $\sigma_{t^{\prime}}$ and $k^{\prime}\in O_{s}$ be the element such that ${\ell_{s}}_{1}(k^{\prime})=d$. We know that $k^{\prime}$ is minimal in $<_{s}$ due to the premise of the rule lin-deq1. Hence, we can obtain $(D^{\prime},\prec^{\prime})$ such that $D^{\prime}=D\cup\{{\ell_{s}}_{1}(k^{\prime})\}$ and $\sigma_{t}$ is a linearization of it.

In addition, $t\xrightarrow{lin(deq,d,k)}_{AbsQ_{0}}t^{\prime}$. The action $lin(deq,d,k)$ is enabled in state $t$ since $d$ is the minimum element of $\sigma_{t}$. Note that the transition relating $t$ to $t^{\prime}$ obeys the definition of normal forward simulation.

• lin-deq2

Let $s\xrightarrow{lin(deq,\texttt{EMPTY},k)}_{AbsQ}s^{\prime}$ and $t^{\prime}\in bs[s^{\prime}]$. We pick $(D,\prec)$ for relating $s$ to $t$ such that $D=\emptyset$. Such a $D$ is a valid choice since all the elements $O_{s}$ are pending. Then, $\sigma_{t}=\langle\rangle$ is the only linearization of $(D,\prec)$. Hence, $lin(deq,\texttt{EMPTY},k)$ action is enabled in $AbsQ_{0}$ and $t\xrightarrow{lin(deq,\texttt{EMPTY},k)}_{AbsQ_{0}}t^{\prime}$ holds.

• ret-enq1

Let $s\xrightarrow{ret(enq,k)}_{AbsQ}s^{\prime}$, $\ell_{s}(k)=(d,\texttt{PEND})$ and $t^{\prime}\in bs[s^{\prime}]$. Assume $(D,\prec)$ be the partial order of which linearization is $\sigma_{t^{\prime}}$. Pick $D^{\prime}=D$. Then, $\ell_{1}(\texttt{COMP}(O_{s}))\subseteq D\subseteq\ell_{1}(O_{s})$ holds since $\texttt{COMP}(O_{s})=\texttt{COMP}(O_{s^{\prime}})\setminus\{k\}$ and $k\in\texttt{PEND}(O_{s})$. Construct $t\in bs[s]$ such that $\sigma_{t}=\sigma_{t^{\prime}}$ is obtained by linearizing the partial order $(D^{\prime},\prec^{\prime})$. Then, $t\xrightarrow{ret(enq,k)}_{AbsQ_{0}}t^{\prime}$ holds and it is a valid action with respect to normal backward-simulation relation definition.

• ret-enq2

Let $s\xrightarrow{ret(enq,k)}_{AbsQ}s^{\prime}$, $k\notin O_{s}$ and $t^{\prime}\in bs[s^{\prime}]$. Since $O_{s}=O_{s^{\prime}}$ and $\texttt{COMP}(O_{s})=\texttt{COMP}(O_{s^{\prime}})$, we can pick $D^{\prime}=D$ where $(D,\prec)$ is the strict partial order such that $\sigma_{t^{\prime}}$ is its linearization. Construct $t\in bs[s]$ such that $\sigma_{t}=\sigma_{t^{\prime}}$ is obtained by linearizing the partial order $(D^{\prime},\prec^{\prime})$. Then, $t\xrightarrow{ret(enq,k)}_{AbsQ_{0}}t^{\prime}$ holds and it is a valid action with respect to normal backward-simulation relation definition.

• ret-deq

Let $s\xrightarrow{ret(deq,d,k)}_{AbsQ}s^{\prime}$ and $t^{\prime}\in bs[s^{\prime}]$. Assume $(D,prec)$ is the partial order of which linearization is $\sigma_{t^{\prime}}$. Construct $t\in bs[s]$ such that $\sigma_{t}=\sigma_{t^{\prime}}$ and $(D,\prec)$ is the partial order $\sigma_{t}$ is obtained from. $\texttt{COMP}(O_{s})\subseteq D\subseteq O_{s}$ since $\texttt{COMP}(O_{s})=\texttt{COMP}(O_{s^{\prime}})$ and $O_{s}=O_{s^{\prime}}$. Then, $t\xrightarrow{ret(deq,d,k)}_{AbsQ_{0}}t^{\prime}$ holds. We have $rv_{s}(k)=rv^{0}_{t}(k)$ since $t\in bs[s]$. Hence the $ret(deq,d,k)$ is enabled in $t$. Moreover, $ret(deq,d,k)$ is a valid transition with respect to the normal backward simulation relation definition.

Lemma 2

$AbsQ_{0}$* is a refinement of $AbsQ$.*

Proof

We define a normal $C\cup R\cup Lin(deq)$-forward simulation $fs$ from $AbsQ_{0}$ to $AbsQ$ as follows. Given $AbsQ_{0}$ state $t=\langle{\sigma,in^{0},rv^{0},cp^{0}}\rangle$ and an $AbsQ$ state $s=\langle{O,<,\ell,rv,cp}\rangle$ we have that $(t,s)\in fs$ iff the following hold:

• •

the sequence $\sigma$ is a linearization of a partial order $(D,\prec)$ where $D$ contains values labeling elements of $O$ and all the values corresponding to completed enqueues, i.e., $\ell_{1}({\tt COMP}(O))\subseteq D\subseteq\ell_{1}(O)$ ordered according to the happens-before order between the enqueues that added them, i.e., $d_{1}\prec d_{2}$ iff there exists $k_{1},k_{2}$ such that $\ell_{1}(k_{1})=d_{1}$, $\ell_{1}(k_{2})=d_{2}$, and $k_{1}<k_{2}$.

• •

every dequeue is at the same control point in both $s$ and $t$, i.e., for every $k$ and $i\in\{1,2,3\}$, $cp(k)=R_{i}$ iff $cp^{0}(k)=R_{i}$,

• •

every enqueue is pending in $s$ whenever it is pending in $t$, i.e., for every $k$, $cp(k)=A_{1}$ iff $cp^{0}(k)\in\{A_{1},A\}$,

• •

every enqueue is completed in $s$ whenever it is completed in $t$, i.e., for every $k$, $cp(k)=A_{2}$ iff $cp^{0}(k)=A_{2}$,

• •

every pending enqueue which is not linearized or whose value is present in $\sigma$ is a member of $O$, i.e., for every $k$,

[TABLE]

• •

every completed enqueue whose value is present in $\sigma$ is a member of $O$, i.e., for every $k$,

[TABLE]

• •

pending enqueues are maximal in $<$, i.e., for every $k$ and $k^{\prime}$, $k\not<k^{\prime}$ if $\ell_{2}(k)={\tt PEND}$,

• •

the return values fixed at dequeue linearization points are the same, i.e., for every $k$, $rv(k)=rv^{0}(k)$.

In the following, we show that indeed $fs$ is a normal $C\cup R\cup Lin(deq)$-forward simulation from $AbsQ_{0}$ to $AbsQ$.

• $\langle i\rangle$

$fs[s_{0}^{AbsQ_{0}}]=\{s_{0}^{AbsQ}\}$

• call-enq

Let $t\xrightarrow{inv(enq,d,k)}_{AbsQ_{0}}t^{\prime}$ and $s\in fs[t]$. Then, $inv(enq,d,k)$ is an enabled action in $AbsQ$ since premise of call-enq holds in $t$ and $s\in fs[t]$. Obtain $s^{\prime}$ such that $s\xrightarrow{inv(enq,d,k)}_{AbsQ}s^{\prime}$. Note that $s^{\prime}$ is unique since $AbsQ$ is deterministic with respect to $C\cup R\cup Lin(deq)$.

Next, we show that $s^{\prime}\in fs[t^{\prime}]$. Let $(D,\prec)$ be the partial order used while relating $t$ to $s$. Same partial order can be used while relating $\sigma_{s^{\prime}}$ to $t^{\prime}$ since $\texttt{COMP}(O_{s})=\texttt{COMP}(O_{s^{\prime}}$, $O_{s}\subseteq O_{s^{\prime}}$ and $<_{s}\subseteq<_{s^{\prime}}$. The only change we have in control point fields after the actions is that $cp^{0}_{s^{\prime}}(k)=A_{1}$ and $cp_{t^{\prime}}(k)=A_{1}$ which satisfies the conditions on $fs$. Moreover $k$ is a maximal pending node in $t^{\prime}$ as required by the $fs$ conditions. Consequently, $s^{\prime}\in fs[t^{\prime}]$.

• call-deq

Let $t\xrightarrow{inv(deq,k)}_{AbsQ_{0}}t^{\prime}$ and $s\in fs[t]$. Then, $inv(deq,k)$ is an enabled action in $AbsQ$ since premise of call-deq holds in $t$ and $s\in fs[t]$. Obtain $s^{\prime}$ such that $s\xrightarrow{inv(deq,k)}_{AbsQ}s^{\prime}$. Note that $s^{\prime}$ is unique since $AbsQ$ is deterministic with respect to $C\cup R\cup Lin(deq)$.

Next, we show that $s^{\prime}\in fs[t^{\prime}]$. Since $\sigma_{s}=\sigma_{s^{\prime}}$, $O_{s}=O_{s^{\prime}}$ and $\texttt{COMP}(O_{s})=\texttt{COMP}(O_{s^{\prime}}$, we can pick same $(D,\prec)$ partial order in $s^{\prime}$ and show that $\sigma_{t^{\prime}}$ is a linearization of it. The only change in control points after the transitions is that $cp^{0}_{t^{\prime}}(k)=cp_{s^{\prime}}(k)=R_{1}$ which does not violate any condition in $fs$. Consequently, $s^{\prime}\in fs[t^{\prime}]$.

• lin-enq

Let $t\xrightarrow{lin(enq,d,k)}_{AbsQ_{0}}t^{\prime}$ and $s\in fs[t]$. Then, pick $s^{\prime}=s$ such that $s\xrightarrow{\epsilon}_{AbsQ}s^{\prime}$. Note that $\epsilon$ is a valid transition with respect to the normal forward simulation relation definition. We show that $s\in fs[t^{\prime}]$. If $(D,\prec)$ is the partial order in $s$ of which one linearization is $\sigma_{t}$, we pick $D^{\prime}=D\cup\{k\}\subseteq O_{s}$. $(D^{\prime},\prec^{\prime})$ can be linearized to $\sigma_{t^{\prime}}$ since $k$ is a maximal pending node and can be linearized at the end. Moreover, the only change in control point $cp^{0}_{t^{\prime}}(k)=A$ which does not violate the $fs$ conditions.

• lin-deq1

Let $t\xrightarrow{lin(deq,d,k)}_{AbsQ_{0}}t^{\prime}$, $d\neq\texttt{EMPTY}$ and $s\in fs[t]$. Then, $lin(deq,d,k)$ is an enabled action in $AbsQ$. There must exist $d\in D\subseteq\ell_{1}(O_{s})$ such that ${\ell_{s}}_{1}(k^{\prime})=d$ and $k^{\prime}$ is minimal in $D$ (since $d$ is linearized as the minimum element in $\sigma_{t}$ according to premise of lin-deq1 of $AbsQ$). Obtain $s^{\prime}$ such that $s\xrightarrow{lin(deq,d,k)}_{AbsQ}s^{\prime}$. Note that $s^{\prime}$ is unique since $AbsQ$ is deterministic with respect to $C\cup R\cup Lin(deq)$.

Next, we show that $s^{\prime}\in fs[t^{\prime}]$. Let $(D,\prec)$ be the partial order used while relating $t$ to $s$ such that $\sigma_{t}$ is a linearization of this partial order. Since we have shown that $k^{\prime}$ is minimal in that partial order, $\sigma_{t^{\prime}}$ is a linearization of $(D^{\prime},\prec^{\prime})$ where $D^{\prime}=D\setminus\{\ell_{1}(k^{\prime})\}$. Note that $\ell_{1}(\texttt{COMP}(O_{s^{\prime}}))\subseteq D^{\prime}\subseteq\ell_{1}(O_{s^{\prime}})$ holds. The only change in control points is that $cp^{0}_{t^{\prime}}(k)=cp_{s^{\prime}}(k)=R_{2}$ which does not violate the conditions for relating $t^{\prime}$ to $s^{\prime}$. Note that the fifth condition of $fs$ still holds for $k^{\prime}$ while relating $t^{\prime}$ to $s^{\prime}$. After transitions $rv^{0}_{t^{\prime}}(k)=rv_{s^{\prime}}(k)=d$ and the last condition on $fs$ is preserved.

• lin-deq2

Let $t\xrightarrow{lin(deq,\texttt{EMPTY},k)}_{AbsQ_{0}}t^{\prime}$ and $s\in fs[t]$. Then, $lin(deq,d,k)$ is an enabled action in $AbsQ$. If $\texttt{COMP}(O_{t})\neq\emptyset$, then $D$ use for linearization cannot be $\emptyset$ $\sigma_{t}=\langle\rangle$ cannot be a linearization of $(D,\prec)$. Obtain $s^{\prime}$ such that $s\xrightarrow{lin(deq,\texttt{EMPTY},k)}_{AbsQ}s^{\prime}$. Note that $s^{\prime}$ is unique since $AbsQ$ is deterministic with respect to $C\cup R\cup Lin(deq)$.

Next, we show that $s^{\prime}\in fs[t^{\prime}]$. Let $(D,\prec)$ be the partial order used while relating $t$ to $s$ such that $\sigma_{t}=\langle\rangle$ is a linearization of this partial order. We can use the same $(D,\prec)$ for relating $t^{\prime}$ to $s^{\prime}$ because $\sigma$ field is the same for both $s$, $s^{\prime}$; and $O$, $<$, $\ell$ fields are same for both $t$ and $t^{\prime}$. The only change in control points is that $cp^{0}_{t^{\prime}}(k)=cp_{s^{\prime}}(k)=R_{2}$ which does not violate the conditions for relating $t^{\prime}$ to $s^{\prime}$. After transitions $rv^{0}_{t^{\prime}}(k)=rv_{s^{\prime}}(k)=d$ and the last condition on $fs$ is preserved.

• ret-enq

Let $t\xrightarrow{ret(enq,k)}_{AbsQ_{0}}t^{\prime}$ and $s\in fs[t]$. Then, there are two cases assuming data independence: (i) $in^{0}_{t}(k)=d$ and $\exists i.\sigma_{t}(i)=d$ (ii) or not.

First, consider the former case. Then, ret-enq1 rule of $AbSQ$ is applicable. Its precondition holds since fifth condition of $fs$ holds while relating $t$ to $s$. Apply this rule ($ret(enq,k)$) to obtain $s^{\prime}$. Note that $s^{\prime}$ is unique since $AbsQ$ is deterministic with respect to $C\cup R\cup Lin(deq)$ and it is a valid action according to the normal forward-simulation relation definition.

Next, we show that $s^{\prime}\in fs[t^{\prime}]$. Since $\exists i.\sigma_{t}(i)=d$, we know that $d\in D$ where $(D,\prec)$ is the partial order satisfying first condition of $fs$ while relating $t$ to $s$, and $k\in O_{s}$ takes part in the linearization i.e., ${\ell_{t}}_{1}(k)\in D$. We can use the same partial order $(D,\prec)$ for relating $t^{\prime}$ to $s^{\prime}$ such that it satisfies the first condition of $fs$. The only change in control points is that $cp^{0}_{t^{\prime}}(k)=cp_{s^{\prime}}(k)=A_{2}$ which does not violate the conditions for relating $t^{\prime}$ to $s^{\prime}$. Note that the sixth condition of $fs$ also continue to hold for $k$ for the post-states.

Second, consider the latter case: $in^{0}_{t}(k)=d$, but $\forall i.\sigma_{t}(i)\neq d$. Since $(t,s)\in fs$, $k\notin O_{s}$ by the fifth and sixth conditions. Hence, the pre-condition of ret-enq2 is satisfied by $t$. Apply this rule ($ret(enq,k)$) to obtain $s^{\prime}$. Note that $s^{\prime}$ is unique since $AbsQ$ is deterministic with respect to $C\cup R\cup Lin(deq)$ and it is a valid action according to the normal forward-simulation relation definition.

Next, we show that $s^{\prime}\in fs[t^{\prime}]$. For satisfying the first condition, one can use the same $(D,\prec)$ partial order that is used for relating pre-states since $\sigma$ fields of $t$, $t^{\prime}$ and $O$, $<$, $\ell$ fields of $s$ and $s^{\prime}$ are the same. The only change in control points is that $cp^{0}_{t^{\prime}}(k)=cp_{s^{\prime}}(k)=A_{2}$ which does not violate the conditions for relating $t^{\prime}$ to $s^{\prime}$.

• ret-deq

Let $t\xrightarrow{ret(deq,d,k)}_{AbsQ_{0}}t^{\prime}$ and $s\in fs[t]$. Then, $ret(deq,d,k)$ is an enabled action in $AbsQ$ due to premise ret-deq of $AbsQ_{0}$ and the last condition on $fs$ (since $(t,s)\in fs$). Obtain $s^{\prime}$ such that $s\xrightarrow{ret(deq,d,k)}_{AbsQ}s^{\prime}$. Note that $s^{\prime}$ is unique since $AbsQ$ is deterministic with respect to $C\cup R\cup Lin(deq)$.

We see that $s^{\prime}\in fs[t^{\prime}]$. Pre-states are equal to the post-states with the only exception in the control points such that $cp^{0}_{t^{\prime}}(k)=cp_{s^{\prime}}(k)=R_{3}$. All the conditions except the third one continues to hold in the post states since they hold in the pre-states. The third rule regarding the control points of dequeues also continue to the hold since changes in the control point of $k$ does not violate it.

Appendix 0.D Proof of Theorem 5.1

We show that $AbsS$ and $AbsS_{0}$ refine each other. The standard reference implementation $AbsS_{0}$ is defined exactly as the one for queues, $AbsQ_{0}$, except that pop linearization points extract values from the beginning of the sequence stored in the state.

Thus, the states of $AbsS_{0}$ are tuples $\langle{\sigma,in^{0},rv^{0},cp^{0}}\rangle$ where $\sigma\in\<Vals>^{*}$ is a sequence of values, $in^{0}:\<Ops>~{}>\<Vals>$ records the input value of a push, $rv^{0}:\<Ops>~{}>\<Vals>$ records the return value of a pop fixed at its linearization point ($~{}>$ denotes a partial function), and $cp^{0}:\<Ops>~{}>\{A_{1},A,A_{2},R_{1},R_{2},R_{3}\}$ records the control point of every push ($A_{1},A,A_{2}$) or pop operation ($R_{1},R_{2},R_{3}$). All the components are $\emptyset$ in the initial state, and the transition relation $->$ is defined in Fig. 9. The alphabet of $AbsS$ contains call/return actions and push/pop linearization points.

To prove that $AbsS$ is a refinement of $AbsS_{0}$ we define a normal $C\cup R$-backward simulation (i.e, a backward simulation as in Definition 6) from $AbsS$ to $AbsS_{0}$. The reverse is shown using a normal $C\cup R$-forward simulation (i.e, a forward simulation as in Definition 5).

Lemma 3

$AbsS$* is a refinement of $AbsS_{0}$.*

Proof

We define a normal $C\cup R$-backward simulation $bs$ from $AbsS$ to $AbsS_{0}$ as follows. Given an $AbsS$ state $s=\langle{O,<,\ell,rv,cp}\rangle$ and an $AbsS_{0}$ state $t=\langle{\sigma,in^{0},rv^{0},cp^{0}}\rangle$ we have that $(s,t)\in bs$ iff the following hold:

• •

if a pop has committed or respectively, it has returned in $s$, then it had been linearized or respectively, it has returned in $t$, i.e., for every $k$, if $cp(k)\in\{R_{2},R_{3}\}$ then $cp^{0}(k)=cp(k)$,

• •

a push is completed in $s$ whenever the same is true in $t$, i.e., for every $k$, $cp(k)=A_{2}$ iff $cp^{0}(k)=A_{2}$,

• •

a push is pending in $s$ iff either it is a non-linearized pending push in $t$ or its linearization point has been executed, i.e., for every $k$, $cp(k)=A_{1}$ iff $cp^{0}(k)=A_{1}$ and $in^{0}(k)$ doesn’t occur in $\sigma$, or $cp(k)=A$,

• •

if a pop didn’t commit in $s$ then it is pending in $t$ and it may have been linearized, i.e., for every $k$, if $cp(k)=R_{1}$ then $cp^{0}(k)\in\{R_{1},R_{2}\}$,

• •

there exists a partial injective function $g:\{k:cp(k)=R_{1}\}~{}>O$ which associates uncommitted pops to pushes in $O$ such that:

• –

for every $k$, $k\in dom(g)$ iff $g(k)\in be(k)\cup ov(k)$

• –

the sequence $\sigma$ is the mirror of a linearization of a partial order $(D,\prec)$ where $D$ contains values labeling elements of $O$ except for those in the range of $g$, and all the values corresponding to completed pushes which are not in the range of $g$, i.e., $\ell_{1}({\tt COMP}(O)\setminus range(g))\subseteq D\subseteq\ell_{1}(O\setminus range(g))$ ordered according to the happens-before order between the pushes that added them, i.e., $d_{1}\prec d_{2}$ iff there exists $k_{1},k_{2}$ such that $\ell_{1}(k_{1})=d_{1}$, $\ell_{1}(k_{2})=d_{2}$, and $k_{1}<k_{2}$

• –

every pop in the domain of $g$ has been linearized, i.e., for every $k$, $k\in dom(g)$ implies $cp^{0}(k)=R_{2}$,

• –

every pop which is not in the domain of $g$ hasn’t been linearized, i.e., for every $k$, $k\not\in dom(g)$ implies $cp^{0}(k)=R_{1}$,

• –

every push in the range of $g$ has been linearized, i.e., for every $k$, $k\in range(g)$ implies $cp^{0}(k)=A$,

• –

a pending enqueue from $O$ has been linearized when its value is contained in $\sigma$, i.e., for every $k$, if $\ell_{1}(k)\in D$ and $\ell_{2}(k)={\tt PEND}$, then $cp^{0}(k)=A$.

• •

the return values fixed at pop commit points are the same, i.e., for every $k$, if $rv(k)$ is defined, then $rv(k)=rv^{0}(k)$,

• •

every pending push has the same input value in both $s$ and $t$, i.e., for every $k$, $\ell_{1}(k)=in^{0}(k)$,

In the following, we show that indeed $bs$ is a normal $C\cup R$-backward simulation from $AbsS$ to $AbsS_{0}$:

• •

Let $s\xrightarrow{inv(push,d,k)}s^{\prime}$ be a transition in $AbsS$ and $(s^{\prime},t^{\prime})\in bs$. We consider two cases depending on whether the value $d$ occurs on a position $i$ in the sequence $\sigma$ of $t^{\prime}$ or not. If it occurs, let $t$ be a $AbsS_{0}$ state where essentially, the component $\sigma$ is the prefix of the sequence $\sigma$ of $t^{\prime}$ that contains the first $i-1$ positions (except for some set of pushes that will be defined hereafter, all operations are at the same control point). Let $@t$ be the following $AbsS_{0}$ trace:

[TABLE]

where $d_{j}$ is the value on position $j$ in the sequence $\sigma$ of $t^{\prime}$ and $n$ is the length of this sequence (we assume that positions are indexed starting from [math]). Let $k_{i}=k$. For every $k_{j}$ with $i\leq j\leq n-1$, we must have that $cp(k_{j})=A$ in $t^{\prime}$. We take $cp(k_{j})=A_{1}$ in $t$ for every $j\geq i+1$ and $cp$ undefined for $k_{i}$. We have that $t\xrightarrow{@t}t^{\prime}$ is a valid sequence of transitions of $AbsS_{0}$ and $(s,t)\in bs$ (the latter can be proved by taking the same function $g$ used in establishing that $(s^{\prime},t^{\prime})\in bs$). Now, assume that the value $d$ is not in the sequence $\sigma$ of $t^{\prime}$. We consider an $AbsS_{0}$ state $t$ where the component $\sigma$ is the same as the one in $t^{\prime}$. There are two sub-cases depending on whether there exists a pending pop $k^{\prime}$ such that $g(k^{\prime})=k$ when establishing that $(s^{\prime},t^{\prime})\in bs$. If it exists, the operations are at the same control point in both $t$ and $t^{\prime}$ except for the push $k$ for which $cp(k)$ is undefined in $t$, and the the pop $k^{\prime}$ for which we take $cp(k^{\prime})=R_{0}$ in $t$. We have that

[TABLE]

in $AbsS_{0}$. If there exists no such pop $k^{\prime}$, it can be easily seen that there exists $t$ such that $t\xrightarrow{inv(push,d,k)}t^{\prime}$ and $(s,t)\in bs$.

• •

Let $s\xrightarrow{inv(pop,k)}s^{\prime}$ be a transition in $AbsS$ and $(s^{\prime},t^{\prime})\in bs$. We consider two cases depending on whether in the function $g$ used to relate $s^{\prime}$ to $t^{\prime}$ we have that $k\in dom(g)$. In other words, either the newly invoked pop operation $k$ did not linearize yet ($k\not\in dom(g)$) or it linearizes and removes an element inserted by a linearized push ($k\in dom(g)$). The second case also splits into two sub-cases: The value removed by pop $k$ is inserted by a push $k^{\prime}=g(k)$ that is still pending or the push has returned. We will look at all three cases separately. The easiest one is the first case. There exists some $t$ where essentially the component $\sigma$ is the same as the one in $t^{\prime}$, such that $t\xrightarrow{inv(pop,k)}t^{\prime}$ and $(s,t)\in bs$.

For the first sub-case of the second case, we take an $AbsS_{0}$ state $t$ where $\sigma_{t}=d\cdot\sigma_{t^{\prime}}$ (we use $\sigma_{t}$ to denote the component $\sigma$ in $t$). It must happen that $cp^{0}_{t^{\prime}}(k)=R_{2}$. The operations are at the same control point in both $t$ and $t^{\prime}$, except for $k$ in which case $cp^{0}$ is undefined. We have that $t\xrightarrow{inv(pop,k),\ lin(pop,d,k^{\prime})}t^{\prime}$ and $(s,t)\in bs$. The latter holds because essentially, $k^{\prime}$ is a maximal node in $s^{\prime}$ (since it is pending).

For the second sub-case, we define an $AbsS_{0}$ state $t$ where the sequence $\sigma$ is the minimal prefix of $\sigma_{t^{\prime}}$ that includes the value $d$ added by $k^{\prime}$. Let $i$ be the index of this value in $\sigma_{t^{\prime}}$ and $k_{j}$ with $i<j$ the identifiers of the pushes that added the values following $d$ in $\sigma_{t^{\prime}}$. Let $@t$ be the following $AbsS_{0}$ trace:

[TABLE]

where $d_{j}$ is the value on position $j$ in the sequence $\sigma_{t^{\prime}}$ and $n$ is the length of this sequence. We have that $t\xrightarrow{@t}t^{\prime}$ is a valid sequence of transitions of $AbsS_{0}$ and $(s,t)\in bs$. The latter relies on the fact that $k^{\prime}$ is a greatest completed push in $s$ and all pushes $k_{j}$ with $j>i$ are pending in $s$.

• •

Let $s\xrightarrow{com(pop,d,k)}s^{\prime}$ be a transition in $AbsS$ and $(s^{\prime},t^{\prime})\in bs$. When this transition results in removing a greatest completed push or a pending push in $s$, then there exists an $AbsS_{0}$ state $t$ such that $t\xrightarrow{@t}t^{\prime}$ is a valid sequence of $AbsS_{0}$ transitions and $(s,t)\in bs$, for some $t$ and $@t$ defined as in the second case of $inv(pop,k)$. When it removes a completed push which is followed by other completed pushes (in the happens-before in $s$), then we pick $t=t^{\prime}$. We have that $t\xrightarrow{\epsilon}t^{\prime}$ and $(s,t)\in bs$ (for the latter we must choose a function $g$ such that $g(k)=k^{\prime}$ where $k^{\prime}$ is the push removed by the $AbsS$ transition.

• •

Let $s\xrightarrow{ret(push,k)}s^{\prime}$ be a transition in $AbsS$ and $(s^{\prime},t^{\prime})\in bs$. We consider two cases depending on whether the happens-before in $s$ contains push $k$. If it contains push $k$, there are two sub-cases: (1) if its input is present in $\sigma_{t^{\prime}}$ then there exists an $AbsS_{0}$ state $t$ such that $t\xrightarrow{ret(push,k)}t^{\prime}$ is a valid sequence of $AbsS_{0}$ transitions and $(s,t)\in bs$, and (2) otherwise, we take a state $t$ where essentially, $\sigma_{t}=d\cdot\sigma_{t^{\prime}}$ for which we have that $t\xrightarrow{lin(pop,d,k),\ ret(push,k)}t^{\prime}$ and $(s,t)\in bs$. If the happens-before in $s$ doesn’t contain push $k$, then there exists an $AbsS_{0}$ state $t$ such that $t\xrightarrow{ret(push,k)}t^{\prime}$.

• •

The case of pop returns $ret(pop,k)$ is trivial. Such transitions are simulated by $ret(pop,k)$ transitions of $AbsS_{0}$.

Lemma 4

$AbsS_{0}$* is a refinement of $AbsS$.*

Proof

We define a normal $C\cup R$-forward simulation $fs$ from $AbsS_{0}$ to $AbsS$ as follows. Given an $AbsS_{0}$ state $t=\langle{\sigma,in^{0},rv^{0},cp^{0}}\rangle$ and an $AbsS$ state $s=\langle{O,<,\ell,rv,cp}\rangle$ we have that $(t,s)\in fs$ iff the following hold:

every pop is at the same control point in both $t$ and $s$, i.e., for every $k$ and $i\in\{1,2,3\}$, $cp^{0}(k)=R_{i}$ iff $cp(k)=R_{i}$, 2. 2.

a push has been invoked in $t$ whenever it has been invoked in $s$, i.e., for every $k$, $cp^{0}(k)=A_{1}$ iff $cp(k)=A_{1}$, 3. 3.

a push which is linearized in $t$ has been invoked in $s$, i.e., for every $k$, if $cp^{0}(k)=A$ then $cp(k)=A_{0}$, 4. 4.

a push is completed in $t$ iff the same holds in $s$, i.e., for every $k$, $cp^{0}(k)=A_{2}$ iff $cp(k)=A_{2}$, 5. 5.

the pair $(O,\ell)$ in $s$ satisfies the following:

• •

for every $k$, if $in^{0}(k)=d$, $cp^{0}(k)\in\{A_{1},A\}$, and $d$ occurs in $\sigma$, then $k\in O$ and $\ell(k)=(d,{\tt PEND})$,

• •

for every $k$, if $in^{0}(k)=d$, $cp^{0}(k)=A_{2}$, and $d$ occurs in $\sigma$, then $k\in O$ and $\ell(k)=(d,{\tt COMP})$, 6. 6.

every pending push in $O$ is overlapping with every non-linearized pop, i.e., for every $k$, if $cp^{0}(k)=R_{1}$ then $\{k^{\prime}:k^{\prime}\in O\land\ell_{2}(k^{\prime})={\tt PEND}\}\subseteq ov(k)$. 7. 7.

every completed push is either overlapping or was the greatest completed push before a non-linearized pop started, i.e., for every $k$, if $cp^{0}(k)=R_{1}$, then ${\tt COMP}(O)\subseteq ov(k)\cup be(k)$, 8. 8.

for every push that overlaps with a pop $k$ or was maximal in $<$ when $k$ started, its successors are overlapping with $k$, i.e., $k_{1}\in be(k)\cup ov(k)$ and $k_{1}<k_{2}$ implies $k_{2}\in ov(k)$ for each $k,k_{1},k_{2}$ 9. 9.

predecessors of pushes in $be(k)$ for a given pop $k$ are neither overlapping with $k$ nor in $be(k)$, i.e., $k_{1}<k_{2}$ and $k_{2}\in be(k)$ implies $k_{1}\not\in ov(k)\cup be(k)$ for each $k,k_{1},k_{2}$ 10. 10.

pending pushes are maximal in $<$, for every $k$ and $k^{\prime}$, $k\not<k^{\prime}$ if $\ell_{2}(k)={\tt PEND}$, 11. 11.

the sequence $\sigma$ is the mirror of a linearization of a partial order $(D,\prec)$ where $D$ contains values labeling elements of $O$ and all the values corresponding to completed pushes, i.e., $\ell_{1}({\tt COMP}(O))\subseteq D\subseteq\ell_{1}(O)$ ordered according to the happens-before order between the pushes that added them, i.e., $d_{1}\prec d_{2}$ iff there exists $k_{1},k_{2}$ such that $\ell_{1}(k_{1})=d_{1}$, $\ell_{1}(k_{2})=d_{2}$, and $k_{1}<k_{2}$. 12. 12.

the return values fixed at pop linearization/commit points are the same, i.e., for every $k$, $rv(k)=rv^{0}(k)$, 13. 13.

every pending push has the same input value in both $s$ and $t$, i.e., for every $k$, $\ell_{1}(k)=in^{0}(k)$,

In the following, we show that indeed $fs$ is a normal $C\cup R$-backward simulation from $AbsS_{0}$ to $AbsS$:

• •

Let $t\xrightarrow{inv(push,d,k)}t^{\prime}$ be a transition in $AbsS_{0}$ and $(t,s)\in fs$. We have that $(t^{\prime},s^{\prime})\in fs$ where $s\xrightarrow{inv(push,d,k)}s^{\prime}$ (recall that $AbsS$ is deterministic). Since the push $k$ is non-linearized in $t^{\prime}$, the component $\sigma$ of both $t$ and $t^{\prime}$ are the same and $\ell_{2}(k)={\tt PEND}$ in $s^{\prime}$. Then, the component $\sigma$ in $Abs_{0}$ states related by $fs$ to $s^{\prime}$ is allowed to exclude values added by pushes in $s^{\prime}$ which are labeled as pending. The effect of $inv(push,d,k)$ in $AbsS$ implies that $k$ overlaps with all pending pops.

• •

Let $t\xrightarrow{inv(pop,k)}t^{\prime}$ be a transition in $AbsS_{0}$ and $(t,s)\in fs$. We have that $(t^{\prime},s^{\prime})\in fs$ where $s\xrightarrow{inv(pop,k)}s^{\prime}$. The only difference between $s$ and $s^{\prime}$ is that the components $be(k)$ and $ov(k)$ in $s^{\prime}$ contain the greatest completed pushes in $s$ and the pending pushes in $s$, respectively (these components were undefined in $s$). The relation $fs$ doesn’t exclude this particular choice for $be(k)$ and $ov(k)$ when applied to $t^{\prime}$ and $s^{\prime}$.

• •

Let $t\xrightarrow{lin(push,d,k)}t^{\prime}$ be a transition in $Abs_{0}$ and $(t,s)\in fs$. We have that $(t^{\prime},s)\in fs$, i.e., the $AbsS_{0}$ transition is simulated by an empty sequence of $AbsS$ transitions, because essentially the component $\sigma$ of $t^{\prime}$ still corresponds to a linearization of the pushes in $s$ according to item 11 in the definition of $fs$. The sequence $\sigma$ in $t^{\prime}$ contains the value added by the push $k$ at the end, but this is allowed by $fs$ since $k$ is labeled as pending in $s$.

• •

Let $t\xrightarrow{lin(pop,d,k)}t^{\prime}$ be a transition in $AbsS_{0}$ and $(t,s)\in fs$. We have that $(t^{\prime},s^{\prime})\in fs$ where $s\xrightarrow{com(pop,d,k)}s^{\prime}$. The transition labeled by $com(pop,d,k)$ is enabled in $AbsS_{0}$ because $d$ was the first value in the sequence $\sigma$ of $t$. Indeed, this implies that $d$ was added by a push $k^{\prime}$ which is maximal in the happens-before stored in $s$. This clearly implies that $k^{\prime}\in be(k)\cup ov(k)$. In addition, the sequence $\sigma$ in $t^{\prime}$ does correspond to a linearization of the pushes in $s^{\prime}$ (which don’t contain $k$ anymore) because $\sigma$ in $t$ had this property with respect to $s$ and $\sigma$ in $t^{\prime}$ is obtained by deleting the first value in the sequence $\sigma$ of $t$.

• •

Let $t\xrightarrow{ret(push,k)}t^{\prime}$ be a transition in $AbsS_{0}$ and $(t,s)\in fs$. We have that $(t^{\prime},s^{\prime})\in fs$ where $s\xrightarrow{ret(push,k)}s^{\prime}$. There are two cases depending on whether the value added by $k$ is still present in the sequence $\sigma$ of $t$. If it is not, then the push $k$ doesn’t occur in the happens-before from $s$, and the only effect of these two transitions is changing the control point of $k$. Therefore, $(t^{\prime},s^{\prime})\in fs$ clearly holds. When this value is still present, the effect of $ret(push,k)$ in $AbsS$ is changing the flag of push $k$ from ${\tt PEND}$ to ${\tt COMP}$. Since the order between pushes doesn’t change, we have that $(t^{\prime},s^{\prime})\in fs$.

• •

Let $t\xrightarrow{ret(pop,d,k)}t^{\prime}$ be a transition in $AbsS_{0}$ and $(t,s)\in fs$. We have that $(t^{\prime},s^{\prime})\in fs$ where $s\xrightarrow{ret(pop,d,k)}s^{\prime}$. This case is obvious, the only change between $s$ and $s^{\prime}$ being the control point of $k$.

Appendix 0.E Proving the correctness of $TSS$

The LTS corresponding to the description of $TSS$ given in Fig. 4 is defined as usual. The control points and transition labels we use in the following proof are pictured in Fig. 10. To simplify the proof, we take the initializations of some local variables together as atomic.

States of the TS-Stack contains the global variables and local variables as fields. Global variables are just elements of their domains and local variables are maps from operation identifiers to their domains. We say $i_{q}(k)$ for referencing the value of local variable $i$ of operation $k$ in state $q$. There is only one special local variable called $myTID$. Its value is unique to each pending operation in a state i.e., concurrent operations cannot have the same $myTID$ value. TS-Stack states also contains sets $O_{a},O_{r}\in\mathbb{O}$ which are operation identifier sets of push and pops respectively, and the control point function $cp$ which is a map from operation identifiers to the control points set that are presented in the flow diagram Figure  10. Transition relation of the TS-STack is presented in Figure 11 (push rules) and Figure 12 (pop rules). Next, we show that the linearizability of TS Stack.

Lemma 1

$TSS$* is a $C\cup R\cup Com(pop)$-refinement of $AbsS$.*

Proof

We show that the relation $\mathit{fs}_{2}$ defined in Section 5.3 is a $C\cup R\cup Com(pop)$-forward simulation from $TSS$ to $AbsS$. For readability, we recall the definition of $\mathit{fs}_{2}$.

Let us make some clarifications before defining the relation. In order not to confuse nodes in TS Stack and nodes in $AbsS$, we call nodes of $AbsS$ as vertices from now on. We also define ordering relation (called traverse order) among the operations in a state of $TS$. It basically reflects the traverse order of pop operations. For two push operations $m,n\in O_{a}$ is state $s$ we say that $m<^{tr}_{s}n$ iff either $myTid(m)<myTid(n)$ or $myTid(m)=myTid(n)$ and $n_{s}(n)$ is reachable from $n_{s}(m)$ using next pointers. $\geq^{tr}$ is obtained from $<^{tr}$ in the usual way.

The relation $\mathit{fs}_{2}\subseteq Q_{C}\rightarrow Q_{AbsS}$ contains $(s,t)$ iff the following are satisfied:

• Nodes

$k\in O_{t}$ iff $k$ is a push operation in $s$ ($k\in O_{a}$) such that either it has not inserted its node to the pool yet ( $cp_{s}(k)=A_{i}$ and $i<3$) or its node is not taken by a pop ($cp_{s}(k)=A_{i}$, $i\geq 3$ and $n_{s}(k)->taken=false$).

• Pend/Comp

A vertex $k\in O_{t}$ is pending ($\ell_{t}(k)=(d,\texttt{PEND})$) iff $k$ satisfies the previous condition, $x_{s}(k)=d$ and it is not completed in $s$ ($cp_{s}(k)=A_{i}$ and $i<6$). Similarly, this vertex is completed ($\ell_{t}(k)=(d,\texttt{COMP})$) iff $k$ satisfies the previous condition, $x_{s}(k)=d$ and it is completed in $s$ ($cp_{s}(k)=A_{6}$). Pending vertices are maximal with respect to $<_{t}$ i.e., if $k\in O_{t}$ is a pending vertex, then for all $k^{\prime}\in O_{t}$ $k\nless_{t}k^{\prime}$.

• TSOrder

If a node has a smaller timestamp than the other node in $s$, the operations that inserted them cannot be ordered reversely in $t$. More formally, let $k,k^{\prime}\in O_{t}$ s.t. $n_{s}(k)->ts\leq n_{s}(k^{\prime})->ts$. Then, $k^{\prime}\nless_{t}k$.

• TidOrder

Order among the nodes inserted by the same threads in $s$ must be preserved among the operations that inserted them in $t$. Let $k,k^{\prime}\in O_{t}$ s.t. $myTid_{s}(k)=myTid_{s}(k^{\prime})$ and $n_{s}(k)->ts<n_{s}(k^{\prime})->ts$. Then, $k<_{t}k^{\prime}$.

• Frontiers

Every maximally closed or pending vertex can be removed by a pending pop. More formally, let $k\in O_{t}$ such that $\ell_{t}(k)=(\_,\texttt{PEND})$. Then, for all pops $p$, $k\in ov_{t}(p)$. In the other case, let $k\in O_{t}$ such that $\ell_{t}(k)=(\_,\texttt{COMP})$ and for all other $k^{\prime}\in O_{t}$ such that $k<_{t}k^{\prime}$, we know $\ell_{t}(k^{\prime})=(\_,\texttt{PEND})$. Then, for all pop operations $p$, $k\in be_{t}(p)$ or $k\in ov_{t}(p)$.

• MaximalOV

If a push $k\in O_{t}$ is a candidate to be removed by a pop $p$, then every other push $k^{\prime}$ invoked after $k$ is a candidate to be removed by $p$ since $k$ is concurrent with $p$. More formally, let $k,k^{\prime}\in O_{t}$ such that $k<_{t}k^{\prime}$ and there exists a pop $p$ such that $k\in be_{t}(p)$ or $k\in ov_{t}(p)$. Then, $k^{\prime}\in ov_{t}(p)$.

• MinimalBE

If a push $k\in O_{t}$ has finished before the pop $p$ is invoked and yet $k$ is a candidate to be removed by $p$, other pushes completed before $k$ can not be candidates to be removed by $p$ at that state. More formally, let $k,k^{\prime}\in O_{t}$ such that $k<_{t}k^{\prime}$ and there exists a pop $p$ such that $k^{\prime}\in be_{t}(p)$. Then, neither $k\in be_{t}(p)$ nor $k\in ov_{t}(b)$.

• ReverseFrontiers

If all immediate followers $k^{\prime}\in O_{t}$ of a push $k\in O_{t}$ are concurrent with pop $p$, then $k$ is either concurrent or maximally closed with respect to $p$. More formally, let $k\in O_{t}$ and for all $k^{\prime}\in O_{t}$ such that $k\in pred_{<_{t}}(k^{\prime})$, $k^{\prime}\in ov_{t}(p)$, where $p$ is a pop operation. Then, $k\in ov_{t}(p)\cup be_{t}(p)$.

• FixReturn

If a pop $p$ is after its commit point action in $s$, then the $rv$ value of this operation in $t$ is fixed to $youngest_{s}(p)->data$. More formally, Let $p$ be the pop operation such that $cp_{s}(p)=R_{6}$ and $success_{s}(p)=\texttt{true}$. Then, $rv_{t}(p)=youngest_{s}(p)->data$.

• TraverseBefore

If a pop operation $p$ is currently visiting node $n$, it has non-null node $y$ as the $youngest$ and there is a non-null not taken node $m$ coming before $n$ in the traverse order with a greater timestamp than $y$, then the operation that inserts $m$ must be concurrent with $p$. More formally, assume $youngest_{s}(p)=y$ and $y\neq\texttt{null}$. Let $k\in O_{t}$ such that $n_{s}(k)\neq\texttt{null}$, $n_{s}(k)->taken=\texttt{false}$, $n_{s}(k)<^{tr}_{s}n_{s}(p)$ and $n_{s}(k)->ts\geq y->ts$. Then, $k\in ov_{t}(p)$.

• TraverseBeforeNull

If a pop operation $p$ is currently visiting node $n$, and its $youngest$ field is null, then every other node $m$ coming before $n$ in the traverse order must be concurrent with $p$. More formally , let $youngest_{s}(p)=\texttt{null}$ and assume there exists an operation $k\in O_{t}$ such that $n_{s}(k)\neq\texttt{null}$, $n_{s}(k)->taken=\texttt{false}$ and $n_{s}(k)<^{tr}_{s}n_{s}(p)$. Then, $k\in ov_{t}(p)$.

• TraverseAfter

If a pop operation $p$ is currently visiting node $n$ that is not null and its youngest element $m$ is not null and still not taken in state $s$, then either $m$ is a candidate to be removed by $p$ in $t$ or there exists a later node $m^{\prime}$ than $n$ such that $m^{\prime}$ is a candidate in $t$ and it has a bigger timestamp than n. More formally, assume that there exists $k,k^{\prime}\in O_{t}$ such that $youngest_{s}(p)->taken\neq false$, $youngest_{s}(p)=n_{s}(k)$ and $n_{s}(k^{\prime})=n_{s}(p)$. Then, either $k\in ov_{t}(p)\vee k\in be_{t}(p)$ or there exists $k^{\prime\prime}\in O_{t}$ s.t. $n_{s}(k^{\prime\prime})->ts>n_{s}(k)->ts$ and $k^{\prime\prime}\in ov_{t}(p)\vee k^{\prime\prime}\in be_{t}(p)$ and either $k^{\prime}<^{tr}_{s}k^{\prime\prime}$ or $n_{s}(p)=n_{s}(k^{\prime\prime})\wedge cp_{s}(p)=R_{j}\wedge j<5$.

Next, we will show that $\mathit{fs}_{2}$ is really a $C\cup R\cup Com(pop)$-forward simulation relation. Except the trivial base case, we case-split on the transition rules. We first assume $s\xrightarrow{\alpha}_{TSS}s^{\prime}$ and $t\in\mathit{fs}_{2}[s]$. Then, we find corresponding transition $\alpha^{\prime}\in\Sigma_{AbsS}$ obeying the $C\cup R\cup Com(pop)$-forward simulation relation conditions and obtain $t^{\prime}$ such that $t\xrightarrow{\alpha^{\prime}}_{AbsS}st$ and $t^{\prime}\in\mathit{fs}_{2}[s^{\prime}]$.

We observe that if $\alpha\in C\cup R\cup Com(pop)$, then the corresponding rule in $AbsS$ is $\alpha^{\prime}=\alpha$. Otherwise, $\alpha^{\prime}=\epsilon$.

Let the following describe $\alpha$: $\psi\triangleright s\xrightarrow{\alpha}_{TSS}s^{\prime}$ where $\psi$ is the precondition (guard) that needs to be satisfied for enabling $\alpha$ and $\psi^{\prime}\triangleright t\xrightarrow{\alpha^{\prime}}_{AbsS}t^{\prime}$ describe the $\alpha^{\prime}$ if $\alpha^{\prime}\neq\epsilon$ (equivalently $\alpha^{\prime}=\alpha$).

For the cases $\alpha^{\prime}=\alpha$, we first need to show $\alpha^{\prime}$ is enabled in state $t$ i.e., $t$ satisfies $\psi^{\prime}$. If this can not be directly obtained from the information that $s$ satisfies $\psi$ and using one or two obvious conditions on $\mathit{fs}_{2}$ (since $t\in\mathit{fs}_{2}[s]$), we show the derivation in the proof. Then, $t^{\prime}$ is obtained in a unique way since $AbsS$ is deterministic on its alphabet $\Sigma_{AbsS}=C\cup R\cup Com(pop)$. The, only other thing to show is $t^{\prime}\in\mathit{fs}_{2}[t^{\prime}]$. We show this by proving that $t^{\prime}$ does not violate any of the conditions of the $\mathit{fs}_{2}$ described above. Suppose conditions on $\mathit{fs}_{2}$ are of the form $\forall\overline{k}.guard_{s,t}(\overline{k})\triangleright\phi_{s,t}(\overline{k})$ where the $\overline{k}$ is a vector of operation identifiers and $\phi$ defined on states $s$ and $t$ must hold if the guard defined on $s$ and $t$ holds. We say that a vector $\overline{k_{1}}$ is a new instantiation of the condtion if $\overline{k_{1}}$ does not satisfy the $guard_{s,t}$ while relating pre-states, but it satisfies $guard_{s^{\prime},t^{\prime}}$ while relating post-states.

We only explain why the new instantiations due to the difference between $s^{\prime}$ and $s$ or the difference between $t^{\prime}$ and $t$ do not violate the conditions. We skip the instances that we assumed while relating $s$ to $t$.

For the cases in which $\alpha^{\prime}=\epsilon$, we have $t^{\prime}=t$ and the only thing to show is $t\in\mathit{fs}_{2}[s^{\prime}]$. Again, we only explain why the new instantiations due to the difference between $s^{\prime}$ and $s$ do not violate the conditions.

In the following, we show that $\mathit{fs}_{2}$ is a $C\cup R\cup Com(pop)$-forward simulation relation.

• init

$\mathit{fs}_{2}[{q_{0}}_{TSS}]=\{{q_{0}}_{AbsS}\}$

• call-push

The same derivation rule of $TSS$ is applied to $t$ to obtain $t^{\prime}$. The premise of the rule is satisfied by $t$ trivially in the sense explained before. The new vertex $k$ is added to the $O_{t}$ such that $k$ is maximal, pending and every completed vertex is ordered before $k$ in $t^{\prime}$. Moreover, $k$ is overlapping with every pending pop. To see that $t^{\prime}\in\mathit{fs}_{2}[s^{\prime}]$ we observe the following: Nodes condition is preserved because $k\in O_{t^{\prime}}$. Since the newly added vertex $k$ is maximal and pending in $t^{\prime}$, Pend/Comp condition is preserved. Frontiers and MaximalOV conditions are not violated since $k$ is added to $ov(p)$ set for every pending pop operation $p$.

• push1

We have $t^{\prime}=t$ and show $t\in\mathit{fs}_{2}[s^{\prime}]$.Nodes and Pend/Comp conditions are still satisfied since $k$ remains to be a pending vertex. TSOrder is still preserved. Timestamp of $n_{s^{\prime}}(k)$ is maximal and every other nodes of push operations with maximal timestamp in $s^{\prime}$ are pending vertices in $t$. Hence there can be no ordering between those pushes and $k$ in $t$ that can violate TSOrder. Moreover, $k$ is maximal in $t$ which means that it cannot be ordered before another push $k^{\prime}$ of which node has a lower timestamp. TidOrder is also satisfied. Since $k$ is ordered after every completed push in $t$ and every other push by the same thread is completed, ordering required by the TidOrder is present.

• push2

We have $t^{\prime}=t$ and show $t\in\mathit{fs}_{2}[s^{\prime}]$. Nodes and Pend/Comp conditions are still satisfied since $k$ remains to be a pending vertex. One can also see that the TraverseBefore condition is preserved. Let the pop $p$ visiting node $m$ and $n_{s^{\prime}}(k)<^{tr}_{s^{\prime}}m$. Since $k$ and $p$ are both pending in $s$ and $t\in\mathit{fs}_{2}[s]$, $k\in ov_{t}(p)$ (by the Frontiers condition). Hence, TraverseBefore is preserved.

• push3

We have $t^{\prime}=t$ and show $t\in\mathit{fs}_{2}[s^{\prime}]$. We consider two cases: $n_{s}(k)->taken$ is true or it is false. For the former case, $k\notin O_{t}$. The only new instantiation we check is $k\notin O_{t}$ does not violate Nodes condition while relating $s^{\prime}$ to $t$.

For the latter case, we have $k\in O_{t}$. Nodes and Pend/Comp conditions are still satisfied since $k$ remains to be a pending vertex after changing $s$ to $s^{\prime}$.

• push4

We have $t^{\prime}=t$ and show $t\in\mathit{fs}_{2}[s^{\prime}]$.

We consider two cases: $n_{s}(k)->taken$ is true or it is false. For the former case, Nodes condition is still satisfied since $k$ remains to be not a vertex.

For the latter case Nodes and Pend/Comp conditions are still satisfied since $k$ remains to be a pending vertex. TSOrder condition is still not violated since if $k^{\prime}<_{t}k$, then $k^{\prime}$ is a completed vertex in $s$ and $s^{\prime}$. By the premise of the rule (which can be shown to hold for every operation at control point $A_{4}$) $i_{s}(k^{\prime})<i_{s}(k)$ and consequently $n_{s^{\prime}}(k^{\prime})->ts<n_{s^{\prime}}(k)->ts$. Since every other push by the thread of $k$ is completed, TidOrder still continues to hold for the same reasons. TraverseAfter condition is also preserved. Let $k^{\prime}$ be the push and $p$ be the pop such that $n_{s}(k^{\prime})=youngest_{s}(p)$, $n_{s}(k^{\prime})\leq^{tr}_{s}n_{s}(k)$, $n_{s}(k^{\prime})->ts<n_{s}(k)->ts$ and $k\in ov_{t}(p)$ or $k\in be_{t}(p)$. Assume $n_{s^{\prime}}(k^{\prime})->ts\geq N_{s^{\prime}}(k)->ts$ after the action. Then, $k^{\prime}$ must be a pending push both in $s$ and $s^{\prime}$ by the premise of the derivation rule and $k^{\prime}\in ov_{t}(p)$ must be true by Frontiers condition and $t\in\mathit{fs}_{2}[s]$. Hence, the TraverseAfter condition is preserved.

• ret-push

We consider two cases, $n_{s}(k)->taken$ is false or true. For the former case, we obtain $t^{\prime}$ by applying ret-push1 rule of $AbsS$. Nodes and Pend/Comp conditions are still satisfied since $k$ becomes a completed vertex in $t^{\prime}$. Frontiers condition still holds since although $k$ become a maximally closed vertex in $t^{\prime}$, we have $k\in ov_{t^{\prime}}(p)$ for all pending nodes $p$ (due to Frontiers condition, $t\in\mathit{fs}_{2}[s]$ and $k$ was a pending operation in state $t$, $k\in ov_{t}(p)$).

For the latter case, we obtain $t^{\prime}$ by applying ret-push2 rule of $AbsS$. Nodes condition is still satisfied since $k\notin O_{t^{\prime}}$.

• call-pop

The same derivation rule of $TSS$ is applied to $t$ to obtain $t^{\prime}$. Frontiers condition holds for $p=k$ relating $s^{\prime}$ to $t^{\prime}$ since $k^{\prime}\in ov_{t^{\prime}}(k)$ for every pending vertex $k^{\prime}$ and $k^{\prime\prime}\in be_{t^{\prime}}(p)$ for all completed vertex $k^{\prime\prime}$. $t^{\prime}$ due to action $inv(pop,k)$ applied on $t$. MaximalOV condition holds for $p=k$ since pending vertices are maximal in $t^{\prime}$ and for any maximally closed vertex $k^{\prime}$ in $t^{\prime}$, if $k^{\prime}$ is ordered before other vertex $k^{\prime\prime}$, then $k^{\prime\prime}$ is a pending operation by definition of being maximally closed and $k^{\prime\prime}\in ov_{t}(k)$ due to the changes by inv-pop action on $t$. MinimalBE condition holds while relating $s^{\prime}$ to $t^{\prime}$ for the pop $p=k$ because only maximally closed vertices are in $be(k)$ and if a push $k^{\prime}$ is ordered before a maximally closed push $k^{\prime\prime}$ in $t$, neither $k^{\prime\prime}\in be_{t^{\prime}}(k)$ (since $k^{\prime\prime}$ is not maximally closed) nor $k^{\prime\prime}\in ov_{t^{\prime}}$ (since $k^{\prime\prime}$ cannot be pending). ReverseFrontiers condition holds while relating $s^{\prime}$ to $t^{\prime}$ for the pop $p=k$ because, if $k^{\prime\prime}\in ov_{t^{\prime}}(k)$ for all immediate successors of $k^{\prime}$ in $t$, then $k^{\prime\prime}$ are pending vertices (due to call-pop action of $AbsS$), $k^{\prime}$ is a maximally closed vertex and $k^{\prime}\in be_{t^{\prime}}(k)$ (due to call-pop action of $AbsS$).

• pop1

We have $t^{\prime}=t$ and $t\in\mathit{fs}_{2}[s^{\prime}]$.

• pop2

We have $t^{\prime}=t$ and show $t\in\mathit{fs}_{2}[s^{\prime}]$. TraverseBefore condition while relating $s^{\prime}$ to $t$ still holds for $p=k$. Assume $youngest_{s^{\prime}}(k)=y$ is a non-null node. Then, for all nodes $m$ in $s^{\prime}$ such that $n_{s}(k)\leq^{tr}_{s^{\prime}}m<^{tr}_{s^{\prime}}n_{s^{\prime}}(k)$ we have $m->ts<y->ts$ in $s^{\prime}$ because $n_{s}(k)->ts>m->ts$ (since $n_{s}(k)$ is added to the pool after $m$ by the same thread) and $y->ts\geq n_{s}(k)->ts$ in $s^{\prime}$ (since either $youngest_{s^{\prime}}(k)=n_{s}(k)$ or $youngest_{s^{\prime}}(k)->ts>n_{s}(k)->ts$). TraverseAfter does not have any new instatiations since the guard mentions the nodes after $n_{s}(k)$ while relating $s$ to $t$ whereas it mentions nodes after or including $n_{s^{\prime}}(k)$ which contains the all nodes in the former case.

• pop3

We have $t^{\prime}=t$ and $t\in\mathit{fs}_{2}[s^{\prime}]$.

• pop4

We have $t^{\prime}=t$ and $t\in\mathit{fs}_{2}[s^{\prime}]$.

• pop5

We have $t^{\prime}=t$ and show $t\in\mathit{fs}_{2}[s^{\prime}]$. TraverseBefore condition while relating $s^{\prime}$ to $t$ still holds for $p=k$ since $youngest_{s}(k)->ts<youngest_{s^{\prime}}(k)->ts$ and TraverseBefore holds while relating $s$ to $t$.

TraverseAfter condition also continues to hold for $p=k$. There are two possible cases: $youngest_{s}(k)=\texttt{null}$ or not.

First, consider the former case. Since TraverseBeforeNull is satisfied while relating $s$ to $t$, for every operation $k^{\prime},k^{\prime\prime}\in O_{t}$ such that $k^{\prime\prime}<^{tr}_{s}k^{\prime}$ and $n_{s}(k^{\prime})=youngest_{s^{\prime}}(k)$ we have $k^{\prime\prime}\in ov_{t}(k)$. Consider all such $k^{\prime\prime}$ such that $n_{s}(k^{\prime\prime})->ts>n_{s}(k^{\prime})->ts$. If there exists such a $k^{\prime\prime}$ such that $k^{\prime}\in pred_{<_{t}}(k^{\prime\prime})$, then $k^{\prime}\in ov_{t}(k)\cup be_{t}(k)$ since ReverseFrontiers condition holds relating $s$ to $t$. Otherwise, either $k^{\prime}$ is maximal in $t$ or all the vertices $v$ ordered after $k^{\prime}$ in $t$ we have $v>^{tr}_{s}k^{\prime}$. Then, either $k^{\prime}$ or one of these $v$ vertices must be maximal in $t$ and must be in $be_{t}(k)\cup ov_{t}(k)$ since Frontiers condition holds (one of them is maximal in $t$) while relating $s$ to $t$.

Second, assume there exists push operations $j,k^{\prime}$ such that $n_{s}(j)=youngest_{s}(k)\neq\texttt{null}$ and $n_{s}(k^{\prime})=n_{s}(k)=youngest_{s^{\prime}}(k)$ . Since TraverseBefore is satisfied while relating $s$ to $t$, if there exists a push $k^{\prime\prime}<^{tr}_{s}k^{\prime}$ such that $n_{s}(k^{\prime\prime})$ is not taken and $n_{s}(k^{\prime\prime})->ts\geq n_{s}(j)->ts$, then $k^{\prime\prime}\in ov_{t}(k)$. Then, for all $k^{\prime\prime}<^{tr}_{s}k^{\prime}$ such that $n_{s}(k^{\prime\prime})$ is not taken and $n_{s}(k^{\prime\prime})->ts\geq n_{s}(k^{\prime})->ts$, then $k^{\prime\prime}\in ov_{t}(k)$ since $n_{s}(k^{\prime})->ts\geq n_{s}(j)->ts$. If there exists such a $k^{\prime\prime}$ such that $k^{\prime}\in pred_{<_{t}}(k^{\prime\prime})$, then $k^{\prime}\in ov_{t}(k)\cup be_{t}(k)$ since ReverseFrontiers condition holds relating $s$ to $t$. Otherwise, either $k^{\prime}$ is maximal in $t$ or all the vertices $v$ ordered after $k^{\prime}$ in $t$ we have $v>^{tr}_{s}k^{\prime}$. Then, either $k^{\prime}$ or one of these $v$ vertices must be maximal in $t$ and must be in $be_{t}(k)\cup ov_{t}(k)$ since Frontiers condition holds (one of them is maximal in $t$) while relating $s$ to $t$.

• pop6

We have $t^{\prime}=t$ and show $t\in\mathit{fs}_{2}[s^{\prime}]$. TraverseAfter continues to hold while relating $s^{\prime}$ to $t$ for $p=k$. Let $k^{\prime},k^{\prime\prime}\in O_{t}$ such that $youngest_{s}(k)=n_{s}(k^{\prime})$, $n_{s}(k)=n_{s}(k^{\prime\prime})$ and $k^{\prime}\notin ov_{t}(k)\cup be_{t}(k)$. Note that $k^{\prime}<^{tr}_{s}k^{\prime\prime}$. Then, $n_{s}(k^{\prime\prime})->ts<n_{s}(k^{\prime})->ts$ since $n_{s}(k^{\prime\prime})->ts<maxTS(k)$ and $maxTS(k)=n_{s}(k^{\prime})->TS$ ($n_{s}(k^{\prime})->ts$ cannot be MAX_INT since $k^{\prime}$ would be pending and $k^{\prime}\in ov_{t}(k)$ otherwise). Hence, there exists another push $j$ such that $j>^{tr}_{s}$ and $j\in ov_{t}(k)\cup be_{t}(k)$.

• pop7

We have $t^{\prime}=t$ and $t\in\mathit{fs}_{2}[s^{\prime}]$.

• pop8

We have $t^{\prime}=t$ and $t\in\mathit{fs}_{2}[s^{\prime}]$.

• com-pop

$t^{\prime}$ is obtained by applying com-pop1 rule of $AbsS$. We first show that precondition of com-pop1 rule of $AbsS$ si satisfied by $t$. If $com(pop,d,k)$ removes a node $n$ such that there exists a push $k^{\prime}$ such that $n_{s}(k^{\prime})=n$ in $s$, then $k^{\prime}\in O_{t}$ since it is non-null and not taken. Moreover, $k^{\prime}\in ov_{t}(k)\cup be_{t}(k)$ since TraverseAfter is preserved while relating $s$ to $t$ and all the nodes that come after $n_{s}(k)$ in terms of traverse order in $s$ have lower timestamp values than $n_{s}(k)->ts$ and $n_{s}(k)->ts\leq youngest_{s}(k)->ts$.

Next, we show that $t^{\prime}\in\mathit{fs}_{2}[s^{\prime}]$. We case split on the conditions of $\mathit{fs}_{2}$ considering new instantiations.

Nodes condition is still preserved after $k$ removes the node pushed by operation $k^{\prime}$ in $s$ since $k^{\prime}\notin O_{t^{\prime}}$ anymore by due to $com(pop,d,k)$ action.

Frontiers condition is still preserved if $k$ removes the vertex $k^{\prime}$ and makes another $k^{\prime\prime}$ maximally closed in $t$. Since all the other nodes $j$ ordered after $k^{\prime\prime}$ (except possibly $k^{\prime}$) in $t$ are pending, $j\in ov_{t}(p)$ (due to Frontiers condition while relating $s$ to $t$) for some pending pop $p\neq k$. Then, $k^{\prime\prime}\in be_{t^{\prime}}(p)$ by $com(pop,d,k)$ action.

For the MinimalBE condition, we do not have a new instance. If $k^{\prime}\in be_{t^{\prime}}(p)$ becomes true although $k^{\prime}\notin be_{t}(p)$, we cannot have $k^{\prime\prime}\in O_{t^{\prime}}$ such that $k^{\prime}\in pred_{<_{t^{\prime}}}(k^{\prime\prime})$ and $k^{\prime\prime}\in be_{t^{\prime}}(p)$ since $com(pop,d,k)$ does not add $k^{\prime\prime}$ to $ov(p)$ if its successor is not pending with respect to $p$.

ReverseFrontiers condition is still preserved. If $k$ removes the vertex $k^{\prime}$ and there exists an immediate predecessor $k^{\prime\prime}$ of $k^{\prime}$ such that all of immediate successors of $k^{\prime\prime}$ are in $ov_{t^{\prime}}(p)$, then $k^{\prime\prime}\in ov_{t^{\prime}}(p)$ due to the action $com(pop,d,k)$.

TraverseAfter condition is still preserved after $k$ removes the node of push $k^{\prime}$. Let $p\neq k$ be another pop operation such that $n_{s}(j)=youngest_{s}(p)$ for some push $j$ and $n_{s}(k^{\prime})$ be the only node such that $n_{s}(k^{\prime})->ts>youngest_{s}(p)->ts$ and $n_{s}(k^{\prime})$ comes after $n_{s}(p)$ in the traverse order of $s$ and $k^{\prime}\in ov_{t}(p)\cup be_{t}(p)$. Hence, there is no $k^{\prime\prime}$ such that $n_{s}(k^{\prime\prime})$ comes after $n_{s}(p)$ in the traverse order and $j<_{t}k^{\prime\prime}$ except $k^{\prime}$ (i). In other direction, if for all $k^{\prime\prime}\in O_{t}$ such that $n_{s}(k^{\prime\prime})$ comes before $n_{s}(p)$ in the traverse order and $n_{s}(k^{\prime\prime})->ts>youngest_{s}(p)->ts$ , then $k^{\prime\prime}\in ov_{t}(p)$ since TraverseBefore condition holds while relating $s$ to $t$. Then, for all $k^{\prime\prime}\in O_{t}$ such that $n_{s}(k^{\prime\prime})$ comes before $n_{s}(p)$ in the traverse order of $s$ and $k^{\prime\prime}>_{t}j$ implies $k^{\prime\prime}\in ov_{t}(p)$ since $n_{s}(k^{\prime\prime})->ts>n_{s}(j)->ts$ if $k^{\prime\prime}>_{t}j$ (ii). Then, for all $k^{\prime\prime}\in O_{t}$ such that if $k^{\prime\prime}>_{t}j$, then $k^{\prime\prime}\in ov_{t}(p)$ except $k^{\prime}$ due to (i) and (ii). If $j\nless_{t}k^{\prime}$, then $j\in ov_{t}(p)\cup be_{t}(p)$ since ReverseFrontiers hold while relating $s$ to $t$ and $j\in ov_{t^{\prime}}\cup be_{t^{\prime}}$ after applying the action $com(pop,d,k)$. Otherwise, if $j<_{t}k^{\prime}$, then $k\in be_{t^{\prime}}$ after applying $com(pop,d,k)$.

FixReturn condition continues to hold. If $com(pop,d,k)$ removes the node pushed by $k^{\prime}$ in $s$, then $com(pop,d,k)$ removes the vertex $k^{\prime}$ (assuming data independece) and $youngest_{s}(k^{\prime})->data=\ell_{t}(k^{\prime})_{1}$. Then, $youngest_{s^{\prime}}(p)->data=rv_{t^{\prime}}(p)$ after applying commit actions at both sides.

• pop9

We have $t^{\prime}=t$ and $t\in\mathit{fs}_{2}[s^{\prime}]$.

• ret-pop

$t^{\prime}$ is obtained by applying ret-pop rule of $AbsS$ and $t^{\prime}\in\mathit{fs}_{2}[s^{\prime}]$.