A Complete Program Logic for Compositional Linearizability

When designing large computer systems, it is good practice to encapsulate independent functionalities in separate components. This benefits verification, as a well-organized system decomposes into small open components that are completely characterized by their own implementation and their interfaces with the rest of the system.

In this context, given a module $M$ that implements some object with interface $F$ by importing a library with interface $E$, we call the implemented object the overlay of the module and the imported library its underlay. To verify the module against its overlay specification, we only consider the relevant underlay specifications, allowing provers to write independent proofs for separate modules. This means that the internals of the underlay module do not matter for other parts of the system: the module is characterized by its underlay and overlay specifications. This mode of verification is only possible in a compositional verification framework, where each module can be given a correctness property independent of the rest of the system, and then can be used as a building block to construct a larger system, with no side-conditions for the correctness of their compositions.

In the context of concurrent objects, linearizability [16] has been the gold standard since the 90s. It allows programmers to abstract the behavior of a concurrent object $E$’s code M_E into a simpler specification V_E that is atomic¹¹1By atomic we mean that when a thread makes an invocation it receives its response immediately after, with no interference from other threads. and easier to reason about. While there are many efforts to enable the mechanized verification of linearizability, few are truly scalable: either there are concurrent objects like the exchanger with non-atomic specifications that cannot be expressed in these pre-existing frameworks due to their over-reliance on atomicity, or the specification cannot be used as a black box encapsulating its code to modularly verify another object that uses this underlay object.

Over time, linearizability, which was an inherently atomic correctness criterion, has been extended to handle non-atomic objects [25, 5]. Recently, [27, 26] have also presented an analysis of compositional models of computation which reveals that linearizability, even when fully generalized to handle non-atomic blocking concurrent objects, has an underlying compositional structure, which can be exploited to develop a compositional refinement calculus for the verification of concurrent modules. As an application of their theory, [27] develop an axiomatic technique for showing linearizability of individual traces, and then package it as a rely-guarantee program logic. They call their linearizability criterion and underlying framework compositional linearizability.

While an important first step towards the compositional verification of non-atomic concurrent objects, and a convincing showcase of the compositional linearizability theory, the verification technique proposed by [27] could still be improved for the sake of practicality in large systems verification. Some immediate issues are that their framework has not been validated by a mechanization, and while [27] give a paper proof of soundness, they only conjecture its completeness. In this paper, we set out to mechanize the verification technique and formalize the soundness proof of [27], while also proving its completeness. Completeness is the main contribution of our work, and results in the first complete program logic for any of the standard generalizations of linearizability beyond atomicity.

In doing so, we identified an additional issue for the sake of practicality. To exploit the trace-based theory they had developed earlier, [27] use traces as a universal notion of state. Unfortunately, in practice, using traces as state leads to unnecessary complexity in defining predicates, as simple properties that would be readily available in a concrete representation of state become properties that must be stated inductively over the underlying trace.

So, in order to enable us to verify complex examples, we found it paramount to switch to a state-based representation of proof configurations. It turns out that switching from trace-based reasoning to state-based reasoning is not a simple task. There are two aspects to this. First, [27] use a technique inspired by [16] which they call possibility reasoning, where one attempts to maintain a set of possible linearizations for the current computation through a representation of linearizations in a structure they call a possibility. Unfortunately, some of the possibility update rules of [27] do not readily generalize to a state-based formulation, as they involve manipulating the ordering of events on a trace.

Another aspect of switching to state-based reasoning is that many of the algebraic properties [27] rely on to show the compositionality of the verification framework no longer hold strictly. Technically, their trace-based representation allows them to work up to equality to show several categorical properties of their refinement calculus. We had to generalize these categorical properties to hold only up to notions of equivalence in order to generalize their results to concrete states. In the process, we end up mechanizing a large portion of a generalization of the theory in [27].

An effect signature consists of a set E of effects $e$ and two assignments ${\text{par}}_{\text{E}}(-):\text{E}\to \text{Set}$ and ${\text{ar}}_{\text{E}}(-):\text{E}\to \text{Set}$, specifying respectively a set of parameters and a set of return values for each effect $e\in \text{E}$. We find it convenient to encapsulate this information in the following notation, whose usage will become clear shortly:

When it causes no confusion, we omit the subscript on ${\text{par}}_{\text{E}}(-)$ and ${\text{ar}}_{\text{E}}(-)$.

In the context of our paper, effects $e\in E$ are method names, which take as arguments elements of the parameter set $\text{par}(e)$ and return some value in its arity $\text{ar}(e)$. For instance, the signature for the EBStack data structure is the following, where $A$ is the type of stack elements and $\mathrm{𝟏}$ is the unit type.

Signatures also support a union operation, which collects the operations of both signatures into a single, combined signature. Formally:

Programs play the role of method bodies within modules in our mechanization. We formalize programs as interaction trees [34], which we type as Prog. Interaction trees are coinductively defined data structures with the following syntax:
$$p\in \text{Prog }\text{E}R:=\text{Vis}f\left(a\right)k\mid \text{Ret}r\mid \text{Tau}p\text{ where }f\in \text{E}a\in \text{par}\left(f\right)k:\text{ar}\left(f\right)\to \text{Prog }\text{E}Rr\in R$$

A program $p\in \text{Prog }\text{E}R$ represents a (possibly infinite) series of operations that result in a return value of type $R$ (if finite). The three constructors function as follows.

