Foundational and Compositional Verification of Layered Concurrent Objects

One solution to the above problem is to avoid arbitrary program structures and instead focus on programs inherently coming with a compositional program structure, thereby exploiting simpler and more effective compositional verification techniques. In this work, we focus on foundational verification of programs that can be decomposed into multiple abstraction layers, such that a lower layer provides the only operations that its upper layer can perform. This kind of programs is ubiquitous in practice, especially for systems software where layered structures are the most natural abstraction for hiding implementation details.

Following this idea, formal verification has been successfully carried out at large scale for both sequential and concurrent systems software organized into layers. For the former, the most notable examples include Deep Specifications for building certified abstraction layers [21], FSCQ [7], a file system whose end-to-end crash safety is established by composing the proofs of individual layers, and Argosy [5], a compositional framework for verifying layered file systems via recovery refinement. For the latter, the most notable examples include CertiKOS, the first concurrent OS kernel with fine-grained locking that comes with a functional correctness proof [22], seKVM, a verified hypervisor [56], HyperEnclave whose page tables are verified using the layered approach [9], and the Civl verifier [34] which extends the Boogie verifier [3] to support verification of layers of concurrent programs. All that work comes with foundational proofs except for Civl.

Despite those successes, the layered approach alone is not compositional enough to support reuse and extension of existing verified programs, which we elaborate below. The basic unit in this approach is a verified layer, written as $L_0⊢M_1:L_1$, denoting a module $M_1$ invoking APIs provided by a lower layer $L_0$ that in turn implements an upper layer $L_1$, as depicted in Figure 1(a). Its correctness is usually defined as a refinement or simulation between the semantics of $M_1$ running on $L_0$ and that of $L_1$, denoted by $M_1\otimes L_0⊑L_1$ where $\otimes$ is the linking operator. Modular verification is enabled by vertical compositionality of verified layers, as depicted in Figure 1(b) where $M_1\otimes M_2$ denotes the composed (linked) module in which invocations between $M_1$ and $M_2$ through $L_1$ become internal calls. For example, the entire CertiKOS kernel is divided into 38 layers ($L_0,\mathrm{\dots }{L}_{37}$) such that $L_{i-1}⊢M_i:L_i$ for $i\in \{1,\mathrm{\dots },37\}$ where $L_0$ provides the hardware interface and $L_{37}$ exposes the OS APIs. By verifying each layer $M_i$ and vertical compositionality, its correctness is established:

Now, suppose a third party would like to extend CertiKOS with a file system (which it currently lacks), which is formalized as $L_b⊢M_f:L_f$ where $L_b$ is the hardware interface $M_f$ uses and $L_f$ is the file system’s APIs. If $L_b$ is disjoint from $L_0$, one would expect to simply link the file system and CertiKOS side-by-side and get an extended kernel $L_0\otimes L_b⊢M_{\mathrm{𝐶𝑒𝑟𝑡𝑖𝐾𝑂𝑆}}\otimes M_f:L_{37}\otimes L_f$. However, this is not possible because the naive layered approach assumes each layer contains a global program state (e.g., CertiKOS uses one global log for each layer [23]). If this global program state gets extended, then all the proofs about them need to be updated. With the above example, the third party would need to

1. 1.

   Reprove CertiKOS with the extended lowest layer, i.e., prove $L_0\otimes L_b⊢M_{\mathrm{𝐶𝑒𝑟𝑡𝑖𝐾𝑂𝑆}}:L_{37}$;

2. 2.

   Reprove the file system with the extended lowest layer, i.e., prove $L_0\otimes L_b⊢M_f:L_f$;

3. 3.

   Link them together to get $L_0\otimes L_b⊢M_{\mathrm{𝐶𝑒𝑟𝑡𝑖𝐾𝑂𝑆}}\otimes M_f:L_{37}\otimes L_f$.

The first and second steps update and reprove the invariants on the global state with non-interference properties between $L_b$ and every layer of CertiKOS. For linking to succeed, they should use the same invariants. All those involve an undesirable amount of work.

In summary, because of the existence of global states, verified layers could only support horizontal composition with the same lower layer (as depicted in Figure 2(a)), not with independent layers (as in Figure 2(b)). This limitation significantly undermines the value of verified layers, as they cannot be reused without breaching their modularity. This observation is general for naive verified layers and not limited to CertiKOS. For example, both the authors of Civl [34] and seKVM [40] observe that extension of verified layers requires substantial rewriting of proofs and relies heavily on automated proof generation to reduce manual efforts.

