Proving Linearizability Using Partial Orders (Extended Version)

TL;DR

This paper introduces a novel proof method for linearizability of concurrent data structures, constructing partial orders to handle future-dependent linearizations, validated on several complex examples.

Contribution

It presents a new proof technique using partial orders and rely-guarantee reasoning to verify linearizability of challenging concurrent data structures.

Findings

Successfully verified Herlihy-Wing queue

Verified TS queue and Optimistic set

Method handles future-dependent linearizations

Abstract

Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization --- a linear order on operations satisfying the data structure's sequential specification. Proving linearizability is often challenging because an operation's position in the linearization order may depend on future operations. This makes it very difficult to incrementally construct the linearization in a proof. We propose a new proof method that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. We formalise our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the TS queue and the Optimistic set.

Figures

Equations

$$\forall i,j.i\ne j\wedge E(i).\mathsf{tid}=E(j).\mathsf{tid}\wedge i,j\in \mathsf{dom}(G_{\mathsf{ts}})⟹G_{\mathsf{ts}}(i)\ne G_{\mathsf{ts}}(j)$$

$$\mathsf{inQ}(\mathtt{pools},E,G_{\mathsf{ts}})\triangleq \{\mathtt{enqOf}(E,G_{\mathsf{ts}},t,\tau )\mid \exists p.\mathtt{pools}(t)=\_\cdot (p,\_,\tau )\cdot \_\}$$

$$\begin{array}[]{@{}c@{}}\genfrac{}{}{0.5pt}{}{\displaystyle i\notin{\sf id}({E})\quad a\in{\sf Val}\quad E^{\prime}=E[{i}\,{:}\,{(t,{\sf op},a,{\sf todo})}]\quad R^{\prime}=R\cup\{(j,i)\mid j\in\left\lfloor{E}\right\rfloor\}}{\displaystyle\langle{c[{t}\,{:}\,{{\sf idle}}],s,(E,R)}\rangle\mathrel{{\twoheadrightarrow}_{D}}\langle{c[{t}\,{:}\,{D({\sf op})}],s[{{\tt arg}[t]}\,{:}\,{a}],(E^{\prime},R^{\prime})}\rangle}\\[10.0pt] \genfrac{}{}{0.5pt}{}{\displaystyle\langle{C},{s}\rangle\mathrel{{\longrightarrow}_{t}}\langle{C^{\prime}},{s^{\prime}}\rangle}{\displaystyle\langle{c[{t}\,{:}\,{C}],s,(E,R)}\rangle\mathrel{{\twoheadrightarrow}_{D}}\langle{c[{t}\,{:}\,{C^{\prime}}],s^{\prime},(E,R)}\rangle}\\[10.0pt] \genfrac{}{}{0.5pt}{}{\displaystyle i={\sf last}(t,(E,R))\quad E(i)=(t,{\sf op},a,{\sf todo})\quad E^{\prime}=E[{i}\,{:}\,{(t,{\sf op},a,s({\tt res}[t]))}]}{\displaystyle\langle{c[{t}\,{:}\,{{\sf skip}}],s,(E,R)}\rangle\mathrel{{\twoheadrightarrow}_{D}}\langle{c[{t}\,{:}\,{{\sf idle}}],s,(E^{\prime},R)}\rangle}\end{array}$$

$$\frac{\forall \ell .\mathcal{G}{\models }_t\left\{[[P{]]}_{\ell }\right\}\alpha \left\{[[Q{]]}_{\ell }\right\}\wedge \mathsf{stable}([[P{]]}_{\ell },\mathcal{R})\wedge \mathsf{stable}([[Q{]]}_{\ell },\mathcal{R})}{\mathcal{R},\mathcal{G}{⊢}_t\left\{P\right\}\alpha \left\{Q\right\}}$$

$$\mathsf{stable}(p,\mathcal{R})\triangleq \forall \kappa ,{\kappa }^{\prime }.\kappa \in p\wedge (\kappa ,{\kappa }^{\prime })\in \mathcal{R}⟹{\kappa }^{\prime }\in p$$

