Executions of a given program represent traces of shared memory accesses generated by the program. We only consider "partitioned" programs of the form τ∈TId cτ , where denotes parallel composition, and each ci is a sequential program. The set of executions associated with a

**Fig. 1.** An RA-consistent execution of a transactionfree variant of (IRIW+txs) in Sect. 1, with program outcome a = c = 1 and b = d = 0.

given program is then defined by induction over the structure of sequential programs. We do not define this construction formally as it depends on the syntax of the implementation programming language. Each execution of a program P has a particular program *outcome*, prescribing the final values of local variables in each thread (see example in Fig. 1).

In this initial stage, the execution outcomes are unrestricted in that there are no constraints on the rf and mo relations. These restrictions and thus the permitted outcomes of a program are determined by the set of *consistent* executions:

**Definition 2 (RA-consistency).** A program execution *G* is *RA-consistent*, written RA-consistent(*G*), if acyclic(hb*loc* ∪ mo∪rb) holds, where hb - (po∪rf)+ denotes the 'RA-happens-before' relation.

Among all executions of a given program P, only the *RA-consistent* ones define the allowed outcomes of P.

### **3.1 Software Transactional Memory in RA: Specification**

Our goal in this section is to develop a declarative framework that allows us to specify the behaviour of mixed-mode STM programs under weak isolation guarantees. Whilst the behaviour of transactional code is dictated by the particular isolation model considered (e.g. PSI), the behaviour of non-transactional code and its interaction with transactions is guided by the underlying memory model. As we build our STM in the RA fragment of C11, we assume the behaviour of non-transactional code to conform to the RA memory model. More concretely, we build our specification of a program P such that (i) in the absence of transactional code, the behaviour of P is as defined by the RA model; (ii) in the absence of non-transactional code, the behaviour of P is as defined by the PSI model.

**Definition 3 (Specification Executions).** Assume a finite set of *transaction identifiers* TXId. An *execution graph of an STM specification*, Γ, is a tuple of the form (*E*, po,rf, mo, T ) where:

We write T /st for the set of equivalence classes of T induced by st; [a] st for the equivalence class that contains a; and Tξ for the equivalence class of transaction ξ ∈ TXId: Tξ - a tx(a)=ξ . We write N T for non-transactional events: N T - *E* \ T . We often use "Γ." as a prefix to project the Γ components.

*Specification Consistency.* The consistency of specification graphs is modelspecific in that it is dictated by the guarantees provided by the underlying model. In the upcoming sections, we present two consistency definitions of PSI in terms of our specification graphs that lack cycles of certain shapes. In doing so, we often write rT for lifting a relation r ⊆ *E* × *E* to transaction classes: rT st; (r \ st);st. Analogously, we write rI to restrict r to the internal events of a transaction: r∩st.

*Comparison to Dependency Graphs.* Adya et al. proposed *dependency graphs* for declarative specification of transactional consistency models [5,7]. Dependency graphs are similar to our specification graphs in that they are constructed from a set of nodes and a set of edges (relations) capturing certain dependencies. However, unlike our specification graphs, the nodes in dependency graphs denote entire transactions and not individual events. In particular, Adya et al. propose three types of dependency edges: (i) a *read dependency* edge, T1 *WR* → T2, denotes that transaction T2 reads a value written by T1; (ii) a *write dependency* edge T1 *WW*→ T2 denotes that T2 overwrites a value written by T1; and (iii) an *anti-dependency* edge T1 *RW*→ T2 denotes that T2 overwrites a value read by T1. Adya's formalism does not allow for *non-transactional* accesses and it thus suffices to define the dependencies of an execution as edges between transactional classes. In our specification graphs however, we account for both transactional and non-transactional accesses and thus define our relational dependencies between individual events of an execution. However, when we need to relate an entire transaction to another with relation r, we use the transactional lift (rT) defined above. In particular, Adya's dependency edges correspond to ours as follows. Informally, the *WR* corresponds to our rfT; the *WW* corresponds to our moT; and the *RW* corresponds to our rbT. Adya's dependency graphs have been used to develop declarative specifications of the PSI consistency model [14]. In Sect. 4, we revisit this model, redefine it as specification graphs in our setting, and develop a reference lock-based implementation that is sound and complete with respect to this abstract specification. The model in [14] does not account for non-transactional accesses. To remedy this, later in Sect. 5, we develop a declarative specification of PSI that allows for both transactional and non-transactional accesses. We then develop a reference lock-based implementation that is sound and complete with respect to our proposed model.

### **4 Parallel Snapshot Isolation (PSI)**

We present a declarative specification of PSI (Sect. 4.1), and develop a lockbased reference implementation of PSI in the RA fragment (Sect. 4.2). We then demonstrate that our implementation is both sound (Sect. 4.3) and complete (Sect. 4.4) with respect to the PSI specification. Note that the PSI model in this section accounts for transactional code only; that is, throughout this section we assume that Γ.*E* = Γ.T . We lift this assumption later in Sect. 5.

#### **4.1 A Declarative Specification of PSI STMs in RA**

In order to formally characterise the weak behaviour and anomalies admitted by PSI, Cerone and Gotsman [14,15] formulated a declarative PSI specification. (In fact, they provide two equivalent specifications: one using dependency graphs proposed by Adya et al. [5,7]; and the other using abstract executions.) As is standard, they characterise the set of executions admitted under PSI as graphs that lack certain cycles. We present an equivalent declarative formulation of PSI, adapted to use our notation as discussed in Sect. 3. It is straightforward to verify that our definition coincides with the dependency graph specification in [15]. As with [14,15], throughout this section, we take PSI execution graphs to be those in which *E* = T ⊆ (R∪W) \ U. That is, the PSI model handles transactional code only, consisting solely of read and write events (excluding updates).

*PSI Consistency.* A PSI execution graph Γ=(*E*, po,rf, mo, T ) is *consistent*, written psi-consistent(Γ), if the following hold:

$$\begin{array}{l} \bullet \ \mathsf{r}\_{\mathrm{I}} \cup \mathsf{m} \mathsf{o}\_{\mathrm{I}} \cup \mathsf{r} \mathsf{b}\_{\mathrm{I}} \subseteq \mathsf{p} \\ \bullet \ \mathsf{ir} \mathsf{reflex} \mathsf{v} \text{is} \mathsf{e} \ (\mathsf{r}\_{\mathrm{DOT}} \mid \mathsf{r} \mathsf{f}\_{\mathrm{T}} \mid \mathsf{m} \mathsf{c}\_{\mathrm{T}})^{+} \cdot \mathsf{r} \mathsf{h}\_{\mathrm{T}} ? \end{array} \tag{\mathsf{INT}}$$

• irreflexive((poT ∪ rfT ∪ moT)+;rbT ?) (ext)

Informally, int ensures the consistency of each transaction internally, while ext provides the synchronisation guarantees among transactions. In particular, we note that the two conditions together ensure that if two read events in the same transaction read from the same location x, and no write to x is pobetween them, then they must read from the same write (known as 'internal read consistency').

Next, we provide an alternative formulation of PSI-consistency that is closer in form to RA-consistency. This formulation is the basis of our extension in Sect. 5 with non-transactional accesses.

**Lemma 1.** *A PSI execution graph* Γ = (*E*, po,rf, mo, T ) *is consistent if and only if* acyclic(psi-hb*loc* ∪ mo ∪ rb) *holds, where* psi-hb *denotes the* 'PSI-happensbefore' *relation, defined as* psi-hb -(po ∪ rf ∪ rfT ∪ moT)+*.*

*Proof. The full proof is provided in the technical appendix* [4]*.*

Note that this acyclicity condition is rather close to that of RA-consistency definition presented in Sect. 3, with the sole difference being the definition of 'happens-before' relation by replacing hb with psi-hb. The relation psi-hb is a strict extension of hb with rfT ∪ moT, which captures additional synchronisation guarantees resulting from transaction orderings, as described shortly. As in RA-consistency, the po and rf are included in the 'PSI-happens-before' relation psi-hb. Additionally, the rfT and moT also contribute to psi-hb.

Intuitively, the rfT corresponds to synchronisation due to causality between transactions. A transaction T1 is causally-ordered before transaction T2, if T1 writes to x and T2 later (in 'happens-before' order) reads x. The inclusion of rfT ensures that T2 cannot read from T1 without observing its entire effect. This in turn ensures that transactions exhibit an atomic 'all-or-nothing' behaviour. In particular, transactions cannot mix-and-match the values they read.

```
0. for (x ∈ WS) lock vx;
1. for (x ∈ RS) {
2. a := vx;
3. if (is-odd(a) && x ∈ WS) continue;
4. if (x ∈ WS) v[x]:= a;
5. s[x]:= x; }
6. for (x ∈ RS)
7. if (¬valid(x)) goto line 1;
8. -
   T;
9. for (x ∈ WS) unlock vx;
                                         lock vx -

                                            retry: v[x]:= vx;
                                                   if (is-odd(v[x]))
                                                     goto retry;
                                                   if (!CAS(vx,v[x],v[x]+1))
                                                     goto retry;
                                         unlock vx -
                                                     vx:= v[x]+ 2
                                             valid(x) -
                                                        vx == v[x]
                                         validRPSI(x) -
                                                        vx == v[x] && x == s[x]
                                                -
                                                a:= x -
                                                        a:= s[x]
                                                -
                                                x:= a -
                                                        x:=a; s[x]:= a
                                               -
                                                S1;S2 -
                                                        -
                                                          S1;-
                                                               S2
                                           while(e) S -
                                                        while(e) S
                                                ... and so on ...
```
**Fig. 2.** PSI implementation of transaction T given RS, WS; the RPSI implementation (Sect. 5) is obtained by replacing valid on line 7 with validRPSI.

For instance, if T1 writes to both x and y, transaction T2 may not read the value of x from T1 but read the value of y from an earlier (in 'happens-before' order) transaction T0.

The moT corresponds to synchronisation due to conflicts between transactions. Its inclusion enforces the write-conflict-freedom of PSI transactions. In other words, if two transactions T1 and T2 both write to the same location x via events w1 and w2 such that w1 mo → w2, then T1 must commit before T2, and thus the entire effect of T1 must be visible to T2.

### **4.2 A Lock-Based PSI Implementation in RA**

We present an operational model of PSI that is both sound and complete with respect to the declarative semantics in Sect. 4.1. To this end, in Fig. 2 we develop a pessimistic (lock-based) reference implementation of PSI using sequence locks [13,18,23,32], referred to as *version locks* in our implementation. In order to avoid taking a snapshot of the *entire* memory and thus decrease the locking overhead, we assume that a transaction T is supplied with its *read set*, RS, containing those locations that are read by T. Similarly, we assume T to be supplied with its *write set*, WS, containing the locations updated by T. 2

The implementation of T proceeds by exclusively acquiring the version locks on all locations in its write set (line 0). It then obtains a snapshot of the locations in its read set by inspecting their version locks, as described shortly, and subsequently recording their values in a thread-local array s (lines 1–7). Once a snapshot is recorded, the execution of T proceeds locally (via -T on line 8) as

2 A conservative estimate of RS and WS can be obtained by simple syntactic analysis.

follows. Each read operation consults the local snapshot in s; each write operation updates the memory eagerly (in-place) and subsequently updates its local snapshot to ensure correct lookup for future reads. Once the execution of T is concluded, the version locks on the write set are released (line 9). Observe that as the writer locks are acquired pessimistically, we do not need to check for write-conflicts in the implementation.

To facilitate our locking implementation, we assume that each location x is associated with a version lock at address x+1, written vx. The value held by a version lock vx may be in one of two categories: (i) an even number, denoting that the lock is free; or (ii) an odd number, denoting that the lock is exclusively held by a writer. For a transaction to write to a location x in its write set WS, the x version lock (vx) must be acquired exclusively by calling lock vx. Each call to lock vx reads the value of vx and stores it in v[x], where v is a thread-local array. It then checks if the value read is even (vx is free) and if so it atomically increments it by 1 (with a 'compare-and-swap' operation), thus changing the value of vx to an odd number and acquiring it exclusively; otherwise it repeats this process until the version lock is successfully acquired. Conversely, each call to unlock vx updates the value of vx to v[x]+2, restoring the value of vx to an even number and thus releasing it. Note that deadlocks can be avoided by imposing an ordering on locks and ensuring their in-order acquisition by all transactions. For simplicity however, we have elided this step as we are not concerned with progress or performance issues here and our main objective is a reference implementation of PSI in RA.

Analogously, for a transaction to read from the locations in its read set RS, it must record a snapshot of their values (lines 1–7). To obtain a snapshot of location x, the transaction must ensure that x is not currently being written to by another transaction. It thus proceeds by reading the value of vx and recording it in v[x]. If vx is free (the value read is even) or x is in its write set WS, the value of x can be freely read and tentatively stored in s[x]. In the latter case, the transaction has already acquired the exclusive lock on vx and is thus safe in the knowledge that no other transaction is currently updating x. Once a *tentative* snapshot of all locations is obtained (lines 1–5), the transaction must *validate* it by ensuring that it reflects the values of the read set at a single point in time (lines 6–7). To do this, it revisits the version locks, inspecting whether their values have changed (by checking them against v) since it recorded its snapshot. If so, then an intermediate update has intervened, potentially invalidating the obtained snapshot; the transaction thus restarts the snapshot process. Otherwise, the snapshot is successfully validated and returned in s.