Vis f(a) k:

Issues an invocation to the operation $f(a)$ of the underlay signature E, and proceeds with the continuation $k(v)$ after receiving a return value $v\in \text{ar}(f)$.

Ret r:

Once a program executes all of its operations, it terminates by returning a value $r$ of type $R$.

Tau p:

Represents a silent step and is necessary for looping constructs to satisfy Rocq’s productivity checker. We refer readers to [34] for more details.

Prog E _ defines a monad for any E, which allows for programs to be written in a monadic style. The program bodies in Fig. 1 are the sugared version of a monadic expression over Prog E _. The additional control structures, such as the if conditional and the while loop constructs used in Fig. 1, may be defined in a standard way.

A module $M:\text{Mod}\text{E}\text{F}$ implements operations of a signature F, using the operations of the signature E. A module $M:\text{Mod}\text{E}\text{F}$ consists of a mapping from operations $f\in \text{F}$ and arguments $a\in \text{par}(f)$ to programs $M^{f(a)}:\text{Prog }\text{E}\text{ar}(f)$, implementing a call $f(a)$ as a program operating over E and returning a value in its return type $\text{ar}(f)$. In other words, a module $M:\text{Mod}\text{E}\text{F}$ is a collection $M:{\mathrm{\Pi }}_{f\in F}(\text{par}(f)\to \text{Prog }E\text{ar}(f))$. For instance, $M_{\text{EBStack}}$ is the mapping taking push(v) to the program described in Fig. 1 and similarly for pop(). Nonetheless, we write $M^{f(a)}:\text{Prog }E\text{ar}(f)$ for the program corresponding to $f\in F$ and $a\in \text{par}(f)$ in $M$, and $M^f:\text{par}(f)\to \text{Prog }E\text{ar}(f)$.

Modules may be composed vertically by interaction tree substitution. Given modules $M:\text{Mod}\text{E}\text{F}$ and $N:\text{Mod}\text{F}\text{G}$, their vertical composition $M:\mathrm{⊳}N:\text{Mod}\text{E}\text{G}$ implements the operation $g(a)$ of G by running the corresponding program $N^{g(a)}$ with method invocations $f(a^{\prime })$ to F replaced by their corresponding programs $M^{f(a^{\prime })}$. We refer readers to the mechanization for the exact definition. Crucially, the vertical composition operation admits an identity element:

The vertical composition operation $(:\mathrm{⊳})$ and its identity element satisfy the following properties:

where $\approx$ is an equivalence relation defined on modules as the pointwise equivalence of programs up to removal of silent steps (Tau). The first two properties show that idM is the neutral element for vertical composition, up to $\approx$ equivalence, and the third property is its associativity.

We now give a formal definition of labelled transition system (LTS), the specifications we use for objects. Recall that a module $M:\text{Mod}\text{E}\text{F}$ depends on the operations provided by E to implement the operations of F. To define the operational semantics of a module, we first define the behavior of the operations in E using an LTS.

First, we must define what kinds of events we are interested in. We assume as given a set of thread names $𝒯$, which is a parameter over the whole model. We use a set of the form , where $T\in \mathbb{N}$ is the total number of threads, as $𝒯$. In a multicore setting, $𝒯$ is the set of cores available; in a multi-threaded setting, it is the set of available threads. While users can fix the whole set $𝒯$ when verifying an object, we choose to parameterize our theories and proofs over $𝒯$. As a result, our proofs of linearizability universally quantify over such finite sets of thread names.

Then, an event of the signature E consists of

where $\alpha \in 𝒯$, $f\in \text{E}$, $a\in \text{par}(f)$ and $v\in \text{ar}(f)$. An event is either $𝜶:f(a)$, a call to an operation of E, or $𝜶:f(a).v$, a return event tagged with the thread that issued it. Then, a labelled transition system V over E, written $\text{V}:\text{Spec}\text{E}$, is defined as a triple $(S,{\to }_{\text{V}},s_0)$ of a set of states $S$, a transition relation ${\to }_{\text{V}}\subseteq S\times \text{TEvent}\text{E}\times S$, and an initial state $s_0\in S$.

Unlike many approaches for modeling concurrent specifications, which assume operations are logically atomic, the call and return events are separate transitions in our specifications. This is necessary to model objects that are not linearizable to atomic specifications. We do, however, require that the labelled transition system be locally sequential, i.e., the projection to each thread is sequential (it strictly alternates between invocations and responses). As a result, we must carry some extra state, like the operation that is currently executing (e.g., Fig. 2(a)), so we prevent other calls from happening until the current pending call is completed.

We now give a couple of examples of linearized state transition systems used in the verification of the EBStack. In our state diagrams, such as Fig. 2(a), we use conditionals and state updates in the labels, and depict the transitions for abstracted thread names $\alpha$, $\beta$, to mean that for any thread $\alpha$ a certain transition exists (if threads have different names they are distinct $\alpha \ne \beta$). This allows us to make the diagrams finite so they may be depicted succinctly on paper.

We define a trace over a signature E as a list $t\in {(\text{TEvent}\text{E})}^{\ast }$ of thread events. We write Trace E for the set of traces over E. The LTS specification $\text{V}:\text{Spec}\text{E}$ specifies the behavior of an object through $⟦\text{V}⟧$, a set of traces defined as follows: we first define a path in $\text{V}=(S,{\to }_{\text{V}},s_0)$ and then take all paths starting from the initial state as the set of behaviors.