$$\begin{gathered} \mathcal{G}{\models }_t\left\{p\right\}\alpha \left\{q\right\}\triangleq \forall s,s^{\prime },H,G.(s,H,G)\in p\wedge s^{\prime }\in [[\alpha {]]}_t(s)⟹ \\ \exists H^{\prime },G^{\prime }.(s^{\prime },H^{\prime },G^{\prime })\in q\wedge H{⇝}^{\ast }{H}^{\prime }\wedge ((s,H,G),(s^{\prime },H^{\prime },G^{\prime }))\in \mathcal{G} \end{gathered}$$

$$\begin{gathered} (E,R)⇝(E^{\prime },R^{\prime })\triangleq (E=E^{\prime }\wedge R\subseteq R^{\prime })\vee \\ (\exists i,t,\mathsf{op},a,r.(\forall j.j\ne i⟹E(j)=E^{\prime }(j))\wedge \\ E(i)=(t,\mathsf{op},a,\mathsf{todo})\wedge E^{\prime }(i)=(t,\mathsf{op},a,r)) \end{gathered}$$

$$\begin{array}[]{@{}l@{}}\left\langle{s,(E,R),G}\right\rangle\dashrightarrow_{t}\left\langle{s^{\prime},(E^{\prime},R^{\prime}),G^{\prime}}\right\rangle\iff(\forall l\in{\sf Loc}\ldotp l\neq{\tt arg}[t]\implies s(l)=s^{\prime}(l))\\ \hfill{}\land\exists i\notin{\sf id}({E})\ldotp E^{\prime}=E\uplus\{[i:t,\_,\_,{\sf todo}]\}\\ \hfill{}\land R^{\prime}=(R\cup\{(j,i)\mid j\in\left\lfloor{E}\right\rfloor\})\land G=G^{\prime}\end{array}$$

$$\begin{array}[]{r@{\ }c@{\ }l}\llbracket{{\rm started}_{\mathcal{I}}(t,{\sf op})}\rrbracket_{\ell}&=&\{(s,(E,R),G)\mid E({\sf last}(t,(E,R)))=(t,{\sf op},s({\tt arg}[t]),{\sf todo})\\ &&\hfill{}\land\exists\kappa\in\llbracket{\mathcal{I}}\rrbracket_{\ell}\ldotp\left\langle{\kappa}\right\rangle\dashrightarrow_{t}\left\langle{s,(E,R),G}\right\rangle\};\\ \llbracket{{\rm ended}(t,{\sf op})}\rrbracket_{\ell}&=&\{(s,(E,R),G)\mid E({\sf last}(t,(E,R)))=(t,{\sf op},\_,s({\tt res}[t]))\}.\end{array}$$

$$\forall H^{\prime }.\lfloor H\rfloor ⊑H^{\prime }\wedge \mathsf{seq}(H^{\prime })⟹H^{\prime }\in {\mathcal{H}}_{\mathsf{queue}}\wedge same\_data(s,H,G_{\mathsf{ts}},H^{\prime })$$

$$\forall i\in \mathsf{id}(\lfloor E\rfloor ).\forall j\in \mathsf{id}(E\setminus \lfloor E\rfloor ).E(i).\mathsf{op}=E(j).\mathsf{op}=\mathrm{Deq}⟹i\stackrel{R}{\to }j$$

$$\forall i\in \mathsf{id}(\lfloor E\rfloor )\setminus \mathsf{inQ}(s(\mathtt{pools}),E,G_{\mathsf{ts}}).\forall j\in \mathsf{inQ}(s(\mathtt{pools}),E,G_{\mathsf{ts}}).i\stackrel{R}{\to }j$$

$$\forall i,j\in \mathsf{inQ}(s(\mathtt{pools}),E,G_{\mathsf{ts}}).i\stackrel{R}{\to }j⟹G_{\mathsf{ts}}(i){<}_{\mathsf{TS}}{G}_{\mathsf{ts}}(j)$$

$$\begin{gathered} \forall t,{\tau }_1,{\tau }_2.\mathtt{pools}(t)=\_\cdot (\_,\_,{\tau }_1)\cdot \_\cdot (\_,\_,{\tau }_2)\cdot \_⟹ \\ \mathtt{enqOf}(E,G_{\mathsf{ts}},t,{\tau }_1)\stackrel{R}{\to }\mathtt{enqOf}(E,G_{\mathsf{ts}},t,{\tau }_2) \end{gathered}$$