#### **4.3 Implementation Soundness**

The PSI implementation in Fig. 2 is *sound*: for each RA-consistent implementation graph *G*, a corresponding specification graph Γ can be constructed such that psi-consistent(Γ) holds. In what follows we state our soundness theorem and briefly describe our construction of consistent specification graphs. We refer the reader to the technical appendix [4] for the full soundness proof.

**Theorem 1 (Soundness).** *For all RA-consistent implementation graphs G of the implementation in Fig. 2, there exists a PSI-consistent specification graph* Γ *of the corresponding transactional program that has the same program outcome.*

**Constructing Consistent Specification Graphs.** Observe that given an execution of our implementation with t transactions, the trace of each transaction i ∈ {1 ···t} is of the form θi = *Ls*i po → *FS*i po → *S*i po → *Ts*i po → *Us*i, where *Ls*i, *FS*i, *S*i, *Ts*i and *Us*i respectively denote the sequence of events acquiring the version locks, attempting but failing to obtain a valid snapshot, recording a valid snapshot, performing the transactional operations, and releasing the version locks. For each transactional trace θi of our implementation, we thus construct a corresponding trace of the specification as θ i = Bi po → *Ts* i po → Ei, where Bi and Ei denote the transaction begin and end events (lab(Bi)=B and lab(Ei)=E). When *Ts*i is of the form t1 po →··· po → tn, we construct *Ts* i as t 1 po →··· po → t n with each t j defined either as t j - R(x, v) when tj = R(s[x], v) (i.e. the corresponding implementation event is a read event); or as t j - W(x, v) when tj=W(x, v) po → W(s[x], v).

For each specification trace θ i we construct the 'reads-from' relation as:

$$\mathsf{RF}\_{i} \triangleq \left\{ (w, t\_{j}^{\prime}) \middle| \begin{array}{l} \left| t\_{j}^{\prime} \in Ts\_{i}^{\prime} \land \exists \mathbf{x}, v \text{ } t\_{j}^{\prime} = \mathsf{R}(\mathbf{x}, v) \land w = \mathsf{W}(\mathbf{x}, v) \\ \land (w \in Ts\_{i}^{\prime} \Rightarrow w \stackrel{\mathsf{pos}}{\to} t\_{j}^{\prime} \land \\ \qquad \qquad \qquad \qquad \qquad \langle \forall e \in Ts\_{i}^{\prime} \colon w \stackrel{\mathsf{pos}}{\to} t\_{j}^{\prime} \Rightarrow (\mathsf{1oc}(e) \neq \mathsf{x} \lor e \notin \mathcal{W}) \rangle) \\ \land (w \notin Ts\_{i}^{\prime} \Rightarrow \langle \forall e \in Ts\_{i}^{\prime} \colon e \stackrel{\mathsf{pos}}{\to} t\_{j}^{\prime} \Rightarrow (\mathsf{1oc}(e) \neq \mathsf{x} \lor e \notin \mathcal{W}) \rangle) \\ \qquad \qquad \qquad \land \exists r' \in S\_{i} \colon \mathsf{Loc}(r') = \mathsf{x} \land (w, r') \in G. \mathrm{rf} \end{array} \right\} $$

That is, we construct our graph such that each read event t j from location x in *Ts* i either (i) is preceded by a write event w to x in *Ts* i without an intermediate write in between them and thus 'reads-from' w (lines two and three); or (ii) is not preceded by a write event in *Ts* i and thus 'reads-from' the write event w from which the initial snapshot read r in Si obtained the value of x (last two lines).

Given a consistent implementation graph *G* = (*E*, po,rf, mo), we construct a consistent specification graph Γ = (*E*, po,rf, mo, T ) such that:

#### **4.4 Implementation Completeness**

The PSI implementation in Fig. 2 is *complete*: for each consistent specification graph Γ a corresponding implementation graph *G* can be constructed such that RA-consistent(*G*) holds. We next state our completeness theorem and describe our construction of consistent implementation graphs. We refer the reader to the technical appendix [4] for the full completeness proof.

**Theorem 2 (Completeness).** *For all PSI-consistent specification graphs* Γ *of a transactional program, there exists an RA-consistent execution graph G of the implementation in Fig. 2 that has the same program outcome.*

**Constructing Consistent Implementation Graphs.** In order to construct an execution graph of the implementation *G* from the specification Γ, we follow similar steps as those in the soundness construction, in reverse order. More concretely, given each trace θ i of the specification, we construct an analogous trace of the implementation by inserting the appropriate events for acquiring and inspecting the version locks, as well as obtaining a snapshot. For each transaction class Ti ∈ T /st, we must first determine its read and write sets and subsequently decide the order in which the version locks are acquired (for locations in the write set) and inspected (for locations in the read set). This then enables us to construct the 'reads-from' and 'modification-order' relations for the events associated with version locks.

Given a consistent execution graph of the specification Γ = (*E*, po,rf, mo, T ), and a transaction class Ti ∈ Γ.T /st, we write WST*i* for the set of locations written to by Ti. That is, WST*i* - e∈T*i*∩W loc(e). Similarly, we write RST*i* for the set of locations read from by Ti, *prior to* being written to by Ti. For each location x read from by Ti, we additionally record the first read event in Ti that retrieved the value of x. That is,

$$\mathsf{RS}\_{\mathcal{T}\_i} \stackrel{\Delta}{=} \left\{ (\mathbf{x}, r) \, \Big|\, r \in \mathcal{T}\_i \cap \mathcal{R}\_{\mathbf{x}} \land \neg \exists e \in \mathcal{T}\_i \cap E\_{\mathbf{x}} \colon e \stackrel{\rm po}{\to} r \right\}$$

Note that transaction Ti may contain several read events reading from x, prior to subsequently updating it. However, the internal-read-consistency property ensures that all such read events read from the same write event. As such, as part of the read set of Ti we record the first such read event (in program-order).

Determining the ordering of lock events hinges on the following observation. Given a consistent execution graph of the specification Γ = (*E*, po,rf, mo, T ), let for each location x the total order mo be given as: w1 mo|imm → ··· mo|imm → wnx . Observe that this order can be broken into adjacent segments where the events of each segment belong to the *same* transaction. That is, given the transaction classes Γ.T /st, the order above is of the following form where T1, ··· , Tm ∈ Γ.T /st and for each such Ti we have x ∈ WST*i* and w(i,1) ··· w(i,n*i*) ∈ Ti:

$$\underbrace{w\_{\{1,1\}} \stackrel{m\diamondsuit\_{\text{lim}}}{\to} \cdots \stackrel{m\diamondsuit\_{\text{lim}}}{\to} w\_{\{1,n\_1\}}}\_{T\_1} \stackrel{m\diamondsuit\_{\text{lim}}}{\to} \cdots \stackrel{m\diamondsuit\_{\text{lim}}}{\to} \underbrace{w\_{\{m,1\}} \stackrel{m\diamondsuit\_{\text{lim}}}{\to} \cdots \stackrel{m\diamondsuit\_{\text{lim}}}{\to} w\_{\{m,n\_m\}}}\_{T\_m}$$

Were this not the case and we had w1 mo → w mo → w2 such that w1, w2 ∈ Ti and w ∈ Tj = Ti, we would consequently have w1 mo →T w mo →T w1, contradicting the assumption that Γ is consistent. Given the above order, let us then define Γ.MOx = [T1 ···Tm]. We write Γ.MOx| i for the ith item of Γ.MOx. As we describe shortly, we use Γ.MOx to determine the order of lock events.

Note that the execution trace for each transaction Ti ∈ Γ.T /st is of the form θ i = *B*i po → *Ts* i po → *E*i, where *B*i is a transaction-begin (B) event, *E*i is a transaction-end (E) event, and *Ts* i = *t* 1 po →··· po → *t* n for some n, where each *t* j is either a read or a write event. As such, we have Γ.*E* = Γ.T = T*i*∈Γ.T /st Ti = θ i.*E*.

For each trace θ i of the specification, we construct a corresponding trace of our implementation θi as follows. Let RST*i* = {(x1, r1)···(xp, rp)} and WST*i* = {y1 ··· yq}. We then construct θi = *Ls*i po → *S*i po → *Ts*i po → *Us*i, where

• *Ls*i = *L*y1 i po →··· po → *L* y*q* i and *Us*i = *U* y1 i po →··· po → *U* y*q* i denote the sequence of events acquiring and releasing the version locks, respectively. Each *L* y*j* i and *U* y*j* i are defined as follows, the first event Ly1 i has the same identifier as that of Bi, the last event Uy*q* i has the same identifier as that of Ei, and the identifiers of the remaining events are picked fresh:

$$L\_i^{\mathbf{y}\_j} = \mathbb{U}(\mathbf{v}\mathbf{y}\_j, 2a, 2a+1) \quad U\_i^{\mathbf{y}\_j} = \mathbb{W}(\mathbf{v}\mathbf{y}\_j, 2a+2) \quad \text{where} \quad \mathsf{MO}\_{\mathbf{y}\_j}\Big|\_a = \mathcal{T}\_i$$

We then define the mo relation for version locks such that if transaction Ti writes to y immediately after Tj (i.e. Ti is MOy-ordered immediately after Tj ), then Ti acquires the vy version lock immediately after Tj has released it. On the other hand, if Ti is the first transaction to write to y, then it acquires vy immediately after the event initialising the value of vy, written *init* vy. Moreover, each vy release event of Ti is mo-ordered immediately after the corresponding vy acquisition event in Ti:

$$\mathsf{IMO}\_{i} \triangleq \bigcup\_{\mathbf{y} \in \mathsf{W}\mathbf{S}\_{T\_{i}}} \left\{ \begin{matrix} (L\_{i}^{\mathsf{T}}, U\_{i}^{\mathsf{T}}), \\ (w, L\_{i}^{\mathsf{T}}) \end{matrix} \middle| \begin{matrix} (\varGamma.\mathsf{MO}\_{\mathbf{x}})\_{0} = T\_{i} \Rightarrow w = \mathit{init}\_{\mathsf{vy}}) \wedge \\ (\exists T\_{j}, a > 0. \ \Gamma.\mathsf{MO}\_{\mathbf{y}}\big|\_{a} = T\_{i} \land \Gamma.\mathsf{MO}\_{\mathbf{y}}\big|\_{a-1} = T\_{j} \end{matrix} \right\}$$

This partial mo order on lock events of Ti also determines the rf relation for its lock acquisition events: IRF1 i - y∈WS*Ti* (w, Ly i ) (w, Ly i ) ∈ IMOi .

• *S*i = *tr* x1 i po → ··· po → *tr* x*p* i po → *vr* x1 i po → ··· po → *vr* x*p* i denotes the sequence of events obtaining a tentative snapshot (*tr* x*j* i ) and subsequently validating it (*vr* x*j* i ). Each *tr* x*j* i sequence is defined as *ir* x*j* i po → r x*j* i po → s x*j* i (reading the version lock vxj , reading xj and recoding it in s), with *ir* x*j* i , r x*j* i , s x*j* i and *vr* x*j* i events defined as follows (with fresh identifiers). We then define the rf relation for each of these read events in Si. For each (x, r) ∈ RST*i* , when r (i.e. the read event in the specification class Ti that reads the value of x) reads from an event w in the specification graph ((w, r) ∈ Γ.rf), we add (w, rx i ) to the rf relation of *G* (the first line of IRF2 i below). For version locks, if transaction Ti also writes to xj , then *ir* x*j* i and *vr* x*j* i events (reading and validating the value of version lock vxj ), read from the lock event in Ti that acquired vxj , namely Lx*j* i . On the other hand, if transaction Ti does not write to xj and it reads the value of xj written by Tj , then *ir* x*j* i and *vr* x*j* i read the value written to vxj by Tj when releasing it (*U* x j ). Lastly, if Ti does not write to xj and it reads the value of xj written by the initial write, *init* x, then *ir* x*j* i and *vr* x*j* i read the value written to vxj by the initial write to vx, *init* vx.

IRF2 i - (x,r)∈RS*Ti* ⎧ ⎪⎪⎨ ⎪⎪⎩ (w, rx i ), (w , *ir* x i ), (w , *vr* x i ) (w, r) ∈ Γ.rf ∧(x ∈ WST*i* ⇒ w =Lx i ) ∧(x ∈ WST*i* ∧ ∃Tj . w ∈ Tj ⇒ w =Ux j ) ∧(x ∈ WST*i* ∧ w=*init* x ⇒ w =*init* vx) ⎫ ⎪⎪⎬ ⎪⎪⎭ r x*j* i =R(xj , v) s x*j* i =W(s[xj], v) s.t. ∃w. (w, rx*j* i ) ∈ IRF2 i ∧ valw(w)=v *ir* x*j* i =*vr* x*j* i =R(vxj , v) s.t. ∃w. (w, *ir* x*j* i ) ∈ IRF2 i ∧ valw(w)=v

• *Ts*i = *t*1 po → ··· po → *t*n (when *Ts* i = *t* 1 po → ··· po → *t* n), with *t*j defined as follows:

$$\begin{aligned} t\_j &= \mathsf{R}(\mathbf{s}\u{\mathsf{L}x}), v) \text{ when } t'\_j = \mathsf{R}(\mathbf{x}, v) \\ t\_j &= \mathsf{W}(\mathbf{x}, v) \stackrel{\mathsf{po}|\_{\text{lim}}}{\to} \mathsf{W}(\mathbf{s}\u{\mathsf{L}x}), v) \text{ when } t'\_j = \mathsf{W}(\mathbf{x}, v) \end{aligned}$$