One solution to the above problem is to divide a layer with a single global state into objects encapsulating their local states underneath a set of operations so that only through them the local states can be accessed or modified. As a result, we get an even finer-grained compositional structure where non-interference between objects in a single layer may enable the desired horizontal composition. This idea has been successfully realized in the sequential setting. A notable example is the ConFrm framework [25] for verifying sequential file systems that supports both vertical and horizontal compositions. ConFrm verifies layers by establishing refinement mappings [1], i.e., deterministic mappings from implementation states to specification states, by viewing function calls as atomic steps. Horizontal composition is achieved by composing independently verified objects operating on disjoint local states, and deriving a new refinement mapping from those for individual objects. Vertical composition is immediate because of the transitivity of refinement mappings which are essentially functions.

However, adapting this approach from sequential to concurrent settings faces significant challenges. In the presence of multiple threads and non-determinism, a concurrent program must be prepared for operations to be invoked and interleaved at arbitrary points during execution. Consequently, function calls can no longer be regarded as atomic steps. This necessitates mixing of simulation techniques beyond refinement mappings – such as forward, backward, or hybrid simulations with non-deterministic mappings to sets of states [26, 13] – for verifying layers with different levels of non-determinism. This not only complicates foundational verification where new concurrent semantic models and proof techniques are needed, but also makes it unclear if vertical and horizontal compositions still hold when a uniform simulation that is both vertically and horizontally compositional no longer exists.

A solution to supporting verified concurrent objects cannot be easily obtained by modifying existing layered verification frameworks for concurrency. In those frameworks, each layer is verified following the Owicki-Gries style [47] where threads are basic units of reasoning and rely-guarantee conditions of a single global state for threads are employed [27] (e.g., Civl uses yield invariants [36] to reason about thread interference on global states and CertiKOS [22] and subsequent verified hypervisors [56, 9] use global invariants to model interference between threads and CPUs). Obviously, this approach does not answer the question of how to prove non-interference between objects with isolated local states residing in a single layer.

The most recent development for solving this problem is the compositional theory of linearizability [24] based on game semantics [46]. It focuses on linearizable concurrent objects and encodes them into inherently composable denotations of objects, i.e., saturated strategies in game models [18]. As such, vertical and horizontal compositions become possible through algebraic operations on strategies. However, this denotational approach makes foundational verification significantly more difficult. Previously, abstraction layers are given operational semantics, or even written as structured imperative programs (as in Civl [36]). Therefore, the well-known operational techniques (e.g., simulations) for proving refinements are directly applicable. With game semantics, specialized program logics are needed to prove denotational refinements between implementations and specifications [46], and complicated translations between strategies in the mathematical domain and program states are needed in every step of reasoning in the program logic. As such, the framework for compositional linearizability has not yet been formalized in a theorem prover.

We propose an approach to addressing the challenges for verifying layers of concurrent objects, which leads to a framework that is both foundational and fully composable (both horizontally and vertically composable). As shown in Table 1, our framework overcomes the limitations of previous state-of-the-art (SOTA) approaches and supports all the desired features for the first time. Its key ideas are 1) to treat concurrent objects as labeled transition systems (LTS) allowing for non-atomicity so that conventional operational reasoning is directly applicable to generated foundational proofs, and 2) to obtain full compositionality by encapsulating both the state and control information of concurrent objects in LTS and using trace refinements [11] (i.e., inclusion of execution traces consisting of observable events generated by concurrent objects) of LTS as the uniform notion of correctness. The detailed contributions are described below (the full development is formalized in Rocq; see the supplementary materials).

• $\mathrm{■}$

  We introduce a novel form of labeled transition systems (LTS) that encapsulate both local states and control information (i.e., threads) of concurrent objects beneath interfaces that can both be invoked by upper layers and call into lower layers. It not only enables non-atomicity of concurrent function calls, but also enables hierarchical construction and horizontal composition of concurrent objects. As such, we could encode both concurrent objects (i.e., $L$ in Figure 2) and its implementation (i.e., $M$ in Figure 2) as LTS.

• $\mathrm{■}$

  Based on our semantic model, we develop a proof system for compositional verification of multiple layers of concurrent objects. The correctness of layered objects is formalized as trace refinements between LTS, i.e., inclusion of execution traces consisting of interface-level events generated by concurrent objects. We show that, by exploiting the operational structure of objects (instead of eliminating them as in denotational semantics), vertical and horizontal compositions of trace refinements are possible (because non-interference between threads and states in our LTS allows traces to be projected and combined along the LTS structures as we discuss in §6). That is, full compositionality for layered concurrent objects is achieved by using trace refinements as a uniform notion of correctness.