Our notion of refinement is then just behavior containment:

It is straightforward to check that refinement is reflexive and transitive, making it a preorder.

Given an underlay specification $\text{V\_}\text{E}:\text{Spec}\text{E}$, where $\text{V\_E}=(S,{\to }_{\text{V}},s_0)$, and a module $M:\text{Mod}\text{E}\text{F}$, we define the behaviors of $M$ running on top of V_E operationally as a concrete LTS $(\text{V\_}\text{E}\mathrm{⊳}M)$. In § 4, we define the linearizable relation of the concrete LTS w.r.t. the specification LTS (those in Fig. 2).

The operational semantics models executions under an arbitrary scheduler and client to the overlay object F. An arbitrary client may have a thread call any operation available to it, with any argument. Hence, each operational semantics rule non-deterministically chooses a thread to take a step. This ensures we verify our modules as open components.

The states $(ths,s)\in \text{InterState}$ (interaction state) of the operational semantics are pairs of a thread state $ths\in 𝒯\to \text{TState}\text{E}\text{F}$, which is a map from thread names to the continuation of that thread, and an underlay LTS state $s\in S$. The continuation of each thread is defined as

where $f\in \text{F}$, $a\in \text{par}(f)$, $p\in \text{Prog }\text{E}\text{ar}(f)$, $g\in \text{E}$, $b\in \text{par}(g)$, $k:\text{ar}(g)\to \text{Prog }\text{E}\text{ar}(f)$. We use $ths[\alpha \mapsto p]$ as the notation for updating the value of $\alpha$ to $p$ in the map $ths$.

Fig. 3 defines the operational semantics rules. OCall selects an idle thread, non-deterministically chooses an operation $\text{f}\in \text{F}$ and an argument $\text{a}\in \text{par}(\text{f})$, and changes the continuation for $\alpha$ to the code for f(a) defined as $M^{\text{f(a)}}$. UCall locates a thread $\alpha$ whose next step in the continuation is an underlay call g(b), performs the call step $𝜶:\text{g(b)}$ in the underlay object V_E, and updates the underlay LTS state to $s^{\prime }$ accordingly. URet is analogous, except that it takes a return transition and continues with the continuation as specified by $k$. ORet matches on a thread whose continuation indicates it is ready to return from the overlay operation, and performs the overlay return by updating the continuation to Idle. Silent simply skips a Tau with no change to the state.

We then define the concrete LTS of running $M$ on top of V_E as $\text{V\_E}\mathrm{⊳}M:\text{Spec}\text{F}:=(\text{InterState}\text{F}\text{V\_}\text{E},{\to }_{\text{V\_}\text{E}\mathrm{⊳}M},(th{s}_0,s_0))$, where $th{s}_0$ is the constant mapping to Idle and $m\in \text{TEvent}\text{F}$, and transitions are given by the following relation

Notice that only the overlay events $m\in \text{TEvent}\text{F}$ are visible in $\text{V\_E}\mathrm{⊳}M$. The definition allows for a visible step $m$ followed by several steps in the underlay object V_E, as enforced by the requirement that $t\in {(\text{TEvent}\text{E})}^{\ast }$. The underlay event trace is hidden behind an existential quantifier, making these implicit silent steps.

The following are some important properties of the operation - $\mathrm{⊳}$ -. The first two properties are monotonicity of vertical composition w.r.t. $\approx$ and $⊒$, while the third property encodes both associativity of $\mathrm{⊳}$ and $:\mathrm{⊳}$, as well as compatibility of the two operations.

Both modules and specifications can be horizontally composed. For instance, given modules $M_L:\text{Mod}{\text{E}}_L{\text{F}}_L$ and $M_R:\text{Mod}{\text{E}}_R{\text{F}}_R$ we can define their horizontal composition $M_L+M_R:\text{Mod}({\text{E}}_L+{\text{E}}_R)({\text{F}}_L+{\text{F}}_R)$, similarly to how we did with effect signatures, as the union of the two collections:

where $\text{mapProg}(\lambda x.\text{inl}x)$ replaces every event $\text{Vis}e$ in $M_L^f$ by $\text{Vis}(\text{inl}e)$ (and similarly for the other branch).

For specifications $\text{V\_L}:\text{Spec}{\text{E}}_L$ and $\text{V\_R}:\text{Spec}{\text{E}}_R$ we can define a specification $\text{V\_L}\otimes \text{V\_R}$ given by the (locally sequential) asynchronous product of the two transition systems. We refer the reader to the mechanization for the definition. Below, we show the key compositional properties of $-\otimes -$:

The first three properties show that horizontal composition defines an order-isomorphism for specification refinement. The last two properties show that the operation is functorial.

Safety for sequential objects is usually given by functional correctness. For instance, a counter object provides operations $\text{get}:\mathrm{𝟏}\to \mathbb{N}$, taking unit as argument and returning some natural number, and $\text{inc}:\mathrm{𝟏}\to \mathrm{𝟏}$, taking unit as argument and returning unit. An implementation of a counter is correct as long as get always returns the number of previous inc operations. This means that given the trace:

of a correct counter implementation, we are guaranteed that the next event is a return of $1$ to the operation get. However, for a concurrent counter implementation, given the trace:

any number of increment operations by other threads might take effect:

so that $n$ might be any number between $1$ and $k$. What makes a concurrent counter object correct is therefore a more challenging question, and expressing “functional” correctness for concurrent objects remained an open question until the 90s, when linearizability [16] was proposed.