When *t* j is a read event, the *t*j has the same identifier as that of *t* j . When *t* j is a write event, the first event in *t*j has the same identifier as that of *t*j and the identifier of the second event is picked fresh.

We are now in a position to construct our implementation graph. Given a consistent execution graph Γ of the specification, we construct an execution graph *G* = (*E*, po,rf, mo) of the implementation as follows.

### **5 Robust Parallel Snapshot Isolation (RPSI)**

In the previous section we adapted the PSI semantics in [14] to STM settings, in the *absence* of non-transactional code. However, a reasonable STM should account for mixed-mode code where shared data is accessed by both transactional and non-transactional code. To remedy this, we explore the semantics of PSI STMs in the presence of non-transactional code with *weak isolation* guarantees (see Sect. 2.1). We refer to the weakly isolated behaviour of such PSI STMs as *robust parallel snapshot isolation* (RPSI), due to its ability to provide PSI guarantees between transactions even in the presence of non-transactional code.

**Fig. 3.** RPSI-inconsistent executions due to nt-rf (a); and t-rf (b)

In Sect. 5.1 we propose the first declarative specification of RPSI STM programs. Later in Sect. 5.2 we develop a lock-based reference implementation of our RPSI specification in the RA fragment. We then demonstrate that our implementation is both sound (Sect. 5.3) and complete (Sect. 5.4) with respect to our proposed specification.

### **5.1 A Declarative Specification of RPSI STMs in RA**

We formulate a declarative specification of RPSI semantics by adapting the PSI semantics presented in Sect. 4.1 to account for non-transactional accesses. As with the PSI specification in Sect. 4.1, throughout this section, we take RPSI execution graphs to be those in which T ⊆ (R∪W) \ U. That is, RPSI transactions consist solely of read and write events (excluding updates). As before, we characterise the set of executions admitted by RPSI as graphs that lack cycles of certain shapes. More concretely, as with the PSI specification, we consider an RPSI execution graph to be *consistent* if acyclic(rpsi-hb*loc* ∪ mo ∪ rb) holds, where rpsi-hb denotes the *'RPSI-happens-before'* relation, extended from that of PSI psi-hb.

**Definition 4 (RPSI consistency).** An RPSI execution graph Γ = (*E*, po, rf, , mo, T ) is consistent, written rpsi-consistent(Γ), if acyclic(rpsi-hb*loc* ∪ mo∪rb) holds, where rpsi-hb denotes the *'RPSI-happens-before'* relation, defined as the smallest relation that satisfies the following conditions:

The trans and psi-hb ensure that rpsi-hb is transitive and that it includes po, rf and moT as with its PSI counterpart. The nt-rf ensures that if a value written by a non-transactional write w is observed (read from) by a read event r in a transaction T, then its effect is observed by *all* events in T. That is, the w *happens-before* all events in T and not just r. This allows us to rule out executions such as the one depicted in Fig. 3a, which we argue must be disallowed by RPSI.

Consider the execution graph of Fig. 3a, where transaction T1 is denoted by the dashed box labelled T1, comprising the read events r1 and r2. Note that as r1 and r2 are transactional reads without prior writes by the transaction, they constitute a *snapshot* of the memory at the time T1 started. That is, the values read by r1 and r2 must reflect a valid snapshot of the memory at the time it was taken. As such, since we have (w2, r2) ∈ rf, any event preceding w2 by the 'happens-before' relation must also be observed by (synchronise with) T1. In particular, as w1 happens-before w2 ((w1, w2) ∈ po), the w1 write must also be observed by T1. The nt-rf thus ensures that a non-transactional write read from by a transaction (i.e. a snapshot read) synchronises with the entire transaction.

Recall from Sect. 4.1 that the PSI psi-hb relation includes rfT which has not yet been included in rpsi-hb through the first three conditions described. As we describe shortly, the t-rf is indeed a strengthening of rfT to account for the presence of non-transactional events. In particular, note that rfT is included in the left-hand side of t-rf: when rpsi-hb in ([W];st; (rpsi-hb \ st);st; [R]) is replaced with rf ⊆ rpsi-hb, the left-hand side yields rfT. As such, in the absence of non-transactional events, the definitions of psi-hb and rpsi-hb coincide.

Recall that inclusion of rfT in psi-hb ensured transactional synchronisation due to causal ordering: if T1 writes to x and T2 later (in psi-hb order) reads x, then T1 must synchronise with T2. This was achieved in PSI because either (i) T2 reads x directly from T1 in which case T1 synchronises with T2 via rfT; or (ii) T2 reads x from another later (mo-ordered) transactional write in T3, in which case T1 synchronises with T3 via moT, T3 synchronises with T2 via rfT, and thus T1 synchronises with T2 via moT;rfT. How are we then to extend rpsi-hb to guarantee transactional synchronisation due to causal ordering in the presence of non-transactional events?

To justify t-rf, we present an execution graph that does not guarantee synchronisation between causally ordered transactions and is nonetheless deemed RPSI-consistent *without* the t-rf condition on rpsi-hb. We thus argue that this execution must be precluded by RPSI, justifying the need for t-rf. Consider the execution in Fig. 3b. Observe that as transaction T1 writes to x via w1, transaction T2 reads x via r2, and (w1, r2) ∈ rpsi-hb (w1 rf → r1 po → w3 rf → r2), T1 is causally ordered before T2 and hence T1 must synchronise with T2. As such, the r3 in T2 must observe w2 in T1: we must have (w2, r3) ∈ rpsi-hb, rendering the above execution RPSI-inconsistent. To enforce the rpsi-hb relation between such causally ordered transactions with intermediate non-transactional events, t-rf stipulates that if a transaction T1 writes to a location (e.g. x via w1 above), another transaction T2 reads from the same location (r2), and the two events are related by 'RPSI-happens-before' ((w1, r2) ∈ rpsi-hb), then T1 must synchronise with T2. That is, all events in T1 must 'RPSI-happen-before' those in T2. Effectively, this allows us to transitively close the causal ordering between transactions, spanning transactional and non-transactional events in between.

**Fig. 4.** A mixed-mode program with its annotated behaviour disallowed by RPSI (left); an RA-consistent execution graph of its RPSI implementation (right)

#### **5.2 A Lock-Based RPSI Implementation in RA**

We present a lock-based reference implementation of RPSI in the RA fragment (Fig. 2) by using sequence locks [13,18,23,32]. Our implementation is both sound and complete with respect to our declarative RPSI specification in Sect. 5.1.

The RPSI implementation in Fig. 2 is rather similar to its PSI counterpart. The main difference between the two is in how they *validate* the tentative snapshot recorded in s. As before, in order to ensure that no intermediate *transactional* writes have intervened since s was recorded, for each location x in RS, the validation phase revisits vx, inspecting whether its value has changed from that recorded in v[x]. If this is the case, the snapshot is deemed invalid and the process is restarted. However, checking against intermediate transactional writes alone is not sufficient as it does not preclude the intervention of *non-transactional* writes. This is because unlike transactional writes, non-transactional writes do not update the version locks and as such their updates may go unnoticed. In order to rule out the possibility of intermediate non-transactional writes, for each location x the implementation checks the value of x against that recorded in s[x]. If the values do not agree, an intermediate non-transactional write has been detected: the snapshot fails validation and the process is restarted. Otherwise, the snapshot is successfully validated and returned in s. Observe that checking the value of x against s[x] does not entirely preclude the presence of non-transactional writes, in cases where the same value is written (nontransactionally) to x twice.

To understand this, consider the mixed-mode program on the left of Fig. 4 comprising a transaction in the left-hand thread and a non-transactional program in the right-hand thread writing the same value (1) to z twice. Note that the annotated behaviour is disallowed under RPSI: all execution graphs of the program with the annotated behaviour yield RPSI-inconsistent execution graphs. Intuitively, this is because the values read by the transaction (x : 0, y : 0, z : 1) do not constitute a valid *snapshot*: at *no* point during the execution of this program, are the values of x, y and z as annotated.

Nevertheless, it is possible to find an RA-consistent execution of the RPSI implementation in Fig. 2 that reads the annotated values as its snapshot. Consider the execution graph on the right-hand side of Fig. 4, depicting a particular execution of the RPSI implementation (Fig. 2) of the program on the left. The rx, ry and rz denote the events reading the initial snapshot of x, y and z and recording them in s (line 5), respectively. Similarly, the rx , ry and rz denote the events validating the snapshots recorded in s (line 7). As T is the only transaction in the program, the version numbers vx, vy and vz remain unchanged throughout the execution and we have thus omitted the events reading (line 2) and validating (line 7) their values from the execution graph. Note that this execution graph is RA-consistent even though we cannot find a corresponding RPSI-consistent execution with the same outcome. To ensure the soundness of our implementation, we must thus rule out such scenarios.

To do this, we assume that if multiple non-transactional writes write the same value to the same location, they cannot race with the same transaction. More concretely, we assume that *every* RPSI-consistent execution graph of a given program satisfies the following condition:

