Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs that Use Concurrent Objects

TL;DR

This paper explores strong linearizability in concurrent objects, framing it as a form of observational refinement that preserves hyperproperties like security and probability distributions, and introduces strong observational refinement as a more general, hyperproperty-preserving concept.

Contribution

It introduces strong observational refinement, a generalization of strong linearizability, which preserves hyperproperties and is characterized by forward simulations, enabling better reasoning about concurrent programs.

Findings

Strong observational refinement generalizes strong linearizability.

Strong linearizability is equivalent to forward simulation.

It allows compositional reasoning about concurrent objects and hyperproperties.

Abstract

It has been observed that linearizability, the prevalent consistency condition for implementing concurrent objects, does not preserve some probability distributions. A stronger condition, called strong linearizability has been proposed, but its study has been somewhat ad-hoc. This paper investigates strong linearizability by casting it in the context of observational refinement of objects. We present a strengthening of observational refinement, which generalizes strong linearizability, obtaining several important implications. When a concrete concurrent object refining another, more abstract object - often sequential - the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This means that trace properties of a program using the concrete object can be proved by considering the program with the abstract object. This, however, does not hold for hyperproperties, including many security properties and probability distributions of events. We define strong observational refinement, a strengthening of refinement that preserves hyperproperties, and prove that it is equivalent to the existence of forward simulations. We show that strong observational refinement generalizes strong linearizability. This implies that strong linearizability is also equivalent to forward simulation, and shows that strongly linearizable implementations can be composed both horizontally (i.e., locality) and vertically (i.e., with instantiation). For situations where strongly linearizable implementations do not exist (or are less efficient), we argue that reasoning about hyperproperties of programs can be simplified by strong observational refinement of abstract objects that are not necessarily sequential.

Equations

$$T(P\times O_1)|{\Sigma }_p\subseteq T(P\times O_2)|{\Sigma }_p$$

$$S_1$$

$$S_2$$

$$T(P\times O_1,S_1)|{\Sigma }_p=T(P\times O_2,S_2)|{\Sigma }_p$$

$$(\exists \tau \in T.\text{low1}(\tau )\ne \text{high}(\tau ))\wedge (\exists \tau \in T.\text{low2}(\tau )\ne \text{high}(\tau ))$$

$$S_1(a_0\cdot \dots \cdot a_{k-1})$$

$$S_1(a_0\cdot \dots \cdot a_{k-1}[\cdot record(a_{k-1})])$$

$$a_{k-1}\notin {\Sigma }_p$$

$$S_1(a_0\cdot \dots \cdot a_{k-1}\cdot guess(H))$$