Linearizability asks that every trace generated by the concurrent counter implementation, such as trace $s$ above, be linearizable with respect to some trace of a correct sequential counter. This is formalized by defining a partial order called happens-before, which associates to a trace $s$ the partial order $\mathrm{𝗁𝖻}(s)$ defined as the smallest partial order such that $e{\prec }_{\mathrm{𝗁𝖻}(s)}{e}^{\prime }$ whenever $e$ and $e^{\prime }$ are events by the same thread and $e$ appears before $e^{\prime }$ in $s$, or when $e$ is a return event and $e^{\prime }$ is an invocation event. A trace $s$ is then said to be linearizable w.r.t. an atomic trace $t$ when there is a way to complete some pending invocations of $s$ (by adding extra return events), then remove all remaining pending invocations, so as to obtain a trace $s^{\prime }$ satisfying that $\mathrm{𝗁𝖻}(s^{\prime })$ is refined by $\mathrm{𝗁𝖻}(t)$ (in the sense that if $e{\prec }_{\mathrm{𝗁𝖻}(s^{\prime })}{e}^{\prime }$ then $e{\prec }_{\mathrm{𝗁𝖻}(t)}{e}^{\prime }$). Atomic means that every invocation is immediately followed by its return, or, equivalently, that $t$ is locally sequential (every thread alternates invocations and returns) and ${\prec }_{\mathrm{𝗁𝖻}(t)}$ is a linear order. An implementation is then said to be linearizable w.r.t. a specification if all traces generated by the implementation are linearizable w.r.t. the specification.

The requirement that $t$, and consequently specifications, be atomic ensures that concurrent data structures such as stacks, queues, and counters are all specified by essentially the same specification as the corresponding sequential data structures. This requirement, however, proves too restrictive, as many reasonable concurrent objects admit no corresponding sequential object. For example, the exchanger in § 2 is a standard synchronization primitive (for instance, available as part of Java’s standard libraries [4]). Nonetheless, it admits no reasonable atomic specification, intuitively because an exchange can only happen if two threads are running concurrently. To remedy this, set linearizability was proposed [25]. Set linearizability only modifies the definition of linearizability by requiring that the traces of the specification be of the form:

where each $I_k$ is a sequence of invocations and each $R_k$ is a sequence of responses containing all and only the responses to the invocations in $I_k$ (except for $R_n$, which may contain only some such responses). In addition, one requires that if

is in the specification, then so is

where each $I_k^{\prime }$ (resp. $R_k^{\prime }$) is some reordering of $I_k$ (resp. $R_k$). This means that we may see these traces as sequences of sets of invocations, each followed by the set of returns to that set of invocations.

This modification to linearizability allows it to specify many concurrent objects whose behaviors involve some kind of synchronization, such as exchangers, barriers, and blocking stacks (stacks where pop blocks on the empty stack). We will see that it also helps in specifying objects beyond synchronization primitives, such as the TryStack. However, there are concurrent objects and certain distributed tasks whose consistency is even weaker than that provided by set linearizability. For example, it is possible to implement a write-snapshot object [3]²²2A write-snapshot provides a single operation ws that takes a value as argument and returns a set of written values as output. validating the trace:

Here, when $\alpha$ takes its snapshot, $\beta$’s value of $5$ is already visible, but by the time $\beta$ manages to take its own snapshot, $\gamma$’s value is now visible too. Because of this, the return to $\beta$’s call cannot happen together with $\alpha$’s return, and hence set linearizability cannot capture this object’s consistency.

To accommodate such objects, interval linearizability [5] was proposed, which further relaxes the notion of specification in linearizability’s definition so that in a trace

$R_k$ is now allowed to contain returns to pending invocations from $I_l$ for any $l\le k$, and in particular it may contain only some of the returns in any $I_l$ (including $I_k$). The requirement that reorderings within $I_k$ or $R_k$ are all valid remains. This has been shown to be a complete correctness criterion for distributed tasks [5, 12]. Interval linearized specifications therefore allow traces with a significant degree of concurrency, such as $s^{\prime }$ above. Nonetheless, these specifications may still be simpler than the traces generated by the implementation. The write-snapshot we discuss and verify in our mechanization admits an interval linearized specification that is deterministic in the sense that given a trace:

then in any two extensions

where $R_k$ and $R_k^{\prime }$ contain only responses, if $𝜶:\text{ws}(v).S$ appears in $R_k$ then either $𝜶:\text{ws}(v).S$ also appears in $R_k^{\prime }$ or $R_k^{\prime }$ can be extended with $𝜶:\text{ws}(v).S$. In other words, any returns that can happen for any given thread are unique up to the ordering of the responses. This makes the linearized specification significantly easier to work with for a client of the write-snapshot object than using all the traces generated by the implementation, which present more concurrency and non-determinism.