• $\mathrm{■}$

  We demonstrate that foundational verification of layered concurrent objects is possible by exploiting conventional operational techniques. In particular, trace refinements of LTS are derivable via either forward or backward simulations. In contrast to the denotational approaches, our framework keeps states and transitions explicit in the semantic model, enabling simulation-based proofs by avoiding complicated translation between traces and program states. In contrast to existing operational approaches (e.g., ConFrm), our framework does not rely on a particular form of simulation (which may only work in specific concurrent settings) and instead employs simple trace inclusions as the correctness definition, which works in any concurrent setting and enables full compositional reasoning.

• $\mathrm{■}$

  As case studies, we have verified a hierarchical implementation of concurrent timers based on forward simulation, and a lock-free bounded queue implemented using arrays based on backward simulation. Those studies show that our verified object layers are both reusable and extensible for modular construction of large concurrent objects from smaller ones.

In this paper, we consider concurrent programs with preemptive semantics in the setting of sequential consistency, i.e., atomic steps of concurrent processes may freely interleave with each other. In fact, our basic transition systems allow more liberal behaviors and obey sequential consistency only because of an intentionally placed constraint. It indicates that this work may be extended to work with weak memory model, which is left for future work. For generality of our approach, we avoid talking about specific programming languages by using transition relations over abstract states and pseudo code to describe programs. Connection with actual code requires further refinement and is also left for future work. Finally, we only investigate safety properties and leave liveness verification to future work.

In the rest of the paper, we first introduce the background and challenges in §2. We then present the key ideas in §3. In the subsequent three sections, we discuss our technical contributions. We then present evaluation in §7. Finally, we discuss related work and conclude in §8.

The example concerns verification of two concurrent data structures in a layered fashion, as shown in Figure 3(a). The first one is a clock (called Timer) with two operations: TICK increments time by one minute, and TIME returns the current time (in hours and minutes). To implement them, Timer calls an underlying Counter which also has two operations: INC and GET for incrementing and reading a natural number, respectively. Counter itself uses a Register (provided by hardware) to implement counting via compare-and-swap (CAS) instructions. The pseudo code for their implementations is shown in Figure 4. Note that, in this and remaining figures, we assume each atomic step (also called an action) is numbered (which may span multiple lines of code). Note also that the only shared state in Figure 4 is the global variable reg (the register value), with remaining variables local to each function.

The second data structure is a bounded queue (called Queue) which provides two operations: ENQ for appending an element to the tail (if the queue is not full), and DEQ for removing and returning the head element (if the queue is not empty). Queue is given a lock-free implementation following [8]. It uses an array (called Array and given by hardware like registers) with a fixed size $N$ and two Counter (modulo $N$) for recording head and tail indices of Queue, respectively. An example of bounded queue of size 6 is shown in Figure 3(b), which is a snapshot after concurrent enqueue of $\{1,2,3,4\}$ and dequeue of the first element (which happens to be $3$). The code of Queue is given later in Figure 17 when it is needed.

On its own, Timer can be proven correct by layered refinement following the structure in Figure 3(a), which in turn requires verifying Counter. However, the proof of Counter cannot be reused as is to prove Queue, for the same reason as we discuss the extension of CertiKOS with a file system in §1. To see that, let us first look at how Timer and Counter are verified.

A concurrent program is correct if it refines its specification, meaning that all its possible behaviors are allowed by the specification. These behaviors are captured by the preemptive semantics of concurrent programs that describes interleaving of atomic execution steps (or actions) during execution. The first row of Figure 5 shows a sequence of interleaving execution steps for Counter when threads $1$ and $2$ invoke and execute the INC and GET operations. Each node represents the current counter value in reg. Each arrow is labeled with the thread identifier and the action performed. There are three kinds of actions: function calls (e.g., INC), function returns denoted with the suffix ok (e.g., READok 0), and internal steps (e.g., v:=0). Following this sequence, thread $1$ completes the INC operation, updating reg to $1$, while thread $2$ reads the updated value but has not yet returned from GET.

To prove Counter correct, we define its specification in Figure 6. It abstracts Register by maintaining a global variable cnt for counting. INC and GET capture the intended behaviors: the former counts by $1$, and the latter directly returns the counter value. An execution of threads $1$ and $2$ invoking INC and GET is shown in the second row of Figure 5. Each node contains the value of cnt and concurrent interleaving assumes atomic actions in Figure 6.