$$S_{2}(\epsilon)=S_{1}(\epsilon)\hskip 28.45274ptS_{2}(\overline{\tau})=\left\{\begin{array}[]{ll}S_{1}(\tau),\mbox{if $S_{1}(\tau)\subseteq\Sigma_{p}$}\\[2.84526pt] F(S_{1}(\tau)),\mbox{otherwise}\end{array}\right.$$

$$a\in C⟹h^{\prime }=h\cdot a\text{mbox}and{h}_s^{\prime }=h_s$$

$$\displaystyle a\in R\implies h^{\prime}=h\cdot a\mbox{ and $h_{s}^{\prime}=h_{s}$ and $a$ occurs in $h_{s}^{\prime}$}$$

$$\displaystyle a=lin(k)\implies h^{\prime}=h\mbox{ and $h_{s}^{\prime}=h_{s}\cdot call(m,d_{1},k)\cdot ret(m,d_{2},k)$, for some $m$, $d_{1}$, and $d_{2}$.}$$

$$\underset{\text{r}\in \{\text{r1},\text{r2}\}}{\bigwedge }\mathsf{valid}(\text{r},\text{pc})\wedge \mathsf{fst}(\text{r2},\text{n})\le \mathsf{fst}(\text{r1},0)\wedge \mathsf{last}(\text{snaps})=\text{mem}\wedge (\text{pc}=10⟹\text{r1}\in \text{snaps})$$

Full text

\reservestyle\semanticdomain

\semanticdomain Methods[M], Vals[V], Labels[L], Ops[I], Acts[A],

\reservestyle\proglangkeyword\xspace

Putting Strong Linearizability in Context:

Preserving Hyperproperties in

Programs that Use Concurrent Objects

Hagit Attiya1

  

Constantin Enea2

( 1Technion - Israel Institute of Technology, Israel

hagit@cs.technion.ac.il

2Université de Paris, IRIF, CNRS, Paris, France

cenea@irif.fr )

It has been observed that linearizability, the prevalent consistency condition for implementing concurrent objects, does not preserve some probability distributions. A stronger condition, called strong linearizability has been proposed, but its study has been somewhat ad-hoc. This paper investigates strong linearizability by casting it in the context of observational refinement of objects. We present a strengthening of observational refinement, which generalizes strong linearizability, obtaining several important implications.

When a concrete concurrent object refines another, more abstract object—often sequential—the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This means that trace properties of a program using the concrete object can be proved by considering the program with the abstract object. This, however, does not hold for hyperproperties, including many security properties and probability distributions of events.

We define strong observational refinement, a strengthening of refinement that preserves hyperproperties, and prove that it is equivalent to the existence of forward simulations. We show that strong observational refinement generalizes strong linearizability. This implies that strong linearizability is also equivalent to forward simulation, and shows that strongly linearizable implementations can be composed both horizontally (i.e., locality) and vertically (i.e., with instantiation).

For situations where strongly linearizable implementations do not exist (or are less efficient), we argue that reasoning about hyperproperties of programs can be simplified by strong observational refinement of non-atomic abstract objects.

1 Introduction

Abstraction is key to the design and verification of large, complicated software. In concurrent programs, featuring intricate interactions between multiple threads, abstraction is often used to encapsulate low-level shared memory accesses within high-level abstract data types, called concurrent objects. Arguing about properties of such a program $P$ is greatly simplified by considering a concurrent object as a refinement of another, more abstract one: a concrete object $O_{1}$ is said to observationally refine another, abstract object $O_{2}$ if any behavior $P$ can observe with $O_{1}$ is also observed by $P$ with $O_{2}$. When $O_{2}$ is an atomic object, in which each operation is applied in exclusion, observational refinement is equivalent to linearizability [5, 12].111 Linearizability [16] states that a concurrent execution of operations corresponds to some serial sequence of the same operations permitted by the specification.

Intuitively, linearizability, and more generally, observational refinement, seem to imply that anything we can prove about $P$ with $O_{2}$ also holds when $P$ executes with $O_{1}$. This is indeed the case when considering trace properties, i.e., properties that are specified as sets of traces, in particular, safety properties.

Unfortunately, many interesting properties cannot be specified as properties of individual traces, i.e., as trace properties. Notable examples are security properties such as noninterference [13], stipulating that commands executed by users with high clearance have no effect on system behavior observed by users with low clearance. Other examples are quantitative properties like bounds on the probability distribution of events, e.g., the mean response time over sets of executions. Indeed, while the fact that the average response time of an operation in an execution is smaller than some bound $X$ is a trace property, the requirement that the average response time over all executions is smaller than $X$ cannot be stated as a trace property.

Hyperproperties [9], namely, sets of sets of traces, allow to capture such expectations. By definition, every property of system behavior (for systems modeled as trace sets) can be specified as a hyperproperty. It is known that observational refinement does not preserve hyperproperties [18], in general. More recently, it has been shown that linearizability does not preserve probability distributions over traces [14], allowing an adversary scheduler additional control over the possible outcomes of a distributed randomized program. (An example appears in Section 2.)

This paper defines the notion of strong observational refinement, relates it to hyperproperties, and shows its equivalence to forward simulations. We show that strong observational refinement generalizes strong linearizability [14].222 Strong linearizability requires that the linearization of a prefix of a concurrent execution is a prefix of the linearization of the whole execution, see Section 5. We also explore the possibility of using—instead of the classical sequential specifications—concurrent specifications, which are nevertheless simpler.

To explain our results in more detail, consider a labeled transition system (LTS) that, intuitively, represents all the executions of the object under the most general client (that may call methods in any order and from any thread). A state of the LTS corresponds to a state of the object and transitions correspond to method calls/returns, or internal steps within a method invocation. A sequential specification corresponds to a concurrent object where essentially, method bodies consist of a single atomic step that acts according to the sequential specification (hence, they are totally ordered in time during any execution).

An LTS $O_{1}$ observationally refines an LTS $O_{2}$ if and only if the histories (i.e., sequences of call/return actions) generated by $O_{1}$ are included in those generated by $O_{2}$ [5]. In this way, observational refinement of two LTSs reduces to a inclusion between their traces, when projected over some alphabet $\Gamma$ (in this case, $\Gamma$ is the set of call/return actions), called $\Gamma$-refinement.

A forward simulation maps every step of $O_{1}$ to a sequence of steps of $O_{2}$, starting from the initial state of $O_{1}$ and advancing in a forward manner; a backward simulation is similar, but it goes in the reverse direction, from end states back to initial states. When proving linearizability, an important special case of forward simulation is the identification of fixed linearization points. A forward/backward simulation can be parameterized by an alphabet $\Gamma$, in which case the sequence of steps of $O_{2}$ associated to a step of $O_{1}$ should contain a step labeled by an action $a\in\Gamma$ if and only if the step of $O_{1}$ is also labeled by $a$. It is known [17] that $\Gamma$-refinement holds if and only if there is a combination of $\Gamma$-forward and $\Gamma$-backward simulations from $O_{1}$ to $O_{2}$; a forward simulation suffices when the projection of $O_{2}$ on $\Gamma$ is deterministic. (See Section 3.)

The notion of strong observational refinement relies on the concept of a deterministic scheduler that resolves the non-determinism introduced for instance, from the execution of internal actions by parallel threads (it is similar to the notion of strong adversary introduced in the context of randomized algorithms [4]). $O_{1}$ strongly (observationally) refines $O_{2}$ if a program $P$ running under a deterministic schedule with $O_{1}$ makes the same observations as when $P$ runs with $O_{2}$ with a possibly-different deterministic schedule. (The complete definition appears in Section 4.) We prove that strong observational refinement implies the existence of a forward simulation. The converse direction is fairly straightforward, proving the equivalence of these two notions, and imply compositional proof methodologies. (These results appear in Section 5.) By relating strong linearizability to strong observational refinement, we prove that a concrete object is a strong linearization of an atomic object if and only if there is an appropriate forward simulation between the two (Appendix C). This immediately implies methods for composing strongly linearizable concurrent objects.

To address situations where there is no concrete object that strongly linearizes a particular atomic object [15, 10], or in cases where such an object is less efficient, we suggest concrete objects that strongly refine other, more abstract objects that still expose some concurrency. This follows [6] and allows to simplify reasoning about randomized programs even when using objects like the Herlihy&Wing queue [16] or snapshot objects [1], which are not strongly linearizable. For example, in the case of atomic snapshots, the abstract object that obtains several instantaneous snapshots during the scan operation and then arbitrarily returns one of them (see Section 6). Arguing about a program using this abstract object is simpler, while still exposing the power of an adversarial scheduler to manipulate the responses of a scan.

2 Motivating Example: A Stack Implementation that Leaks Information

When an object $O_{1}$ refines a specification object $O_{2}$, any safety property of a program $P$ using $O_{2}$ (that refers only to $P$’s state and is agnostic to the internal state of the object $O_{2}$) is preserved when $O_{2}$ is replaced by its refinement $O_{1}$. However, refinement does not preserve hyperproperties [9], i.e., properties of sets of traces.

We explain this issue by considering noninterference [13] in the program of Figure 1. This program invokes methods of a concurrent stack, and we wish to show that independently of the thread scheduler, none of the low clearance variables low1 and low2 can leak the value of the high clearance variable ${\tt high}$, i.e., it is impossible to define a thread scheduler which admits only executions where ${\tt low1}={\tt high}$ or only executions where ${\tt low2}={\tt high}$. A precise notion of scheduler will be defined below, but for now, it is enough to think of a thread scheduler as a monitor that chooses to activate threads depending on the history of the execution. This property is satisfied by the program when invoking an atomic concurrent stack. Indeed, assuming that push(0) is scheduled before the one of push(1) (the other case is similar), then either (i) push(2) is scheduled before at least one of the pop invocations, and then, ${\tt low1},{\tt low2}\in\{1,2\}$ which shows that none of these two variables equals the value of ${\tt high}$ when ${\tt high}=0$, or (ii) push(2) is scheduled after the pop invocations, and then, the scheduler admits executions where ${\tt low1}=b_{1}$, ${\tt low2}=b_{2}$, and ${\tt high}=0$ if and only if it admits executions where ${\tt low1}=b_{1}$, ${\tt low2}=b_{2}$, and ${\tt high}=1$ (for $b_{1},b_{2}\in\{0,1,2\}$).

This property is however not satisfied by this program when using the concurrent stack of Afek et al. [2]. This stack stores the elements into an infinite array items; a shared variable range keeps the index of the first unused position in items. The push method stores the input value in the array while also incrementing range (the details are irrelevant for our example). The pop method first reads range and then traverses the array backwards starting from this position, until it finds a position storing a non-null element (array cells can be nullified by concurrent pop invocations). It atomically reads this element and stores null in its place. If the pop reaches the bottom of the array without finding non-null cells, then it returns that the stack is empty. Unlike the case of atomic stacks, Figure 2 shows a thread scheduler where low1 stores the value of high. This scheduler imposes that push(0) executes before push(1) (so that 0 occurs before 1 in the array items),333 A similar scheduler can be defined when push(1) executes before push(0). and then preempts pop invocations just after reading the value of range which equals 1 (assuming the array indexing starts at 0). Then, it schedules the third thread and, depending on the value of high, it schedules the rest of the pop invocations such that the pop in the first thread extracts a value which equals high. This ensures that low1 == high.

This shows that noninterference in programs invoking the atomic stack is not preserved when the latter is replaced by the concurrent stack of Afek et al. [2], although the latter is a refinement of the atomic stack. Section 4 presents a stronger notion of observational refinement that preserves hyperproperties and in particular, noninterference.

3 Modelling Concurrent Objects as Labeled Transition Systems

Labeled transition systems (LTS) capture shared-memory programs with an arbitrary number of threads, abstracting away the details of any particular programming system irrelevant to our development.

An LTS $A=(Q,\Sigma,s_{0},\delta)$ over the possibly-infinite alphabet $\Sigma$ is a possibly-infinite set $Q$ of states with initial state $s_{0}\in Q$, and a transition relation $\delta\subseteq Q\times\Sigma\times Q$. The $i$th symbol of a sequence $\tau\in\Sigma^{*}$ is denoted $\tau_{i}$, and $\epsilon$ is the empty sequence. An execution of $A$ is an alternating sequence of states and transition labels (also called actions) $\rho=s_{0},a_{0},s_{1}\ldots a_{k-1},s_{k}$ for some $k>0$ such that $(s_{i},a_{i},s_{i+1})\in\delta$ for each $0\leq i<k$. We write $s_{i}\xrightarrow{a_{i}\ldots a_{j-1}}_{A}s_{j}$ as shorthand for the subsequence $s_{i},a_{i},...,s_{j-1},a_{j-1},s_{j}$ of $\rho$. (in particular $s_{i}\xrightarrow{\epsilon}s_{i}$).

The projection $\tau|\Gamma$ of a sequence $\tau$ is the maximum subsequence of $\tau$ over alphabet $\Gamma$. This notation is extended to sets of sequences as usual. A trace of $A$ is the projection $\rho|\Sigma$ of an execution $\rho$ of $A$. The set of executions, resp., traces, of an LTS $A$ is denoted by $\mathit{E}(A)$, resp., $\mathit{T}(A)$. An LTS is deterministic if for any state $s$ and any sequence $\tau\in\Sigma^{*}$, there is at most one state $s^{\prime}$ such that $s\xrightarrow{\tau}s^{\prime}$. More generally, for an alphabet $\Gamma\subseteq\Sigma$, an LTS is $\Gamma$-deterministic if for any state s and any sequence $\tau\in\Gamma^{*}$, there is at most one state $s^{\prime}$ such that $s\xrightarrow{\tau^{\prime}}s^{\prime}$ and $\tau$ is a subsequence of $\tau^{\prime}$.

An object is a deterministic LTS over alphabet $C\cup R\cup\Sigma_{o}$ where $C$, resp., $R$, is the set of call, resp., return, actions, and $\Sigma_{o}$ is an alphabet of internal actions. Formally, a call action $call(m,d,k)$, resp., a return action $ret(m,d,k)$, combines a method $m$ and argument, resp., return value, $d$ with an operation identifier $k$. Operation identifiers are used to pair call and return actions. We assume that the traces of an object satisfy standard well-formedness properties, e.g., return actions correspond to previous call actions. Given a standard description of an object implementation as a set of methods, its LTS represents the executions of its most general client (that may call methods in any order and from any thread). The states of the LTS represent the shared state of the object together with the local state of each thread. The transitions correspond to statements in the method bodies (in which case they are labeled by internal actions in $\Sigma_{o}$), or call and return actions. For simplicity, we ignore the association of method invocations to threads since it is irrelevant to our development. A trace $\tau$ of an object $O$ projected over call and return actions is called a history of $O$, and it is denoted by $\mathit{hist}(\tau)$. The set of histories admitted by an object $O$ is denoted by $H(O)$. Call and return actions $call(m,\_,k)$ and $ret(m,\_,k)$ are called matching when they contain the same operation identifier. A call action is called unmatched in a history $h$ when $h$ does not contain the matching return. A history $h$ is called sequential if every call $call(m,d,k)$ is immediately followed by the matching return $ret(m,\_,k)$. Otherwise, it is called concurrent.

Linearizability [16] is a standard correctness criterion for concurrent objects expressing conformance to a given sequential specification. This criterion is based on a relation $\sqsubseteq$ between histories: $h_{1}\sqsubseteq h_{2}$ iff there exists a well-formed execution $h_{1}^{\prime}$ obtained from $h_{1}$ by appending return actions that correspond to unmatched call actions in $h_{1}$ or deleting unmatched call actions, such that $h_{2}$ is a permutation of $h_{1}^{\prime}$ that preserves the order between return and call actions, i.e., a given return action occurs before a given call action in $h_{1}^{\prime}$ iff the same holds in $h_{2}$. We say that $h_{2}$ is a linearization of $h_{1}$. A history $h_{1}$ is called linearizable w.r.t. an object $O_{2}$ iff there exists a sequential history $h_{2}\in H(O_{2})$ such that $h_{1}\sqsubseteq h_{2}$. An object $O_{1}$ is linearizable w.r.t. $O_{2}$, written $O_{1}\sqsubseteq O_{2}$, iff each history $h_{1}\in H(O_{1})$ is linearizable w.r.t. $O_{2}$.

Linearizability has been shown equivalent to a criterion called observational refinement which states that every behavior of every program possible using a concrete object would also be possible were the abstract object used instead [5, 12] (the precise meaning of behavior is given below). Actually, this result holds only when the abstract object is atomic, i.e., it admits every history which is linearizable w.r.t. a set of sequential histories $Seq$ (formally, $H(O)=\{h:\exists h^{\prime}\in\mathit{Seq}.\ h\sqsubseteq h^{\prime}\}$). Intuitively, an atomic object corresponds to an implementation where the methods of a sequential object are guarded by global-lock acquisition.

A program is a deterministic LTS over alphabet $C\cup R\cup\Sigma_{p}$ where $\Sigma_{p}$ is an alphabet of program actions. Program actions can be interpreted for instance, as assignments to some program variables which are disjoint from the variables used by the object, or as different outcomes of a random choice. Call and return actions represent the interaction between the program and the object. The executions of a program $P$ with an object $O$ are obtained as the executions of the LTS product $P\times O$ 444The product $A_{1}\times A_{2}$ of two LTSs is defined as usual, respecting $E(A_{1}\times A_{2})|(\Sigma_{1}\cap\Sigma_{2})=E(A_{1})|\Sigma_{2}\cap E(A_{2})|\Sigma_{1}$.. As program and object alphabets only intersect on call and return actions, our formalization supposes that programs and objects communicate only through method calls and returns, and not, e.g., through additional shared random-access memory.

Observational refinement between objects $O_{1}$ and $O_{2}$ means that any “observation” extracted from a program execution possible with $O_{1}$ (referred to as a “concrete” object), is also possible with $O_{2}$ (referred to as the “specification”), where an “observation” in this context is the projection over the program actions.

Definition 3.1**.**

The object $O_{1}$ observationally refines $O_{2}$, written $O_{1}\leq O_{2}$, iff

[TABLE]

for all programs $P$ over alphabet $\Sigma_{p}\cup C\cup R$.

The following theorem relates observational refinement to a standard notion of refinement between LTSs, defined roughly as inclusion of traces, in the context of concurrent objects.555 This relationship has been shown under natural assumptions about objects and programs [5]. For instance, concerning objects, it is assumed that call actions cannot be disabled and they cannot disable other actions (they can be reordered to the left while preserving the computation), and return actions cannot enable other actions. For two LTSs $A_{1}$ and $A_{2}$, we say that $A_{1}$ refines $A_{2}$ when $T(A_{1})\subseteq T(A_{2})$. More generally, for an alphabet $\Gamma$, $A_{1}$ $\Gamma$-refines $A_{2}$ when $T(A_{1})|\Gamma\subseteq T(A_{2})|\Gamma$. By an abuse of notation, $A_{1}\subseteq_{\Gamma}A_{2}$ denotes the fact that $A_{1}$ $\Gamma$-refines $A_{2}$ (we will omit $\Gamma$ when it is understood from the context). Intuitively, the alphabet $\Gamma$ represents a set of actions which are “observable” in both $A_{1}$ and $A_{2}$, the actions not in $\Gamma$ are considered to be “internal” to $A_{1}$ or $A_{2}$. Observational refinement is equivalent to $(C\cup R)$-refinement which means that the histories of the concrete object are included in those of the specification (note that “plain” refinement would not hold because the internal actions may differ).

Theorem 3.2** ([5, 12]).**

$O_{1}\leq O_{2}$* iff $O_{1}\subseteq_{C\cup R}O_{2}$. If $O_{2}$ is atomic, then $O_{1}\leq O_{2}$ iff $O_{1}\sqsubseteq O_{2}$.*

In the rest of the paper, since observational refinement and ($C\cup R$)-refinement are equivalent, we will not make the distinction between the two and refer to both as refinement.

4 Strong Observational Refinement

As discussed in Section 2, refinement does not preserve hyperproperties, which are properties of sets of traces and not individual traces as in the case of safety properties. In the following, we define a stronger notion of observational refinement that preserves such properties, using a notion of scheduler that is actually just a mechanism for resolving the non-determinism induced by internal actions, irrespectively of whether it comes from executing a set of parallel threads.

A scheduler for a deterministic LTS $A=(Q,\Sigma,s_{0},\delta)$ over alphabet $\Sigma$ is a function $S:\Sigma^{*}\rightarrow 2^{\Sigma}$ which prescribes a possible set of next actions to continue an execution based on a sequence of previous actions. A trace $\tau=a_{0}\cdot\ldots\cdot a_{k-1}$ is consistent with a scheduler $S$ if $a_{i}\in S(a_{0}\cdot\ldots\cdot a_{i-1})$ for all $0\leq i<k$ (where by an abuse of notation, $a_{0}\cdot a_{-1}$ represents the empty sequence). The set of executions of an LTS $A$ consistent with a scheduler $S$ can be defined using an LTS which is the product between $A$ and an LTS $A_{S}$ whose states are sequences in $\Sigma^{*}$ and the transitions link a state $\tau\in\Sigma^{*}$ to a state $\tau\cdot a\in\Sigma^{*}$ provided that $S(\tau)=a$ (such a transition is labeled by $a$). Let $T(A,S)$ denote the set of traces of $A$ consistent with $S$. A scheduler is admitted by $A$ if for every $k$, if $\tau=a_{0}\cdot\ldots\cdot a_{k-1}$ is a trace of $A$ consistent with $S$, then $S(a_{0}\cdot\ldots\cdot a_{k-1})$ is non-empty and every $a\in S(a_{0}\cdot\ldots\cdot a_{k-1})$ is enabled in the state $s_{k}$ with $s_{0}\xrightarrow{a_{0}\cdot\ldots\cdot a_{k-1}}_{A}s_{k}$.

A scheduler of an LTS $P\times O$ (the product of a program $P$ and an object $O$) is called deterministic when it fixes in a unique way the actions of $O$ to continue an execution, i.e., for every sequence $\tau$, $S(\tau)\subseteq\Sigma_{p}$ or $|S(\tau)|=1$ (where $\Sigma_{p}$ is the set of program actions). When program actions represent outcomes of random choices made by the program, a deterministic scheduler can be used to model a strong adversary [4] which schedules threads depending on those outcomes. An object $O_{1}$ strongly (observationally) refines an object $O_{2}$ if any deterministic schedule admitted by a program $P$ when using $O_{1}$ leads to exactly the same set of “observations” as a deterministic schedule admitted by $P$ were $O_{2}$ used instead. Formally,

Definition 4.1**.**

The object $O_{1}$ strongly (observationally) refines $O_{2}$, written $O_{1}\leq_{s}O_{2}$, iff

[TABLE]

for all programs $P$ over alphabet $\Sigma_{p}\cup C\cup R$.

A hyperproperty of a program $P$ over alphabet $\Sigma_{p}\cup C\cup R$ is a set of sets of sequences over $\Sigma_{p}$. For instance, the hyperproperty discussed in the context of the program in Figure 1 is the set of all sets $T$ s.t.

[TABLE]

where for any variable $x$, $x(t)$ is the value of $x$ at the end of trace $t$. A hyperproperty $\varphi$ is satisfied by a program $P$ with an object $O$, written $P\times O\models\varphi$, if $T(P\times O,S)|\Sigma_{p}\in\varphi$ for every deterministic scheduler $S$.

Theorem 4.2**.**

If $O_{1}\leq_{s}O_{2}$, then $P\times O_{2}\models\varphi$ implies $P\times O_{1}\models\varphi$ for every hyperproperty $\varphi$ of $P$.

This preservation result applies to probabilistic hyperproperties as well, for instance when reasoning about randomized consensus protocols [4]. Since a deterministic scheduler fixes in a unique way the object’s actions to continue an execution, probability distributions can be assigned only to actions which are internal to the program $P$. This holds for randomized protocols, where randomization is due to coin flip operations that are internal to the protocol and do not concern the behavior of the objects it invokes. Then, the probabilities associated with program actions can be encoded in the action names, thereby encoding probabilistic (hyper)properties as properties of (sets of) traces (see [9] for more details).

5 Characterizing Strong Refinement Using Forward Simulations

In general, proving refinement between two LTSs relies on simulation relations which roughly, are relations between the states of the two LTSs showing that one can mimic every step of the other one. Forward simulations show that every outgoing transition from a given state can be mimicked by the other LTS while backward simulations show the same for every incoming transition to a given state. Applying induction, forward simulations show that every trace of an LTS is admitted by the other LTS starting from initial states and advancing in a forward manner, while backward simulations consider the backward direction, from end states to initial states. It has been shown that ($\Gamma$-)refinement is equivalent to the existence of a composition of forward and backward simulations, and to the existence of only a forward simulation provided that $A_{2}$ is ($\Gamma$-)deterministic [17]. In the following, we show that strong observational refinement is equivalent to the existence of a forward simulation, which implies that refinement is strictly weaker than strong observational refinement (forward simulations do not suffice to establish refinement in general).

Definition 5.1**.**

Let $A_{1}=(Q_{1},\Sigma_{1},s_{0}^{1},\delta_{1})$ and $A_{2}=(Q_{2},\Sigma_{2},s_{0}^{2},\delta_{2})$ be two LTSs and $\Gamma$ an alphabet. A relation $F\subseteq Q_{1}\times Q_{2}$ is called a $\Gamma$-forward simulation from $A_{1}$ to $A_{2}$ iff $(s_{0}^{1},s_{0}^{2})\in F$ and:

• •

for all $s_{1},s_{1}^{\prime}\in Q_{1}$, $a\in\Sigma_{1}$, and $s_{2}\in Q_{2}$, such that $(s_{1},a,s_{1}^{\prime})\in\delta_{1}$ and $(s_{1},s_{2})\in F$, we have that there exists $s_{2}^{\prime}\in Q_{2}$ such that $(s_{1}^{\prime},s_{2}^{\prime})\in F$ and $s_{2}\xrightarrow{\tau}_{A_{2}}s_{2}^{\prime}$ and $\tau|\Gamma=a|\Gamma$.

A $\Gamma$-forward simulation states that every step of $A_{1}$ is simulated by a sequence of steps of $A_{2}$ (this sequence can be empty to allow for stuttering). Since it should imply that $A_{1}$ $\Gamma$-refines $A_{2}$, every step of $A_{1}$ labeled by an observable action $a\in\Gamma$ should be simulated by a sequence of steps of $A_{2}$ where exactly one transition is labeled by $a$ and all the other transitions are labeled by non-observable actions (this is implied by $\tau|\Gamma=a|\Gamma$). Also, every internal step of $A_{1}$ should be simulated by a sequence of internal steps of $A_{2}$.

An instantiation of forward simulations are linearizability proofs using the so-called “fixed linearization points”. Linearizability of a history can be proved by showing that each invocation can be seen as happening at some point, called linearization point, occurring somewhere between the call and return actions of that invocation. Then, the linearization points are fixed when they are mapped to a certain fixed set of statements (usually, one statement per method). This defines a mapping between steps of a concrete implementation and steps of an atomic object, i.e., those fixed statements map to linearization point actions in the atomic object and all the other statements correspond to stuttering steps of the atomic object, thereby defining a forward simulation between the two. As a side remark, backward simulation is necessary to prove linearizability w.r.t. atomic specifications, when linearization points depend on future steps in the execution, the Herlihy&Wing queue [16] being a classic example (Schellhorn et al. [20] present such a proof).

The easier direction is showing that forward simulations imply strong refinement. A forward simulation from $O_{1}$ to $O_{2}$ can be used to simulate any scheduler $S_{1}$ of a program $P$ using $O_{1}$ by a scheduler of the same program $P$ when using $O_{2}$. Program actions will be replayed exactly as in $S_{1}$ while the actions of $O_{2}$ simulating actions of $O_{1}$ can be chosen according to the forward simulation (see Appendix B).

Lemma 5.2**.**

If there exists a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$, then $O_{1}\leq_{s}O_{2}$.

We now prove our key technical result: strong observational refinement (from $O_{1}$ to $O_{2}$) implies the existence of a $(C\cup R)$-forward simulation (from $O_{1}$ to $O_{2}$). Since the latter implies refinement, a corollary of this result is that strong observational refinement implies observational refinement. Thus, we define a program $P$ which corresponds to the most general client (of $O_{1}$) and which uses particular program actions to guess the possible continuations of a given execution with call and return actions. Then, we define a scheduler $S_{1}$ which ensures that the executions of $P$ with $O_{1}$ are consistent with the guesses made by the program. By strong observational refinement, there exists a scheduler $S_{2}$ such that $P$ produces the same sequences of “guess” actions and call/return actions when using $O_{2}$ and constrained by $S_{2}$ as when using $O_{1}$ and constrained by $S_{1}$ (the preservation of call/return actions is not guaranteed explicitly by strong observational refinement, but it can be enforced using additional program actions used to record them). If $\Gamma$ is the union of the set of “guess” actions and the set of call/return actions, then the program $P$ used in conjunction with $O_{2}$ and constrained by the scheduler $S_{2}$ is $\Gamma$-deterministic. Therefore, there exists a forward simulation between the two variations of $P$. Because the program states are disjoint from the object states, this forward simulation between programs leads to a forward simulation between objects.

Lemma 5.3**.**

If $O_{1}\leq_{s}O_{2}$, then there exists a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$.

Proof.

Let $\Sigma_{p}=\{\mathit{record}({a}),\mathit{guess}({H}):a\in C\cup R,H\subseteq(C\cup R)^{*}\}$ be a set of program actions for recording a call/return action $a$ ($\mathit{record}({a})$) or guessing a set $H$ of possible continuations with sequences of call/return actions ($\mathit{guess}({H})$). We define a program $P$ with a single state and self-loop transitions labeled by all symbols in $\Sigma_{p}\cup C\cup R$, i.e., $P=(\{s_{0}\},\Sigma_{p}\cup C\cup R,s_{0},\delta)$ where $\delta(s_{0},\alpha,s_{0})$ for all $\alpha\in\Sigma_{p}\cup C\cup R$.

We define a deterministic scheduler $S_{1}$ which ensures that the guesses made by $P$ when using $O_{1}$ are correct, and that the call/return actions are tracked correctly using $\mathit{record}$ actions. To ensure the correctness of guesses, we define a mapping $\mathit{after}_{1}:Q_{1}\rightarrow 2^{(C\cup R)^{*}}$ which associates every state $s$ with the set of call/return sequences admitted from $s$, i.e., $\mathit{after}_{1}(s)=\{\sigma:\sigma\in(C\cup R)^{*},\exists s^{\prime}.\ s\xrightarrow{\tau}_{O_{1}}s^{\prime}\land\tau|(C\cup R)=\sigma\}.$

Let $S_{1}$ be a deterministic scheduler such that for every $a_{0},\ldots,a_{k-1}\in\Sigma_{1}$ and $k\geq 0$,

[TABLE]

Informally, the first rule enforces that every call/return action $a$ is followed by a program action $\mathit{record}({a})$. The second rule ensures that $S_{1}$ is permissive enough, i.e., it allows all the successors of the current object state that have different $\mathit{after}_{1}$ images (for a sequence $\sigma$, $\sigma[\cdot a]$ denotes a sequence where the character $a$ is optional). The third rule ensures that every $\mathit{guess}({H})$ is followed by an action leading to an object state $s$ with $H=\mathit{after}_{1}(s)$. Collectively, these last two cases ensure that every action $a$ of $O_{1}$ is preceded by a $\mathit{guess}({H})$ program action where $H$ is the set of call/return sequences admitted from the post-state of $a$.

Although $S_{1}$ does not admit all the executions of $O_{1}$ (because of the arbitrary choice of $a$ in the third case above), we show that the set of executions it admits simulate all the executions of $O_{1}$: let $O_{1}[S_{1}]$ be an LTS representing the set of executions of $O_{1}$ consistent with $S_{1}$ (obtained from the set of executions of $P$ consistent with $S_{1}$ by projecting out the program state and actions). We show that the relation $F_{1}$ between states of $O_{1}$ and $O_{1}[S_{1}]$, respectively, defined by $(s,s^{\prime})\in F_{1}$ iff $\mathit{after}_{1}(s)=\mathit{after}_{1}(s^{\prime})$, is a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{1}[S_{1}]$. The fact that it relates the initial object states $s_{0}^{1}$ and $s_{0}^{1}$ is trivial. Now, let $s,s_{1}\in Q_{1}$ and $a\in\Sigma_{1}$ such that $(s,a,s_{1})\in\delta_{1}$ and $(s,s^{\prime})\in F_{1}$. Using a simple induction on the length of executions, it can be shown that there exists a state $s_{1}^{\prime}$ with $\mathit{after}_{1}(s_{1})=\mathit{after}_{1}(s_{1}^{\prime})$ such that $(s^{\prime},b,s_{1}^{\prime})$ for some action $b$. If $a\in C\cup R$, then $b=a$ because otherwise, the continuations with call/return actions admitted from $s_{1}$ will be different from those admitted from $s_{1}^{\prime}$ (for instance, if $a$ is a call action and $b$ is an internal action, then the matching return action will be eventually enabled in executions starting from $s_{1}$ but not from $s_{1}^{\prime}$, at least not before $a$ occurs). For the same reason, if $a$ is an internal action, then $b$ is also an internal action. This concludes the proof that $F_{1}$ is a forward simulation.

Since $O_{1}\leq_{s}O_{2}$, there exists a scheduler $S_{2}$ such that $T(P\times O_{1},S_{1})|\Sigma_{p}=T(P\times O_{2},S_{2})|\Sigma_{p}$. Let $P[O_{2},S_{2}]$ denote the LTS representation of the set of executions of $P$ with $O_{2}$ and consistent with $S_{2}$ (explained in Section 4). It can be easily seen that $P[O_{2},S_{2}]$ is $\Sigma_{p}$-deterministic (the interleaving of a sequence of $\Sigma_{p}$ actions with internal actions of $O_{2}$ is uniquely determined by $S_{2}$ because it is a deterministic scheduler). Since $T(P[O_{1},S_{1}])|\Sigma_{p}\subseteq T(P[O_{2},S_{2}])|\Sigma_{p}$,666Note that $T(P\times O_{i},S_{i})$ and $T(P[O_{i},S_{i}])$ with $i\in\{1,2\}$ denote exactly the same set of traces. we get that there exists a $\Sigma_{p}$-forward simulation $F_{S_{1},S_{2}}$ from $P[O_{1},S_{1}]$ to $P[O_{2},S_{2}]$. Such a forward simulation defines a relation between states of $O_{1}$ and $O_{2}$, respectively, by removing the program state, i.e., $s_{1}$ and $s_{2}$ are related whenever $((s_{0},s_{1}),(s_{0},s_{2}))\in F_{S_{1},S_{2}}$. For simplicity, this relation is denoted by $F_{S_{1},S_{2}}$ as well. Because of the $\mathit{record}({a})$ actions in $\Sigma_{p}$, we get that $F_{S_{1},S_{2}}$ is a $(C\cup R)$-forward simulation from $O_{1}[S_{1}]$ to $O_{2}$. It is easy to check that $F_{1}\circ F_{S_{1},S_{2}}$ (where $\circ$ is the usual composition of relations) is a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$.

∎

The two lemmas above imply that:

Theorem 5.4**.**

$O_{1}\leq_{s}O_{2}$* iff there exists a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$.*

The fact that forward simulations are necessary for strong refinement allows to derive in a simple way compositional methods for proving strong refinement. In the following we consider the case of composed objects defined as a product of a fixed set of objects, and parametrized objects defined from a set of “base” objects which are considered as parameters.

We show that strong refinement is a local property, i.e., it holds for composed objects if and only if it holds for individual objects in this composition. As usual, we consider compositions of objects with disjoint states and sets of actions. Indeed, any forward simulation between composed objects can be “projected” to a set of forward simulations that hold between individual objects, and vice versa. We state this result for compositions of two objects, the extension to an arbitrary number of objects is obvious.

Theorem 5.5**.**

Let $O_{1}$ and $O_{2}$, resp., $O_{1}^{\prime}$ and $O_{2}^{\prime}$, be two objects over an alphabet $\Sigma$, resp., $\Sigma^{\prime}$, such that $\Sigma\cap\Sigma^{\prime}=\emptyset$. Then, $O_{1}\times O_{1}^{\prime}\leq_{s}O_{2}\times O_{2}^{\prime}$ iff $O_{1}\leq_{s}O_{2}$ and $O_{1}^{\prime}\leq_{s}O_{2}^{\prime}$.

Next, we consider the case of parametrized objects whose implementation is parametrized by a set of base objects, e.g., snapshot objects defined from a set of atomic registers. We show that if the parametrized object is a strong refinement of an abstract specification $S$ assuming that the base objects behave according to their own abstract specifications $S_{i}$, then instantiating any base object with an implementation that is a strong refinement of $S_{i}$ leads to an object which remains a strong refinement of $S$. Assuming for simplicity only one base object, a parametrized object $O$ can be formally defined as a product $O=S_{1}\times C$ where $S_{1}$ is the base object’s specification and $C$ is the context in which this object is used to derive the implementation of $O$ 777For a parametrized object $O=S_{1}\times C$, the alphabets of $S_{1}$ and $C$ share the call/return actions of $S_{1}$ (the base object) and the alphabet of $C$ contains the call/return actions of $O$. This is different from the the composition of two objects $O_{1}\times O_{1}^{\prime}$ where the alphabets of $O_{1}$ and $O_{1}^{\prime}$ are disjoint.. To distinguish parametrization from composition, we use $O[S_{1}]$ to denote an object parametrized by a base object $S_{1}$. The next result is an immediate consequence of the fact that the forward simulation admitted by the base object can be composed 888Here, we refer to classical composition of relations. with the one admitted by the parametrized object (assuming base object’s specification) to derive a forward simulation for the instantiation.

Theorem 5.6**.**

If $O[S_{1}]\leq_{s}S$ and $O_{1}\leq_{s}S_{1}$, then $O[O_{1}]\leq_{s}S$.

Finally, it can be shown that the existence of forward simulations is equivalent to strong linearizability [14] when concrete objects are related to atomic abstract objects. Thus, let $O_{2}$ be an atomic object defined by a set of sequential histories $\mathit{Seq}$, i.e., $H(O_{2})=\{h:\exists h^{\prime}\in\mathit{Seq}.\ h\sqsubseteq h^{\prime}\}$. We say that an object $O_{1}$ is strongly linearizable w.r.t. $O_{2}$, written $O_{1}\sqsubseteq_{s}O_{2}$, when there exists a function $f:T(O_{1})\rightarrow Seq$ such that (1) for any trace $\tau\in T(O_{1})$, $\mathit{hist}(\tau)\sqsubseteq f(\tau)$, and (2) $f$ is prefix-preserving, i.e., for any two traces $\tau_{1},\tau_{2}\in T(O_{1})$ such that $\tau_{1}$ is a prefix of $\tau_{2}$, $f(\tau_{1})$ is a prefix of $f(\tau_{2})$. It can be shown that the function $f$ induces a forward simulation and vice-versa (the proof is given in Appendix C).

Theorem 5.7**.**

If $O_{2}$ is atomic, then $O_{1}\sqsubseteq_{s}O_{2}$ iff there exists a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$.

6 Strong Observational Refinements of Non-Atomic Specifications

We demonstrate that many concurrent objects defined in the literature are strong observational refinements of much simpler abstract objects, even though not necessarily atomic. We focus on objects which are not strongly linearizable, since by Theorem 5.7, the latter are strong refinements of atomic objects.

Figure 3 lists an implementation of a snapshot object with two methods update(i,data) for writing the value data to a location i of a shared array mem, and scan() for returning a snapshot of the array mem.999This is a simplified version of the snapshot object defined by Afek et al. [1]. While the implementation of update is obvious, a scan operation performs several “collect” phases, where it reads successively all the cells of mem, until two consecutive phases return the same array.

This object does not admit a forward simulation towards the standard atomic specification where the method scan takes a single instantaneous snapshot of the entire array which is subsequently returned (it is not a strong refinement of such a specification). Intuitively, this holds because the linearization point of scan depends on future steps in the execution, e.g., a read in the second for loop is a linearization point only if it is not followed by updates on array cells before and after the current loop index. This is exactly the scenario in which backward simulations are necessary, intuitively, reading an execution backwards it is possible to identify precisely the linearization points of scan invocations. The impossibility of defining such a forward simulation is also a consequence of the fact that this object is not strongly linearizable [14].

However, this object is a strong refinement of the simpler “concurrent” specification given on the right of Figure 3 (see Appendix D). The implementation of update remains the same, while a scan operation performs a sequence of instantaneous snapshots of the entire array mem and returns any snapshot in this sequence. Compared to the implementation on the left, it is simpler because it does not allow that reading the array mem is interleaved with other operations. However, it is not atomic since an execution of scan contains more than one step. In comparison with the atomic specification, the sequence of snapshots in scan allows that an adversary (scheduler) decides on the return value “lazily” after observing other invocations, e.g., updates, exactly as in the concrete implementation. Therefore, the abstract specification in Figure 3 can be used while reasoning about hyperproperties of clients, which is not the case for the atomic specification.

Beyond snapshot objects, Bouajjani et al. [6] show that a similar simplification holds even for concurrent queues and stacks which are not strongly linearizable, e.g., Herlihy&Wing queue [16] and Time-Stamped Stack [11]. These objects admit forward simulations towards “concurrent” specifications where roughly, the elements are stored in a partially-ordered set instead of a sequence (which is consistent with the real-time order between the enqueues/pushes that added those elements). The enqueues/pushes have no internal steps, while the dequeues/pops have a single internal step which roughly, corresponds to a linearization point that extracts a minimal (for queues) or maximal (for stacks) element from the partially-ordered set. The stack of Afek at al. [2] can also be proved to be a strong refinement of such a specification. These forward simulations imply that these objects are strong refinements of their specifications.

7 Related Work and Discussion

An important contribution of our paper is to put the work on strong linearizability [10, 15, 14] in the context of standard results concerning hyperproperties [9, 8] and property-preserving refinements [3, 17, 18]. McLean [18] showed that refinements do not preserve security properties, which were later found to be instances of the more generic notion of hyperproperty [9]. By exploiting the equivalence between linearizability and refinement [5, 12], our paper clarifies that a stronger notion of linearizability is needed because standard linearizability does not preserve hyperproperties.

Our notion of strong observational refinement is a variation of the hyperproperty-preserving refinement introduced in [9], which takes into account the specificities of concurrent object clients. The relationship between forward simulations and preservation of hyperproperties has been investigated in [3]. They show that the existence of forward simulations is sufficient for preserving some specific class of hyperproperties (information-flow security properties like non-interference), corresponding to the straightforward direction of Theorem 5.4 (Lemma 5.3); they also show that their condition is not necessary in their context. In contrast, our work shows that the existence of forward simulations is both necessary and sufficient for preserving any hyperproperty in the context of concurrent object clients.

An important consequence of our results is that strong linearizability [14] is equivalent to the existence of a forward simulation towards an atomic specification. The equivalence to the well-studied notion of forward simulation immediately implies methods for composing concurrent objects, in particular, locality and instantiation. This stands in contrast to the effort needed to prove similar results in [14] and [19].

While [14] relates strong linearizability to an ad-hoc notion of reasoning about randomized programs when replacing objects by their atomic specifications, the equivalence we prove implies that strong linearizability is necessary and sufficient for preserving hyperproperties in this context. Note that forward simulations are more general than strong linearizability. Section 6 presents several objects which are not strongly linearizable, but which admit forward simulations towards non-atomic abstract specifications. Our results imply that it is sound to use such specifications when reasoning about hyperproperties of client programs. Moreover, as opposed to strong linearizability, forward simulations are applicable to interval-linearizable objects [7], which do not have any atomic specification, but are essentially LTSs as in our formalization.

Finally, Bouajjani et al. [6] show that intricate implementations of concurrent stacks and queues like Herlihy&Wing queue [16] and Time-Stamped Stack [11] admit forward simulations towards non-atomic abstract specifications, but they do not discuss the connection between existence of forward simulations and preservation of hyperproperties, which is the main contribution of our paper.

Our definition of strong observational refinement and its deep relation to forward simulations deepens our understanding of the role of strong linearizability in preserving hyperproperties. We plan to explore strong observational refinement of almost-atomic objects and develop additional proof methodologies. Also, our notion of strong observational refinement uses deterministic schedulers that model strong adversaries w.r.t. Aspnes’ classification [4], and it is interesting to explore variations of this notion that take into account other adversary models.

Appendix A Proof of Theorem 4.2

Proof.

Assume that $O_{1}\leq_{s}O_{2}$ and $P\times O_{2}\models\varphi$ for some hyperproperty $\varphi$ of $P$. Let $S_{1}$ be a deterministic scheduler admitted by $P\times O_{1}$. Since $O_{1}\leq_{s}O_{2}$, there exists a deterministic scheduler $S_{2}$ admitted by $P\times O_{2}$ such that $T(P\times O_{1},S_{1})|\Sigma_{p}=T(P\times O_{2},S_{2})|\Sigma_{p}$. Since, $P\times O_{2}\models\varphi$, we get that $T(P\times O_{2},S_{2})|\Sigma_{p}\in\varphi$, which implies that $T(P\times O_{1},S_{1})|\Sigma_{p}\in\varphi$. Therefore, $P\times O_{1}\models\varphi$. ∎

Appendix B Proof of Lemma 5.3

Proof.

Let $O_{1}=(Q_{1},\Sigma_{1},s_{0}^{1},\delta_{1})$ and $O_{2}=(Q_{2},\Sigma_{2},s_{0}^{2},\delta_{2})$ be two objects, and $F$ a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$. Let $P$ be a program and $S_{1}$ a deterministic scheduler admitted by $P\times O_{1}$. We define a deterministic scheduler $S_{2}$ admitted by $P\times O_{2}$ inductively as follows:

[TABLE]

where $\overline{\tau}$ is the trace of $P\times O_{2}$ associated to the trace $\tau$ of $P\times O_{1}$ by previous iterations of this inductive definition, and $F(S_{1}(\tau))$ is a sequence of actions of $O_{2}$ simulating the action $S_{1}(\tau)$ (which is an action of $O_{1}$ in this case) in the state reached after the trace $\tau|\Sigma_{1}$. Formally, if $s_{0}^{1}\xrightarrow{\tau|\Sigma_{1}}_{O_{1}}s_{1}$, then a simple induction on the length of executions can show that $(s_{1},s_{2})\in F$ where $s_{0}^{2}\xrightarrow{\overline{\tau}|\Sigma_{2}}_{O_{2}}s_{2}$. Then, since $s_{1}\xrightarrow{S_{1}(\tau)}_{O_{1}}s_{1}^{\prime}$ is a transition of $O_{1}$ and $F$ is a forward simulation, we get that there exists $s_{2}^{\prime}$ such that $(s_{1}^{\prime},s_{2}^{\prime})\in F$ and $s_{2}\xrightarrow{\sigma}_{O_{2}}s_{2}^{\prime}$ and $\sigma|(C\cup R)=S_{1}(\tau)|(C\cup R)$. We define $F(S_{1}(\tau))=\sigma$.

The scheduler $S_{2}$ is a slight deviation from the definition of a deterministic scheduler because $F(S_{1}(\tau))$ is not necessarily a singleton. However, the definition of $S_{2}$ can be adapted easily such that this sequence of steps is performed one by one.

Since $F$ is a $(C\cup R)$-forward simulation, $T(P\times O_{1},S_{1})|\Sigma_{p}\subseteq T(P\times O_{2},S_{2})|\Sigma_{p}$ is obvious. The reverse follows from the fact that $S_{2}$ is defined inductively following the definition of $S_{1}$. ∎

Appendix C Relating Forward Simulations and Strong Linearizability

The following result uses a concrete definition of atomic specifications as LTSs. Thus, an atomic object is an LTS $O=(Q,\Sigma,s_{0},\delta)$ where the states are pairs formed of a history $h$ and a linearization $h_{s}$ of $h$, i.e., $Q=\{(h,h_{s}):h_{s}\in Seq\mbox{ and }h\sqsubseteq h_{s}\}$, the internal actions are linearization point actions $\mathit{lin}(k)$ (for linearizing an operation with identifier $k$), i.e., $\Sigma=C\cup R\cup\{\mathit{lin}(k):k\in\<Ops>\}$, the initial state contains an empty history and linearization, i.e., $s_{0}=(\epsilon,\epsilon)$, and the transition relation is defined by: $((h,h_{s}),a,(h^{\prime},h_{s}^{\prime}))\in\delta$ if

[TABLE]

Call actions are only appended to the history $h$, return actions ensure that additionally, the linearization $h_{s}^{\prime}$ contains the corresponding operation, and linearization points extend the linearization with a new operation.

Lemma C.1**.**

Let $O_{1}$ be an object and $O_{2}$ an atomic object. If $O_{1}$ is strongly linearizable w.r.t. $O_{2}$, then there exists a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$.

Proof.

Let $\mathit{state}(\tau)$ denote the state of $O_{1}$ reached after a trace $\tau$ (since $O_{1}$ is deterministic, this state is unique). Also, let $F$ be a relation between states of $O_{1}$ and $O_{2}$ defined by $(s_{1},s_{2})\in F$ iff there exists a trace $\tau$ such that $s_{1}=\mathit{state}(\tau)$ and $s_{2}=(\mathit{hist}(\tau),f(\tau))$ (by the definition of $f$ in strong linearizability, the latter is a valid state of $O_{2}$) 101010We use the definition of atomic objects given in Section 3..

We show that $F$ is a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$. The fact that it relates the initial object state $s_{0}^{1}$ and the initial state $(\epsilon,\epsilon)$ of $O_{2}$ is trivial. Now, let $s_{1},s_{1}^{\prime}\in Q_{1}$, $a\in\Sigma_{1}$, and $s_{2}\in Q_{2}$, such that $(s_{1},a,s_{1}^{\prime})\in\delta_{1}$ and $(s_{1},s_{2})\in F$. We have to show that there exists $s_{2}^{\prime}\in Q_{2}$ and $\sigma\in\Sigma_{2}$ such that $(s_{1}^{\prime},s_{2}^{\prime})\in F$, $s_{2}\xrightarrow{\sigma}_{O_{2}}s_{2}^{\prime}$, and $\sigma|(C\cup R)=a|(C\cup R)$. ( Let $\tau$ be a trace such that $s_{1}=\mathit{state}(\tau)$ and $s_{2}=(\mathit{hist}(\tau),f(\tau))$. Then, $s_{1}^{\prime}=\mathit{state}(\tau\cdot a)$ and $f(\tau)$ is a prefix of $f(\tau\cdot a)$. Several cases are to be discussed:

• •

if $a\in C$, then $\mathit{hist}(\tau\cdot a)=\mathit{hist}(\tau)\cdot a$ and $\mathit{hist}(\tau)\cdot a\sqsubseteq f(\tau)$ provided that $\mathit{hist}(\tau)\sqsubseteq f(\tau)$. Therefore, $s_{2}\xrightarrow{a}_{O_{2}}(\mathit{hist}(\tau)\cdot a,f(\tau))$ and $(s_{1}^{\prime},(\mathit{hist}(\tau)\cdot a,f(\tau)))\in F$.

• •

if $a\in R$ and the operation identifier $k$ in $a$ occurs in $f(\tau)$, then $s_{2}\xrightarrow{a}_{O_{2}}(\mathit{hist}(\tau)\cdot a,f(\tau))$ and $(s_{1}^{\prime},(\mathit{hist}(\tau)\cdot a,f(\tau)))\in F$ like above. If $k$ does not occur in $f(\tau)$, then $f(\tau\cdot a)=f(\tau)\cdot c\cdot a$ where $c$ is the call action corresponding to $a$ (otherwise, $f(\tau\cdot a)$ would not be a linearization of $\mathit{hist}(\tau\cdot a)$). By the definition of $O_{2}$, we have that $s_{2}\xrightarrow{\mathit{lin}(k)\cdot a}_{O_{2}}(\mathit{hist}(\tau)\cdot a,f(\tau\cdot a))$ which concludes the proof of this case.

• •

if $a\not\in C\cup R$, then $f(\tau\cdot a)$ is obtained from $f(\tau)$ by appending some sequence of operations with identifiers $k_{1}$, $\ldots$, $k_{n}$ (this follows from the fact that $f$ is prefix-preserving). Then, $s_{2}\xrightarrow{\mathit{lin}(k_{1})\cdot\ldots\cdot\mathit{lin}(k_{n})}_{O_{2}}(\mathit{hist}(\tau),f(\tau\cdot a))$ and $(s_{1}^{\prime},(\mathit{hist}(\tau),f(\tau\cdot a)))\in F$ (because in this case, $\mathit{hist}(\tau\cdot a)=\mathit{hist}(\tau)$).

∎

Lemma C.2**.**

Let $O_{1}$ be an object and $O_{2}$ an atomic object. If there exists a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$, then $O_{1}$ is strongly linearizable w.r.t. $O_{2}$.

Proof.

Let $F$ be a $(C\cup R)$-forward simulation from $O_{1}$ to $O_{2}$. We define a function $f:T(O_{1})\rightarrow Seq$ by $f(\tau)=h_{s}$ where $h_{s}$ satisfies $(\mathit{state}(\tau),(h,h_{s}))\in F$. The fact that $\mathit{hist}(\tau)\sqsubseteq f(\tau)$ for every trace $\tau$ follows from the definition since $(h,h_{s})$ is a valid state of $O_{2}$ and $h=\mathit{hist}(\tau)$ (because $F$ preserves call and return actions). The fact that $f$ is prefix-preserving follows from the fact that $F$ is a forward simulation. ∎

Appendix D Snapshot Object

We show that the “concrete” implementation of the snapshot is a strong refinement of this specification using our characterization in terms of forward simulations. The pseudo-code descriptions in Figure 3 define LTSs whose states are formed of an array mem and for each active method invocation, a valuation of its local variables including the current program location. The local variable valuation of an invocation $k$ in a state $s$ is denoted by $s[k]$. We define a forward simulation $F$ from the LTS of the “concrete” snapshot object to the LTS of its specification. Thus, $(s,s^{\prime})\in F$ iff the mem arrays in $s$ and $s^{\prime}$ are the same, the two states contain the same set of active method invocations (matched using their identifiers), and for each scan invocation $k$, the local state $s[k]$ in the concrete object, i.e., a valuation of r1 and r2, and the current program location pc, is related to the local state $s^{\prime}[k]$ in the specification, i.e., a valuation of snaps, if the following holds:

[TABLE]

The predicate ${\sf valid}$ says that r1 and r2 are obtained by reading from a sequence of snapshots in snaps such that the value at position $j>i$ comes from a snapshot which is at least as recent as the one from which the value at position $i$ is taken (with a slight deviation for r1). Thus, let ${\sf fst}(v,i)$ be the smallest index of a snapshot $s\in\texttt{snaps}$ which contains the value $v$ on the $i$-th position. We define ${\sf fst}(\text{\tt r1},i)$ as $\infty$ when the invocation $k$ is “inside” a for loop and not yet set the $i$-th position of r1 (which can be derived from the current program location pc), or ${\sf fst}(\texttt{r1}[i],i)$, otherwise. Also, ${\sf fst}(\text{\tt r2},i)$ is simply ${\sf fst}(\texttt{r2}[i],i)$ for every $i$. Then, ${\sf valid}(\text{\tt r},\text{\tt pc})::=\forall i,j.\ i<j\implies{\sf fst}(\text{\tt r},i)\leq{\sf fst}(\text{\tt r},j).$ Besides the ${\sf valid}$ predicates, (1) states that r1 reads from more recent snapshots than r2, that the last element of snaps is the current value of mem, and that r1 is a member of snaps when the invocation reaches line 10 (right after the equality test).

We show that indeed the specification can mimic every step of the concrete implementation w.r.t. the simulation relation $F$ described above. The most interesting part concerns internal steps (every call/return action of the concrete implementation is mimicked by exactly the same action in the specification).

The internal step of update is simulated by the same step of update in the specification followed by a sequence of steps in which every scan takes an instantaneous snapshot of mem and appends it to its own snaps variable. This ensures the last element of every snaps variable is the value of mem after the update.

The internal steps of scan are all simulated by stuttering steps in the specification, i.e., if $(s_{1},s_{2})\in F$ and $s_{1}^{\prime}$ is a successor of $s_{1}$ by such a step, then $(s_{1}^{\prime},s_{2})\in F$. Thus, for a step of scan reading a new position in mem, i.e., r1[i] = mem[i], we have that $(s_{1}^{\prime},s_{2})\in F$ because the value of r1[i] is taken directly from mem which is the last snapshot in every snaps variable (therefore, the requirements on r1 from (1) hold when adding this new value). For a step of scan where the equality between r1 and r2 is established, we have that $(s_{1}^{\prime},s_{2})\in F$ because this equality implies $\texttt{r1}\in\texttt{snaps}$. Indeed, the only way that r1 which reads from more recent snapshots in snaps than r2 is equal to the latter is that they both read from the same snapshot in snaps. The simulation of the other internal steps of scan is obvious.