Nonetheless, interval linearizability still does not accommodate all concurrent objects. This last issue is more subtle, and we recommend that the interested reader consult [27] for a more thorough treatment. Succinctly, the requirement that all pending invocations that have not been completed must be removed in the linearization is too strong for certain concurrent objects. There are circumstances where an invocation is detectable to other threads even though its response is still not enabled. Compositional linearizability [26, 27] further weakens interval linearizability by allowing some invocations to be completed, some to be removed, and some to remain in the linearization. This makes compositional linearizability complete for concurrent objects. However, perhaps the main advance of compositional linearizability is that it gives a novel treatment of the theory of linearizability showing that, within a compositional model of computation, linearizability can be characterized entirely in terms of composition and refinement. In this paper, we adopt compositional linearizability as our notion of correctness and mechanize many aspects of the comprehensive theory of [27]. In particular, they present rather algebraic proofs of all the key properties of linearizability based on a different (but equivalent) formulation that circumvents the use of partial orders or rewrite systems. We have found that this reformulation makes mechanization tractable despite the significantly more challenging setting of working with non-atomic and potentially blocking specifications. At the same time, we find it productive to formulate their ideas using LTSs rather than strategies (final coalgebras for these LTSs). To do so, we made several improvements to their proof technique based on possibilities. The remainder of this section concerns our mechanization of compositional linearizability and possibilities, ultimately leading to our proof technique in § 5.

The observation at the core of [27] is that, in the context of a compositional model for computation, the linearizability theory can be entirely derived from the definition of the identity for composition of modules. They refer to their notion of linearizability as compositional linearizability and demonstrate that it is a conservative generalization of Herlihy-Wing linearizability [16], set linearizability [25], and interval linearizability [5], as it becomes equivalent to these criteria under appropriate restrictions.

In our mechanization, we choose to formalize compositional linearizability using its refinement-based definition, which can be defined using idM as follows:

Intuitively, the reason why this definition agrees with the usual linearizability definition is that the set of behaviors of K V is exactly the set of all traces linearizable w.r.t. some behavior of V. The operations of E made by the overlay to idM form a bracket around the corresponding underlay operations. Because of this, happens-before ordering is preserved from the overlay of idM to its underlay. The fact that pending calls may be removed or completed in a trace corresponds to the fact that in the operational semantics of $\text{V}\mathrm{⊳}\text{idM}$, one can be in a state where the call has been made in the overlay of idM but not in the underlay yet. There are states where a return has been made to the underlay operation in idM but has not returned to the overlay yet. Therefore, K V defined above contains all traces linearizable w.r.t. the specification. We refer readers to [27] for a detailed treatment of how this definition relates to previous definitions of linearizability.

Our definition of linearizability enjoys observational refinement and locality (Theorem 4). They follow from generalizing the proofs of compositional linearizability from [27] to handle our more heterogeneous compositional structure, discussed in § 3.

Through compositional linearizability [27], LHL gains horizontal and vertical composition without any additions to the logic. LHL’s soundness provides linearizability proofs of different modules, which can be horizontally and vertically composed together to obtain the linearizability of a larger system. These results are obtained by combining locality and observational refinement with the compositional structure of the model defined in § 3.

Horizontal composition enables importing multiple objects together through the tensor operator ($\otimes$) and using them concurrently. The locality of compositional linearizability guarantees that both objects will preserve their original specifications, and users of both objects can enjoy the interface ${\text{F}}_1+{\text{F}}_2$ with both sets of operations available.

Vertical composition ($\mathrm{⊳}$) “links” the overlay object’s code with the imported underlay object’s code. Since vertical composition ($\mathrm{⊳}$) is compatible with linking ($:\mathrm{⊳}$), the observational refinement [27] ensures running the linked code $\text{M\_E}:\mathrm{⊳}\text{M\_F}$ above the lower-level specification ${\text{V\_E}}^{\prime }$ still produces traces linearizable to the top-level specification V_F.

This is how we “glue” together the individual verified components in Fig. 1 into the whole implementation of the EBStack to obtain the correctness of the entire system.

To prove linearizability, we employ possibility reasoning. [27] have shown a bisimulation between possibilities and their formulation of the operational semantics of idM running on top of V_F, implying that possibility reasoning is sound and complete for compositional linearizability proofs. In our setting, we redesign the possibility reasoning technique to contend with our use of state as explained in § 1.

Assuming we want to show $M$ running above V_E is linearizable w.r.t. V_F, i.e., $(\text{V\_E}\mathrm{⊳}M)\mathrm{⤳}\text{V\_F}$, a possibility $\rho \in \text{Poss}$ is defined as a triple $⟨{\rho }_S,{\rho }_C,{\rho }_R⟩$ of (1) the linearized state ${\rho }_S$ in V_F, (2) a partial map ${\rho }_C$ from thread names $\alpha \in 𝒯$ to call events of F, and (3) a partial map ${\rho }_R$ from thread names $\alpha \in 𝒯$ to return events of F. We write ${\rho }_C(\alpha )$ for the event that ${\rho }_C$ maps $\alpha$ to; ${\rho }_C(\alpha )=\perp$ when it is undefined; and ${\rho }_C[\alpha \mapsto m]$ for substitution of $m$ for ${\rho }_C(\alpha )$; and similarly for ${\rho }_R$. The mapping ${\rho }_C$ stores pending calls that have happened in the concrete execution but have not been performed in the linearized state $s$; ${\rho }_R$ stores returns that have been made in the linearized state ${\rho }_S$, but not in the concrete execution. Therefore, from the perspective of a particular thread $\alpha$, a possibility can be in one of four states:

Idle:

The last transition by $\alpha$ in V_F was a return, and both ${\rho }_C(\alpha )=\perp$ and ${\rho }_R(\alpha )=\perp$.

Pending Call:

$\alpha$’s last transition in V_F was a return, ${\rho }_C(\alpha )=\text{m}$ for some $m\in \text{F}$ and ${\rho }_R(\alpha )=\perp$.