An implementation $M$ refines its specification $L$, denoted by $M{⊑}_{R}L$ if there exists a forward simulation with an invariant $R$ relating states of $M$ to $L$. For the counter example, we establish $M_{\text{cnt}}^{\prime }{⊑}_R{L}_{\text{cnt}}$ where $M_{\text{cnt}}^{\prime }$ denotes the combination of code in Figure 4(a) and 4(b) and $L_{\text{cnt}}$ denotes Figure 6. Here, $R=\{(\text{reg},\text{cnt})|\text{reg}=\text{cnt}\}$, i.e., $R$ is identity (also written as $R(\text{reg})=\text{cnt}$). It is easy to check the execution of the implementation is simulated by the specification while preserving $R$, as Figure 5 shows where vertical lines represent $R$.

A verified layer, denoted by $L_0{⊢}_R{M}_1:L_1$, is a concurrent program $M_1$ running on top of a specification $L_0$ to correctly implement the specification $L_1$, i.e.,

We adopt the notation of Certified Concurrent Abstraction Layers (CCAL) [23]. Similar definitions are found in other works on layered refinement [34, 36, 35]. Then, $L_{\mathrm{𝑟𝑒𝑔}}{⊢}_R{M}_{\mathrm{𝑐𝑛𝑡}}:L_{\mathrm{𝑐𝑛𝑡}}$ holds where $L_{\mathrm{𝑟𝑒𝑔}}$ and $M_{\mathrm{𝑐𝑛𝑡}}$ denote Figure 4(a) and Figure 4(b), respectively.

With the implementation of counter abstracted into $L_{\mathrm{𝑐𝑛𝑡}}$, we can now prove the correctness of Timer by using $L_{\mathrm{𝑐𝑛𝑡}}$. Given a timer specification $L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$, we prove $L_{\mathrm{𝑐𝑛𝑡}}{⊢}_S{M}_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}:L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ where $M_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ denotes Figure 4(c) and $S$ is an invariant ($L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ is in our Rocq code). By vertical composition of the verified layers $M_{\mathrm{𝑐𝑛𝑡}}$ and $M_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$, we prove that $L_{\mathrm{𝑟𝑒𝑔}}{⊢}_{R\circ S}{M}_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}\otimes M_{\mathrm{𝑐𝑛𝑡}}:L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ where $R\circ S$ is the transitive composition of $R$ and $S$. This concludes that the complete implementation of timer in Figure 4 is correct with respect to its specification $L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$.

However, existing approaches provide limited support for reusing or extending verified layers. Consider verifying the bounded queue in Figure 3, which makes use of two counters and an array. We naturally would like to exploit the already established correctness of Counter. That is, to compose two instances of Counter to prove the implementation of two counters (each relying on its own register) is correct with respect to their specification. Figure 7 illustrates this desired horizontal composition where a single counter (and register) layer is extended with another one by duplicating the state and method.

Unfortunately, such horizontal composition is not supported in verified layers with global states. One instead needs to update the global invariant from $R(\text{reg})=\text{cnt}$ to $H({\text{reg}}_0,{\text{reg}}_1)=({\text{cnt}}_0,{\text{cnt}}_1)$ and go through the following proof steps as discussed in §1.1:

1. 1.

   Prove $L_{\mathrm{𝑟𝑒𝑔}}^0\otimes L_{\mathrm{𝑟𝑒𝑔}}^1{⊢}_H{M}_{\mathrm{𝑐𝑛𝑡}}^0:L_{\mathrm{𝑐𝑛𝑡}}^0$

2. 2.

   Prove $L_{\mathrm{𝑟𝑒𝑔}}^0\otimes L_{\mathrm{𝑟𝑒𝑔}}^1{⊢}_H{M}_{\mathrm{𝑐𝑛𝑡}}^1:L_{\mathrm{𝑐𝑛𝑡}}^1$

3. 3.

   Compose them into $L_{\mathrm{𝑟𝑒𝑔}}^0\otimes L_{\mathrm{𝑟𝑒𝑔}}^1{⊢}_H{M}_{\mathrm{𝑐𝑛𝑡}}^0\otimes M_{\mathrm{𝑐𝑛𝑡}}^1:M_{\mathrm{𝑐𝑛𝑡}}^0\otimes L_{\mathrm{𝑐𝑛𝑡}}^1$