$$\forall i,a,b.G_{\mathsf{ts}}(i)=(a,b)⟹b<s(\mathtt{counter})$$

$$\forall i.i\in \mathsf{dom}(G_{\mathsf{ts}})⟹E(i).\mathsf{op}=\mathrm{Enq}$$

$$\forall t,v,\tau .\mathtt{pools}(t)=\_\cdot (\_,v,\tau )\cdot \_⟹\exists i.E(i)=(t,\mathrm{Enq},v,\_)\wedge G_{\mathsf{ts}}(i)=\tau$$

$$\forall i,j.i\ne j\wedge E(i).\mathsf{tid}=E(j).\mathsf{tid}\wedge i,j\in \mathsf{dom}(G_{\mathsf{ts}})⟹G_{\mathsf{ts}}(i)\ne G_{\mathsf{ts}}(j)$$

$$\begin{array}[]{l}\forall i\ldotp{E(i)}.{\sf op}={\rm Enq}\implies(i\not\in{\sf id}({\left\lfloor{E}\right\rfloor})\iff i\notin{\sf dom}(G_{\sf ts})\lor G_{\sf ts}(i)=\top)\end{array}$$

$$\begin{gathered} \mathsf{seen}((s,(E,R),G_{\mathsf{ts}}),d)\triangleq \{e\mid e\in \mathsf{id}(\lfloor E\rfloor )\cap \mathsf{inQ}(s(\mathtt{pools}),E,G_{\mathsf{ts}}) \\ \wedge e\stackrel{R}{\to }d\wedge \neg (s(start\_ts){<}_{\mathsf{TS}}{G}_{\mathsf{ts}}(e))\wedge E(e).\mathsf{tid}\in \mathtt{A}\} \end{gathered}$$

$$\forall e\in \mathsf{inQ}(s(\mathtt{pools}),\mathtt{E},{\mathtt{G}}_{\mathsf{ts}}).E(e).\mathsf{tid}\in \mathtt{A}⟹\neg (e\stackrel{R}{\to }\mathtt{CAND})$$

$${\mathcal{G}}_{t,\hat{\alpha },P}\triangleq \{(\kappa ,{\kappa }^{\prime })\mid \exists \ell .\kappa \in [[P{]]}_{\ell }\wedge {\kappa }^{\prime }\in [[\hat{\alpha }{]]}_t(\kappa )\}$$

$$\begin{array}[]{rcl}P_{\sf op}&\triangleq&{\sf INV}\land{\rm started}(t,{\sf op})\\ \mathcal{G}_{t}&\triangleq&(\bigcup_{t^{\prime}\in{\sf ThreadID}}\mathcal{G}_{t,{\tt scan(t^{\prime})},P_{\rm Deq}})\cup\mathcal{G}_{t,{\tt remove},P_{\rm Deq}}\\ &&\hfill{}\cup\mathcal{G}_{t,{\tt insert},P_{\rm Enq}}\cup\mathcal{G}_{t,{\tt setTS},P_{\rm Enq}}\cup\mathcal{G}_{t,{\tt genTS},{\sf INV}}\cup\mathcal{G}_{t,{\tt local}},\\ \mathcal{R}_{t}&\triangleq&\cup_{t^{\prime}\in{\sf ThreadID}\setminus\{t\}}(\mathcal{G}_{t^{\prime}}\cup{\dashrightarrow}_{t^{\prime}})\end{array}$$

$$\forall \kappa ,{\kappa }^{\prime }.(\kappa ,{\kappa }^{\prime })\in {\mathcal{R}}_t⟹\mathsf{seen}({\kappa }^{\prime },\mathtt{DEQ})\subseteq \mathsf{seen}(\kappa ,\mathtt{DEQ})$$