Call Done:

The last transition by $\alpha$ in V_F was a call $𝜶:m$, ${\rho }_C(\alpha )=\text{m}$ and ${\rho }_R(\alpha )=\perp$.

Pending Return:

The last transition by $\alpha$ in V_F was a return $𝜶:m.n$, ${\rho }_C(\alpha )=\text{m}$ and ${\rho }_R(\alpha )=\text{m}.\text{n}$.

We formalize possibility updates, the axioms to manipulate possibilities, as a transition system whose states are possibilities over V_F and transitions are given by:

Intuitively, a possibility encodes a proof of linearizability. The Invoke and Return model the events of the concrete trace, and CCommit and RCommit the corresponding events in the linearization. The axioms on possibility updates ensure that as long as the initial possibility is valid, the updated possibility always corresponds to some valid linearization, i.e., (1) only call events that happened in the concrete execution can be added to the possibility, (2) only transitions respecting local sequentiality can be made to the possibility, and (3) return events missing in the concrete execution can be added to complete pending calls in the possibility. The remaining obligation to show the consistency of linearized return values and actual returned values will be addressed by the program logic. For instance, a possible proof that the trace $t^{\prime }$ below is linearizable w.r.t. $t_{i,j}$ corresponds to the sequence of possibility updates shown in Fig. 5.

When verifying a stack implementation, we can determine if the correct linearization is $t_{1,2}$ or $t_{2,1}$ by inspecting the underlay state. If we focus on Invoke and Return events, we can reconstruct the concrete trace $t^{\prime }$, and if we focus on CCommit and RCommit, we can rebuild the linearized trace $t_{i,j}$.

Single possibilities are not sufficient in general when constructing proofs of future-dependent linearizations inductively. We must maintain multiple possibilities simultaneously to contend with current possibilities being invalidated in the future. To accomplish this, we lift the possibility axioms from a single possibility $\rho$ to a non-empty set of possibilities $\overline{\rho }$, and define the lifted transition $-\twoheadrightarrow -$.³³3Formally, we have described how to construct the equivalent of forward simulations. Using a power-set construction, we obtain the equivalent of a forward-backward simulation, which is complete for trace equivalence [24]. In other words, a set of possibilities $\overline{\rho }$ can be updated into $\overline{\sigma }$ as long as every possibility in $\overline{\sigma }$ is reachable after zero or finitely many valid updates from some possibility in $\overline{\rho }$.

In the stack example above, if the stack’s linearizability proof were future-dependent (e.g., the timestamped stack [8]), we would maintain a set $\overline{\rho }=\{{\rho }_{1,2},{\rho }_{2,1}\}$ for the trace $t^{\prime }$. The possibility ${\rho }_{1,2}$ corresponds to the case $i=1$ and $j=2$, and ${\rho }_{2,1}$ the other case. We would then update $\overline{\rho }$ according to the updates in the example above for the corresponding assignments of $i$ and $j$. When the pop() operation reaches its linearization point, we would find out which of the two pushes was deemed to have occurred first, and remove whichever of ${\rho }_{1,2}$ or ${\rho }_{2,1}$ has been invalidated.

In LHL, a proof configuration is a tuple $(s,\overline{\rho })$ of a concrete LTS state $s\in \text{InterState}$ and a set of possibilities $\overline{\rho }\in 𝒫(\text{Poss})$. The component $s$ represents the current state of the program, which follows the actual semantics of the program, while $\overline{\rho }$ represents linearized overlay LTS states, which are managed by the prover following the possibility update rules in § 4.2.

By using a set of possibilities instead of a single possibility, users of LHL can track different linearizations corresponding to the current state. They can remove extra possibilities later when future events invalidate these linearizations. This allows us to support objects (such as the Herlihy-Wing queue [16]) with future-dependent linearizations [32], which is essential for the completeness proof of LHL.

We define preconditions $P$ as predicates over the proof state, while rely/guarantee conditions $ℛ,𝒢$ and postconditions $Q$ are defined as relations over the state. We use binary postconditions relating pre-/post-states to make certain proofs easier.

LHL consists of three judgments: (1) the module judgment $V_E,V_F,ℛ,𝒢,P,Q\models M$ groups all side conditions and implies our linearizability condition $(\text{V\_E}\mathrm{⊳}\text{M\_F})\mathrm{⤳}\text{V\_F}$, (2) the program judgment $ℛ,𝒢⊢\{P\}e\{Q\}$ verifies the correctness of the method body, and (3) the commit judgment $𝒢{⊢}_{\alpha }\{P\}m\{Q\}$ handles individual underlay events and applies possibility updates.

To establish module correctness, the prover needs to find pre-/post-conditions for each $f\in \text{F}$ and rely/guarantee relations, and show the following:

where $\text{Inv}(-):={\cup }_{f\in F}\text{Inv}(f)$, $\text{Ret}(-):={\cup }_{f\in F}\text{Ret}(f)$. The first few conditions are standard rely-guarantee conditions, respectively: that $ℛ[\alpha ]$ is reflexive and self-stable, that threads respect each other’s relies, and that method pre-conditions are stable. Other than the standard rely-guarantee side conditions, we require for all methods that (1) the initial proof state satisfies its pre-condition, (2) the required Hoare triples can be established for it, and (3) its post-condition implies the pre-condition of any method, so the system can still run safely afterwards.