To prove the first two steps, we need to show that there is no interference between $M_{\mathrm{𝑐𝑛𝑡}}^0$ and $L_{\mathrm{𝑟𝑒𝑔}}^1$, hence the execution of $M_{\mathrm{𝑐𝑛𝑡}}^0$ maintains the invariant for $L_{\mathrm{𝑟𝑒𝑔}}^1$. Although this may seem obvious in this example, it requires substantial changes to the old proof because function calls are not atomic in a concurrent setting. Furthermore, in more complicated situations, non-interference may be violated and results in failure of proofs. For example, this could happen if we replace ${\text{GET}}_i(i\in \{0,1\})$ in Figure 7(b) with the following implementation:

In our example, the state of a counter is only accessed by INC and GET (i.e., the ill-behaved case above does not happen). Therefore, non-interference between a counter and its environment is immediate if we could encapsulate the counter’s state under INC and GET. That is, by dividing a verified layer into encapsulated and verified objects, we may achieve the desired horizontal composition in Figure 7(c).

ConFrm [25] implements this solution for layered sequential programs. A verified object $L_0⊢M_1:L_1$ generalizes a verified layer by encapsulating local states in $L_i$. Due to encapsulation, invariants for proving individual objects are hidden from the outside. Therefore, the desired horizontal composition is possible without reproving non-interference properties.

However, ConFrm is designed for sequential programs, in that its semantics treat function calls as atomic steps, which is not compatible with concurrent methods (e.g., those in Figure 4) that could be interrupted arbitrarily during execution. Therefore, refinements provided by ConFrm could not directly handle our examples. Furthermore, different simulation techniques are needed for proving concurrent objects with different levels of non-determinism. For example, Counter and Timer could be proved via a forward simulation with deterministic invariants (i.e., essentially a refinement mapping), while the lock-free bounded queue needs a much more complex backward simulation [8]. If different layers of objects make use of different simulation relations, we inevitably need to combine them into some uniform notion of simulation. However, there is at least a dozen of such simulations, none of which is agreed as a standard and all of which seem quite non-trivial (even in a sequential setting [6]).

Compositional theory of linearizability [46] provides one way to solve the above problem. It shows that linearizability could be characterized as a relation between strategies in game models. By interpreting concurrent objects as strategies (i.e., a set of traces they could produce), locality of linearizability [24] is proved. As locality denotes non-interference and state encapsulation for linearizable objects, the horizontal composition in Figure 7(c) becomes possible by treating all $L$ and $M$ as linearizable strategies, as depicted on the right of Figure 8.

Theoretically, this approach is capable of verifying layered concurrent objects. In reality, it is highly difficult to generate foundational proofs with this approach. Despite its denotational nature, the actual proofs are carried out operationally with a non-trivial embedding of a program logic based on operational semantics [31] into game semantics. The soundness of this logic ensures operational proofs indeed imply refinements in game semantics. To carry out operational reasoning in this logic, one must define translation functions which decode denotational traces to get back program states of objects. For example, the translation function for Counter in Figure 8 is defined as follows:

where cntval translates any trace $p$ that contains only complete INC and INCok pairs into the number of INC events in the trace as the value of Counter (where $p_i$ denotes the ith event in $p$), and any other trace into a bottom value.

Using these auxiliary functions, the invariants are then formulated and proofs are built in the program logic. In fact, translation functions must be used in every step of proof building. This is already a lot of work for the small Counter example, and could get overwhelming for any non-trivial example (e.g., see page 71 of [46]). We conjecture that this complexity is why neither the compositional theory nor its accompanying case studies has yet been mechanized in a theorem prover at the time this paper is written.

We represent concurrent objects as labeled transition systems (LTS) that encapsulate both object states and all concurrent accesses. Such an LTS has interfaces for interacting with upper and lower layers, thereby enabling vertical composition. Horizontal composition with other concurrent objects becomes possible thanks to state and concurrency encapsulation. Below we illustrate key features of LTS by using the example in Figure 4. We rewrite it into an object-oriented style in Figure 9 to emphasize state encapsulation, i.e., global variables in Figure 4 become member variables, and to make the dependency between objects clear.