$$\begin{array}[]{@{}c@{}}{\sf insOf}(E,n)=\begin{cases}i,\mbox{if }G_{\sf node}(i)=n,{E(i)}.{\sf op}={\sf insert}\mbox{ and }{E(i)}.{\sf rval}={\sf true}\\ \mbox{undefined otherwise}\end{cases}\\[15.0pt] {\sf lastRemOf}(E,R,v)=\begin{cases}i,&\mbox{if }E(i)=(\_,{\sf remove},v,{\sf true})\\ &{}\land(\forall i^{\prime}\ldotp{E(i)}.{\sf op}={\sf remove}\land{E(i^{\prime})}.{\sf arg}=v\implies{}\\ &\hfill{i^{\prime}}\xrightarrow{R}{i})\\ \bot,&\mbox{if }\lnot\exists i\ldotp E(i)=(\_,{\sf remove},v,{\sf true})\end{cases}\end{array}$$

$$C\in \mathsf{Com}::=\alpha \mid C;C\mid C+C\mid C^{\ast }\mid \mathsf{skip},\text{mbox}where\alpha \in \mathsf{PCom}$$

$$[[\mathtt{assume}(\mathcal{E}){]]}_t(s)\triangleq (\text{mbox}if[[\mathcal{E}{]]}_s\ne 0\text{mbox}then\{s\}\text{mbox}else\varnothing ).$$

$$\mathtt{if}\mathcal{E}\mathtt{then}{C}_1\mathtt{else}{C}_2\triangleq (\mathtt{assume}(\mathcal{E});C_1)+(\mathtt{assume}(!\mathcal{E});C_2)$$

$$\mathtt{while}\mathcal{E}\mathtt{do}C\triangleq (\mathtt{assume}(\mathcal{E});C{)}^{\ast };\mathtt{assume}(!\mathcal{E})$$

$$\begin{array}[]{@{}c@{}}\genfrac{}{}{0.5pt}{}{\displaystyle i\notin{\sf id}({E})\quad a\in{\sf Val}\quad E^{\prime}=E[{i}\,{:}\,{(t,{\sf op},a,{\sf todo})}]\quad R^{\prime}=R\cup\{(j,i)\mid j\in\left\lfloor{E}\right\rfloor\}}{\displaystyle\langle{c[{t}\,{:}\,{{\sf idle}}],s,(E,R)}\rangle\mathrel{{\twoheadrightarrow}_{D}}\langle{c[{t}\,{:}\,{D({\sf op})}],s[{{\tt arg}[t]}\,{:}\,{a}],(E^{\prime},R^{\prime})}\rangle}\\[10.0pt] \genfrac{}{}{0.5pt}{}{\displaystyle\langle{C},{s}\rangle\mathrel{{\longrightarrow}_{t}}\langle{C^{\prime}},{s^{\prime}}\rangle}{\displaystyle\langle{c[{t}\,{:}\,{C}],s,(E,R)}\rangle\mathrel{{\twoheadrightarrow}_{D}}\langle{c[{t}\,{:}\,{C^{\prime}}],s^{\prime},(E,R)}\rangle}\\[10.0pt] \genfrac{}{}{0.5pt}{}{\displaystyle i={\sf last}(t,(E,R))\quad E(i)=(t,{\sf op},a,{\sf todo})\quad E^{\prime}=E[{i}\,{:}\,{(t,{\sf op},a,s({\tt res}[t]))}]}{\displaystyle\langle{c[{t}\,{:}\,{{\sf skip}}],s,(E,R)}\rangle\mathrel{{\twoheadrightarrow}_{D}}\langle{c[{t}\,{:}\,{{\sf idle}}],s,(E^{\prime},R)}\rangle}\end{array}$$