The program judgment consists of the following Hoare-style rules:

These core rules are applicable to all programs. In practice, though, the user will define control structures along with their corresponding derived rules, and the core rules will not be used directly. For instance, bind and call may be defined, and their derived rules are as follows.

The final component of the proof is the commit judgment $G{⊢}_i\{P\}m\{Q\}$ generalizing linearization points into possibility updates.

The commit judgment asks the following: for any state $(s,\overline{\rho })$ satisfying the pre-condition $P$ and any $t$ reachable from $s$ through the operational semantics, the user needs to produce new linearizations $\overline{\sigma }$ reachable after finitely many possibility updates ($\overline{\rho }\twoheadrightarrow \overline{\sigma }$, defined in § 4.4) and ensure the postcondition and guarantee relation are satisfied. In LHL, these updates are restricted to CCommit or RCommit; the necessary Invoke and Return updates are applied automatically by the logic. The central proof obligation of LHL is to manage the set of possibilities $\overline{\rho }$ and maintain a sufficient set of correct linearizations. The user uses the commit judgment to update the linearization as they verify an operation, until they reach the postcondition $Q_f$. After this, the user will have to show that the series of commits they performed resulted in a linearization with the same return value as that produced by the operational semantics.

We observe that the transition from $s$ to $t$ makes the accepted case of the precondition impossible, so we are left with $\text{offered}(\alpha ,v)$ as the precondition. We choose to use $(\{\},\{\})$ as $\sigma$ (the same as $\rho$) and perform the possibility update $(\rho ⇢\sigma )$ by making two transitions with event labels $𝜶:\text{exch}(v)$ and $𝜶:\text{exch}(v).\perp$. The return value of this linearization is $\perp$, and the actual return value of this branch is also $\perp$, so this linearization is valid. This possibility update is also safe because no concurrent exchange operation will successfully exchange its value for $v$ and the new proof state satisfies the cleared disjunct of the post-condition.

Formally, the following rely-guarantee definition justifies this update, which matches the ${𝒢}_{\text{fail}}$ relation.

Fig. 6 shows how these relations move the proof state among the three disjuncts of the invariant.

After the current thread makes the offer, other threads can only perform the accept transition ${𝒢}_{\text{acc}}$, so the precondition in the Hoare triple is stable. The post-condition is also stable because no guarantee condition can step outside the invariant.

Other commands are verified similarly, and together, they establish the entire Hoare triple for the exch method:

which discharges the remaining obligation in the module judgment of the exchanger. We refer readers to the extended version and the Rocq mechanization for more details.

Other than the elimination-backoff stack, we also verified (1) a family of lock-protected objects, proving correct the pattern of protecting operations of any racy but atomic objects with locks, and (2) the one-shot write-snapshot object [5], which is an interval linearizable object that no existing system can verify.

We prove our program logic to be both sound (Theorem 10) and complete (Theorem 11) with regard to compositional linearizability. We outline the proofs here.

Ours is the first paper with the technology to mechanize the proof of linearizability of the one-shot write-snapshot [5] object against its interval-sequential specification, and we believe we are also the first to give a truly modular proof of the EBStack. We compare other works that have verified the EBStack at the end of this section.

Our approach is mainly inspired by [16], [21], and [27]. [16] not only proposed the notion of linearizability but also introduced possibility reasoning as an axiomatic method for proving atomic linearizability, and showed it is complete and sound for proofs of linearizability for individual traces. Their original technique has been recently mechanized by [17].Their technique focuses only on atomicity, however, and only on verifying a single component, and does not provide the ability to verify large object systems either modularly or compositionally. Our approach is strictly more general in that it handles non-atomic objects and is compatible with theirs, so we could have verified any example they can verify.

[21] packaged possibility reasoning in a program logic for the first time, and used interval partial orders to represent a set of possibilities of an execution. [26, 27] show that [21]’s program logic is not complete for atomically linearizable objects, and extend it further to support compositional linearizability. They conjectured that their program logic was complete due to its relationship with possibility reasoning. Neither work has been mechanized. Our program logic mechanization builds upon their theory, and extends the possibilities from [27] with state, making possibility reasoning simpler and more usable than using either partial orders or traces, and embeds this method into a mechanized program logic. We provide a further extensive comparison with the closely related work of [27] in the extended version of the paper [14].

It is worth mentioning that other than Herlihy-Wing possibilities, [28] have provided a technique based on forward and backward simulation that is sound and complete for Herlihy-Wing linearizability. Backward simulations are often deemed hard to reason about, however, because they go against the natural forward flow of executions, introduce backward non-determinism, require knowledge of the future, and often require introducing history variables to provide information that would be available under a forward technique. A similar approach is that of [6], who prove a direct simulation between the EB stack and its abstract model. However, this simulation is based on the execution of the entire thread pool. When showing the simulation, the prover needs to discuss the execution of all threads. In contrast, our approach and other program logics focus on enabling thread-local reasoning, which is more accessible to programmers and makes proofs more intuitive.