Recall that the basic component of layered verification is a verified layer of the form $L{⊢}_{R}M:L^{\prime }$ indicating that a library layer $L^{\prime }$ is implemented by a program $M$ invoking another library layer $L$. We generalize it to a verified concurrent object of the form $L⊢M:L^{\prime }$ in which a concurrent object $L^{\prime }$ is verified to be implemented by a concurrent program $M$ invoking the underlying object $L$. Here, $L:\mathrm{\varnothing }\to A$ and $L^{\prime }:\mathrm{\varnothing }\to B$ are closed objects, i.e., they do not depend on other objects (their underlying interface is empty), while $M:A\to B$ is an open object. We sometimes call the former an object and the latter an implementation (of an object) when it is obvious from context. Formally, a verified concurrent object is defined via trace refinement between the implementation and specification, as follows:

A trace refinement $M⊑M^{\prime }$ holds if the observable behaviors of $M$, i.e., traces containing only events in the interfaces, are also the observable behaviors of $M^{\prime }$. $L⊑\text{sc}L$ (or $M⊑\text{sc}M$) effectively means that $L$ and $\text{sc}L$ (or $M⊑\text{sc}M$) are observably equivalent since $\text{sc}N⊑N$ holds for any $N$. Therefore, $L$ and $M$ are both sequentially consistent. For example, we get the verified concurrent object $L_{\mathrm{𝑟𝑒𝑔}}⊢M_{\mathrm{𝑐𝑛𝑡}}:L_{\mathrm{𝑐𝑛𝑡}}$ by proving $L_{\mathrm{𝑟𝑒𝑔}}\overline{⊲}{M}_{\mathrm{𝑐𝑛𝑡}}⊑\text{sc}{L}_{\mathrm{𝑐𝑛𝑡}}$. An example of this refinement is given in Figure 14 which shows the observable behavior of the composed implementation (i.e., $[(\text{1, INC}),(\text{2, GET}),(1,\text{INCok})]$) also occurs in the specification. Verified concurrent objects enable foundational and compositional verification by exploiting the following features:

Compositional reasoning for verified concurrent objects is realized via the sound proof rules in Figure 16. VCOMP enables vertical composition of layers as described in Figure 1(b) except that a new vertical composition operator of LTS is used. HCOMP enables horizontal composition as described in Figure 2(b) which was not previously possible for vanilla verified layers. Notice that HCOMP makes use of $\overline{\otimes }$ instead of $\otimes$ to ensure that the horizontally composed objects are sequentially consistent. This is not necessary for VCOMP because 1) by definition its premises ensure $M_1$ and $M_2$ are sequentially consistent, and 2) the $⊲$ operator preserves sequential consistency. The remaining rules are for deriving final refinement results for composed objects. In particular, the linking rule LINK pushes the intermediate layer $M_1$ downwards and instantiates the underlying object that $M_2$ is built upon. The weakening rule WEAKEN enables replacement of an underlying layer with a more refined one where $L_1^{\prime }⊑\{L_1,\text{sc}{L}_1^{\prime }\}$ denotes $L_1^{\prime }⊑L_1$ and $L_1^{\prime }⊑\text{sc}{L}_1^{\prime }$.

A significant difference between our rules and existing work is that the former does not mention global state or global invariant. Therefore, they are more modular and succinct than before. For example, in CCAL (see Fig. 9 in [23]), horizontal composition employs rely-guarantee reasoning on global invariants; additional compatibility and parallel composition rules are needed for reasoning about multi-threading, which also employ global reasoning.

To get an intuition of how foundational and compositional verification work in our framework, we discuss the verification of our running example following the layered structure in Figure 3(a).

We have already proved the correctness of Counter running on top of Register in §3.2, i.e., $L_{\mathrm{𝑟𝑒𝑔}}⊢M_{\mathrm{𝑐𝑛𝑡}}:L_{\mathrm{𝑐𝑛𝑡}}$. We finish verifying Timer by following the same process as described at the end of §2.2. That is, we define the specification of Timer as an object $L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ (its definition is omitted and can be found in our Rocq proofs). We then prove $L_{\mathrm{𝑐𝑛𝑡}}⊢M_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}:L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ by forward simulation where $M_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ denotes Figure 9(c). By applying VCOMP, we get $L_{\mathrm{𝑟𝑒𝑔}}⊢M_{\mathrm{𝑐𝑛𝑡}}⊲M_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}:L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$, which is reduced to $L_{\mathrm{𝑟𝑒𝑔}}⊲M_{\mathrm{𝑐𝑛𝑡}}⊢M_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}:L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$ by LINK. Finally, by unfolding its definition and stripping away sc by observing sequential consistency of objects, we get $L_{\mathrm{𝑟𝑒𝑔}}⊲M_{\mathrm{𝑐𝑛𝑡}}⊲M_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}⊑L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$. That is, the Timer program in Figure 9 correctly implements (refines) its specification $L_{\mathrm{𝑡𝑖𝑚𝑒𝑟}}$.