$$\mathsf{last}(t,(E,R))\triangleq \{\begin{array}{ll}i,& \text{mbox}suchthatE(i).\mathsf{tid}=t\\ & \text{mbox}and(\forall j.j\ne i\wedge E(j).\mathsf{tid}=t⟹j\stackrel{R}{\to }i)\\ \perp ,& \text{mbox}if\forall i.E(i).\mathsf{tid}\ne t\end{array}$$

Full text

We propose a new proof method that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. We formalise our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the TS queue and the Optimistic set.

1 Introduction

Linearizability is a commonly accepted notion of correctness of concurrent data structures. It matters for programmers using such data structures because it implies contextual refinement: any behaviour of a program using a concurrent data structure can be reproduced if the program uses its sequential implementation where all operations are executed atomically [4]. This allows the programmer to soundly reason about the behaviour of the program assuming a simple sequential specification of the data structure.

Linearizability requires that for any execution of operations on the data structure there exists a linear order of these operations, called a linearization, such that: (i) the linearization respects the order of non-overlapping operations (the real-time order); and (ii) the behaviour of operations in the linearization matches the sequential specification of the data structure. To illustrate this, consider an execution in Figure 1, where three threads are accessing a queue. Linearizability determines which values $x$ the dequeue operation is allowed to return by considering the possible linearizations of this execution. Given (i), we know that in any linearization the enqueues must be ordered before the dequeue, and Enq(1) must be ordered before Enq(3). Given (ii), a linearization must satisfy the sequential specification of a queue, so the dequeue must return the oldest enqueued value. Hence, the execution in Figure 1 has three possible linearizations: [Enq(1); Enq(2); Enq(3); Deq():1], [Enq(1); Enq(3); Enq(2); Deq():1] and [Enq(2); Enq(1); Enq(3); Deq():2]. This means that the dequeue is allowed to return 1 or 2, but not 3.

For a large class of algorithms, linearizability can be proved by incrementally constructing a linearization as the program executes. Effectively, one shows that the program execution and its linearization stay in correspondence under each program step (this is formally known as a forward simulation). The point in the execution of an operation at which it is appended to the linearization is called its linearization point. This must occur somewhere between the start and end of the operation, to ensure that the linearization preserves the real-time order. For example, when applying the linearization point method to the execution in Figure 1, by point (A) we must have decided if Enq(1) occurs before or after Enq(2) in the linearization. Thus, by this point, we know which of the three possible linearizations matches the execution. This method of establishing linearizability is very popular, to the extent that most papers proposing new concurrent data structures include a placement of linearization points. However, there are algorithms that cannot be proved linerizable using the linearization point method.

In this paper we consider several examples of such algorithms, including the time-stamped (TS) queue [7, 2]—a recent high-performance data structure with an extremely subtle correctness argument. Its key idea is for enqueues to attach timestamps to values, and for these to determine the order in which values are dequeued. As illustrated by the above analysis of Figure 1, linearizability allows concurrent operations, such as Enq(1) and Enq(2), to take effect in any order. The TS queue exploits this by allowing values from concurrent enqueues to receive incomparable timestamps; only pairs of timestamps for non-overlapping enqueue operations must be ordered. Hence, a dequeue can potentially have a choice of the “earliest” enqueue to take values from. This allows concurrent dequeues to go after different values, thus reducing contention and improving performance.

The linearization point method simply does not apply to the TS queue. In the execution in Figure 1, values 1 and 2 could receive incomparable timestamps. Thus, at point (A) we do not know which of them will be dequeued first and, hence, in which order their enqueues should go in the linearization: this is only determined by the behaviour of dequeues later in the execution. Similar challenges exist for other queue algorithms such as the baskets queue [12], LCR queue [16] and Herlihy-Wing queue [11]. In all of these algorithms, when an enqueue operation returns, the precise linearization of earlier enqueue operations is not necessarily known. Similar challenges arise in the time-stamped stack [2] algorithm. We conjecture that our proof technique can be applied to prove the time-stamped stack linearizable, and we are currently working on a proof.

In this paper, we propose a new proof method that can handle algorithms where incremental construction of linearizations is not possible. We formalise it as a program logic, based on Rely-Guarantee [13], and apply it to give simple proofs to the TS queue [2], the Herlihy-Wing queue [11] and the Optimistic Set [17]. The key idea of our method is to incrementally construct not a single linearization of an algorithm execution, but an abstract history—a partially ordered history of operations such that it contains the real-time order of the original execution and all its linearizations satisfy the sequential specification. By embracing partiality, we enable decisions about order to be delayed, mirroring the behaviour of the algorithms. At the same time, we maintain the simple inductive style of the standard linearization-point method: the proof of linearizability of an algorithm establishes a simulation between its execution and a growing abstract history. By analogy with linearization points, we call the points in the execution where the abstract history is extended commitment points.

The extension can be done in several ways: (1) committing to perform an operation; (2) committing to an order between previously unordered operatons; (3) completing an operation.

Consider again the TS queue execution in Figure 1. By point (A) we construct the abstract history in Figure 2(a). The edge in the figure is mandated by the real-time order in the original execution; Enq(1) and Enq(2) are left unordered, and so are Enq(2) and Enq(3). At the start of the execution of the dequeue, we update the history to the one in Figure 2(b). A dashed ellipse represents an operation that is not yet completed, but we have committed to performing it (case 1 above). When the dequeue successfully removes a value, e.g., 2, we update the history to the one in Figure 2(c). To this end, we complete the dequeue by recording its result (case 3). We also commit to an order between the Enq(1) and Enq(2) operations (case 2). This is needed to ensure that all linearizations of the resulting history satisfy the sequential queue specification, which requires a dequeue to remove the oldest value in the queue.

We demonstrate the simplicity of our method by giving proofs to challenging algorithms that match the intuition for why they work. Our method is also similar in spirit to the standard linearization point method. Thus, even though in this paper we formulate the method as a program logic, we believe that algorithm designers can also benefit from it in informal reasoning, using abstract histories and commitment points instead of single linearizations and linearization points.

2 Linearizability, Abstract Histories and Commitment Points

Preliminaries. We consider a data structure that can be accessed concurrently via operations ${\sf op}\in{\sf Op}$ in several threads, identified by $t\in{\sf ThreadID}$. Each operation takes one argument and returns one value, both from a set ${\sf Val}$; we use a special value $\bot\in{\sf Val}$ to model operations that take no argument or return no value. Linearizability relates the observable behaviour of an implementation of such a concurrent data structure to its sequential specification [11]. We formalise both of these by sets of histories, which are partially ordered sets of events, recording operations invoked on the data structure. Formally, an event is of the form $e=[{i}\,{:}\,{(t,{\sf op},a,r)}]$. It includes a unique identifier $i\in{\sf EventID}$ and records an operation ${\sf op}\in{\sf Op}$ called by a thread $t\in{\sf ThreadID}$ with an argument $a\in{\sf Val}$, which returns a value $r\in{\sf Val}\uplus\{{\sf todo}\}$. We use the special return value ${\sf todo}$ for events describing operations that have not yet terminated, and call such events uncompleted. We denote the set of all events by ${\sf Event}$. Given a set $E\subseteq{\sf Event}$, we write $E(i)=(t,{\sf op},a,r)$ if $[{i}\,{:}\,{(t,{\sf op},a,r)}]\in E$ and let $\left\lfloor{E}\right\rfloor$ consist of all completed events from $E$. We let ${\sf id}({E})$ denote the set of all identifiers of events from $E$. Given an event identifier $i$, we also use ${E(i)}.{\sf tid}$, ${E(i)}.{\sf op}$, ${E(i)}.{\sf arg}$ and ${E(i)}.{\sf rval}$ to refer to the corresponding components of the tuple $E(i)$.

Definition 1

A *history111 For technical convenience, our notion of a history is different from the one in the classical linearizability definition [11], which uses separate events to denote the start and the end of an operation. We require that $R$ be an interval order, we ensure that our notion is consistent with an interpretation of events as segments of time during which the corresponding operations are executed, with $R$ ordering $i_{1}$ before $i_{2}$ if $i_{1}$ finishes before $i_{2}$ starts [5]. * is a pair $H=(E,R)$, where $E\subseteq{\sf Event}$ is a finite set of events with distinct identifiers and $R\subseteq{\sf id}({E})\times{\sf id}({E})$ is a strict partial order (i.e., transitive and irreflexive), called the real-time order. We require that for each $t\in{\sf ThreadID}$:

• •

events in $t$ are totally ordered by $R$:

$\forall i,j\in{\sf id}({E})\ldotp i\neq j\land{E(i)}.{\sf tid}={E(j)}.{\sf tid}=t\implies({i}\xrightarrow{R}{j}\lor{j}\xrightarrow{R}{i})$;

• •

only maximal events in $R$ can be uncompleted:

$\forall i\,{\in}\,{\sf id}({E})\ldotp\forall t\,{\in}\,{\sf ThreadID}\ldotp{E(i)}.{\sf rval}={\sf todo}\implies\neg\exists j\in{\sf id}({E})\ldotp{i}\xrightarrow{R}{j}$;

• •

$R$ is an interval order:

$\forall i_{1},i_{2},i_{3},i_{4}\ldotp{i_{1}}\xrightarrow{R}{i_{2}}\land{i_{3}}\xrightarrow{R}{i_{4}}\implies{i_{1}}\xrightarrow{R}{i_{4}}\lor{i_{2}}\xrightarrow{R}{i_{3}}$.

We let ${\sf History}$ be the set of all histories. A history $(E,R)$ is sequential, written ${\sf seq}(E,R)$, if ${\sf id}({E})=\left\lfloor{E}\right\rfloor$ and $R$ is total on $E$.

Informally, ${i}\xrightarrow{R}{j}$ means that the operation recorded by $E(i)$ completed before the one recorded by $E(j)$ started. The real-time order in histories produced by concurrent data structure implementations may be partial, since in this case the execution of operations may overlap in time; in contrast, specifications are defined using sequential histories, where the real-time order is total.

Linearizability. Assume we are given a set of histories that can be produced by a given data structure implementation (we introduce a programming language for implementations and formally define the set of histories an implementation produces in §5). Linearizability requires all of these histories to be matched by a similar history of the data structure specification (its linearization) that, in particular, preserves the real-time order between events in the following sense: the real-time order of a history $H=(E,R)$ is preserved in a history $H^{\prime}=(E^{\prime},R^{\prime})$, written ${H}\sqsubseteq{H^{\prime}}$, if $E=E^{\prime}$ and $R\subseteq R^{\prime}$.

The full definition of linearizability is slightly more complicated due to the need to handle uncompleted events: since operations they denote have not terminated, we do not know whether they have made a change to the data structure or not. To account for this, the definition makes all events in the implementation history complete by discarding some uncompleted events and completing the remaining ones with an arbitrary return value. Formally, an event $e=[{i}\,{:}\,{(t,{\sf op},a,r)}]$ can be completed to an event $e^{\prime}=[{i^{\prime}}\,{:}\,{(t^{\prime},{\sf op}^{\prime},a^{\prime},r^{\prime})}]$, written ${e}\unlhd{e^{\prime}}$, if $i=i^{\prime}$, $t=t^{\prime}$, ${\sf op}={\sf op}^{\prime}$, $a=a^{\prime}$ and either $r=r^{\prime}\neq{\sf todo}$ or $r^{\prime}={\sf todo}$. A history $H=(E,R)$ can be completed to a history $H^{\prime}=(E^{\prime},R^{\prime})$, written ${H}\unlhd{H^{\prime}}$, if ${\sf id}({E^{\prime}})\subseteq{\sf id}({E})$, $\left\lfloor{E}\right\rfloor\subseteq\left\lfloor{E^{\prime}}\right\rfloor$, $R\cap({\sf id}({E^{\prime}})\times{\sf id}({E^{\prime}}))=R^{\prime}$ and $\forall i\in{\sf id}({E^{\prime}})\ldotp{[{i}\,{:}\,{E(i)}]}\unlhd{[{i}\,{:}\,{E^{\prime}(i)}]}$.

Definition 2

A set of histories $\mathcal{H}_{1}$ (defining the data structure implementation) is linearized by a set of sequential histories $\mathcal{H}_{2}$ (defining its specification), written $\mathcal{H}_{1}\sqsubseteq\mathcal{H}_{2}$, if $\forall H_{1}\in\mathcal{H}_{1}.\,\exists H_{2}\in\mathcal{H}_{2}.\,\exists H^{\prime}_{1}.\,{H_{1}}\unlhd{H^{\prime}_{1}}\wedge{H^{\prime}_{1}}\sqsubseteq{H_{2}}$.

Let $\mathcal{H}_{\sf queue}$ be the set of sequential histories defining the behaviour of a queue with ${\sf Op}=\{{\rm Enq},{\rm Deq}\}$. Due to space constraints, we provide its formal definition in the extended version of this paper [14], but for example, [Enq(2); Enq(1); Enq(3); Deq():2] $\in\mathcal{H}_{\sf queue}$ and [Enq(1); Enq(2); Enq(3); Deq():2] $\not\in\mathcal{H}_{\sf queue}$.

Proof method. In general, a history of a data structure ($H_{1}$ in Definition 2) may have multiple linearizations ($H_{2}$) satisfying a given specification $\mathcal{H}$. In our proof method, we use this observation and construct a partially ordered history, an abstract history, all linearizations of which belong to $\mathcal{H}$.

Definition 3

A history $H$ is an abstract history of a specification given by the set of sequential histories $\mathcal{H}$ if $\{H^{\prime}\mid\lfloor H\rfloor\sqsubseteq H^{\prime}\land{\sf seq}(H^{\prime})\}\subseteq\mathcal{H}$, where $\left\lfloor{(E,R)}\right\rfloor=(\left\lfloor{E}\right\rfloor,R\cap({\sf id}({\left\lfloor{E}\right\rfloor})\times{\sf id}({\left\lfloor{E}\right\rfloor})))$. We denote this by ${\sf abs}(H,\mathcal{H})$.

We define the construction of an abstract history $H=(E,R)$ by instrumenting the data structure operations with auxiliary code that updates the history at certain commitment points during operation execution. There are three kinds of commitment points:

When an operation ${\sf op}$ with an argument $a$ starts executing in a thread $t$, we extend $E$ by a fresh event $[i:(t,{\sf op},a,{\sf todo})]$, which we order in $R$ after all events in $\left\lfloor{E}\right\rfloor$. 2. 2.

At any time, we can add more edges to $R$. 3. 3.

By the time an operation finishes, we have to assign its return value to its event in $E$.

Note that, unlike Definition 2, Definition 3 uses a particular way of completing an abstract history $H$, which just discards all uncompleted events using $\lfloor-\rfloor$. This does not limit generality because, when constructing an abstract history, we can complete an event (item 3) right after the corresponding operation makes a change to the data structure, without waiting for the operation to finish.

In §6 we formalise our proof method as a program logic and show that it indeed establishes linearizability. Before this, we demonstrate informally how the obligations of our proof method are discharged on an example.

3 Running Example: the Time-Stamped Queue

We use the TS queue [7] as our running example. Values in the queue are stored in per-thread single-producer (SP) multi-consumer pools, and we begin by describing this auxiliary data structure.

SP pools. SP pools have well-known linearizable implementations [7], so we simplify our presentation by using abstract pools with the atomic operations given in Figure 3. This does not limit generality: since linerarizability implies contextual refinement (§1),

properties proved using the abstract pools will stay valid for their linearizable implementations. In the figure and in the following we denote irrelevant expressions by $\_$.

The SP pool of a thread contains a sequence of triples $(p,v,\tau)$, each consisting of a unique identifier $p\in{\sf PoolID}$, a value $v\in{\sf Val}$ enqueued into the TS queue by the thread and the associated timestamp $\tau\in{\sf TS}$. The set of timestamps ${\sf TS}$ is partially ordered by $\mathrel{{}<_{\sf TS}{}}$, with a distinguished timestamp $\top$ that is greater than all others. We let ${\tt pool}$ be the set of states of an abstract SP pool. Initially all pools are empty. The operations on SP pools are as follows:

• •

insert(t,v) appends a value v to the back of the pool of thread t and associates it with the special timestamp $\top$; it returns an identifier for the added element.

• •

setTimestamp(t,p,$\tau$) sets to $\tau$ the timestamp of the element identified by p in the pool of thread t.

• •

getOldest(t) returns the identifier and timestamp of the value from the front of the pool of thread t, or $({\rm NULL},{\rm NULL})$ if the pool is empty.

• •

remove(t,p) tries to remove a value identified by p from the pool of thread t. Note this can fail if some other thread removes the value first.

Separating insert from setTimestamp and getOldest from remove in the SP pool interface reduces the atomicity granularity, and permits more efficient implementations.