$$\begin{array}{l} \mathsf{Vx. } \forall r \in \mathcal{T} \cap \mathcal{R}\_{\texttt{x.}} \,\forall w, w' \in \mathcal{N}\mathcal{T} \cap \mathcal{W}\_{\texttt{x.}}\\\ w \neq w' \land \texttt{val}\_{\texttt{v}}(w) = \texttt{val}\_{\texttt{v}}(w') \land (r, w) \notin \texttt{rpsi-hb} \land (r, w') \notin \texttt{rpsi-hb} \\\ \Rightarrow (w, r) \in \texttt{rpsi-hb} \land (w', r) \in \texttt{rpsi-hb} \end{array} \qquad (\*)$$

That is, given a transactional read r from location x, and any two distinct non-transactional writes w, w of the same value to x, either (i) at least one of the writes RPSI-happen-after r; or (ii) they both RPSI-happen-before r.

Observe that this does not hold of the program in Fig. 2. Note that this stipulation does not prevent two *transactions* to write the same value to a location x. As such, in the absence of non-transactional writes, our RPSI implementation is equivalent to that of PSI in Sect. 4.2.

#### **5.3 Implementation Soundness**

The RPSI implementation in Fig. 2 is *sound*: for each consistent implementation graph *G*, a corresponding specification graph Γ can be constructed such that rpsi-consistent(Γ) holds. In what follows we state our soundness theorem and briefly describe our construction of consistent specification graphs. We refer the reader to the technical appendix [4] for the full soundness proof.

**Theorem 3 (Soundness).** *Let* P *be a program that possibly mixes transactional and non-transactional code. If every RPSI-consistent execution graph of* P *satisfies the condition in* (∗)*, then for all RA-consistent implementation graphs G of the implementation in Fig. 2, there exists an RPSI-consistent specification graph* Γ *of the corresponding transactional program with the same program outcome.*

**Constructing Consistent Specification Graphs.** Constructing an RPSIconsistent specification graph from the implementation graph is similar to the corresponding PSI construction described in Sect. 4.3. More concretely, the events associated with non-transactional events remain unchanged and are simply added to the specification graph. On the other hand, the events associated with transactional events are adapted in a similar way to those of PSI in Sect. 4.3. In particular, observe that given an execution of the RPSI implementation with t transactions, as with the PSI implementation, the trace of each transaction i ∈ {1 ···t} is of the form θi = *Ls*i po → *FS*i po → *S*i po → *Ts*i po → *Us*i, with *Ls*i, *FS*i, *S*i, *Ts*i and *Us*i denoting analogous sequences of events to those of PSI. The difference between an RPSI trace θi and a PSI one is in the *FS*i and *S*i sequences, obtaining the snapshot. In particular, the validation phases of *FS*i and *S*i in RPSI include an additional read for each location to rule out intermediate nontransactional writes. As in the PSI construction, for each transactional trace θi of our implementation, we construct a corresponding trace of the specification as θ i = Bi po → *Ts* i po → Ei, with Bi, Ei and *Ts* i as defined in Sect. 4.3.

Given a consistent RPSI implementation graph *G* = (*E*, po,rf, mo), let *G*.N T - *G*.*E* \ i∈{1···t} θ.*E* denote the non-transactional events of *G*. We construct a consistent RPSI specification graph Γ = (*E*, po,rf, mo, T ) such that:

We refer the reader to the technical appendix [4] for the full proof demonstrating that the above construction of Γ yields a consistent specification graph.

### **5.4 Implementation Completeness**

The RPSI implementation in Fig. 2 is *complete*: for each consistent specification graph Γ a corresponding implementation graph *G* can be constructed such that RA-consistent(*G*) holds. We next state our completeness theorem and describe our construction of consistent implementation graphs. We refer the reader to the technical appendix [4] for the full completeness proof.

**Theorem 4 (Completeness).** *For all RPSI-consistent specification graphs* Γ *of a program, there exists an RA-consistent execution graph G of the implementation in Fig. 2 that has the same program outcome.*

**Constructing Consistent Implementation Graphs.** In order to construct an execution graph of the implementation *G* from the specification Γ, we follow similar steps as those in the corresponding PSI construction in Sect. 4.4. More concretely, the events associated with non-transactional events are unchanged and simply added to the implementation graph. For transactional events, given each trace θ i of a transaction in the specification, as before we construct an analogous trace of the implementation by inserting the appropriate events for acquiring and inspecting the version locks, as well as obtaining a snapshot. For each transaction class Ti ∈ T /st, we first determine its read and write sets as before and subsequently decide the order in which the version locks are acquired and inspected. This then enables us to construct the 'reads-from' and 'modificationorder' relations for the events associated with version locks.

Given a consistent execution graph of the specification Γ = (*E*, po,rf, mo, T ), and a transaction class Ti ∈ Γ.T /st, we define WST*i* and RST*i* as described in Sect. 4.4. Determining the ordering of lock events hinges on a similar observation as that in the PSI construction. Given a consistent execution graph of the specification Γ = (*E*, po,rf, mo, T ), let for each location x the total order mo be given as: w1 mo|imm → ··· mo|imm → wnx . This order can be broken into adjacent segments where the events of each segment are *either* non-transactional writes *or* belong to the *same* transaction. That is, given the transaction classes Γ.T /st, the order above is of the following form where T1, ··· , Tm ∈ Γ.T /st and for each such Ti we have x ∈ WST*i* and w(i,1) ··· w(i,n*i*) ∈ Ti:

$$\underbrace{w\_{\{1,1\}} \stackrel{mo|\_{\text{imm}}}{\stackrel{mo|\_{\text{imm}}}} \cdots \stackrel{mo|\_{\text{imm}}}{\stackrel{mo|\_{\text{imm}}}} w\_{\{1,n\_1\}} \stackrel{mo|\_{\text{imm}}}{\stackrel{mo|\_{\text{imm}}}} \cdots \stackrel{mo|\_{\text{imm}}}{\stackrel{mo|\_{\text{imm}}}} \underbrace{w\_{\{m,1\}} \stackrel{mo|\_{\text{imm}}}{\stackrel{mo|\_{\text{imm}}}} \cdots \stackrel{mo|\_{\text{imm}}}{\stackrel{mo|\_{\text{imm}}}} w\_{\{m,n\_m\}}$$

Were this not the case and we had w1 mo → w mo → w2 such that w1, w2 ∈ Ti and w ∈ Tj = Ti, we would consequently have w1 mo →T w mo →T w1, contradicting the assumption that Γ is consistent. We thus define Γ.MOx = [T1 ···Tm].

Note that each transactional execution trace of the specification is of the form θ i = *B*i po → *Ts* i po → *E*i, with *B*i, *E*i and *Ts* i as described in Sect. 4.4. For each such θ i, we construct a corresponding trace of our implementation as θi = *Ls*i po → *S*i po → *Ts*i po → *Us*i, where *Ls*i, *Ts*i and *Us*i are as defined in Sect. 4.4, and *S*i = *tr* x1 i po →··· po → *tr* x*p* i po → *vr* x1 i po →··· po → *vr* x*p* i denotes the sequence of events obtaining a tentative snapshot (*tr* x*j* i ) and subsequently validating it (*vr* x*j* i ). Each *tr* x*j* i sequence is of the form *ivr* x*j* i po → *ir* x*j* i po → s x*j* i , with *ivr* x*j* i , *ir* x*j* i and s x*j* i defined below (with fresh identifiers). Similarly, each *vr* x*j* i sequence is of the form *fr* x*j* i po → *fvr* x*j* i , with *fr* x*j* i and *fvr* x*j* i defined as follows (with fresh identifiers). We then define the rf relation for each of these read events in Si in a similar way.

For each (x, r) ∈ RST*i* , when r (the event in the specification class Ti that reads the value of x) reads from w in the specification graph ((w, r) ∈ Γ.rf), we add (w, *ir* x i ) and (w, *fr* x i ) to the rf of *G* (the first line of IRF2 i below). For version locks, as before if transaction Ti also writes to xj , then *ivr* x*j* i and *fvr* x*j* i events (reading and validating vxj ), read from the lock event in Ti that acquired vxj , namely Lx*j* i . Similarly, if Ti does not write to xj and it reads the value of xj

written by the initial write, *init* x, then *ivr* x*j* i and *fvr* x*j* i read the value written to vxj by the initial write to vx, *init* vx. Lastly, if transaction Ti does not write to xj and it reads xj from a write other than *init* x, then *ir* x*j* i and *vr* x*j* i read from the unlock event of a transaction Tj (i.e. Ux j ), who has x in its write set and whose write to x, wx, maximally 'RPSI-happens-before' r. That is, for all other such writes that 'RPSI-happen-before' r, then wx 'RPSI-happens-after' them.

IRF2 *i* - - (x*,r*)∈RS*Ti* ⎧ ⎪⎪⎪⎪⎪⎨ ⎪⎪⎪⎪⎪⎩ (w, *ir* x *i* ), (w, *fr* x *i* ), (w , *ivr* x *i* ), (w , *fvr* x *i* ) (w, r) ∈ Γ.rf ∧ (x ∈ WST*i* ⇒ w =Lx *i* ) ∧(x ∈ WST*i* ∧ w=*init* x ⇒ w =*init* vx) ∧(x ∈ WST*i* ∧ w=*init* x ⇒ ∃wx, T*j* . wx ∈ T*j* ∩ Wx ∧ wx rpsi-hb → r ∧ w =Ux *j* ∧[∀w x, T*k*. w x∈T*k* ∩ Wx ∧ w x rpsi-hb → r ⇒ w x rpsi-hb → wx]) ⎫ ⎪⎪⎪⎪⎪⎬ ⎪⎪⎪⎪⎪⎭ *ir* x*j i* =*fr* x*j i* =R(x*j* ,v) s x*j i* =W(s[x*j*],v) s.t. ∃w. (w, *ir* x*j i* ) ∈ IRF2 *i* ∧ valw(w)=v *ivr* x*j i* =*fvr* x*j i* =R(vx*j* , v) s.t. ∃w. (w, *ivr* x*j i* ) ∈ IRF2 *i* ∧ valw(w)=v

We are now in a position to construct our implementation graph. Given a consistent execution graph Γ of the specification, we construct an execution graph of the implementation, *G* = (*E*, po,rf, mo), such that:

$$\bullet \text{ } G.\text{mo} = \Gamma.\text{mo} \cup \left( \bigcup\_{T\_i \in \Gamma.T\_i/\text{st}} \mathsf{l}\mathsf{MO}\_i \right)^+, \text{ with } \mathsf{l}\mathsf{MO}\_i \text{ as defined in Sect. 4.4.}$$

### **6 Conclusions and Future Work**

We studied PSI, for the first time to our knowledge, as a consistency model for STMs as it has several advantages over other consistency models, thanks to its performance and monotonic behaviour. We addressed two significant drawbacks of PSI which prevent its widespread adoption. First, the absence of a simple lock-based reference implementation to allow the programmers to readily understand and reason about PSI programs. To address this, we developed a lock-based reference implementation of PSI in the RA fragment of C11 (using sequence locks), that is both sound and complete with respect to its declarative specification. Second, the absence of a formal PSI model in the presence of mixed-mode accesses. To this end, we formulated a declarative specification of RPSI (robust PSI) accounting for both transactional and non-transactional accesses. Our RPSI specification is an extension of PSI in that in the absence of non-transactional accesses it coincides with PSI. To provide a more intuitive account of RPSI, we developed a simple lock-based RPSI reference implementation by adjusting our PSI implementation. We established the soundness and completeness of our RPSI implementation against its declarative specification.

As directions of future work, we plan to build on top of the work presented here in three ways. First, we plan to explore possible lock-based reference implementations for PSI and RPSI in the context of other weak memory models, such as the full C11 memory models [9]. Second, we plan to study other weak transactional consistency models, such as SI [10], ALA (asymmetric lock atomicity), ELA (encounter-time lock atomicity) [28], and those of ANSI SQL, including RU (read-uncommitted), RC (read-committed) and RR (repeatable reads), in the STM context. We aim to investigate possible lock-based reference implementations for these models that would allow the programmers to understand and reason about STM programs with such weak guarantees. Third, taking advantage of the operational models provided by our simple lock-based reference implementations (those presented in this article as well as those in future work), we plan to develop reasoning techniques that would allow us to verify properties of STM programs. This can be achieved by either extending existing program logics for weak memory, or developing new program logics for currently unsupported models. In particular, we can reason about the PSI models presented here by developing custom proof rules in the existing program logics for RA such as [22,39].

**Acknowledgments.** We thank the ESOP 2018 reviewers for their constructive feedback. This research was supported in part by a European Research Council (ERC) Consolidator Grant for the project "RustBelt", under the European Union's Horizon 2020 Framework Programme (grant agreement no. 683289). The second author was additionally partly supported by Len Blavatnik and the Blavatnik Family foundation.

### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

### Eventual Consistency for CRDTs

Radha Jagadeesan and James Riely(B)

DePaul University, Chicago, USA<EMAIL_ADDRESS>
Abstract. We address the problem of *validity* in eventually consistent (EC) systems: In what sense does an EC data structure satisfy the sequential specification of that data structure? Because EC is a very weak criterion, our definition does not describe every EC system; however it is expressive enough to describe any Convergent or Commutative Replicated Data Type (CRDT).

### 1 Introduction

In a replicated implementation of a data structure, there are two impediments to requiring that all replicas achieve consensus on a global total order of the operations performed on the data structure (Lamport 1978): (a) the associated serialization bottleneck negatively affects performance and scalability (*e.g.* see (Ellis and Gibbs 1989)), and (b) the cap theorem imposes a tradeoff between consistency and partition-tolerance (Gilbert and Lynch 2002).

In systems based on *optimistic replication* (Vogels 2009; Saito and Shapiro 2005), a replica may execute an operation without synchronizing with other replicas. If the operation is a mutator, the other replicas are updated asynchronously. Due to the vagaries of the network, the replicas could receive and apply the updates in possibly different orders.

For sequential systems, the correctness problem is typically divided into two tasks: proving *termination* and proving *partial correctness*. Termination requires that the program eventually halt on all inputs, whereas partial correctness requires that the program only returns results that are allowed by the specification.

For replicated systems, the analogous goals are *convergence* and *validity*. Convergence requires that all replicas eventually agree. Validity requires that they agree on something sensible. In a replicated list, for example, if the only value put into the list is 1, then convergence ensures that all replicas eventually see the same value for the head of the list; validity requires that the value be 1.

Convergence has been well-understood since the earliest work on replicated systems. Convergence is typically defined as *eventual consistency*, which requires that once all messages are delivered, all replicas have the same state. *Strong eventual consistency* (sec) additionally requires convergence for all subsets of messages: replicas that have seen the same messages must have the same state.

Perhaps surprisingly, finding an appropriate definition of validity for replicated systems remains an open problem. There are solutions which use concurrent specifications, discussed below. But, as Shavit (2011) noted:

"It is infinitely easier and more intuitive for us humans to specify how abstract data structures behave in a sequential setting, where there are no interleavings. Thus, the standard approach to arguing the safety properties of a concurrent data structure is to specify the structure's properties sequentially, and find a way to map its concurrent executions to these 'correct' sequential ones."

In this paper we give the first definition of validity that is both (1) derived from standard sequential specifications and (2) validates the examples of interest.

We take the "examples of interest" to be *Convergent/Commutative Replicated Data Types* (crdts). These are replicated structures that obey certain monotonicity or commutativity properties. As an example of a crdt, consider the *add-wins set*, also called an "observed remove" set in Shapiro et al. (2011a). The add-wins set behaves like a sequential set if add and remove operations on the same element are ordered. The concurrent execution of an add and remove result in the element being added to the set; thus the remove is ignored and the "add wins." This concurrent specification is very simple, but as we will see in the next section, it is quite difficult to pin down the relationship between the crdt and the sequential specification used in the crdt's definition. This paper is the first to successfully capture this relationship.

Many replicated data types are crdts, but not all (Shapiro et al. 2011a). Notably, Amazon's Dynamo (DeCandia et al. 2007) is not a crdt. Indeed, interest in crdts is motivated by a desire to avoid the well-know concurrency anomalies suffered by Dynamo and other ad hoc systems (Bieniusa et al. 2012).

Shapiro et al. (2011b) introduced the notion of crdt and proved that every crdt has an sec implementation. Their definition of sec includes convergence, but not validity.

The validity requirement can be broken into two components. We describe these below using the example of a list data type that supports only two operations: the mutator put, which adds an element to the end of the list, and the query q, which returns the state of the list. This structure can be specified as a set of strings such as "put(1); put(3); q=[1,3]" and "put(1); put(2); put(3); q=[1,2,3]".

Burckhardt et al. (2012) provide a formal definition of validity using partial orders over events: linearizations respect the partial order on events; monotonicity is ensured by requiring that evolution extends the partial order. Similar definitions can be found in Jagadeesan and Riely (2015) and Perrin et al. (2015). Replicated data structures that are sound with respect to this definition enjoy many good properties, which we discuss throughout this paper. However, this notion of correctness is not general enough to capture common crdts, such as the add-wins set.

This lack of expressivity lead Burckhardt et al. (2014) to abandon notions of validity that appeal directly to a sequential specification. Instead they work directly with *concurrent* specifications, formalizing the style of specification found informally in Shapiro et al. (2011b). This has been a fruitful line of work, leading to proof rules (Gotsman et al. 2016) and extensions (Bouajjani et al. 2014). See (Burckhardt 2014; Viotti and Vukolic 2016) for a detailed treatment.

Positively, concurrent specifications can be used to validate any replicated structure, including crdts as well as anomalous structures such as Dynamo. Negatively, concurrent specifications have no the clear connection to their sequential counterparts. In this paper, we restore this connection. We arrive at a definition of sec that admits crdts, but rejects Dynamo.

The following "corner cases" are a useful sanity-check for any proposed notion of validity.

psts and psm say that a replicated structure should behave sequentially when replication is not used. ppe says that the order of independent operations should not matter. Our definition implies all three conditions. Dynamo fails ppe (Bieniusa et al. 2012), and thus fails to pass our definition of sec.

In the next section, we describe the validity problem and our solution in detail, using the example of a binary set. The formal definitions follow in Sect. 3. We state some consequences of the definition and prove that the add-wins set satisfies our definition. In Sect. 4, we describe a collaborative text editor and prove that it is sec. In Sect. 5 we characterize the programmer's view of a crdt by defining the *most general* crdt that satisfies a given sequential specification. We show that any program that is correct using the most general crdt will be correct using a more restricted crdt. We also show that our validity criterion for sec is *local* in the sense of Herlihy and Wing (1990): independent structures can be verified independently. In Sect. 6, we apply these results to prove the correctness of a graph that is implemented using two sec sets.

Our work is inspired by the study of relaxed memory, such as (Alglave 2012). In particular, we have drawn insight from the rmo model of Higham and Kawash (2000).

### 2 Understanding Replicated Sets

In this section, we motivate the definition of sec using replicated sets as an example. The final definition is quite simple, but requires a fresh view of both executions and specifications. We develop the definition in stages, each of which requires a subtle shift in perspective. Each subsection begins with an example and ends with a summary.

#### 2.1 Mutators and Non-mutators

An *implementation* is a set of *executions*. We model executions abstractly as labelled partial orders (lpos). The ordering of the lpo captures the history that precedes an event, which we refer to as *visibility*.

$$
\begin{array}{c}
\boxed{\underbrace{\cdots}}^a \xrightarrow{a} \boxed{\underbrace{\cdots}}^b \xrightarrow{b} \boxed{\underbrace{\cdots}}^c \xrightarrow{c} \boxed{\underbrace{\cdots}}^d \cdots \\
\boxed{\underbrace{\cdots}}^a
\end{array}
\tag{1}
$$

$$
\begin{array}{c}
\boxed{\underbrace{\cdots}}^a \xrightarrow{a} \boxed{\underbrace{\cdots}}^b \xrightarrow{b} \boxed{\underbrace{\cdots}}^a
\end{array}
\tag{1}
$$

Here the events are a through j, with labels +0, +1, etc., and order represented by arrows. The lpo describes an execution with two replicas, shown horizontally, with time passing from left to right. Initially, the top replica receives a request to add 0 to the set (+0a). Concurrently, the bottom replica receives a request to add 1 (+1b). Then each replica is twice asked to report on the items contained in the set. At first, the top replica replies that 0 is present and 1 is absent (✓0b✗1c), whereas the bottom replica answers with the reverse (✗0g✓1h). Once the add operations are visible at all replicas, however, the replicas give the same responses (✓0d✓1e and ✓0i ✓1j ).

lpos with non-interacting replicas can be denoted compactly using sequential and parallel composition. For example, the prefix of (1) that only includes the first three events at each replica can be written (+0a; ✓0b; ✗1c) -(+1f ; ✗0g; ✓1h).

A *specification* is a set of *strings*. Let set be the specification of a sequential set with elements 0 and 1. Then we expect that set includes the string "+0✓0✗1", but not "+0✗0✓1". Indeed, each specification string can uniquely be extended with either ✓0 or ✗0 and either ✓1 or ✗1.

There is an isomorphism between strings and labelled *total* orders. Thus, specification strings correspond to the restricted class of lpos where the visibility relation provides a total order.

*Linearizability* (Herlihy and Wing 1990) is the gold standard for concurrent correctness in tightly coupled systems. Under linearizability, an execution is valid if there exists a linearization τ of the events in the execution such that for every event e, the prefix of e in τ is a valid specification string.

Execution (1) is not linearizable. The failure can already be seen in the sublpo (+0a; ✗1c) - (+1f ; ✗0g). Any linearization must have either +1f before ✗1c or +0a before ✗0g. In either case, the linearization is invalid for set.

Although it is not linearizable, execution (1) is admitted by every crdt set in Shapiro et al. (2011a). To validate such examples, Burckhardt et al. (2012) develop a weaker notion of validity by dividing labels into *mutators* and *accessors* (also known as non-mutators). Similar definitions appear in Jagadeesan and Riely (2015) and Perrin et al. (2015). Mutators change the state of a replica, and accessors report on the state without changing it. For set, the mutators **M** and non-mutators **M** are as follows.

**M** = {+0, -0, +1, -1}, representing addition and removal of bits 0 and 1. **M** = {✗0, ✓0, ✗1, ✓1}, representing membership tests returning false or true.

Define the *mutator prefix* of an event e to include e and the *mutators* visible to e. An execution is valid if there exists a linearization of the execution, τ , such that for every event e, the *mutator prefix* of e in τ is a valid specification string.

It is straightforward to see that execution (1) satisfies this weaker criterion. For both ✓0b and ✗1c, the mutator prefix is +0a. This includes +0a but not +1f , and thus their answers are validated. Symmetrically, the mutator prefixes of ✗0g and ✓1h only include +1f . The mutator prefixes for the final four events include both +0a and +1f , but none of the prior accessors.

*Summary:* Convergent states must agree on the final order of mutators, but intermediate states may see incompatible subsequences of this order. By restricting attention to mutator prefixes, the later states need not linearize these incompatible views of the partial past.

This relaxation is analogous to the treatment of non-mutators in update serializability (Hansdah and Patnaik 1986; Garcia-Molina and Wiederhold 1982), which requires a global serialization order for mutators, ignoring non-mutators.

#### 2.2 Dependency

The following lpo is admitted by the add-wins set discussed in the introduction.

$$
\begin{array}{c}
\square \square^{\scriptstyle{a}} \square^{\scriptstyle{b}} \square^{\scriptstyle{c}} \square^{\scriptstyle{c}} \\
\square^{\scriptstyle{a}} \square^{\scriptstyle{b}} \square^{\scriptstyle{c}}
\end{array}
\begin{array}{c}
\square \square^{\scriptstyle{a}} \\
\square^{\scriptstyle{a}} \\
\square^{\scriptstyle{b}}
\end{array}
\begin{array}{c}
\square \square^{\scriptstyle{a}} \\
\square^{\scriptstyle{a}} \\
\square^{\scriptstyle{b}}
\end{array}
\begin{array}{c}
\square \square^{\scriptstyle{a}} \\
\square^{\scriptstyle{a}} \\
\square^{\scriptstyle{b}}
\end{array}
\tag{2}
$$

In any crdt implementation, the effect of +1b is negated by the subsequent -1c The same reasoning holds for +0e and -0f . In an add-wins set, however, the *concurrent* adds, +0a and +1d, win over the deletions. Thus, in the final state both 0 and 1 are present.

This lpo is not valid under the definition of the previous subsection: Since ✓0g and ✓1h see the same mutators, they must agree on a linearization of (+0a; +1b; -1c) - (+1d; +0e; -0f ). Any linearization must end in either -1c or -0f ; thus it is not possible for both ✓0g and ✓1h to be valid.

Similar issues arise in relaxed memory models, where program order is often relaxed between uses of independent variables (Alglave et al. 2014). Generalizing, we write m # n to indicate that labels m and n are dependent. Dependency is a property of a *specification*, not an implementation. Our results only apply to specifications that support a suitable notion of dependency, as detailed in Sect. 3. For set, # is an equivalence relation with two equivalence classes, corresponding to actions on the independent values 0 and 1.

# = {+0, -0, ✗0, ✓0}2 ∪ {+1, -1, ✗1, ✓1}2, where D2 = D × D.

While the dependency relation for set is an equivalence, this is not required: In Sect. 4 we establish the correctness of collaborative text editing protocol with an intransitive dependency relation.

The *dependent restriction* of (2) is as follows.

$$
\overbrace{\underbrace{\text{-0}}^{\text{-}}}^{\text{-}}\underbrace{\text{-1}}^{\text{-}}\underbrace{\text{-1}}^{\text{-}}\underbrace{\text{-1}}^{\text{-}}\overbrace{\text{-2}}^{\text{-}}\overbrace{\text{-3}}^{\text{-}}\overbrace{\text{-4}}^{\text{-}}\overbrace{\text{-6}}^{\text{-}}\tag{3}
$$

In the previous subsection, we defined validity using the *mutator prefix* of an event. We arrive at a weaker definition by restricting attention to the *mutator prefix of the dependent restriction*.

Under this definition, execution (2) is validated: Any interleaving of the strings +0e-0f +0a✓0g and +1b-1c+1d✓1h linearizes the dependent restriction of (2) given in (3).

*Summary:* crdts allow independent mutators to commute. We formalize this intuition by restricting attention to mutator prefixes of the dependent restriction. The crdt must respect program order between dependent operations, but is free to reorder independent operations.

This relaxation is analogous to the distinction between *program order* and *preserved* program order (ppo) in relaxed memory models (Higham and Kawash 2000; Alglave 2012). Informally, ppo is the suborder of program order that removes order between independent memory actions, such as successive reads on different locations without an intervening memory barrier.

#### 2.3 Puns

The following lpo is admitted by the add-wins set.

As in execution (2), the add +0a is undone by the following remove -0b, but the concurrent add +0e wins over -0b, allowing ✓0c. In effect, ✓0c sees the order of the mutators as +0a -0b +0e. Symmetrically, ✓0g sees the order as +0e -0f +0a. While this is very natural from the viewpoint of a crdt, there is no linearization of the events that includes both +0a -0b +0e and +0e -0f +0a, since +0a and +0e must appear in different orders.

Indeed, this lpo is not valid under the definition of the previous subsection. First note that all events are mutually dependent. To prove validity we must find a linearization that satisfies the given requirements. Any linearization of the mutators must end in either -0b or -0f . Suppose we choose +0a -0b +0e -0f and look for a mutator prefix to satisfy ✓0g. (All other choices lead to similar problems.) Since -0f precedes ✓0g and is the last mutator in our chosen linearization, every possible witness for ✓0g must end with mutator -0f . Indeed the only possible witness is +0a +0e -0f ✓0g. However, this is not a valid specification string.

The problem is that we are linearizing *events*, rather than *labels*. If we shift to linearizing labels, then execution (4) is allowed. Fix the final order for the mutators to be +0 -0 +0 -0. The execution is allowed if we can find a subsequence that linearizes the labels visible at each event. It suffices to choose the witnesses as follows. In the table, we group events with a common linearization together.

$$\begin{array}{cccc} \text{+0}^a, & \text{+0}^e; & \text{+0} & & \text{X} \otimes^c, \ \mho^g & \text{5} & \text{0} & \text{0} & \text{0} \\ \text{-0}^b, & \text{-0}^f; & \text{+0}-\text{0} & & \text{X} \otimes^d, \ \mho^h & \text{+0}-\text{0}+\text{0} & \text{0} & \text{0} & \text{0} \\ \end{array}$$

Each of these is a valid specification string. In addition, looking only at mutators, each is a subsequence of +0 -0 +0 -0.

In execution (4), each of the witnesses is actually a *prefix* of the final mutator order, but, in general, it is necessary to allow *subsequences*.

$$\underbrace{\square^{\circ}}\_{\square^{\circ}} \xleftarrow{\square^{\circ}}\_{\square^{\circ}} \xleftarrow{\square^{\circ}}\_{\square} \xleftarrow{\square^{\circ}}\_{\square} \tag{5}$$

Execution (5) is admitted by the add-wins set. It is validated by the final mutator sequence -0 +0. The mutator prefix +0 of b is a subsequence of -0 +0, but not a prefix.

*Summary:* While dependent events at a single replica must be linearized in order, concurrent events may slip anywhere into the linearization. A crdt may *pun* on concurrent events with same label, using them in different positions at different replicas. Thus a crdt may establish a final total over the labels of an execution even when there is no linearization of the events.

#### 2.4 Frontiers

In the introduction, we mentioned that the validity problem can be decomposed into the separate concerns of *linearizability* and *monotonicity.* The discussion thus far has centered on the appropriate meaning of linearizability for crdts. In this subsection and the next, we look at the constraints imposed by monotonicity.

Consider the prefix {+0a, -0b, +0e, ✓0c, -0f } of execution (4), extended with action ✗0x, with visibility order as follows.

This execution is *not strong* ec, since ✓0c and ✗0x see exactly the same mutators, yet provide incompatible answers.

Unfortunately, execution (6) is valid by the definition given in the previous section: The witnesses for a–f are as before. In particular, the witness for ✓0c is "+0-0+0✓0". The witness for ✗0x is "+0+0-0✗0". In each case, the mutator prefix is a subsequence of the global mutator order "+0-0+0-0".

It is well known that punning can lead to bad jokes. In this case, the problem is that ✗0x is punning on a concurrent -0 that cannot be matched by a visible -0 in its history: the execution -0 that is visible to ✗0x must appear *between* the two +0 operations; the specification -0 that is used by ✗0x must appear *after*. The final states of execution (4) have seen both remove operations, therefore the pun is harmless there. But ✓0c and ✗0x have seen only one remove. They must agree on how it is used.

Up to now, we have discussed the linearization of each event in isolation. We must also consider the relationship between these linearizations. When working with linearizations of *events*, it is sufficient to require that the linearization chosen for each event be a subsequence for the linearization chosen for each visible predecessor; since events are unique, there can be no confusion in the linearization about which event is which. Execution (6) shows that when working with linearizations of *labels*, it is insufficient to consider the relationship between individual events. The linearization "+0+0-0✗0" chosen for ✗0x is a supersequence of those chosen for its predecessors: "+0" for +0e and "+0-0" for -0b. The linearization "+0-0+0✓0" chosen for ✓0c is also a supersequence for the same predecessors. And yet, ✓0c and ✗0x are incompatible states.

Sequential systems have a single state, which evolves over time. In distributed systems, each replica has its own state, and it is this *set* of states that evolves. Such a set of states is called a *(consistent) cut* (Chandy and Lamport 1985).

A *cut* of an lpo is a sub-lpo that is down-closed with respect to visibility. The *frontier* of cut is the set of maximal elements. For example, there are 14 frontiers of execution (6): the singletons {+0a}, {-0b}, {✓0c}, {+0e}, {-0f }, {✗0x}, the pairs {+0a, +0e}, {+0a, -0f }, {-0b, +0e}, {-0b, -0f }, {✓0c, -0f }, {✓0c, ✗0x}, {✗0x, -0f }, and the triple {✓0c, ✗0x, -0f }. As we explain below, we consider non-mutators in isolation. Thus we do not consider the last four cuts, which include a non-mutator with other events. That leaves 10 frontiers. The definition of the previous section only considered the 6 singletons. Singleton frontiers are generated by *pointed cuts*, with a single maximal element.

When applied to frontiers, the monotonicity requirement invalidates execution (6). Monotonicity requires that the linearization chosen for a frontier be a subsequence of the linearization chosen for any extension of that frontier. If we are to satisfy state ✓0c in execution (6), the frontier {-0b, +0e} must linearize to "+0-0+0". If we are to satisfy state ✗0x, the frontier {-0b, +0e} must linearize to "+0+0-0". Since we require a unique linearization for each frontier, the execution is disallowed.

Since crdts execute non-mutators locally, it is important that we ignore frontiers with multiple non-mutators. Recall execution (4):

There is no specification string that linearizes the cut with frontier {✓0c, ✓0g}, since we cannot have ✓0 immediately after -0. If we consider only pointed cuts for non-mutators, then the execution is sec, with witnesses as follows.

In order to validate non-mutators, we *must* consider singleton non-mutator frontiers. The example shows that we *must not* consider frontiers with multiple non-mutators. There is some freedom in the choices otherwise. For set, we can "saturate" an execution with accessors by augmenting the execution with accessors that witness each cut of the mutators. In a saturated execution, it is sufficient to consider only the *pointed accessor* cuts, which end in a maximal accessor. For non-saturated executions, we are forced to examine each mutator cut: it is possible that a future accessor extension may witness that cut. The status of "mixed" frontiers, which include mutators with a single maximal nonmutator, is open for debate. We choose to ignore them, but the definition does not change if they are included.

*Summary:* A crdt must have a strategy for linearizing all mutator labels, even in the face of partitions. In order to ensure *strong* ec, the definition must consider sets of events across multiple replicas. Because non-mutators are resolved locally, sec must ignore frontiers with multiple non-mutators.

Cuts and frontiers are well-known concepts in the literature of distributed systems (Chandy and Lamport 1985). It is natural to consider frontiers when discussing the evolving correctness of a crdt.

#### 2.5 Stuttering

Consider the following execution.

This lpo represents a partitioned system with events a–e in one partition and x–z in the other. As the partition heals, we must be able to account for the intermediate states. Because of the large number of events in this example, we have elided all accessors. We will present the example using the semantics of the add-wins set. Recall that the add-wins set validates ✓0 if and only if there is a maximal +0 beforehand. Thus, a replica that has seen the cut with frontier {+0a, -0y, -0z} must answer ✓0, whereas a replica that has seen {-0b, -0y, -0z} must answer ✗0.

Any linearization of {+0a, -0y, -0z} must end in +0, since the add-win set must reply ✓0: the only possibility is "+0-0-0+0". The linearization of {-0b, -0y, -0z} must end in -0. If it must be a supersequence, the only possibility is "+0-0-0+0-0". Taking one more step on the left, {+0c, -0y, -0z} must linearize to "+0-0-0+0-0+0". Thus the final state {-0d, -0e, -0y, -0z} must linearize to "+0 -0-0+0-0+0-0-0". Reasoning symmetrically, the linearization of {-0d, -0e, +0x} must be "+0-0+0-0-0+0", and thus the final {-0d, -0e, -0y, -0z} must linearize to "+0-0+0-0-0+0-0-0". The constraints on the final state are incompatible. Each of these states can be verified in isolation; it is the relation between them that is not satisfiable.

Recall that monotonicity requires that the linearization chosen for a frontier be a *subsequence* of the linearization chosen for any extension of that frontier. The difficulty here is that subsequence relation ignores the similarity between "+0 -0-0+0-0+0-0-0" and "+0-0+0-0-0+0-0-0". Neither of these is a subsequence of the other, yet they capture exactly the same sequence of *states*, each with six alternations between ✗0 and ✓0. The canonical state-based representative for these sequences is "+0-0+0-0+0-0".

crdts are defined in terms of states. In order to relate crdts to sequential specifications, it is necessary to extract information about states from the specification itself. Adapting Brookes (1996), we define strings as *stuttering equivalent* (notation σ ∼ τ ) if they pass through the same states. So +0+1+0 ∼ +0+1 but +0-0+0 ∼ +0. If we consider subsequences up to stuttering, then execution (7) is sec, with witnesses as follow:

{a}, {x}, {a, x} : +0 {b}, {y}, {y, z}, {z} : +0-0 {a, y}, {a, y, z}, {a, z}, {b, x} : +0-0+0 {b, y}, {b, y, z}, {b, z}, {d}, {d, e}, {e} : +0-0+0-0 {c, y}, {c, y, z}, {c, z}, {d, x}, {d, e, x}, {e, x} : +0-0+0-0+0 {d, y}, {d, y, z}, {d, z}, {e, y}, {e, y, z}, {e, z}, {d, e, y}, {d, e, y, z}, {d, e, z}: +0-0+0-0+0-0

Recall that without stuttering, we deduced that {+0c, -0y, -0z} must linearize to "+0-0-0+0-0+0" and {-0d, -0e, +0x} must linearize to "+0-0+0-0-0+0". Under stuttering equivalence, these are the same, with canonical representative "+0 -0+0-0+0". Thus, monotonicity under stuttering allows both linearizations to be extended to satisfy the final state {-0d, -0e, -0y, -0z}, which has canonical representative "+0-0+0-0+0-0".

*Summary:* crdts are described in terms of convergent states, whereas specifications are described as strings of actions. Actions correspond to labels in the lpo of an execution. Many strings of actions may lead to equivalent states. For example, idempotent actions can be applied repeatedly without modifying the state.

The stuttering equivalence of Brookes (1996) addresses this mismatch. In order to capture the validity of crdts, the definition of subsequence must change from a definition over individual specification strings to a definition over *equivalence classes* of strings *up to stuttering*.

### 3 Eventual Consistency for CRDTs

This section formalizes the intuitions developed in Sect. 2. We define executions, specifications and strong eventual consistency (sec). We discuss properties of eventual consistency and prove that the add-wins set is sec.

### 3.1 Executions

An execution realizes *causal delivery* if, whenever an event is received at a replica, all predecessors of the event are also received. Most of the crdts in Shapiro et al. (2011a) assume causal delivery, and we assumed it throughout the introductory section. There are costs to maintaining causality, however, and not all crdts assume that executions incur these costs. In the formal development, we allow non-causal executions.

Shapiro et al. (2011a) draw executions as timelines, explicitly showing the delivery of remote mutators. Below left, we give an example of such a timeline.

This is a non-causal execution: at the bottom replica, +1 is received before +0, even though +0 precedes +1 at the top replica.

Causal executions are naturally described as Labelled Partial Orders (lpos), which are transitive and antisymmetric. Section 2 presented several examples of lpos. To capture non-causal systems, we move to *Labelled Visibility Orders* (lvos), which are merely acyclic. Acyclicity ensures that the transitive closure of an lvo is an lpo. The right picture above shows the lvo corresponding to the timeline on the left. The zigzag arrow represents an intransitive communication. When drawing executions, we use straight lines for "transitive" edges, with the intuitive reading that "this and all preceding actions are delivered".

lvos arise directly due to non-causal implementations. As we will see in Sect. 4, they also arise via projection from an lpo.

lvos are unusual in the literature. To make this paper self-contained, we define the obvious generalizations of concepts familiar from lpos, including isomorphism, suborder, restriction, maximality, downclosure and cut.

Fix a set **L** of labels. A *Labelled Visibility Order* (lvo, also known as an *execution*) is a triple u = Eu, λu, u where Eu is a finite set of events, λu ∈ (Eu → **L**) and u ⊆ (Eu × Eu) is reflexive and acyclic.

Let u, v range over lvos. Many concepts extend smoothly from lpos to lvos.

*Replica-Specific Properties.* In the literature on replicated data types, some properties of interest (such as "read your writes" (Tanenbaum and Steen 2007)) require the concept of "session" or a distinction between local and remote events. These can be accommodated by augmenting lvos with a replica labelling ρu ∈ (Eu → **R**), which maps events to a set **R** of *replica identifiers*.

Executions can be generated operationally as follows: Replicas receive mutator and accessor events from the local client; they also receive mutator events that are forwarded from other replicas. Each replica maintains a set of *seen* events: an event that is received is added to this set. When an event is received from the local client, the event is additionally added to the execution, with the predecessors in the visibility relation corresponding to the current *seen* set. If we wish to restrict attention to causal executions, then we require that replicas forward all the mutators in their *seen* sets, rather than individual events, and, thus, the visibility relation is transitive over mutators.

All executions that are operationally generated satisfy the additional property that u is per-replica total: if ρ(d) = ρ(e) then either d u e or e u d.

1 We use the standard definitions for restriction on functions and relations. Given a function f : E → X, R: E × E and D ⊆ E, define f D = {d, f(d) | d ∈ D} and R D = {d1, d2 | d1, d2 ∈ D and d1 R d2}.

We do not demand per-replica totality because our results do not rely on replicaspecific information.

### 3.2 Specifications and Stuttering Equivalence

Specifications are sets of strings, equipped with a distinguished set of mutators and a dependency relation between labels. Specifications are subject to some constraints to ensure that the mutator set and dependency relations are sensible; these are inspired by the conditions on Mazurkiewicz executions (Diekert and Rozenberg 1995). Every specification set yields a derived notion of stuttering equivalence. This leads to the definition of *observational subsequence* (≤obs ).

We use standard notation for strings: Let σ and τ range over strings. Then στ denotes concatenation, σ∗ denotes Kleene star, σ τ denotes the set of interleavings, ε denotes the empty string and σi denotes the i th element of σ. These notations lift to sets of strings via set union.

A *specification* is a quadruple **L**, **M**, #, Σ where

Let **M** = **L** \ **M** be the sets of *non-mutators*.

A specification must satisfy the following properties:

Property (b) ensures that non-mutators do not affect the state of the data structure. Property (c) ensures that commuting of independent actions does not affect the state of the data structure.

Recall that the set specification takes **M** = {+0, -0, +1, -1}, representing addition and removal of bits 0 and 1, and **M** = {✗0, ✓0, ✗1, ✓1}, representing membership tests returning false or true. The dependency relation is # = {+0, -0, ✗0, ✓0}2 ∪ {+1, -1, ✗1, ✓1}2, where D2 = D × D.

The dependency relation for set is an equivalence, but this need not hold generally. We will see an example in Sect. 4.

The definitions in the rest of the paper assume that we have fixed a specification **L**, **M**, #, Σ. In the examples of this section, we use set.

*State and Stuttering Equivalence.* Specification strings σ and τ are *state equivalence* (notation σ ≈ τ ) if every valid extension of σ is also a valid extension of τ , and vice versa. For example, +0+1+0 ≈ +0+1 and +0-0+0 ≈ +0, but +0-0 ≈ +0. In particular, state equivalent strings agree on the valid accessors that can immediately follow them: either ✓0 or ✗0 and either ✓1 or ✗1. Formally, we define state equivalence, ≈ ⊆ **L**∗ × **L**∗, as follows2.

$$(\sigma \approx \sigma') \stackrel{\scriptstyle \circ}{=} (\sigma = \sigma') \text{ or } (\{\sigma, \sigma'\} \subseteq \Sigma \text{ and } \forall \tau \in \mathbf{L}^\*. \,\sigma\tau \in \Sigma \text{ iff } \,\sigma'\tau \in \Sigma).$$

From specification property (b), we know that non-mutators do not affect the state. Thus we have that ua ≈ u whenever a ∈ **M** and ua ∈ Σ. From specification property (c), we know that independent actions commute. Thus we have that σab ≈ σba whenever ¬(a # b) and {σab, σba} ⊆ Σ.

Two strings are *stuttering equivalent*3 if they only differ in operations that have no effect on the state of the data structure, as given by Σ. Adapting Brookes (1996) to our notion of state equivalence, we define stuttering equivalence, ∼ ⊆ **L**∗ × **L**∗, to be the least equivalence relation generated by the following rules, where a ranges over **L**.

$$\begin{array}{ccc} \hline \sigma \sim \varepsilon & \quad \frac{\sigma \sim \sigma'}{\sigma a \sim \sigma' a} & \quad \frac{\sigma \approx \sigma a}{\sigma \sim \sigma a} & \quad \frac{\sigma b \sim \sigma \quad \neg(a \not\neq b)}{\sigma ab \sim \sigma a} \\\hline \end{array}$$

The first rule above handles the empty string. The second rule allows stuttering in any context. The third rule motivates the name stuttering equivalence, for example, allowing +0+0 ∼ +0. The last case captures the equivalence generated by independent labels, for example, allowing +0+1+0 ∼ +0+1 but not +0-0+0 ∼ +0-0. Using the properties of ≈ discussed above, we can conclude, for example, that +0✓0✓0+0-0✗0 ∼ +0-0.

Consider specification strings for a unary set over value 0. Since stuttering equivalence allows us to remove both accessors and adjacent mutators with the same label we deduce that the *canonical representatives* of the equivalence classes induced by ∼ are generated by the regular expression (+0)?(-0+0)∗(-0)?.

*Observational Subsequence.* Recall that ac is a *subsequence* of abc, although it is not a *prefix*. We write ≤seq for subsequence and ≤obs for *observational subsequence*, defined as follows.

$$
\sigma\_1 \cdots \sigma\_n \leq\_{\mathsf{seq}} \tau\_0 \sigma\_1 \tau\_1 \cdots \sigma\_n \tau\_n \qquad \sigma \leq\_{\mathsf{obs}} \tau \quad \text{if} \ \exists \sigma' \sim \sigma. \ \exists \tau' \sim \tau. \ \sigma' \leq\_{\mathsf{seq}} \tau'
$$

Note that observational subsequence includes both subsequence and stuttering equivalence (≤obs ) ⊆ (≤seq ) ∪ (∼).

≤seq can be understood in isolation, whereas ≤obs can only be understood with respect to a given specification. In the remainder of the paper, the implied specification will be clear from context. ≤seq is a partial order, whereas ≤obs is only a preorder, since it is not antisymmetric.

Let σ and τ be strings over the unary set with canonical representatives aσ and bτ . Then we have that σ ≤obs τ exactly when either a = b and - σ - - ≤ - τ - -

2 To extend the definition to non-specification strings, we allow σ ≈ σ when σ = σ- .

3 Readers of Brookes (1996) should note that mumbling is not relevant here, since all mutators are visible.

or a = b and - σ - - < - τ - -. Thus, observational subsequence order is determined by the number of alternations between the mutators.

Specification strings for the binary set, then, are stuttering equivalent exactly when they yield the same canonical representatives when restricted to 0 and to 1. Thus, observational subsequence order is determined by the number of alternations between the mutators, when restricted to each dependent subsequence. (The final rule in the definition of stuttering, which allows stuttering across independent labels, is crucial to establishing this canonical form.)

### 3.3 Eventual Consistency

Eventual consistency is defined using the *cuts* of an execution and the *observational subsequence order* of the specification. As noted in Sects. 2.2 and 2.4, it is important that we not consider all cuts. Thus, before we define sec, we must define *dependent cuts*.

The *dependent restriction* of an execution is defined: v # = Ev, λv, # v, where d # v e when λv(d) # λv(e) and d v e. See Sect. 2.2 for an example of dependent restriction.

The *dependent cuts* of v are cuts of the dependent restriction. As discussed in Sect. 2.4, we only consider pointed cuts (with a single maximal element) for non-mutators. See Sect. 2.4 for an example.

$$\mathsf{cuts}\_{\#}(v) = \left\{ u \in \mathsf{cuts}(v \mid \#) \: \left| \: \forall e \in \mathsf{E}\_{u}. \text{ if } \lambda\_{u}(e) \in \overline{\mathbf{M}} \text{ then } \mathsf{max}(u) = \{e\} \right\} \right\}$$

An execution v is *Eventually Consistent* (sec) for specification **L**, **M**, #, Σ iff there exists a function τ : cuts#(v) → Σ that satisfies the following.

Linearization: ∀p ∈ cuts#(v). p linearizes to τ (p), and Monotonicity: ∀p, q ∈ cuts#(v). p ⊆ q implies τ (p) ≤obs τ (q).

A data structure implementation is sec if all of its executions are sec.

In Sect. 2, we gave several examples that are sec. See Sects. 2.4 and 2.5 for examples where τ is given explicitly. Section 2.4 also includes an example that is not sec.

The concerns raised in Sect. 2 are reflected in the definition.

– Monotonicity ensures that the system evolves in a sensible way: new order may be introduced, but old order cannot be forgotten. As discussed in Sect. 2.5, the preserved order is captured in the observational subsequence relation, which allows stuttering (Brookes 1996).

#### 3.4 Properties of Eventual Consistency

We discuss some basic properties of sec. For further analysis, see Sect. 5.

An important property of crdts is *prefix closure*: If an execution is valid, then every prefix of the execution should also be valid. Prefix closure follows immediately from the definition, since whenever u is a prefix of v we have that cuts#(u) ⊆ cuts#(v).

Prefix closure looks back in time. It is also possible to look forward: A system satisfies *eventual delivery* if every valid execution can be extended to a valid execution with a maximal element that sees every mutator. If one assumes that every specification string can be extended to a longer specification string by adding non-mutators, then eventual delivery is immediate.

The properties psts, psm and ppe are discussed in the introduction. An sec implementation must satisfies ppe since every dependent set of mutators is linearized: sec enforces the stronger property that there are no new intermediate states, even when executing all mutators in parallel. For causal systems, where u is transitive, psts and psm follow by observing that if there is a total order on the mutators of u then any linearization of u is a specification string.

Burckhardt (2014, Sect. 5) provides a taxonomy of correctness criteria for replicated data types. Our definition implies NoCircularCausality and CausalArbitration, but does not imply either ConsistentPrefix or CausalVisibility. For lpos, which model causal systems, our definition implies CausalVisibility. ReadMyWrites and MonotonicReads require a distinction between local and remote events. If one assumes the replica-specific constraints given in Sect. 3.1, then our definition satisfies these properties; without them, our definition is too abstract.

#### 3.5 Correctness of the Add-Wins Set

The add-wins set is defined to answer ✓k for a cut u exactly when

$$
\exists d \in u. \,\lambda\_u(d) = \text{\textbullet} \,\,\wedge \,\,\langle \exists e \in u. \,\,\lambda\_u(e) = \text{\textbullet} \,\,\wedge \,\, d \,\,\stackrel{\sim}{\sim} u \,\,e).
$$

It answers ✗k otherwise. The add-wins set is called the "observed-remove" set.

We show that any lpo that meets this specification is sec with respect to set. We restrict attention to lpos since causal delivery is assumed for the addwins set in (Shapiro et al. 2011a).

For set, the dependency relation is an equivalence. For an equivalence relation R, let **L**/R ⊆ 2**L** denote the set of (disjoint) equivalence classes for R. For set, **L**/# = {{+0, -0, ✗0, ✓0}, {+1, -1, ✗1, ✓1}}. When dependency is an equivalence, then *every* interleaving of independent actions is valid if *any* interleaving is valid. Formally, we have the following, where denotes interleaving.

$$\forall D \in (\mathbf{L}/\#). \forall \sigma \in D^\*. \forall \tau \in (\mathbf{L} \nmid D)^\*. (\sigma \parallel \tau) \cap \Sigma \neq \emptyset \text{ implies } (\sigma \parallel \tau) \subseteq \Sigma^\*$$

Using the forthcoming composition result (Theorem 2), it suffices for us to address the case when u only involves operations on a single element, say 0. For any such lvo u, we choose a linearization τ (u) ∈ (-0|+0)∗ that has a maximum number of alternations between -0 and +0. If there is a linearization that begins with -0, then we choose one of these. Below, we summarize some of the key properties of such a linearization.

The first property above ensures that the accessors are validated correctly, *i.e.*, 0 is deemed to be present iff there is an +0 that is not followed by any -0.

We are left with proving monotonicity, *i.e.*, if u ⊆ v, then τ (u) ≤obs τ (v). Consider τ (u) = aσ and τ (v) = bρ.

### 4 A Collaborative Text Editing Protocol

In this section we consider a variant of the collaborative text editing protocol defined by Attiya et al. (2016). After stating the sequential specification, text, we sketch a correctness proof with respect to our definition of eventual consistency. This example is interesting formally: the dependency relation is not an equivalence, and therefore the dependent projection does not preserve transitivity. The generality of intransitive lvos is necessary to understand text, even assuming a causal implementation.

*Specification.* Let a, b range over *nodes*, which contain some text, a unique identifier, and perhaps other information. Labels have the following forms:

We demonstrate the correct answers to queries by example. Initially, the document is empty, whereas after initialization, the document contains a single node; thus the specification contains strings such as "?ε !c ?c", where ε represents the empty document. Nodes can be added either before or after other nodes; thus "!c +b<c +d>c" results in the document ?bcd. Nodes are always added adjacent to the target; thus, order matters in "!c +e>c +d>c" which results in ?cde rather than ?ced. Removal does what one expects; thus "!c +e>c +d>c -c" results in ?de.

Attiya et al. (2016) define the interface for text using integer indices as targets, rather than nodes. Using the unique correspondence between the nodes and it indices (since node are unique), one can easily adapt an implementation that satisfies our specification to their interface.

We say that node a is a *added* in the actions !a, +ab. Node b is a *target* in +ab. In addition to correctly answering queries, specifications must satisfy the following constraints:

These constraints forbid adding to a target that has been removed; thus "!c +d>c -c" is a valid string, but "!c -c +d>c" is not. It also follows that initialization must precede any other mutators.

Because add operations use unique identifiers, punning and stuttering play little role in this example. In order to show the implementation correct, we need only choose an appropriate notion of dependency. As we will see, it is necessary that removes be independent of adds with disjoint label sets, but otherwise all actions may be dependent. Let **L**!+? be the set of add and query labels, and let nodes return the set of nodes that appear in a label. Then we define dependency as follows.

$$\ell \# k \text{ iff } \{\ell, k\} \subseteq \mathbf{L}\_{\mathsf{l}\star \mathsf{?}} \text{ or } \mathsf{nodes}(\ell) \cap \mathsf{nodes}(k) \neq \emptyset$$

*Implementation.* We consider executions that satisfy the same four conditions above imposed on specifications. We refer the reader to the algorithm of Attiya et al. (2016) that provides timestamps for insertions that are monotone with respect to causality.

As an example, Attiya et al. (2016) allow the execution given on the left below. In this case, the dependent restriction is an intransitive lvo, even though the underlying execution is an lpo: in particular, !b does not precede -d in the dependent restriction. We give the order considered by dependent cuts on the right—this is a restriction of the dependent restriction: since we only consider pointed accessor cuts, we can safely ignore order out of non-mutators.

This execution is not linearizable, but it is sec, choosing witnesses to be subsequences of the mutator string "!b +d>b +c>b +ad -b -d". Here, the document is initialized to b, then c and d are added after b, resulting in ?bcd. The order of c and d is determined by their timestamps. Afterwards, the top replica removes d and adds a; the bottom replica removes b and adds e, resulting in the final state ?ace. In the right execution, the removal of order out of the nonmutators shows the "update serializability" effect; the removal of order between -b and +e>d (and between -d and +a<b) shows the "preserved program order" effect.

*Correctness.* Given an execution, we can find a specification string s1s2 that linearizes the mutators in the dependent restriction of the execution such that s1 contains only adds and s2 contains only removes. Such a specification string exists because by the conditions on executions, deletes do not have any outgoing edges to other mutators in the dependent restriction; so, they can be moved to the end in the matching specification string. In order to find s1 that linearizes the add events, any linearization that respects causality and timestamps (yielded by the algorithm of Attiya et al. (2016)) suffices for our purposes. The conditions required by sec follow immediately.

### 5 Compositional Reasoning

The aim of this section is to establish compositional methods to reason about replicated data structures. We do so using *Labelled Transition Systems* (ltss), where the transitions are labelled by dependent cuts. We show how to derive an lts from an execution, lts(u). We also define an lts for the *most general* crdt that validates a specification, lts(Σ). We show that u is sec for Σ exactly when lts(u) is a refinement of lts(Σ). We use this alternative characterization to establish composition and abstraction results.

*LTSs.* An lts is a triple consisting of a set a states, an initial state and a labelled transition function between states. We first define the ltss for executions and specifications, then provide examples and discussion.

For both executions and specifications, the labels of the lts are dependent cuts: for executions, these are dependent cuts of the execution itself; for specifications, they are drawn from the set L# = v∈L cuts#(v) of all possible dependent cuts. We compare lts labels up to isomorphism, rather than identity. Thus it is safe to think of lts labels as (potentially intransitive) pomsets (Plotkin and Pratt 1997).

The states of the lts are different for the execution and specification. For executions, the states are cuts of the execution u itself, cuts(u); these are general cuts, not just dependent cuts. For specifications, the states are the stuttering equivalence classes of strings allowed by the specification, Σ/∼.

There is an isomorphism between strings and total orders. We make use of this in the definition, treating strings as totally-ordered lvos.

Define lts(u) = cuts(u), ∅, −→i, where p v −→i q if v ∈ cuts#(q) and

Define lts(Σ) = Σ/∼, ε, −→s, where [σ] v −→s [ρ] if v ∈ L# and

We explain the definitions using examples from set, first for executions, then for specifications. Consider the execution on the left below. The derived lts is given on the right.

The states of the lts are cuts of the execution. The labels on transitions are *dependent* cuts. The requirements for execution transitions relate the source p, target q and label v. The leftmost requirements state that the target state must extend both the source and the label; thus the target state must be a combination of events and order from source and label. The middle requirements state that the maximal elements of the label must be new in the target; only the maximal elements of the label are added when moving from source to target. The upper right requirement states that the non-maximal order of the label must be respected by the source; thus the causal history reported by the label cannot contradict the causal history of the source. The lower right requirement ensures that maximal elements of the label are also maximal in the target. The restriction to dependent cuts explains the labels on transitions (-0-+0) +1 −→i (-0-+0); +1 and (-0-+0); (✓0-+1); ✓0 (-0+0);✓0 −−−−−−→i (-0-+0); (✓0-+1). By definition, there is a selftransition labelled with the empty lvo at every state; we elide these transitions in drawings.

The specification lts for set is infinite, of course. To illustrate, below we give two sub-ltss with limitations on mutators. On the left, we only allow +0 and +1. On the right, we only allow +0 and -0 and only consider the case in which there is at most one alternation between them. The states are shown using their canonical representatives. Because of the number of transitions, we show all dependent accessors as a single transition, with labels separated by commas.

The requirements for specification transitions are similar to those for implementations, but the states are equivalence classes over specification strings: with source [σ] and target [τ ]. There is a transition between the states if there are members of the equivalence classes, σ and τ , that satisfy the requirements. Since these are total orders, the leftmost requirements state that there must be linearizations of the source and label that are subsequences of the target. Similarly, the upper right requirement states that the non-maximal order of the label must be respected by the source; thus we have +0 +0-0 −−→s +0-0 but not +0 -0+0 −−→s σ, for any σ. The use of sub-order rather than subsequence allows +0-0 +0-0 −−→s +0-0-0 but prevents nonsense transitions such as +0-0 +0-0 −−→s -0+0-0. Because the states are total orders, we drop the implementation lts requirement that maximal events of the label must be maximal in the target. If we were to impose this restriction, we would disallow -0 +0 −→s +0-0.

It is worth noting that the specification of the add-wins set removes exactly three edges from the right lts: ε -0|+0 −−−→s +0-0, +0 -0 −→s +0-0, and -0 +0 −→s +0-0.

*Refinement.* Refinement is a functional form of simulation (Hoare 1972; Lamport 1983; Lynch and Vaandrager 1995). Let P = SP , p0, −→P and Q = SQ, q0, −→Q be ltss. A function f : SP → SQ is a *(strong) refinement* if p v −→P p and f(p) = q imply that there exist w =iso v and q ∈ SQ such that q w −→Q q and f(p ) = q . Then P *refines* Q (notation P ∼ ❁ Q) if there exists a refinement f : SP → SQ such that the initial states are related, *i.e.*, f(p0) = q0.

We now prove that sec can be characterized as a refinement. We write p0 −→∗ P pn when pn is reachable from p0 via a finite sequence of steps pi u*i* −→P pi+1.

Theorem 1. u *is* EC *for the specification* Σ *iff* lts(u) ∼ ❁ lts(Σ)*.*

*Proof.* For the forward direction, assume u is *EC* and therefore there exists a function τ : cuts#(u) → Σ such that ∀E ∈ cuts#(u). τ (E) is a linearization of E. For each cut p ∈ cuts(u), we start with the dependent restriction, p#. We further restriction attention to mutators, p#**M**. The required refinement maps p to the equivalence class of the linearization of p#**M**chosen by τ : f(p) - = [τ (p # **M**)]. We abuse notation below by identifying each equivalence class with a canonical element of the class.

We show that p v −→i q implies f(p) ≤obs f(q). Since p ⊆ q, we deduce that p # **M** ⊆ q # **M** and by monotonicity, f(p) = τ (p # **M**) ≤obs τ (q # **M**) = f(q).

We show that p v −→i q implies τ (v) ≤obs f(q). Suppose v only contains mutators. Since v ⊆ q, we deduce that v ⊆ q # **M** and by monotonicity, τ (v) ≤obs τ (q # **M**) = f(v). On the other hand, suppose v contains the nonmutator a. Let A = **M** ∪ {a}. Since v ⊆ q, we deduce that v **M** ⊆ q # A. By monotonicity, τ (v **M**) ≤obs τ (q A). Since τ (q A) = τ (q **M**), we have τ (v **M**) ≤obs τ (q **M**) = f(q), as required.

Thus f(p) v −→s f(q), completing this direction of the proof.

For the reverse direction, we are given a refinement f : cuts(u) → Σ/∼. For any p ∈ cuts#(u), define τ (p) to be a string in the equivalence class f(p) that includes any non-mutator found in p.

We first prove that τ (p) is a linearization of p. A simple inductive proof demonstrates that for any p ∈ cuts#(u), there is a transition sequence of the form ∅ −→∗ i p −→i p. Thus, we deduce from the label on the final transition into p that the τ (p) related to p is a linearization of p.

We now establish monotonicity. A simple inductive proof shows that for any p, q ∈ cuts(u), p ⊆ q implies p −→∗ i q. Thus τ (p) ≤obs τ (q), by the properties of f and the definition of τ .

*Composition.* Given two *non-interacting* data structures whose replicated implementations satisfy their sequential specifications, the implementation that combines them satisfies the interleaving of their specifications. We formalize this as a composition theorem in the style of Herlihy and Wing (1990).

Given an execution u and L ⊆ **L**, write u L for the execution that results by restricting u to events with labels in L: u L = u {e ∈ Eu | λu(e) ∈ L}. This notation lifts to sets in the standard way: U L = u∈U {u L}. Write u sec Σ to indicate that u is sec for Σ.

Theorem 2 (Composition). *Let* L1 *and* L2 *be mutually independent subsets of* **L***. For* i ∈ {1, 2}*, let* Σi *be a specification with labels chosen from* Li*, such that* Σ1 - Σ2 *is also a specification.

The proof is immediate. Since L1 and L2 are mutually independent, any interleaving of the labels will satisfy the definition.

*Abstraction.* We describe a process algebra with parallel composition and restriction and establish congruence results. We ignore syntactic details and work directly with ltss. Replica identities do not play a role in the definition; thus, we permit implicit mobility of the client amongst replicas with the only constraint being that the replica has at least as much history on the current item of interaction as the client. This constraint is enforced by the synchronization of the labels, defined below. While the definition includes the case where the client itself is replicated, it does not provide for out-of-band interaction between the clients at different replicas: All interaction is assumed to happen through the data structure.

The relation | is defined between ltss so that P | Q describes the system that results when client P interacts with data structure Q. For ltss P and Q, define −→× inductively, as follows, where ∅ represents the empty lvo.

$$\begin{array}{llll} q \stackrel{v}{\xleftarrow{v}}\_{Q} q'\\ \hline \langle p,q\rangle \stackrel{v}{\underset{-\infty}{\longleftarrow}}\_{\times} \langle p,q'\rangle \end{array} \quad \begin{array}{llll} p \stackrel{v}{\underset{-\infty}{\longleftarrow}}\_{P} p' & q \stackrel{w}{\underset{-\infty}{\longleftarrow}}\_{Q} q'\\ \hline \langle p,q\rangle \stackrel{\mathfrak{h}}{\longleftarrow}\_{\times} \langle p',q'\rangle \end{array} \exists v' = \mathsf{i\_0} \ v . \; v' \subseteq w \text{ and } \mathsf{max}(v') = \mathsf{max}(w) \ \langle p,q\rangle \stackrel{\mathfrak{h}}{\longleftarrow}\_{\times} \langle p,q'\rangle \end{array}$$

Let S× = {p, q | ∃p , q . p, q −→∗ × p , q and ∃v, p. p v −→P p}

$$P \parallel Q = \begin{cases} \{ \langle S\_{\times}, \langle p\_0, q\_0 \rangle, \longleftrightarrow\_{\times} \rangle \} & \text{if } S\_{\times} \text{ is non-empty} \\ \emptyset & \text{otherwise} \end{cases}$$

The | operator is asymmetric between the client and data structure in two ways. First, note that every action of the client must be matched by the data structure. The condition of client quiescence in the definition of S×, that all of the actions of the client P must be matched by Q; otherwise P | Q = ∅. However, the first rule for −→× explicitly permits actions of the data structure that may not be matched by the client. This asymmetry permits the composition of the data structure with multiple clients to be described incrementally, one client at a time. Thus, we expect that (P1 | P2) | Q -P1 | (P2 | Q).

Second, note that right rule for −→× interaction permits the data structure Q to introduce order not found in the clients. This is clearly necessary to ensure that that the composition of client ✓0|+0 with the set data structure is nonempty. In this case, the client has no order between +0 and ✓0 whereas the data structure orders ✓0 after +0. In this paper, we do not permit the client to introduce order that is not seen in the data structure. For a discussion of this issue, see (Jagadeesan and Riely 2015).

We can also define restriction for some set A ⊆ **L** of labels, a lá CCS. P\A = SP , p0, {p, v, q|p, v, q ∈ ( −→P ) and labels(v) ∩ A = ∅}. The definitions lift to sets: P | Q = P ∈P, Q∈Q P | Q and P\A = {(P\A) | P ∈ P}.

Lemma 3. *If* P ∼ ❁ P *and* Q ∼ ❁ Q *then* P | Q ∼ ❁ P | Q *and* P\A ∼ ❁ P \A*.*

It suffices to show that: P ∼ ❁ lts(u) implies P | lts(u) ∼ ❁ P | lts(Σ). The proof proceeds in the traditional style of such proofs in process algebra. We illustrate by sketching the case for client parallel composition.  The proof proceeds by constructing a "product" refinement S relation of the identity on the states of P with f, *i.e.*: f(q) = q implies p, qSp, q .

Thus, an sec implementation can be replaced by the specification.

Theorem 4 (Abstraction). *If* u *is* sec *for* Σ*, then* P | lts(u) ∼ ❁ P | lts(Σ)*.*

### 6 A Replicated Graph Algorithm