We then verify the lock-free bounded queue (Figure 3(b)) whose code is presented in Figure 17. Queue is implemented by an Array object of size N which could be thought as a sequence of Register objects (i.e., with similar CAS and READ operations) implemented by hardware. A difference is that an element in the array is a structure of type elem with two fields: val for storing the actual value and ref for recording how many times this element has been modified. In particular, val could be null to indicate that no value is stored, and ref is a “version number” for distinguishing the same values appearing at different moments. Queue additionally employs two Counter objects as indices: front indexes the head of queue and rear indexes the tail of queue as shown in Figure 3(b); both are used modulo N.

Queue provides an enqueue operation ENQ and a dequeue operation DEQ. ENQ pushes a value to its tail. At line 1 and 2, it gets the value x at the tail. At line 3 to 5, it checks if any concurrent ENQ has taken effect. If so, it restarts from line 1. At line 6, the method attempts to enqueue v by invoking CAS on the array. If it succeeds, it increments the tail index at line 7. DEQ follows a similar strategy to pop the head value.

Verification of Queue is carried out in the following steps. First, we prove that Queue object correctly implements a top-level specification $L_{\text{queue}}$, which formalizes code in Figure 18 where both ENQ and DEQ are atomic operations over a list of size N. By assuming specifications for its underlying counters and arrays, we need to prove

where $L_{\text{ary}}$ denotes Array and $M_{\text{queue}}$ denotes Queue in Figure 17. Because Queue contains more sophisticated non-determinism, this is proved by backward simulation with a set of highly non-trivial invariants on object states (see Example 20). Unlike the existing approaches, such complexity is never exposed to users thanks to encapsulation of invariants.

Second, by applying HCOMP on $L_{\text{reg}}⊢M_{\text{cnt}}:L_{\text{cnt}}$ and $L_{\text{ary}}⊢M_{\text{id}}:L_{\text{ary}}$ where $M_{\text{id}}$ is an “copycat” implementation (i.e., identity), we get

Unlike the cumbersome rewriting shown in §2.3, we compose two verified counters as they are with minimum effort, thanks to encapsulation and isolation of interference between objects.

Finally, by vertical composition of (1) and (2) we get

By LINK and a sequence of WEAKEN, it is reduced to (where $M_{\text{id}}$ is absorbed):

By unfolding this definition and eliminating sc, we get the final trace refinement:

That is, the code in Figure 17 correctly implements the atomic concurrent queue in Figure 18.

In summary, the above example shows that verified concurrent objects can be foundationally verified, reused as they are, and freely composed with other objects. In the subsequent three sections, we shall formally discuss the above key ideas in more depth.

We first formalize the labeled transition systems equipped with layered interfaces.

The transition relations are organized according to the system’s layered interfaces. They precisely characterize how a transition system interacts with higher-level systems (via ${\to }_i$ and ${\to }_f$) and with lower-level systems (via ${\to }_x$ and ${\to }_y$). A key difference between our LTS and the traditional ones (like in CertikOS and ConFrm) is that ours by definition captures only the threads running inside the LTS, i.e., thread behaviors are encapsulated with the LTS, which enables horizontal compositionality (see §6.2). Additionally, we prefer to use explicit transition relations (rather than a single transition relation with multiple labels) to model interactions with the environment because of the openness and layered nature of our LTS. Since an implementation may both invoke and be invoked by its environment, such transitions are separated into queries and replies. Furthermore, because an implementation may interact with both upper and lower layers, these transitions are further classified according to their layers. Thanks to such explicit structures, formal definitions of operations on our LTS become more structured and intuitive, as we shall see in the rest of §4.

By definition, our LTS are quite liberal: they make no assumptions about the execution order of programs or threads. This could result in violation of sequential consistency as we discussed in §3.1. To solve this problem, we introduce a sequential consistency operator ($\text{sc}-$), which augments a transition system with an additional thread state $h$ that records the states of threads currently executing within the system. Each such thread is either actively running (denoted $\mathrm{𝑟𝑢𝑛}$) or waiting (denoted $\mathrm{𝑤𝑎𝑖𝑡}$) for the return of an external call, meaning that its control has been temporarily transferred to another transition system.

In the following sections, the sequential consistency operator will be used to define both horizontal and vertical composition, ensuring that the behaviors of threads in the composed system still satisfy sequential consistency.