Regarding the mechanization, the closest work to ours is [22]. It focuses on using linearizability to verify serializability. Our encoding of modules as interaction trees is the same as theirs, and some aspects of their treatment of atomic linearizability are compatible with ours. Despite that, their framework is restricted to atomicity. This means that their LTSs pair call and return events and cannot handle non-atomic objects. As a result, they can’t compute overlay objects ($\text{V}\mathrm{⊳}M$), as these can be non-atomic even if V is atomic, so they define an object as a pair of an underlay (atomic) LTS and a module instead. Meanwhile, an object for us is just an LTS. While they prove several compositional properties of the modules, which boil down to properties of interaction trees, we prove several more properties related to computing overlay objects, monotonicity w.r.t. trace refinement, etc. These enable the compositional linearizability framework and make up a significant portion of our mechanization. Due to the compatibility of their approach with ours, we believe that their results around encoding serializability as atomic linearizability could be carried over.

Although previous linearizability-based works cannot support non-atomic objects like the exchanger, it is still possible to use Hoare triples to give them a tight specification. [29] specifies the functional correctness of the exchange operation through Hoare triples and develops a Hoare logic verifying the exchanger in Rocq. However, due to the limitation of functional correctness, their Hoare triple specification can only be used when the execution of all interleaving threads is known, i.e., composed through the parallel composition rule. In contrast, our work focuses on object-level verification, where the client would access the object in an arbitrary concurrent environment. Moreover, [29] only verified a simple example as the client of the exchanger, instead of a complex object such as the elimination-backoff stack. It is unclear whether their logic can appropriately handle complex examples such as the helping mechanism in the elimination-backoff stack or future-dependent linearizations.

Logical atomicity [7, 19] uses logically atomic Hoare triples $⟨P⟩\text{op}()⟨Q⟩$ to specify the ability of the given operation to perform the update abstracted as a transition from assertion $P$ to assertion $Q$ at a single physically atomic statement. Since its focus is on atomicity, it cannot generally specify set and interval linearizable objects satisfactorily. It is compositional as one may directly use the logically atomic Hoare triple in proofs of other functions that use this operation. It is known that a logically atomic triple implies Herlihy-Wing linearizability [2], but there is no evidence that logical atomicity can be used to specify all Herlihy-Wing linearizable objects, so its completeness is unknown. Moreover, logically atomic triples rely on a concrete assertion language, a concrete programming language, and their underlying semantic models. This limits the compositionality to within its own program logic framework, while our approach can specify any object using an abstract LTS, without assuming the actual semantic model or the program logic verifying the object against the specification.

Contextual refinement provides an alternative to linearizability. It uses an abstract piece of code A_E to specify the concrete implementation M_E by requiring that the behavior of M_E running in any context $C$ is bounded by the behavior of A_E running in the same context, usually denoted as $\text{M\_E}⊒\text{A\_E}$. Contextual refinement is equivalent [9] to Herlihy-Wing linearizability and supports vertical composition in a sequential setting [30]. However, contextual refinement relies on a concrete programming language for the abstract code, and an embedding of this language into the original language for the concrete code is necessary for composing a concrete context with an “abstract” specification. In contrast, our framework only uses the signature of an object and applies to any programming language whose behaviors are characterized by call and return events, without any modification to the language. This is a major benefit of verifying objects directly against linearizability specifications. Moreover, there has been no work to support modular verification of non-atomic objects like the exchanger and the interval-linearizable write-snapshot within the contextual refinement framework.

Relational Hoare logic [1] is widely used to show contextual refinement. [23] used local rely-guarantee reasoning to implement a relational logic that verifies the contextual refinement of concurrent objects w.r.t. their atomic abstract code. [35] later applied this technique to verify an operating system using their relational program logic. They achieved this using logically atomic triples [7] to establish a contextual refinement between the two. Their work allows modular verification, but with limited encapsulation: an object’s abstract code A_F must also include all its sub-components’ abstract code A_E. They can verify sub-components against corresponding abstract code A_E and use their Hoare triples to execute A_E embedded in A_F. Consequently, the top-level specification consists of very complicated abstract code that does not intuitively specify its behaviors. In contrast, our LTS specification encapsulates all details of the underlay object and provides an implementation-agnostic interface for users to verify overlay objects.

[31] encodes the contextual refinement obligation into a ghost state to verify it with CSL. Iris [19] is a higher-order logic for verifying fine-grained concurrent programs and also features logical atomicity. It leads to the ReLoC framework [10, 11, 33], which shows contextual refinement of concurrent programs using a program logic, with prophecy variables [20] enabling future-dependent linearization. ReLoC achieves compositionality by first encapsulating reusable code into smaller functions, then verifying these functions against logically atomic Hoare triples encoded as a logical relation, and lastly verifying the refinement of the top-level object using these intermediate proofs. However, it is unknown how to reuse the top-level refinement specification when verifying objects that use this top-level object. As a result, every time they build new objects using the one verified against the refinement specification, they need to prove a different functional correctness specification before they can reuse its proof. In contrast, our framework imposes LTS specifications uniformly at any level of abstraction.

As shown in Table 1, both lines of work have verified the elimination-backoff stack but failed to achieve the same level of compositionality as we do. [23] directly inlined all underlay code in the EBStack code. ReLoC [10] broke down the exchanger into three atomic operations: make_offer, accept_offer, and revoke_offer, exposing implementation details, and implemented the EBStack using these operations. They built and verified the EBStack using these three methods and their specifications. This effectively inlines a specific protocol for implementing the exchanger object within the stack implementation. As a result, to verify other objects using the exchanger, nothing except the specifications for these low-level atomic operations can be salvaged and reused from their proof. They still need to inline all the implementation code of the exchanger in the overlay object. In contrast, our approach allows direct composition above the ready-to-use exchanger implementation and specification.