We define horizontal composition as combination of two transition systems into a new system that integrates the functionalities of both components. To preserve sequential consistency, we first apply sc to the components before combining them together.

By definition, the horizontally composed LTS accepts any initial call to its components and behaves like one of its components after that. The transition rules of horizontal composition ensure thread encapsulation: after composition each transition is contributed by exactly one thread in one component, while the other component’s state remains unchanged. Horizontal composition also ensures that every thread is active only in a single LTS at any moment. In particular, we require that no thread may execute in both components simultaneously, ensured by the conditions in brackets (“[]”) in the invocation rules in Figure 22.

Vertical composition links objects in two adjacent layers by synchronization, which models interaction between LTS, and hiding, which abstracts away these interactions. It is similar to functional composition in game semantics [18], albeit applied to LTS instead of strategies.

We model synchronization as the control transfer of threads between two layers with a common interface. Consider two LTS $M_1:A\to B$ and $M_2:B\to C$ that share the interface $B$. When a thread $p$ executing in $M_2$ triggers an external call, we model its control transfer to $M_1$ by triggering a simultaneous invocation transition in $M_1$. Conversely, when $p$ reaches the end of a call into $M_1$ by performing a completion transition, its control transfers to $M_2$, represented by a simultaneous external return transition in $M_2$.

First, we formalize LTS with explicitly synchronized queries and replies called synchronized labeled transition systems, which serve as an intermediate form for vertical composition.

A synchronized LTS $G$ exposes an interface with three layers: it offers interface $C$ to the higher-level, relies on interface $A$ from the lower-level, and interacts internally via interface $B$. The first eight components of $G$ have the same meaning as in the standard LTS. Additionally, a synchronized LTS has two specialized relations: synchronized query transitions (${\to }_q\subseteq S\times P\times Q_B\times S$) and synchronized reply transitions (${\to }_r\subseteq S\times P\times R_B\times S$), which model interactions via interface $B$ in the system.

As indicated by their multilayer interfaces, the synchronized query and reply transitions are still observable to the environment in synchronized transition systems, which provides information for deriving vertical compositionality (see §6.3). However, these interactions are desired to be abstracted away when this composite system is used as a building block for more complex systems. We formalize this abstraction as hiding.

Finally, we define vertical composition as the combination of synchronization and hiding.

The composition operators ($-\overline{\otimes }-$ and $-\overline{⊲}-$) apply sc to enforce sequential consistency. This raises two issues. First, traces of $M$ that violate sequential consistency are silently removed by $\text{sc}M$, so verifying $\text{sc}M$ does not convincingly establish properties of $M$ itself. Second, each composition reapplies sc, introducing unnecessary reasoning overhead.

To address the first issue, we treat sequential consistency as a property to be verified, rather than an inherent assumption about every transition system. Consequently, we decouple the sc operator from the composition operators, which also solves the second issue. Below, we define such plain composition operators and establish refinements with the original ones.

We call this plain horizontal composition as it does not concern itself with consistency of threads during execution. Similarly, we define plain synchronization and vertical composition.

We decouple the sc operator from composition by the following extraction lemmas (See the extended version of the paper for the detailed proofs of extraction lemmas).

We establish horizontal composition by proving soundness of HCOMP in Figure 16 (soundness of VCOMP is in §6.3, and the remaining rules are straightforwardly sound). As stated in Theorem 26, two verified concurrent objects relying on separate lower-level objects can be horizontally composed into a new verified concurrent object. This follows from encapsulation of threads and invariants in our transition systems, which prevents interference across objects.

By unfolding the definitions, Theorem 26 is reduced to proving that trace refinement is preserved after horizontal composition, as shown in Lemma 27.

This can be derived by further proving that the execution of a horizontally composed system can be projected to the execution of its two components, and that the execution of components can be again combined to form an execution of the composite system, as follows.

Horizontal projection states that an execution of the horizontal composition can be decomposed into the executions of its two components (${\circ }_X\text{es}$ denotes the subsequence of es consisting only of events in $X$):

Horizontal combination states that the executions of two transition systems can be interleaved to form an execution of their horizontal composition. It is more subtle than horizontal projection because we must ensure that every event in the interleaved trace is admissible in the horizontally composed system, which preserves sequential consistency. We introduce the notion of horizontal consistency ($h_1|h_2{⊢}_h\text{es}$) to capture such constraints (See the extended version for the definition of horizontal consistency).