TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

Safety arguments are centred around invariants: That is, facts of the form always P, encoded using regions in TaDA. TaDA Live’s basic observation is that to represent help from the environment, all that is needed is liveness invariants: That is, facts of the form always eventually P. By combining liveness invariants and safety invariants one can encode more complex progress conditions such as . To represent liveness invariants in a thread-local way, TaDA Live introduces a new kind of ghost state called obligations. Similarly to guards, they form a PCM. The interference protocol is augmented by a component that explains how an update affects the obligations. In our example, we want to represent the liveness invariant always eventually which, together with the invariant that can only be set to 1, implies . We therefore introduce an obligation (for pdate-to-1), where again undefined captures exclusivity, and extend the protocol to link to the update:This transition to update the region can be executed by a thread with both the guard and the obligation; the effect of the update is to “consume” the resource, as the obligation resulting from the update is the unit . We say the update fulfils the obligation .

A safety rely, as expressed by specification (1), says: Verify a thread under the assumption that the environment steps will obey the protocol. As a first approximation, our liveness rely, as expressed by Equation (2), additionally says: Verify a thread under the assumption that the environment will always eventually fulfil the obligations it owns. (We will refine this idea in the next section to avoid unsound circular reasoning.) We say an obligation is assumed live if the environment always eventually fulfils . In other words: If, at any time, the environment owns , it eventually fulfils .

This idea introduces a complication: We need to locally keep track of which (relevant) obligations are owned by the environment to make use of the liveness rely assumption. We solve this problem by taking inspiration from the concept of subjective separation of Reference [29]. We introduce subjective obligation assertions: local obligations, , asserting local ownership of the obligation associated with region , and environmental obligations, , asserting environment ownership of the obligation . What makes these assertions interesting is the way they compose: That is, . If we start with local obligation and we want to fork into two threads, then we use to give responsibility of to one thread and knowledge that the environment has this responsibility to the other.

To complete the proof sketch for our example, we first need to extend the region interpretation by adding the obligation protocol:²When the value at is 1, the obligation is owned by the interpretation, and hence owned by no thread. A thread owning and setting to 1 fulfils the obligation precisely by leaving it inside the interpretation. There is no other way of losing ownership of an obligation, because we adopt a classical interpretation of separation: That is, . For soundness, the interpretation of a region with ID is only allowed to own obligations of .

The TaDA Live proof starts by using viewshift to transform the resource in the precondition into this new region that is shared between the two threads:where and are the preconditions of the proofs of and , respectively. To discharge in the proof of the while loop of , we can use , which holds throughout the loop: If we are in a state , then either , in which case we are in a target state and the value of will remain 1 forever; or in which case we know . By the liveness rely, when the environment owns , it will eventually fulfil it, which by Equation (2) can only be done by setting . Section 4 explains in detail how this argument is carried out formally in TaDA Live.

At this point, we are able to prove the total triples and . However, the standard parallel rule is unsound in the sense that the two triples can be proven even with but, in this case, the parallel composition would not terminate! TaDA Live’s parallel rule can recover soundness by checking that the postconditions of the two threads do not own pending obligations, which we can show by proving the stronger triples and . This condition is too restrictive in general, and we will relax it appropriately in the next section.

Structuring liveness invariants through obligations, as sketched, presents a significant problem for soundness due to the possibility of making unsound circular liveness assumptions. Consider the following variant of our busy-waiting example:There are two shared heap cells at and , respectively. The thread on the left () is busy-waiting on , which is supposed to be set by the thread on the right (), and vice versa, causing a classic high-level deadlock³ situation: The program does not terminate.

Let us try to replicate the argument we used for the busy-waiting example. We require a region sharing both cells, , where is the value stored at . We use two guards and , and two obligations, and linked to the update of and , respectively:Without additional precautions, we would be able to derive the triples (for )where . Given the interpretation we sketched earlier, these triples mean: Thread terminates provided its environment (i.e., thread ) always eventually fulfils obligation . This leads, in the application of the parallel rule, to an unsound circular argument: To show thread fulfils obligation , thread is relying on the assumption about the eventual fulfilment of by the environment, which, in turn, relies on the eventual fulfilment of by thread itself. The question is then: How can we rule out circular arguments, while keeping the proof thread-local? In particular, we want a solution that allows us to keep the abstraction of the environment as local and abstract as possible, without revealing unnecessary structure of the other threads.

Our solution is to specify dependencies between liveness invariants. We do this by imposing a partial order on obligations: Each obligation is associated with a layer, denoted lay , which is an element of a user-defined well-founded partial order, . Using layers, we can refine our reasoning principle and gain soundness: To be allowed to assume is live, one has to show all the locally owned obligations have layers greater than lay . The intuition is that local fulfilment of can depend on the environment’s fulfilment of only if lay .

In our deadlocking example, layers expose the circularity issue and prevent the triples (5) from being derivable. Specifically, the proof of the loop of requires us to prove . At this point, we are continuously holding the obligation so, to be able to assume live, we require lay . However, the proof of the loop of would require the symmetric constraint, lay , leading to a contradiction.

If we replace with , then the program terminates and indeed the proof goes through with lay . This is because the first instruction of fulfils so the loop no longer constantly owns it while assuming live. The structure of does not impose any dependency on the two liveness invariants.

The generalisation of the liveness rely to use obligations with layers enables us to give a general parallel rule: Instead of just forbidding pending obligations in the postconditions, we require that the postcondition of each thread only owns obligations with layers greater than the layers of obligations assumed live in the other thread’s proof.

Let us contrast our layered obligations with other solutions found in the literature. The LiLi logic cannot verify the above examples, as it lacks support for parallel composition.⁴ LiLi’s while rule does share the same high-level structure as WhileB, a structure that can be traced as far back as Reference [37]. The main crucial difference is in how is proven. LiLi proposes the idea of definite actions, a reincarnation of “leads-to” assertions of Reference [37], to build a liveness rely. Definite actions require the identification of a logical global “queue” of threads where the thread at the front is always able to execute its action and that action implies global progress. In LiLi, the target states are the ones where the local thread is at the head of this queue, and the condition is proven by showing that when the head of the queue executes an action, there is some local well-founded progress measure that decreases. Definite actions have a number of drawbacks:

Layered obligations are key to resolving these problems:

There has been work on proving various safety (e.g., global deadlock-freedom) [16, 27] and progress (e.g., deadlock-freedom, termination) [3, 22, 26, 28] properties of concurrent programs, which assume the only source of blocking behaviour comes from the use of blocking primitives (e.g., built-in locks or channels). Although none of them can handle busy-waiting patterns like our previous examples, they typically detect deadlocks using “tokens” (often also called obligations) that represent the responsibility to call a blocking primitive. These tokens are arranged in an acyclic graph of dependencies. Superficially, these tokens are related to our layered obligations in that they both are devices to rule out cyclical dependencies. There are, however, deep differences between the two. Tokens are linked (ad hoc in the operational semantics and through ghost code) to blocking primitive operations calls, and dependencies between the tokens represent causal dependencies between these primitive events. By contrast, our layers represent dependencies between liveness assumptions and reflect a purely logical structure. This makes our layered obligations particularly general and flexible: They are able to express arbitrary high-level blocking patterns and not just primitive blocking operations, enabling truly abstract specifications.

Understanding blocking behaviour as the need for an abstraction of the environment that includes liveness invariants unlocks a novel approach in giving abstract, precise and reusable total specifications for abstractly atomic operations. Building on Total TaDA, we propose a new specification format that expresses the atomic effect of a linearisable operation, and succinctly states the liveness invariant required for ensuring termination, at the right level of abstraction. To see the problem and our solution, let us consider the paradigmatic example of two fine-grained implementations of a lock module.

Two Lock Implementations. Consider the spin lock and the CLH lock given in Figure 1. The implementations enable threads to compete for the acquisition of a lock at address by running concurrent invocations of the operation. Only one thread will succeed, leaving the others to wait until the operation is called by the winning thread.

The primitive commands, such as assignment, lookup and mutation, are primitive atomic and non-blocking: every primitive command, if given a CPU cycle, will terminate in one step. Since reads and writes may race, the language is equipped with a compare-and-swap primitive command, , which checks if the value stored at is : If so, it atomically stores at and returns 1; otherwise it just returns 0. Similarly, the fetch-and-set primitive command, , stores at returning the value that was stored at just before overwriting it.

The spin lock in Figure 1 is standard. Its state comprises a heap cell at that stores either 0 (unlocked) or 1 (locked). The Craig-Landin-Hagersten (CLH) lock [18] in Figure 1 serves threads competing for the lock in a FIFO order. It queues requests, keeping a head and a tail pointer (at and , respectively). The predecessor pointers are stored in each thread’s local state (in ). The lock can be acquired by a thread once its predecessor signals release of the lock by setting its queue node to 0. Unlocking the lock corresponds to setting the queue’s head node value to 0.

Let us focus on the lock operation of the CLH lock. The interesting aspect is that displays blocking behaviour that is observable by the client of the module (it is indeed the quintessence of blocking). We cannot just provide a total triple for it: The operation does not always terminate. The challenge is to design a specification format that accurately captures the abstract functionality of the operation and its subtle termination properties.

First off, one would like a specification that hides the implementation details and only exposes the abstract state of the lock to the client: A lock instance is represented by an abstract resource ,⁵ where indicates the lock is locked, and means it is unlocked. It is worth noting that traditional Hoare triples are not able to represent the useful behaviour of . The triple requires the client to establish that the lock is unlocked before calling the operation, defying the very purpose of the operation’s functionality. The triple allows the operation to be called in the locked state, but is not precise enough, since the same triple holds for a simple assignment . It does not express the property that, upon termination of the operation, we can claim that we have acquired the lock. A partial specification of a lock is already a challenge; a total specification more difficult still.

Proposed solutions in the literature can be divided into history-based, refinement-based, and abstract atomicity-based approaches. The history-based approach (e.g., Reference [38] for safety, References [15, 25] for progress) is expressive but at the price of complex and indirect specifications; the verification requires explicit manipulation of the histories, complicating client reasoning. The only progress-aware refinement-based approach that can modularly verify the CLH lock is the LiLi logic [31]. LiLi’s refinement is progress-preserving and contextual, allowing the result to be reused in arbitrary client contexts. For example, the LiLi proof for CLH lock (under weak fair scheduling) shows thatwhere is defined (in pseudocode) as⁶

The abstract state of the lock is represented by , but to represent the fact that threads will not be starved, an abstract FIFO queue at keeps track of the threads to be served; morekeywords=self]self is the thread ID of the caller. The command morekeywords=await]await(){} is a blocking primitive introduced to express the non-primitive blocking of the implementation. The potential absence of progress of the implementation’s busy-waiting steps is represented by potential absence of a step ahead in the specification.

LiLi’s specification style has three major drawbacks:

These problems limit the abstraction capabilities, proof reuse, and scalability of the approach.

The abstract atomicity approach has been pioneered by the TaDA logic. It directly influenced logical atomicity in Iris [24] and was extended to provide total specification for non-blocking programs in Total TaDA [8]. The aim of the TaDA approach is to keep the Hoare-triple style of specification while being able to give precise and abstract specifications to fine-grained code like CLH lock. The TaDA solution is to provide a Hoare triple for , which embraces the fact that, between the invocation of the operation and the execution of the atomic update of the lock, there is a phase of interference where the environment can change the value of the lock. It is important to be able to distinguish the imprecise precondition that holds during the interference phase, , and the precise precondition, , that holds just before the atomic update performed by the lock operation at its linearisation point [20].

The TaDA safety specification for is the partial atomic triple:The interference precondition describes the interference phase. It states that the environment must preserve the existence of the lock at but may change the value of , and the implementation of the lock must tolerate these environmental changes. The pseudo-quantifier is unusual, behaving like an evolving universal quantifier in that the environment is able to keep changing over time and behaving like an existential quantifier in that the implementation can assume that the lock always exists with . The triple (6) states that, if the environment satisfies the interference precondition and the operation terminates, then the implementation guarantees that, just before the linearisation point, the lock must have been available for locking () and, just afterwards, the lock has been locked by the operation (). Exclusive ownership of the lock after the operation terminates can be derived from the assertion in the postcondition: Just before we locked it, nobody else could claim that they owned the lock. The TaDA safety specification for is the partial atomic tripleThis triple⁷ states that, to be used correctly, the unlock operation requires the lock to be locked and not changed by the environment during the interference phase; in return, the operation promises to atomically set the lock to be unlocked.

TaDA Live builds on the TaDA specification format. To turn the TaDA triple for into a total specification, the termination guarantee must depend on the environment: If the environment decides to hold the lock indefinitely, then no lock implementation should allow the operation to terminate. Hence, we express blocking as a liveness condition on the environment during the interference phase of an abstractly atomic operation. The CLH operation will terminate under weak fairness, provided that, if the lock is locked by the environment during the interference phase, then the environment will eventually unlock it. In general, a blocking operation will require an environment that is live: It will always eventually bring the abstract state to a good (e.g., unlocked) state.

The TaDA Live total specification of the CLH operation is:The interference precondition is with the pseudo-quantifier now incorporating the environment liveness condition. As well as stating that the environment can keep changing the lock, the interference precondition also states that if the lock is in a bad state (), then the environment must always eventually change it to a good state (). The implementation needs to ensure termination under the assumption that the lock always eventually returns to the unlocked state. Note that the environment is allowed to change back to 1 arbitrarily many times, provided it always eventually sets it back to 0. To see why this is enough to ensure termination, consider Figure 2(a), where we chart the evolution of the abstract state induced by a live environment in the interference phase of . Progress towards termination of is guaranteed by the progress measure charted in Figure 2(b): Every time the environment unlocks, the value of decreases from 1 to 0; when the environment locks, although increases to 1, the number of threads in front of us in the queue decreases. One crucial aspect of our specification design is that we do not want to expose the progress argument to the client unless part of the argument needs to be made by the client. With CLH, the part of the argument appealing to the queue of threads is completely internal to the implementation of the operation, while the argument for the environment’s liveness must be provided by the client (the implementation has no power over this). We prove this formally in Section 5.

Now let us consider the spin lock implementation. The spin operation cannot promise to terminate just by relying on a live environment. The problem is that when the environment locks the lock, there is no measure of progress that decreases: We are genuinely delayed by this action. We call this effect impedance. We conceptualise impedance as a greater leaking of the progress argument to the client. In the spin lock example, the whole of the progress argument needs to be provided by the client: The client needs to ensure that the environment will always eventually unlock the lock and that it will only impede the operation a bounded number of times. To represent this extra bounded impedance requirement (depicted in Figure 2(c)), we extend the abstract state of the lock with an ordinal , an impedance budget that strictly decreases when the lock state is set to 1. We arrive at the following TaDA Live specification for spin :The lock is now represented by the predicate assertion with ordinal , which can also be changed by the environment during the interference phase. As well as expressing the dependency on a live environment on , this triple states that every operation consumes the budget by a non-trivial amount, thus providing a logical measure of progress from good to bad states. The initial value of the budget and the function from ordinals to ordinals is determined by the client, which must demonstrate that the budget is enough to make all its calls.

The TaDA Live total specification of for the CLH is the same as the TaDA partial specification. By contrast, the TaDA Live specification of for the spin lock needs to incorporate the ordinals: The impedance budget is preserved by unlock. This encodes the fact that does not impede the other operations, but also that by unlocking we cannot increase the budget. By combining these assumptions about the budget (it decreases when locking, stays constant when unlocking), it is possible to conclude that the implementation of the spin lock terminates using the progress measure in Figure 2(d). Crucially, for spin lock, the whole of the progress argument is provided by (and thus visible to) the client.

The impedance budget technique was first introduced to concurrent separation logics for non-blocking operations in Total TaDA [8]. Here, we smoothly integrate ordinals into TaDA Live, which fully supports blocking.

The TaDA Live program logic works with hybrid triples of the form:which generalises both Hoare triples and abstract atomic triples. This triple comprises: a pseudo-quantifier with its environment liveness condition; atomic pre-/post-conditions and ; and Hoare pre-/post-conditions, and . The Hoare pre-/post-conditions describe stable resources that are owned locally by and can be updated non-atomically. Hoare triples correspond to the case where and . Abstract atomic triples correspond to the case when and are empty. We have omitted some details from the hybrid triples, such as layers and levels, since they are not important for the ideas of this section; the full details are given in Section 3.8.

The integration of the liveness annotations in triples achieves the goal of keeping the specification abstract and atomic. To obtain the goal of reuse of proofs, there are two missing ingredients: a mechanism to make use of the assumption in a proof of an implementation of the specification; and a way to reuse the specification in an arbitrary client context.

Imagine proving the CLH implementation correct with respect to specification (7). The while loop needs to discharge that “finally, the current thread is at the head of the queue, and the lock is unlocked.” This can only be proven with the help of the liveness assumption coming from the lock specification. To this end, in addition to liveness assumptions given by obligation assertions, TaDA Live extends judgements to allow contexts with liveness assumptions, used to discharge the condition in the while rule. The full details are given in Section 3.8.

Now consider proving a client of a lock using the specifications of the lock operations for the calls to these operations. This requires the Liveness Check rule:The rule’s crucial effect is to remove the liveness annotation , which can only be done in a situation where the corresponding liveness assumption is satisfied. Just like the WhileB rule, we frame an assertion which is information that holds for the duration of the call. Typically, asserts the existence of some shared region and that the environment holds some obligations depending on the state of the region. We also need to provide a set of target states capturing when (second premise). The crucial check of the rule is the first premise, which examines the traces where holds everywhere, and asks us to prove that in those traces we see satisfied infinitely often (and thus infinitely often). If that is true, then we can conclude that the command terminates in the current context without the extra assumption in the pseudo-quantification. The resulting triple can then be manipulated using standard TaDA reasoning.

Take the typical use of (CLH) locks in a client . To share the lock resource , the client proof would specify some region where is the abstract state of the lock. A typical client would include the abstract state of other shared resources, too, but for simplicity, we focus here on the lock. The client needs to specify in its protocol that the lock will be always eventually unlocked by the threads sharing it. We therefore introduce an exclusive obligation (the ey of the lock), which is obtained when locking the lock and fulfilled when unlocking it:The protocol is mirrored in the region’s interpretation .

With the application of standard TaDA reasoning, it is possible to derive

which amounts to saying that if atomically locks the lock region, then it also atomically updates the client region containing the lock. Notice that the annotation is propagated as is. In other words, the update on the lock is put in the context of the current client. In such context, we can set the frame to be : according to the protocol of the current client, the environment holds an obligation when . Because of the liveness invariant encoded by , it is true that the environment will always eventually unlock the lock, allowing us to discharge the side condition of LiveC’:Indeed, if , then the precondition gives us , which means that the environment owns and will therefore eventually fulfil it, which can only be done by setting . The environment is allowed to then lock again, but that is fine: As we discussed, a CLH lock can promise termination under this milder condition.

Thanks to the smooth integration of liveness annotations in the specifications and liveness invariants expressed as obligations, TaDA Live proofs can properly abstract and encapsulate behaviour. Consider a module implementing a counter that can be safely used concurrently, thanks to the internal use of locks to protect access to the shared cell holding the value of the counter. For example, the increment operation can be implemented as

While the use of locks involves blocking behaviour, the blocking is handled completely internally and a client of the counter cannot observe it. The TaDA Live specification of the increment operation thus does not leak this implementation detail:A client of the counter does not need to worry about the internal blocking, since the specification does not entail any liveness proof obligation. The proof of discharges the liveness assumption of the specification of by using obligations analogous to above, specified in an internal protocol that is not exposed to the client proof. In Section 4.9, we discuss the encapsulation properties of TaDA Live’s specifications in more detail.

Our approach contrasts significantly with previous work [3, 22] where blocking is represented in specifications by the acquisition of tokens acting as obligations. In this work, the specification style fixes an expected protocol to be followed by the client. For example, the axiom for a built-in lock acquisition operation returns a built-in token representing the need for calling a lock release primitive.

In contrast, our lock specification does not impose on the client any particular way in which its environment liveness assumption should be enforced. It is the job of the client to devise a protocol that ensures the environment liveness assumptions of the lock specifications will be provable. For locks, this is indeed often achieved by making sure every thread that locks a lock eventually unlocks it. Such a protocol is encoded by the liveness invariants of the client’s region (e.g., in the example above) and the k-obligation pattern. The specification of the lock, however, does not transfer obligations to the client, leaving open the possibility for clients to use completely different protocols. The following example client illustrates the added flexibility of our approach:

The code assumes a lock has been allocated at , and initially stores 0. In the specification style where the expected (liveness) protocol is built-in, the call in the left-hand thread would return a built-in token that can only be consumed by calling . This, in turn, requires an extension of the logic—as done, e.g., in Reference [17]—providing some mechanism for the sound delegation of tokens from one thread to the other. In TaDA Live, there is no need for such an extension. The protocol of this client does not need to associate obligations with the lock; one can simply define an obligation (owned initially by the left-hand thread) that is fulfilled when is set to 1 and use it to prove the appropriate environment liveness conditions for the proof.

In this informal overview, we used temporal logic formulas to represent the key liveness conditions in the WhileB and LiveC’ rules. The formal versions of these TaDA Live rules, however, implement those checks with what we call the environment liveness condition, which reduces these liveness properties to safety checks via a dedicated set of rules (explained in Section 4). Remarkably, the liveness checks of both rules can be phrased in terms of the environment liveness condition, which therefore provides a uniform proof principle for blocking termination.

The rest of the article proceeds by introducing the assertion language and the semantic model of TaDA Live in full detail (Section 3), then presenting the proof rules through the proof of an example (Section 4), then walking through the proofs of our case studies and commenting on limitations (Section 5), and finally discussing related work (Section 6). A reader interested in the proof rules can skim through Sections 3.3 to 3.5 and 3.8 and the beginning of Section 3.9 to familiarise with the basic definitions, and then move to Section 4 to understand how the rules themselves work, and the typical proof patterns.

We write for the set of partial functions from to , and for the set of finite partial functions. Given , we write if is undefined on , and . We write for the finite function that maps each of the to and is undefined on any other input. We write for the partial function that coincides with except on where it returns , and write analogously. The disjoint union between partial functions is defined if their domains are disjoint. In contexts where the expected type is a function, we write for the empty function.

We present a standard first-order imperative language, called While, with shared-memory concurrency and fine-grained non-blocking primitives, and we define the fair concrete trace semantics of its commands. Our While language is parametrised by the following sets: the Booleans, ; the values, ; the program variables, ; and the function names, . The set contains a special element, , the name of a local variable that holds a function’s return value.

We place some restrictions on these commands to simplify exposition. We write for the free program variables of a command. The set is the set of free variables that are potentially modified by a command, i.e., any free of appearing in instructions of the form ; in particular, . In a command , we apply the mild syntactic restriction that . Each individual thread is still able to modify variables that are created locally and to modify shared heap cells, but are not allowed to modify the free variables.⁸ In a function definition , we use the natural restriction . Also for simplicity, we assume each function name is given at most one definition. The function returns the function names occurring in that are not bound by a . Although function definitions may be recursive, we will disallow recursion in our logical rules to simplify the development. In the programs we consider, all potentially divergent behaviour stems from . It is straightforward to reformulate the While rule into a Let rule that supports terminating recursion.

Commands manipulate heaps (where and is the empty heap) and local variable stores, . A command can contain free function names, so we use a function implementation context,, to map function names to pairs comprising a finite list of distinct variables (the formal arguments) and a command (the body of the function).

A command induces transitions over program configurations that keep track of the current variable store and global heap, and the program states (see Figure 3) that represent the set of the active threads and their execution state. The program configuration represents a faulty configuration, e.g., the one reached after dereferencing an unallocated address. For the details of program states, we refer to Appendix D; what is relevant is that ✓ is the program state of a terminated thread, and we can define a function that computes the set of thread identifiers () of the active threads of a program configuration (details in Appendix).

To model fair traces of commands, we use a small-step operational semantics, parametrised by a function implementation context and defined by a relation . In a transition , the scheduling annotation, , keeps track of who executed the step:that is, either a local active thread or the environment. Environment steps can have arbitrary effects on the heap and can generate faults at any time:

The full definition of the transition semantics is defined in Figure 36 and Figure 37 of the Appendix.

We call program traces the infinite sequences of the form where, for all , and . We use to range over infinite suffixes of program traces and for the set of all program traces. We define the set of -program traces

The open-world program semantics defines the behaviour of a command when run concurrently with an arbitrary environment. It corresponds to the fair program traces of a command, with the information about program states and thread identifiers removed.

The goal of TaDA Live is to prove termination of the local command.

It might seem odd that our program semantics only contains infinite traces, since our goal is proving termination. Traces that locally terminate simply have an infinite tail of environment steps. To simulate a closed system, one can select for the traces where the environment steps are all identity steps.

We formally introduce the TaDA Live assertion language, and its semantics in terms of its models, called worlds. The TaDA Live assertions are built from the standard classical connectives and quantifiers of separation logic,⁹ TaDA region and guard assertions, and new TaDA Live obligation and layer assertions. To formalise the assertions, we assume a number of basic domains:

For layers, we use the abbreviations and . The set of abstract values is .

As is standard, when used in assertions, we extend numeric and Boolean expressions to use logical variables and abstract values, too. A logical variable store, , assigns values to logical variables. Given a logical and a program variable store , the evaluation of expressions and of Boolean expressions are standard.

Assertions and worlds are built using partial commutative monoids.

The partial heaps form a PCM , as standard in separation logics. We also use guard algebras and obligation algebras, which are PCMs for describing auxilary ghost state, specified by the user of the logic.

As discussed, the obligations represent ghost state for describing liveness invariants. They form an obligation algebra that is little more complicated to define due to the association of obligations with layers.

In Section 2, we have seen examples of obligation algebras. For instance, the example used two atoms and , giving rise to the obligation algebra with elements , , and . As mentioned, we make no difference between an atom and the obligation using the symbol of the former for both. For our examples, it is enough to assign layers to atoms, e.g., lay , and extend the layers to obligations by taking the minimum layer of the composed atoms, for example lay . Note that, by construction, each obligation is incompatible with itself: .

We summarise the intuitive meaning of our assertions before giving their formal semantics.

We introduce the worlds of TaDA Live, which are instrumented heaps providing the models of the assertions of TaDA Live. A world is a local model in the sense that it reflects the state as seen from the perspective of a single thread. It is built from a local heap and a set of shared regions with associated guards and obligations. Worlds are parametrised by a set of region identifiers that, intuitively, are the regions that the current operation is supposed to update abstractly exactly once. We say the regions in are tracked for proving atomicity, using special ghost state given by the atomicity tracking algebra that supports the semantics of the atomicity tracking assertions.

A shared region with identifier , given by , has type and abstract state . For a world , we write and and so on, for the corresponding components of . We also define , , and , if .

We define a PCM on worlds (called world algebra). We define how worlds compose by first definining composition on each component of a world. Heap composition is disjoint union. Region maps only compose if they are equal. Given , the compositions and are:and undefined otherwise. The composition on is defined analogously to on .

The local and environment obligation maps compose in a subtle way inspired by the subjective separation of Reference [29]. To express this interaction, we define a composition on pairs of local/environment obligation maps. Given , we defineNote that, for obligation algebras, the minimum taken by the definition is always unique if it exists. Indeed, in general one can set . For example, assuming , , , , , and are distinct atoms, we haveprovided the composition is defined. Furthermore, this definition supports the implication , since .

Notice that the units are worlds with arbitrary shared regions, atomicity components from , and arbitrary environment obligations.

Subjective composition of worlds is lifted to composition of sets of worlds , defined as .

We want the region and environment obligations assertions to enjoy the elimination rule, e.g., . Assertions therefore denote sets of worlds that are upward-closed with respect to adding regions and adding environment obligations. Formally, we define the world ordering as the smallest reflexive and transitive relation such that:The upward-closed sets of worlds are the semantic domain of our assertions.

We write if, for , we have , and write for any assertion . It is easy to check that for every and .

A world describes the state of the current thread, both the local state owned by the thread (the heap, guards, local obligations, and atomity tracking components), the shared state (the regions) and the environment obligations describing obligations owned locally by the environment. We define the world rely relation, which describes how the world may change as a result of the “well-behaved” interference of the environment characterised by the region interference relations, the atomicity tracking components, and the environment obligations. To define the world rely, we need to introduce two other components of TaDA Live: the region protocols, expressed by the region interference function, and atomicity contexts.

The type of each region is associated with a region interference function that establishes which updates to a shared region are allowed by the owner of which guards.

The final concept we need before introducing the world rely relation is the atomicity context, . In TaDA Live proofs, we keep in the context of the judgement information about which updates we are currently proving are abstractly atomic. The rule driving this bookkeeping is the MkAtom rule. Although we will properly explain the rule in Section 4.7, we sketch the main idea as a motivation for the atomicity context now. The relevant “skeleton” of the rule is as follows:The judgements include the context information such as the layer , the level and the atomicity context , and the pseudo-quantifier includes a layer . We formally introduce these details in Section 3.8. Here, we focus on motivating the use of the atomicity context . This rule describes how an update to the state of a region can be declared atomic even if it was realised through a series of steps. It does this by converting a Hoare triple to an atomic triple, provided the Hoare triple bears evidence (through the atomicity tracking assertions of the premise) that, although many steps might have been taken, the abstract state was changed by the command exactly once. The atomic triple may constrain the environment interference with a non-trivial pseudo-quantifier. The proof of the premise in general needs to make use of these assumptions about the environment, but the conversion to a Hoare triple means we cannot use pseudo-quantification to represent them. These assumptions are instead made available to the proof of the Hoare triple using the atomicity context, which records the information from the pseudo-quantifier and the relation that stores the update that we are proving happens atomically.

Assuming , we write , , , which we write , and . For every , we require . The set declares the regions for which we are tracking atomicity: For , the environment will only change the abstract state within and will obey the liveness condition given by that the environment will always eventually return to a good state in ; and the local thread will only change the abstract state at most once according to the relation . We write for , and similarly for , , and .

Rule wr describes the case where the environment can update the abstract state of a region according to the interference relation . Notice that, for this rule, when , the environment can only change the abstract state to something in . When is undefined or a pair of abstract states, then the environment does not have this restriction and can do any update consistent with . Also, notice how the environment obligations map is affected by the transition. Rule wr describes the case where the atomic update given by has been delegated to the environment () in which case the current thread can observe the abstract state change corresponding to the update.

So far, we have introduced assertions and worlds as their models. These structures express information mostly over ghost state, that is, state that is purely logical and has no representation in concrete executions. For example, the notion that there is some shared region is purely fictional, as in the concrete machine there is no special way to mark a portion of the heap as shared. We introduced interference protocols and the world rely as a way to specify the expected well-behaved transformations shared resources may be subjected to. Since well-behaved interference from the environment can change the state of shared regions, a single world (describing a single state for each region) cannot capture the logical state we may be in when interleaved with environment actions. Views are the sets of worlds that can explain the logical state we may be in after being suspended for an arbitrary number of environment steps. Views represent information about the logical state, which cannot be invalidated by a well-behaved environment.

We write for the set of all A-views and for the set of all A-stable assertions.

Notice that the composition of views always gives rise to a view: In the case where there are no compatible pairs of worlds in the views, the result is the empty view (the denotation of ).

On checking stability. TaDA Live proofs require checking stability of assertions in some crucial steps. The notion of stability of Definition 3.16 is given in terms of the semantics of assertions, but it is possible, in principle, to provide a set of lemmas to prove stability of common cases without reasoning at the level of the model. For example, any traditional separation logic assertion (such as , , pure formulas) is always stable; guard and local obligation assertions are also automatically stable; stability is preserved by , , , and existential quantification. The crucial sources of instability are region assertions, environment obligation assertions, and . Stability of the first two can be established by inspecting the protocol of regions. A rule that would be expressive enough to prove most stability checks for our examples is:It is similarly easy to extract from Figure 6 rules involving the atomicity context information:

As we mentioned, worlds and views represent ghost information about state. Ultimately, however, we want to use this information to express properties of concrete execution traces. To do so, we need to formalise the link between worlds with their logical instrumentation and concrete states comprising variable stores and heaps. The first component that contributes to this link is a region interpretation, which specifies the implementation-dependent content of a shared region: For example, for a shared spin lock, the interpretation of the abstract shared region is the view given by , a single cell storing at .

It is important to understand that interpretations are not merely an indirect way of writing assertions. In our spin lock example, the crucial difference between the two assertions and is that the first is subjected to interference, while the latter expresses ownership of the cell at . The requirement that the interpretation of some region with ID must imply forbids an intepretation to own local obligations of other regions. This is necessary for soundness: If we removed the restriction, then we could fool ourselves into thinking that we fulfilled an obligation by creating another region with the obligation in its interpretation.

The second component that expresses the link between the instrumented worlds and concrete states is the reification function. Reification has two main purposes. First, at level , all the regions with level lower than are closed, which means that the resources in their interpretation do not exist as far as the world is concerned. The concrete heap cells accounted for inside these interpretations will, however, correspond to cells in the concrete heap. To bridge this gap, the reification opens all closed regions importing the resources in their interpretation as local resources, obtaining a “collapsed” world. Second, all the “ghost” components of collapsed worlds (such as regions, guards, or obligations) do not have any representation in memory, so reification erases them.

To understand if a world can represent local resources consistent with some global heap , we need to identify if there is a world representing the resources of the environment such that . That would mean that it is possible to factor as , where are the cells fully owned by the local thread, are the ones fully owned by the environment, and the cells in are the ones that are shared and come from opening the interpretations of closed regions in the world collapse. When collapsing, we are assuming, conceptually, that we are collapsing a world that represents every resource in the system. Correspondingly, the definitions that use reification—crucially, Definitions 3.20 and 3.22—always complete the local resources with some “global” frame before applying reification.

In addition to opening shared regions, the collapse function also checks that no environment obligations are assumed. To understand this, consider a world representing local resources, and a world completing it to a world representing the global resources. The global world cannot assert the existence of obligations in the environment: all those have been already accounted for in . The definition of collapse explicitly enforces this constraint by the condition on the environment obligation map. We explain why this condition is important in Section 3.7.

Having established the link between worlds/views and concrete state, we can move to establishing a link between concrete steps in a trace and their logical justification in terms of logical state. The fundamental driver of this link is the notion of frame-preserving update, inspired by the frame-preserving update from Reference [24], which represents the essence of the Rely/Guarantee reasoning in TaDA Live. The frame-preserving update looks at a specific concrete update from some to and states under which conditions this logical update can be described as an update from logical state to logical state . The and are sets of worlds describing local resource, whereas the and are global concrete heaps. We therefore need to complete with some frame and use reification to relate this logical state to : That is, . There will usually be more than one such . The frame-preserving update requires that any such that is a view should remain a valid frame after the update: That is, .

TaDA Live implements the Rely/Guarantee proof principle by requiring every update to be frame-preserving. Views are resources that are preserved by protocol-compliant environment interference. The idea of a Rely, a set of allowed environment updates, is represented by assuming environment steps are frame-preserving updates on resources that are compatible with our current view. By frame preservation, any such update would preserve our view. Conversely, the idea of a Guarantee, an over-approximation of the effects of local steps under the assumption of Rely, is encoded by requiring every local step to be a frame-preserving update, and thus unable to disrupt any view held by the environment.

To see how this works more concretely, let us consider an example. We use the notation to mean , that is, holds when to can be used to justify some concrete update.

This definition of frame-preserving update simplifies drastically the semantics of TaDA specifications. For TaDA Live, however, we need to introduce the stronger notion of atomic frame-preserving update. To see the motivation behind the stronger condition, consider the region interference relation and . The update from to via is very different from a direct update from to . The intermediate step to fulfils the obligation , which may be crucial information for the progress argument. We therefore want to enforce that if we are justifying a step as going from to , then all the allowed transitions between region states need to match a single transition in the interference protocol.

Intuitively, this says that if the environment has some resource compatible with , then it should expect that after a step, the resource might be transformed into . When is a view, one gets back Definition 3.20, as views are precisely the resources that cannot be invalidated by any number of updates of the environment. We will use atomic frame-preserving updates to check the safety of logical traces with respect to some specification in Definition 3.28.

Before moving to specifications, we define viewshift, a semantic generalisation of implication, which is a prime example of application of frame-preserving update, used in our Cons rule. They correspond to “purely logical” updates in that they update the ghost resources without affecting the concrete memory.

Viewshifts are typically employed to “allocate” a new region by sharing some local resource (a form of weakening). For example, assume . We have that viewshifts to : The underlying reification does not change, and any frame of with non-empty reification must only have regions reifying to cells disjoint from ; moreover, such frame will only have finitely many regions allocated, so it is always possible to draw a fresh from the infinite set to satisfy the existential quantification over .

Viewshifts also ensure that obligation information is not updated inconsistently. For example, in the “region allocation” step above, we cannot viewshift to , which would mean we are pretending there is an obligation in the environment without any evidence of that being true. To show that the viewshift does not hold, we can choose and show that is false. To see this, pick as the global frame; is in the reification of but the reification of is empty: The frame has empty local obligation map, so every world considered by the region collapse of has . The idiomatic, and correct, pattern of creation of environment obligations would viewshift to, say, for some relevant obligation compatible with , and then with implication obtain : In this case, the environment obligation has been created from the evidence of the existence of a corresponding local obligation.

It is important to note that, in a logic with the ability to share assertions, as regions in TaDA or invariants in Iris allow, having classical resources does not have the expected effect. By definition, a classical resource cannot be “forgotten,” i.e., . By using viewshift, however, it is possible to create a region with interpretation defined so it contains and immediately discard it (regions are not classical resources), obtaining . This, for example, makes TaDA Live incapable of proving absence of memory leaks even if its heap assertions are classical. We, however, manage to avoid this issue for local obligation assertions because of their specific semantics. First, can only ever be part of the interpretation for the region , as imposed by our restrictions on region interpretations. Second, the very notion of fulfilling the obligation is defined as transferring its ownership to the interpretation. Moreover, the region protocol constrains the loss of an obligation to happen only in correspondence with some region state change, so the only way to get rid of a local obligation is to induce the desired state change in the region and transfer the obligation to the interpretation. We need obligations to be classical resources for this to be the only way of losing them. We made heaps and guards behave classically for the sake of uniformity, but this is not essential.

The issue of having genuinely classical resources in a logic with regions/invariants has been tackled in Reference [1], with the main use cases being proving absence of memory leaks. The techniques presented there could provide the basis for an alternative way of handling TaDA Live-style obligations.

With all these definitions in place, we can now proceed to define TaDA Live specifications and their trace semantics. Most of the time, TaDA Live proofs manipulate triples of two forms:

called atomic triples and Hoare triples, respectively. It is, however, possible for a command to manipulate some resources non-atomically, and some other resources atomically, at the same time. In general, specifications use hybrid triples:a minor generalisation¹¹ of hybrid triple discussed in Section 2.1. Intuitively, the Hoare precondition is a resource that is owned by the command and, as such, cannot be invalidated by actions of the environment. The command is allowed to manipulate this owned resource non-atomically, provided it satisfies the Hoare postcondition upon termination. The atomic precondition represents the resource that can be shared between the command and the environment. The environment can update it, but only with the effect of going from for some to for some . The command is allowed to update it exactly once from to perform its linearisation point, transforming it to a resource satisfying the atomic postcondition . The atomic postcondition only needs to be true just after the linearisation point, as the environment is allowed to update it immediately afterwards. The pseudo-quantified variable has two important uses: It represents the “surface” of allowed interference by the environment; it is bound in the postcondition to the value of the parameter of the atomic precondition just before the linearisation point.

The atomic and Hoare triples in Equations (11a) and (11b) are then special cases of the hybrid triple:¹²

respectively, where , , and (for technical reasons the atomic pre-/post-conditions in the general triples cannot contain program variables). We omit the pseudo-quantifier from an atomic triple (as above) when the pseudo-quantified variable does not occur in the triple, and thus could be quantified as . We also use the abbreviated form when the liveness assumption is trivial, i.e., .

In addition to the atomicity context , the context of a specification consists also of a layer , and a level . These components record information about the proof context of the judgement. The layer indicates that we are in a context where we are forbidden from assuming as live obligations with layers (or incomparable to ). The level indicates that the regions with level are open (and cannot be re-opened).

Finally, we can define the semantics of a specification. The idea of the semantics is to collect all traces that are deemed as acceptable to a specification , so we can later say a command satisfies if its traces are all accepted by the semantics of . The general principle in accepting a trace is the following: The local steps are only expected to be correctly implementing the functionality declared by if the environment satisfies the assumptions implied by the (safety and liveness) protocols and itself. If a trace has gone wrong as a consequence of the environment making moves outside of the assumptions, then that trace is accepted, as the problem is not the responsibility of the local command itself. If a trace has gone wrong as a consequence of local steps, then the trace is rejected.

The semantics of a specification therefore traverses a trace to decide whether to accept or reject it by determining who is to blame for failures. We decouple the traversal needed for checking the safety constraints and the one checking the liveness ones. In terms of safety, a specification like ($\color{blue}\maltese$) (in Definition 3.24) expects that:

If any of the above are violated, then the blame is on the environment. In return, the local steps are expected to:

In this sense, the resources in should be understood as shared: The environment can use them to change the value of , and the local steps can use them atomically to perform the linearisation point. Note that is only guaranteed to hold immediately after the linearisation point.

Key idea of the liveness semantics. In terms of termination, the specification ($\color{blue}\maltese$) guarantees local termination only if the environment is live, i.e., it satisfies the layered liveness invariants represented by the pseudo-quantifiers (of the specification and in ) and the obligations. The idea is again to identify when non-termination is caused by a bad environment or by bad local steps. Consider the case of liveness invariants encoded by obligations. Imagine we annotate each position of a trace indicating which obligations are held at that point by the environment and which are held locally. Now suppose the environment always eventually fulfils every obligation (i.e., for each obligation there are infinitely many positions where is not held by the environment). This environment is certainly live, so it cannot be blamed for non-termination. The layer structure, however, allows the environment to fulfil obligations of layer by relying on eventual fulfilment of obligations at layer . Therefore, if there is an obligation that is locally held forever, the environment is still considered live if it never fulfils obligations at layer . In this scenario, the local steps are blamed for non-termination: By holding forever, the local steps are not allowed to rely on the environment being live at higher layers than lay .

This scheme leads to the following semantic interpretation of layers. The local steps can blame the environment for non-termination by waiting for the fulfilment of some environment obligation indefinitely; in turn, the environment can blame the local steps for the inability to fulfil by claiming to be waiting for the fulfilment of some local obligation with lay ; the local step can justify the indefinite postponement of the fulfilment of by shifting blame on the environment again, appealing to an environment obligation with even lower layer, and so on. This blame-shifting cannot be unbounded: Every time the blame is shifted, the layers considered are strictly lower and, by well-foundedness of layers, this cannot happen ad libitum. Ultimately, the blame is unambiguously placed on the environment or the local steps and the trace is accepted or rejected accordingly.

This intuition about obligations extends to liveness assumptions attached to pseudo-quantifications in the triple and in the atomicity context. All these assumptions need to be layered to avoid unsound circularities, which is why the pseudo-quantifier carries a layer . The specifications mention another layer, , which represents a (strict) upper bound on the layers that we may consider live when proving some command satisfies the specification. An environment is still considered live by the specification if it keeps an obligation of layer forever unfulfilled.

We now define the formal semantics of specifications, as set of concrete traces that satisfy the specification. To check if a concrete trace satisfies a specification, the semantics first collects all the possible “logical” justifications of the trace in a set . To justify a trace means to instrument each step with sets of worlds that show how the trace respects the (safety) logical constraints of the specification. The set is then further analysed to check that every instrumented trace where the environment satisfies the liveness assumptions is locally terminating.

We begin by defining the trace safety judgement, of the form , the purpose of which is to check the safety constraints implied by . The judgement formalises the idea of a specification as a trace acceptor, that is, an automaton reading a trace step-by-step, and either accepting or rejecting it. If we ignore for a moment, then the trace safety judgement represents a snapshot of the state of this imaginary automaton at a point when some prefix of the trace has been already successfully processed, and is the suffix that remains to be processed. The automaton traverses the trace producing a guess for an instrumentation, i.e., logical resources corresponding to the concrete memory contents that explains why the trace is acceptable. The instrumentation needs to describe, for instance, when the linearisation point is thought of taking place, what portions of the state are considered as shared and which owned. Let be the current concrete state, i.e., . The triple in the judgement encode the automaton’s current state, representing the current guess for the instrumentation of . The resources currently considered as locally owned are represented by the view ; the can be either an abstract value, in which case the automaton thinks that we are still in the interference phase, or it can be a pair , which means we are past the linearisation point, which updated the abstract state from to ; the is a set of worlds parametric on and corresponds to the shared atomic resources if we are before the linearisation point, or it is the empty resource if we are past it. The judgement assumes that for some frame , i.e., the current concrete state is consistent with the current instrumentation guess. The initial state of the automaton will be chosen so this holds at the beginning of the trace, and each transition of the automaton will by construction preserve this correspondence.

As it walks down a trace, the automaton updates , , and , trying to construct a consistent instrumentation for the whole trace. Such a sequence of automaton states constitute its run over the trace. Specification traces augment each state of a trace with the instrumentation from a run of the automaton.

The trace safety judgement accumulates, as it traverses a trace, all the successful instrumentations of the trace in , which we can later check against liveness properties. Let us define the judgement formally, and then explain it in detail.

The judgement assumes the initial configuration of the trace satisfies . Rule Stutter checks that any local step other than the linearisation point updates the local Hoare view (to some ) in a frame-preserving manner; this implies that, before the linearisation point, the abstract state needs to be preserved by such step. Rule LinPt checks that the linearisation point is frame-preserving and consistent with the atomic postcondition . Both rules Stutter and LinPt check that the Hoare postcondition is satisfied if we are considering the last local step of the trace (i.e., if holds). Rule Env checks whether the current environment step, assumed to happen before the linearisation point, can be seen as a transition changing the abstract state from to in a way that does not disrupt any frame (including ). If that is the case, then the rest of the trace is checked for safety. Rule Env’ performs the same check but after the linearisation point. In both cases, if the environment step cannot be seen as frame-preserving, then the trace is accepted, since the environment did not respect the assumptions. Similarly, Rule Env accepts the trace after a fault caused by the environment.

As we briefly mentioned, Definition 3.26 is inspired by alternating automata [40]. The “alternation” aspect is necessary because of the angelic/demonic duality between local and environment steps: When processing an environment step, we need to be prepared to handle every possible interpretation of the update that took place; for local steps, we are allowed to pick any interpretation of the update. Note that these ambiguities arise purely from the fact that we are instrumenting the trace with “ghost” logical state: At each step there is no ambiguity in a trace about how the concrete state has been updated. This dual interpretation gives rise to the two kinds of transitions in an alternating automaton. An automata-based presentation of the trace safety judgement would use existentially branching transitions for local steps and universally branching transitions for environment steps. We further mimic alternating automata in the way we factor safety and liveness constraints. Alternating automata impose safety constraints by constructing sets of runs that linearise the choices for the existential transitions and the branching due to universal transitions. In our setting these sets of runs correspond to . The liveness constraints can then be checked by, for example, requiring each run in the set to visit final states infinitely often, the usual Büchi-style acceptance condition. Here, we also examine the instrumented traces of individually and impose a liveness acceptance condition; the condition in our case is more complex, as it has to take into account layers, pseudo-quantifiers, and obligations. One key simplification introduced by this approach is that we can cleanly separate the branching (safety) aspect—the quantifier alternation due to duality environment/local steps—from the linear-time liveness aspect.

Building on trace safety, we can now define the semantics of a specification as the set of traces that are safe and that additionally satisfy the liveness constraints implied by the obligations and the liveness assumptions of . Conceptually, we want to require local termination if the environment satisfies the layered liveness invariants represented by pseudo-quantifiers and obligations. To harmonise the pseudo-quantification and obligation-related liveness assumptions of a specification, , we collect all of them in a set of so-called pseudo-obligations:where , and are taken from the specification.

We extend the layer function to lay by setting lay if and lay , or , or . Furthermore, define

Now, we want to understand, for each position of a specification trace, which pseudo-obligations we are holding locally and which are held by the environment. This information is contained in the single worlds, so as a first step, we extract, from a specification trace, the set of traces of worlds that it represents.

We can now define two predicates indicating when a pseudo-obligation is considered to be held by the environment () or locally () in a position of a world trace:

Equipped with these definitions, we can state the liveness constraints associated with a specification. The idea is that one can assign the “blame” for local non-termination either to the environment or to the local behaviour. If we deem the environment responsible for non-termination, then the specification will classify the trace as acceptable, otherwise it will reject it. The idea behind this “blame” assignment is to examine the world traces justifying the safety of a trace and consider, for each position, which obligations are held by the environment and which are held locally. To understand the intuition, consider the case of liveness invariants encoded by obligations. Suppose the environment always eventually fulfils every obligation, i.e., for each obligation there are infinitely many positions where is not held by the environment. This environment is certainly live, i.e., it respects the liveness assumptions and the local code is responsible for any non-terminating behaviour. But what if the environment itself is blocking on some locally held obligation, and as a consequence is not able to fulfil some ? Whether the environment or the local code is to blame depends on the layers. The environment is to blame if, from some point in the trace, it never fulfils some but the local steps always eventually fulfil every obligation of layer strictly lower than lay . Conversely, an environment that keeps unfulfilled because of some forever-unfulfilled obligation held locally with lay cannot be blamed for local non-termination.

This intuition about obligations extends to liveness assumptions attached to pseudo-quantifications in the triple and in the atomicity context. The predicate given in Definition 3.28 formalises the above blame-assigning mechanism. A world trace that satisfies is one where the environment cannot be blamed for local non-termination. The specification semantics then is the set of safe traces where, if is satisfied, then the trace is locally terminating.

The more precise intuition behind the specification semantics is as follows: Once it has been established that there is a way to instrument the trace to justify why the local steps satisfy the safety constraints of , we consider the set of valid instrumentations . First, we extract the set of world traces represented by the traces of . Each such world trace should either be locally terminating, in which case the trace is accepted, or, if it is non-terminating, the non-termination should be due to the environment not satisfying the liveness assumptions of . The predicate holds for a specification trace if the environment always eventually fulfils any pseudo-obligation with layer and if no obligation of layer is constantly held by the local thread. Blame for non-termination can be unambiguously assigned, thanks to well-foundedness of layers: If there is a forever-unfulfilled local obligation , then we can try to blame the environment by identifying a lower-layer obligation that is forever-unfulfilled by the environment; the environment can shift the blame back to the local steps if one can find a lower-layer local obligation that is forever-unfulfilled. Well-foundedness implies this blame-shifting game must be bounded in length and the ultimate culprit can always be identified. This effectively encodes the acyclicity of the layered termination argument.

We are now ready to define the semantic version of our judgements, , indexed by a function specification context, , which, for each function, provides the arguments of the function and the specification of the function body.

Since the semantics of our triples is a complex conditional termination statement, it is useful to show when it corresponds to unconditional termination. Intuitively, to state facts about the behaviour of a command in an “empty” environment, we should be using a Hoare triple (no resource needs to be shared, no interference experienced) and there should be no assumption of obligations being owned by the environment. We characterise the preconditions that ensure this as the ones that always admit as a global frame.

Examples of grounded assertions are standard separation logic assertions like or .

Unconditional termination applies to programs running in isolation. Note that, technically, we cannot consider traces without environment steps as the fairness constraint requires infinitely many of those. We therefore model the isolated executions of a command as the executions where the environment steps do not modify the current state. It is easy to check that, for each finite or infinite sequence of local steps of , there is a corresponding fair trace of with only identity environment steps and vice versa.

As a corollary, we have that if holds, then every isolated execution of from the empty heap and arbitrary store terminates.

Let us formalise the argument in TaDA Live, introducing the proof rules as they are needed. Recall the specifications of CLH lock:where we make explicit the previously omitted layers (we justify the choice of layers in the proof of CLH lock). These specifications will be available in the proof as “axioms” stored in a function specification context parametrising every triple of the client proof; we omit the parametrisation to aid readability. The predicate is given a definition in the proof of the lock module, and, in the spirit of CAP, the client proof should not be relying on the Definition of the predicate but in its abstract properties. Here, we rely on the fact that is false, expressing that a lock is an exclusively owned resource—see Section 4.8 for the other properties of exposed to the client.

The two threads of the distinguishing client both access the lock and the heap cell . Consider the precondition . Both resources in the precondition are non-duplicable, so if we give them to , then the other thread would not be able to also have them. As we anticipated, shared state in TaDA is handled using regions. We therefore introduce a new region type (for istinguishing lient) that encapsulates the resources in the precondition: is the shared resource encapsulating a lock at with state and a cell at storing the Boolean . Although in this case the abstract state is not hiding any detail, since both and are visible, in general the abstraction of the contents is an essential mechanism for reasoning about abstract atomicity. In the proof of CLH lock, for example, to be able to see the operations as abstractly atomic, it is essential to hide the queue from the abstract state.

Assuming the lock region encapsulated by the predicate has level , the lock specifications will have level in the context, indicating they consider the lock region closed. To allow to encapsulate the lock region and use the lock specifications to derive updates to its own state, we let it have level . The top-level triples for the distinguishing client have level as a consequence. We will elide all details about levels, as they can be mechanically inferred from the applications of the LiftA and UpdReg rules.

We now design the protocol of the region, with the intent of encoding the following safety invariants:

and the following liveness invariants:

Note that, together, invariants 3 and 2 imply that eventually the value at will always be true. To encode invariants 2 and 3, we introduce a guard algebra for generated from two guards (for ey) and (for one), with and to represent exclusivity of the permissions they give on the lock and flag, respectively. We can reuse the same guard algebra for the obligation algebra associated with : The atom obligations and will represent liveness invariants 1 and 2, respectively. The protocol formalises all the invariants:The fact that no transition can change and encodes 1; this is such a common pattern that we adopt the convention to declare which are the fixed components of the abstract state and omit them from the protocol transitions completely. The choice for the guards of Equations (14) and (15) reflects 2 and 3, respectively; we will give to the left-hand thread, and will be obtained by locking the lock. The obligation is obtained by locking and fulfilled by unlocking; the obligation is fulfilled by setting to ; these facts encode 1 and 2.

We assign layers to the obligations to reflect the intuitive dependency: The lock needs to be assumed live in the process of fulfilling the obligation on the flag. We therefore set .

To complete the definition of shared region , we link its abstract state to the actual heap content that it encapsulates using the region interpretation:This assertion describes a portion of the heap being shared (the lock at and the cell at ) and the linking of the ghost state (the guards and obligations) with the abstract state. The assertion is an abbreviation for , which indicates local ownership of the guard and obligation . The interpretation of a region establishes the invariant that, when , the guard and obligation will be “owned” by the region (and by no thread as a consequence). Similar links are established between the value of and .

Now that we set the scene, we can proceed with the proof, outlined in Figure 8. The first operation to do is to transform the precondition to an assertion about the region. We can do that by using the consequence rule:which allows the use of viewshift to logically manipulate the assertions. Since triples are only well-defined if the Hoare pre-/post-conditions are stable, the rule asks to check stability of the assertions of the conclusion, as this does not follow from stability of the assertions of the triple in the premise. An analogous rule, called Cons, holds for hybrid triples—with no stability checks on the atomic pre-/post-conditions—so viewshifting is available at any point in a derivation.

In our example, we want to create the guards and obligations needed to match the interpretation of and create the region, replacing its interpretation. Here, we might be tempted to match the interpretation with and , to viewshift to . While this viewshift holds, there is an issue: In TaDA Live, all the assertions in Hoare triples (or in Hoare position in hybrid triples) need to be stable for the triple to have well-defined semantics. The proof system enforces the stability of these assertions, by inserting stability checks in crucial rules. This means that if we viewshift now to a non-stable assertion, then we would fail at some point in the derivation to satisfy a stability check. While is stable, as we own these resources, the assertion is not stable: A region is subjected to the transitions of the protocol. Since we have the guard (from ) the environment cannot own it, hence cannot fire the transitions guarded by ; this makes stable. The transitions changing the state of the lock, however, can affect the region. This leads us to¹⁴ where we also add when , a stable fact.

We now want to proceed with an application of the parallel rule:The abbreviation means , that is, all the obligations owned by have layer . means and . The intuition behind these constraints is as follows: The layer in the context of the triples indicates a strict upper bound on the layers that can be assumed live in the proofs of the triples. If thread 2 needs layers lower than , then if thread 1 has unfulfilled obligations by the end of its execution, these cannot conflict with the assumptions made by the proof of thread 2. It is not, however, sound to leave an obligation of layer unfulfilled by thread 1: If thread 1 terminates first, leaving unfulfilled in its postcondition, then thread 2 may be assuming live in a situation where it will never be fulfilled.

In our example, we need to apply consequence again to massage the viewshifted precondition into an assertion of the form . The region assertion is duplicable, as is , but we want to give the non-duplicable resource to the thread on the left, as it is the one that will fulfil the obligation. This has a side-effect though: Since the guard is given to the left thread, the value of from the right thread’s perspective is not stably . Moreover, we want to know that the left thread has the obligation . So, we use to give to the thread on the right, and we stabilise the assertion to . All in all, we obtain:which allows us to apply consequence and the standard Elim rule to obtain a precondition in the form required by the Par rule. For both threads, we are aiming at postcondition which has no obligation, so it satisfies the layer conditions trivially.

To see why the layer conditions are important for soundness, imagine we forgot to unlock in the left thread, obtaining a non-terminating program. We would obtain in the postcondition of , but the check would fail as . Choosing for the context layer of the triple for would not work: In its proof, we need to assume live, and lay .

Let us focus on the proof of the left-hand thread first. The difficult step is the execution of the first instruction, since this is the only potentially non-terminating instruction of the thread. If we let , then Step 1 can be derived as follows:

Let us unpack the derivation. As a first step, we would like to frame the irrelevant resources, in this case . In TaDA Live, this step is more subtle and interesting than usual, because of the layer-related side-conditions of rule FrameH (a special case of rule Frame):With this rule, one can only frame obligations if they are of layer greater or equal the context layer. Here, we can use consequence (omitted) to obtain a stable frame of the pre- and postconditions. We have but ; since the layer in the context of the goal is , before we can apply FrameH, we need to artificially lower the layer using LayWH before applying frame:Notice that lowering the layer in the context is always sound (even for hybrid triples): If we can prove the triple assuming live only layers , then the proof is valid in contexts where layers up to can be assumed live.

The layer constraint of Frame is crucial for soundness. Suppose we remove the constraint. Then, we would be able to frame a locally held obligation with layer , i.e., one of the layers that might be assumed live by the proof. This would allow the proof to assume live environment obligations that have layer , the eventual fulfilment of which might depend on the eventual fulfilment of . But, since is in the frame, it is constantly held and not fulfilled for the whole duration of the execution of the command we are proving. The frame condition forces us to record the “minimum” layer of the frame in the context, ruling out unsound circular reasoning.

After framing, we use the rule of consequence to massage the assertions to prepare them to the form required for the later application of LiveC.

The rest of the derivation does not involve liveness reasoning and follows a standard TaDA proof pattern. We use AElim and AtomW to turn the Hoare triple into an atomic triple:Rule AElim says that if one can prove the command is resilient to interference on and does not affect the resource on until its atomic update, then we can relax the specification to state that the command allows changes to and might also affect during the interference phase. Rule AtomW says that if you prove a command is atomic, then you can relax the specification not to insist on atomicity; this can be done provided the atomic pre- and postcondition are stable, as required for the Hoare triple to be well-defined.

The combination of AElim and AtomW simply states that if we can prove a command performs an update atomically, and the pre- and postconditions are stable, then we can prove that the command also performs the update non-atomically.

Now let us consider the derivation for Step 2, which lifts the specification of CLH lock to the context of the client:

Rule SubPqA simply gives a way to manipulate the pseudo-quantified variable and its domain:These are manipulations that would normally be carried out using consequence, but need to be done specially, since the pseudo-quantifier is a component of triples and not of assertions. In our example, we simply use it to remove the unused variable , choosing to be the first projection.

The interesting step of the derivation of Step 2 is the application of LiftA:

Let us unpack it. The purpose of the rule is to take an atomic specification that applies to some resource and lift it to the effect the atomic update has on some region that contains that resource in its interpretation. In our example, it says: You have proven that the command locks the lock; the lock is part of the interpretation of and the update to the lock amounts to going from the interpretation with to the interpretation with . The rule needs to make sure that the region update is among the ones permitted by the associated protocol. It does so by checking:

To check the first condition, the rule uses a relation between abstract states of the region; by the fourth premise, can only include updates that the owner of is allowed to perform. The second condition is enforced by requiring the precondition to own . The third condition is ensured by going from owning to owning , which, according to the fourth premise, is the expected update of obligations. In our example, we have and and the update matches transition (13). The third premise uses the abbreviation “,” which stands for . This implies that and cannot own obligations of , and so and capture the whole of the updated obligations. Note that because of the well-formedness restrictions on triples, in the conclusion of the rule the obligations are transferred to the Hoare pre-/post-conditions: There they belong to a closed region. The first premise says: If the region we are updating is tracked by the atomicity context, then this needs to be a trivial update, or else it would count as a linearisation point (which is instead handled using rule UpdReg). In our example , as we are not proving atomicity of the client, we are allowed any protocol compliant update.

Finally, the second premise requires to preserve its meaning at level . The formal definition of -safety is given in Appendix B.2.1; all the -safety conditions in our proofs can be immediately discharged by applications of the following lemma:

In a TaDA safety proof, the derivations of Step 1 and Step 2 could be plugged together: The safety specification of the operation does not contain the component, and the premise of Step 1 matches exactly the conclusion of Step 2 (modulo framing , which would anyway not be used in a safety proof). In TaDA Live, the discrepancy between the two steps expresses the need for a termination argument for this call. What needs to be proven is the fact that, in the current context of the protocol, during the interference phase of this call to , the environment will always eventually unlock the lock. The LiveC rule allows to remove the liveness condition of the specification in a context where the corresponding liveness invariant can be proven to hold:

The first premise is called the environment liveness condition, and it roughly corresponds to checking (with acting as a certificate of the property holding, explained later). Here, we pick:and we can conclude because when does not hold, i.e., , then we know, from , that holds; if we can show is live, then the protocol says that if the environment holds , then it will eventually fulfil it; under the protocol the transition fulfilling it is setting , which brings us to . The environment can always set again after that, but the same argument then applies.

To show is live, we have to look at the layers. Here, we have and . Recall that holds if . We can therefore set : holds, since . Since we do not own any obligation locally ( has been framed, recording this fact in the context layer ), we can consider live when proving the environment liveness condition.

The environment liveness condition is the central component of both LiveC and While; we explain it in depth now, and then resume our proof of the distinguishing client.

The essence of the termination argument is captured in LiveC and While by the conditions of the form . They establish “always eventually holds” facts. The condition is parametrised by , an assertion that holds at any point in the traces we are considering, an assertion , characterising the so-called target states, and an assertion parametric on some ordinal , which represents the environment progress measure. Intuitively, the condition states that, from any state satisfying , for some , we can find an environment transition that must eventually happen that would take us either to , or to some state satisfying with . Additionally, any transition from to that may happen does not strictly increase the progress measure, unless they end in a target state. The transitions that must happen are characterised by being those that either:

This entails that, under an environment that always eventually fulfils the obligations we are assuming live, holds, as desired.

In the While rule, an environment liveness condition is combined with the conditionwhich requires us to prove that any protocol-compliant step from a state satisfying for some will take us to a state satisfying for some . In other words, in traces satisfying the progress measure never increases. This, in conjunction with , entails , as needed for soundness of rule While.

Take the environment liveness condition required by the application of LiveC in the proof of the distinguishing client. Given and , we have to prove:That is, during the interference phase, we know that at any point in time the lock will be in some state ; we want to prove that the environment will always eventually set to 0. Here, this is particularly easy to show: states that when the obligation is held by the environment; since lay (and does not hold obligations), we can assume the obligation will be eventually fulfilled; the only transition that can fulfil it is the one that sets , so in exactly one such step we reach . This justifies the trivial definition of : We do not need to keep track of progress towards , as we reach it in exactly one of the steps that must eventually happen.

The environment liveness condition can be proven using the rules in Figure 10. The only rule that applies directly is EnvLive, which checks that in a state satisfying one can always measure progress (second premise), and then asks to discharge an auxiliary judgement of the form , which is best explained with the help of the illustration in Figure 11. The condition works under the hypothesis that the assertion holds at any point of the traces under consideration, so in the picture we are considering infinite sequences of steps within the outer rectangle. The target states describe some subset of , which we want to show is visited infinitely often¹⁵ by any infinite trace that complies with the liveness rely as specified by the region protocols and pseudo-quantifiers. Rule ECase allows the splitting of the invariant into a disjunction of, say, , and as in the picture. We need to prove there is going to be eventual progress towards reaching from each of these cases. If we start from , then we already reached the target, and this case can be discharged by rule LiveT. The other cases are covered by Rule LiveO, which justifies progress by appealing to an environment-owned atomic obligation that is live (premises two and three); and Rule LiveA, which justifies progress by appealing to a liveness assumption stored in the atomicity context. The EQuant rule is a generalisation of rule ECase.

To see how progress is justified, consider the trace of Figure 11 starting from . Assume the progress measure at is (i.e., holds in ). Each case can be discharged with either rule LiveO or rule LiveA. Imagine is discharged using LiveO: The rule requires us to find an obligation that, in every state of , is necessarily owned by the environment () for some region . Then the condition checks that the progress measure will improve when the environment will fulfil ; formally:

Intuitively, the condition considers an arbitrary transition from the current case to , obeying the atomic rely (thus allowed by the safety constraints of the protocols). It then compares the progress measure and , taken before and after the transition, checking that:

Examine the trace from in Figure 11. While the trace stays within the environment obligation stays unfulfilled (steps are labelled with the obligation they fulfil, if any), and requires the measure to decrease, or in the worst case stay constant. Since is live, the environment will eventually fulfil it, thus taking us outside of . If such transition takes us to another case, in the illustration, then requires the measure to strictly decrease to some . This process cannot repeat ad libitum: The progress measure is an ordinal and hence well-founded. The effect is that, eventually, the only option is to reach the target. Note that transitions that end in the target are allowed by to increase the progress measure: In the picture the transition reaching increases the measure from to . This allows the “reset” of the measure so the trace can go outside of and the whole process of reaching again can be repeated an unbounded number of times.

The idea behind Rule LiveA is analogous to the above description, but progress is justified by appealing to an environment liveness assumption stored in . The layer of the assumption needs to be lower than any layer we may be holding. Since the environment liveness assumptions only hold in the interference phase of an update, the rule needs evidence that the linearisation point on has not occurred yet, which is provided by .

In the proof of the distinguishing client, the environment liveness condition for the application of rule LiveC between Step 1 and Step 2, is proved by:

where and are defined in Equations (16) and (17), and . Since trivially implies , we can apply EnvLive, setting . Then, we apply ECase to split on the value of : where and . If , then we can apply LiveT, as we are already in ; if , entails , so we can apply LiveO with and . The atomic obligation is live: , and holds no obligations. To check that the condition is satisfied, we need to consider the transitions allowed by the protocol :

Although in this case the progress measure is trivial and the proof of the environment liveness condition simple, the generality provided by non-trivial progress measures is needed for more interesting examples. For instance, our proofs of spin lock (Section 5.1) and CLH lock (Section 5.2) do make use of this added generality.

We chose to state the condition as a semantic check; while this achieves full generality, in typical proofs the environment liveness condition only involves a single region, and can be checked by examining the region’s protocol.

By using the rules we described so far, one can justify most of the proof outline of the distinguishing client in Figure 8. For instance, the proof of for the left thread can be reused as is to prove the call in the body of the loop of the right-hand thread.

The main missing step is the application of the While rule:Let us review the main differences with the simplified WhileB rule presented in Section 2. First, the two triples in the premises of WhileB (corresponding to the blocked and unblocked case) are compressed here in a single triple: This is convenient in proofs, as the proof of the two triples only differs on the treatment of the variant. When , , obtaining the first triple of WhileB, when , we obtain the other triple. Second, the target states are parametrised over the variant : Each value of the variant may represent a different “phase” of the local progress of the while loop; in each of these phases the loop may be blocked waiting for a different set of target states to be reached. Third, as anticipated, the condition is expressed as the conjunction of the first and third premise.

There are two additional side-conditions. Since and assert facts about arbitrary intermediate states of an iteration, they cannot refer to any local variable that may be modified by the body of the loop, hence the fourth premise.

The most important addition is the layer condition of the second premise. The idea is that we should be forbidden from constantly owning obligations of layers that we might assume live in the proof of the environment liveness condition. By requiring , we make sure that the loop invariant only owns obligations of layer higher than , and the in the context of the environment liveness condition indicates that only layers lower than that may be assumed live. The layer in the context of the triple in the conclusion is an upper bound for any layer that may be assumed live in the proof of the loop.

Consider the application of While in the proof of the distinguishing client. The while loop of the right-hand thread is busy-waiting until is set to true. The target states are therefore . In this example, the target states do not depend on the variant , which itself is quite trivial: when the loop is finally unblocked, it needs at most one iteration to terminate. The local variant can simply be , i.e., when is there needs to be one unblocked iteration to terminate, and when is finally the loop will take no more iterations. The loop invariant ison which we can frame the stable assertionSince the loop invariant owns no obligations, we can set , and we need to prove the environment liveness condition ; here, as for the application of LiveC, with the fulfilment of the environment obligation , we immediately reach the target, so can be trivial (). The derivation is as follows:

where . We split into two cases using ECase. In the first case holds, so LiveT applies. In the second, and, since lay , is a live obligation. The condition is satisfied: The allowed transitions either keep constant or set it to , taking us directly to .

The stability of holds trivially, as is constantly 0. The condition is this trivial in this case, because it checks that transitions to and from are not resetting the progress measure; here, once is set to true, it will not be set to anymore, so once is reached there is no way to leave it.

Non termination of distinguishing client with spin lock. If the lock at is implemented as a spin lock, then the distinguishing client may not terminate. Indeed, there is no TaDA Live proof for the distinguishing client if one assumes the spin lock specifications: In the precondition, we need to specify an impedance budget for the lock ; whatever ordinal we may choose for , there is no way to consume some budget at every potential iteration of the loop of and never exhaust the budget, as the number of iterations is effectively unbounded.

The rules in Figure 9 are the most important TaDA Live-specific rules. We have omitted standard rules, such as the axioms for primitive atomic commands, the rules handling sequencing, function calls (recall that for simplicity, we restrict to non-recursive function definitions), and structural manipulations. They are reproduced in full in the Appendix.

Let us conclude with an explanation of the two TaDA Live-specific rules of Figure 9 that are not illustrated by the proof of distinguishing client: rules UpdReg and MkAtom. While the goal of LiftA is to lift an atomic update on a resource inside the interpretation of a region to the corresponding update on the region itself, UpdReg obtains the same effect but on a region that is supposed to be updated once atomically (i.e., ). While LiftA applies to regions with , the update allowed in that case needs to be an identity step from the point of view of the abstract state of the region. A genuine update to the region needs to be recorded as the unique linearisation point on that region; this is precisely the purpose of UpdReg. Most of the premises of UpdReg have the same function as in LiftA: checking that the update of the abstract state and the obligations comply with the protocol. The difference is that here the update expected to take place in the linearisation point is recorded in (i.e., the components of recording the expected update to abstract state and obligations of ). To be able to claim the linearisation point took place exactly once, the precondition of the triple requires the resource, which represents the unique permission to perform the linearisation point. The postcondition allows for two cases: Either the update was successful, in which case the atomicity tracking component is recording the update ; or the update was not performed () and the resource is still available for future updates.

Rule MkAtom is another crucial rule for proving abstract atomicity: It states that a Hoare triple can be promoted to an atomic triple if it contains a “certificate,” in the form of being updated to , that the region in question was updated atomically exactly once, with the expected update. The expected update and the additional interference assumptions given by the pseudo-quantifiers need to be stored in the atomicity context so the triple in the premise can make use of the interference precondition assumptions and certify the right update took place. Any expected update must be protocol-compliant (). Notice how the atomicity context records the liveness assumption expressed by the pseudo-quantifier, so it is available for termination proofs in the proof of the triple in the premise; in particular, they can be used by applications of LiveA. The proof of spin lock and CLH lock in Section 5 illustrate applications of MkAtom and UpdReg.

In the spirit of CAP, abstract resources provided by a library should be presented to clients by only exposing their abstract properties, and not their definition.

In our example, the predicate is defined internally to the proof of the lock module, say, using internal regions (of some maximum level ) expressing the internal protocols of the module.

The proof of our distinguishing client only relies on the following abstract properties:

For instance, the interpretation is well-formed, thanks to properties 2 and 4. The proof also involves side conditions on layers, stability, and ’-safety, which can be discharged by appealing to 2, 3, and 4.

More generally, a module would typically expose to clients viewshifts representing separation properties of the abstract predicates (e.g., duplicability), stability properties, -safety, obligation freedom, and relevant facts.

TaDA Live’s triples are rather expressive: They support strong specifications of updates via logical atomicity, and conditional termination properties via liveness assumptions. It is natural to ask whether our triples force the leak of any unnecessary detail about the implementation. In particular, there are three components of the proof system that have a “global” flavour: the level and layer in the context of the judgement and the layer decorating the liveness assumption of the pseudo-quantification. Although necessary for soundness, the management of levels is tedious but relatively straightforward. Iris introduced namespaces for invariants to ease the management of so-called masks, which serve essentially the same function as levels in TaDA. A similar construction could be used to ease management of layers. Here, we keep it simple and require proofs of clients to use layers high enough to be able to reuse the libraries specifications.

The layers decorating a triple, however, are a more delicate matter. The main complication arises from the choice of parametrising TaDA Live with a global layer structure. If a specification insists on the use of a specific subset of layers, then that could seem like an unnecessary leak of implementation details. For example, there could be two valid implementations of a module that use wildly different internal layer structures to justify their internal blocking behaviour. Should the abstract specification of the module insist on a specific layer structure for the internal layers, that would rule out valid implementations for no good reason. In TaDA Live modularity of the layers can be achieved by exploiting a crucial property of derivations: Their validity is invariant under a strict-ordering-preserving remapping of layers. This allows a style of specification that generalises the one we have seen in our examples until now, where the layer structure relevant for the proof of an implementation is parametrised over a client-provided remapping of layers. To avoid cluttering the proofs, we do not explicitly parametrise the proofs in Section 5. In Section 5.5, where the construction becomes relevant and used in a non-trivial way, we explain how to convert a proof so it is parametric on the layer remapping.

In terms of behaviour, TaDA Live’s specifications are able to hide internal blocking, as shown by the blocking counter example of Section 2.1 (formalised in Appendix 5.3). There is, in fact, one progress property leaked by the specification layers that is currently not exploited by TaDA Live. In the special case when the layer in the context is the globally smallest layer , the proof of the triple cannot rely on any liveness assumption at all. This can be used to differentiate, for example, a wait-free counter implemented as a hardware-atomic fetch-and-add (which admits a proof with in the context) and a blocking counter (which only admits proofs with layer ). This is a useful distinction: Wait-freedom is an important progress property, asserting termination without assumptions on liveness of other threads and without fairness assumptions on the scheduler [19]. Currently, however, TaDA Live’s semantics does not support deriving wait-freedom as a consequence of as the context layer: The current triple semantics only implies termination of the fair traces. Extending TaDA Live’s semantics to encompass wait-freedom is left as future work.

We have proven soundness of TaDA Live rules against the semantic judgement of Definition 3.30.

The detailed proofs of the liveness-related rules are produced in Appendix E. The soundness of most rules is an adaptation of the soundness arguments of the corresponding TaDA rules. The rules that drive the liveness argument are rule Par, rule LiveC, and rule While.

The soundness of the parallel rule follows from the layered liveness invariants semantics explained in Section 3.9. The argument is roughly as follows: There are two possible ways the parallel composition may fail to terminate: Either one thread terminates and the other does not, or they both do not terminate. In the first case, when the terminating thread, say, , terminated, we are in a state where thread 1 does not own any obligation of layers that may be assumed live by (this is from the conditions on the layers of the postcondition of ). By the triple about in the premises, is only allowed not to terminate if the environment is constantly owning an obligation of layer lower than . Since cannot do that, we obtain that said must be owned by the overall environment of the parallel composition. In such case the triple of the conclusion allows the program to diverge.

In the second case, both threads are not terminating. Each of the threads, say, 1, is allowed to keep an obligation constantly unfulfilled, as long as it can blame thread 2 by showing an obligation of strictly lower layer that is kept constantly unfulfilled by 2. Since layers are well-founded there needs to be some thread that will not be justified in not fulfilling some of its obligations. This cannot be, as we were able to prove the two triples in the premises.

The soundness of rule While considers the worst-case scenario for progress: an infinite sequence of iterations, all of which do not start from a target state in , and therefore do not decrease the variant . In such case, we know that the assertion holds at every point of the trace: it has been framed so the local steps and the environment steps must preserve it, and it is stable (as checked by EnvLive). We are thus within the hypothesis of the environment liveness condition, which proves, together with the premise asking the progress measure to never increase, that eventually the target states will be reached. Although they may be reached in the middle of an iteration, instead of at the beginning, as it would be required to invoke the triple that decreases the variant ; in the worst case this can happen boundedly many times (the progress measure is well-founded and must always decrease). Therefore, we eventually reach and do not leave it until the next iteration starts from a state satisfying , which matches the premise that ensures the variant decreases. This can only happen boundedly many times, as the variant is well-founded.

Rule LiveC’s soundness argument is a variation of the one for While.

As a simple corollary of soundness and Theorem 3.33, if we can prove , then run in isolation terminates from the empty heap. For our distinguishing client (Example 4.1) for instance, we can wrap up the proof by initialising the state and provewhich implies termination of the program.

Code. The spin lock module implements a lock by storing a single bit in a heap cell; locking is implemented by trying to CAS the heap cell from 0 to 1 until the CAS succeeded; unlocking simply sets the cell back to 0. In Figure 12, we give all the operations of a spin lock module.

Specifications. We will prove the module satisfies the following specifications:where abstractly represents the lock resource at abstract location (omitted for readability in Section 2) and concrete address , with abstract state and impedance budget (an ordinal). The purpose of the impedance budget, as described in Section 2, is to prevent the environment from taking possession of the lock an unbounded number of times. Without this bound, the operation in the implementation of could be indefinitely preempted by the environment locking the lock, preventing it from ever taking its possession and terminating, even if the environment always unlocks the lock when it is locked. This is enforced by requiring the lock operation to strictly decrease the impedance budget using , a function that can be freely instantiated by the client upon usage of the specification, which indicates precisely how much the budget will decrease after this call (which is client-dependent information). The specification of then allows the client to pick an arbitrary ordinal as the initial budget.

Shared Region. The abstract shared lock resource will be represented by a region where , , . Here, is a fixed parameter of the region.

Guards and Obligations. For the region, we only have the exclusive guard , and no obligation constructors, as the implementation has no internal blocking. All the blocking behaviour is represented by the liveness assumption in the pseudo-quantifier of the specification of . Note that without the exclusive guard, the specification of would not hold as the lock would not be stably unlocked.

Region protocol. The interference protocol for is very simple:It states that whoever owns can freely acquire or release the lock, provided that at each acquisition, some budget is spent (), preventing the lock from being locked an unbounded number of times.

Region interpretation. The implementation uses a single cell stored in the heap, and we have no non-trivial guards/obligations; the interpretation is thus straightforward:Note how is pure ghost state in that it is not linked to any information in the concrete memory.

Predicates. The lock resource is abstractly represented by the predicate

Verification of . Figure 13 is the proof of the operation. The only step that involves reasoning about liveness is the application of the While rule. To apply this rule, we must first define the loop invariant, , the target states, , the persistent loop invariant, , , and the environmental progress measure, .

The loop invariant iswhich contains:

Indeed, whenever some budget is spent, the loop approaches termination, as, eventually, the exhaustion of the budget prevents further interference, allowing the operation to succeed and the loop to terminate. Therefore, decreasing the upper bound to the interference budget corresponds to progress for the operation. Without additional information, however, we cannot show the local variant must eventually strictly decrease, indeed, in the case , we cannot exit the loop and the environment is not forced to spend budget. Therefore, the termination argument will need the assumption that the environment always eventually unlocks the lock to allow the termination of the loop or further decrease of the variant due to the environment locking the lock. This guarantee is given by the atomicity context with .

The target states, , must clearly include unlocked states, where , but, as it must eventually be stable, this is insufficient, since once the lock is unlocked, the environment can lock it again. However, when the lock is unlocked, if the environment takes possession of it, then the environment must also simultaneously decrease the impedance budget, i.e., .

The argument that is always eventually true relies on the assumption from the atomicity context that the environment will always eventually unlock the lock. However, this assumption only holds before the linearisation point. In particular, as the loop variant must contain , since the loop body may perform the linearisation point, the persistent loop invariant cannot, and therefore must also contain a disjunct where the linearisation point has occurred and holds a witness .

We therefore declare the target states as the ones where either the linearisation point has been performed, the lock is unlocked, or some budget was spent:

The persistent loop invariant here is simply , which is a valid stable frame of the loop.

To apply While, we also need to specify , which in this case is simply , which satisfies the layer constraints of the rule; and the environment progress measure :(Here, we use the variable for the environment progress measure variable to avoid clashes with the impedance budget .) This environmental progress measure is decreased by both the environment locking and unlocking the lock:

Given these parameters, the proof first establishes the loop invariant holds at the beginning for some , by applying Cons:Note that we will often implicitly apply the Cons rule in proofs, only detailing the application when emphasis is desired. Next, Elim on gets rid of the existential quantification, so we are ready to apply While.

To complete the application of the rule, we need to show

Condition (19) is easily seen to hold, as we showed above, all possible environmental interference on the region decreases the environmental progress metric, which is sufficient for this to hold.

Condition (20) is also easily seen to hold, as the only program variable predicated over in , and is , which is not modified by the body of the loop.

Finally, condition (18) is proven as follows. We observe that:We can then derive the environment liveness condition:

Formally, the application of EnvLive requires us to prove which is trivial. An application of the ECase rule then splits between the cases where and hold. Intuitively, represents the case where we performed the linearisation point or the lock is unlocked, while the case where we still have not performed the linearisation point and the lock is locked. If holds, then holds, so no progress of the environment is required, therefore, this case can be discharged via an application of rule LiveT. In the case where holds, we can apply rule LiveA to invoke the liveness assumption stored in : If the lock is unlocked, then the metric strictly decreases.

To show that the liveness assumption encoded in the atomicity context for the region , is active, the LiveA rule requires that in the current case:

If these hold, then the predicate shows that discharging the liveness invariant will strictly decrease . To show this holds, taking arbitrary and lettingwe need to showThis holds, as, given an arbitrary , any step taken from by the atomic world rely relation either leaves the state of the region unchanged, preserving the state , or releases the lock, decreasing the metric. Therefore, for any , holds, which implies the goal.

To conclude the argument, we briefly comment on the proof of the body of the loop. The full proof of the body can be found in Figure 14. The applications of rules UpdReg and Frame lift the concrete atomic to a (potential) update to the region. An application of Cons allows us to introduce as an upper bound to the impedance budget, initially after the linearisation point.

Then, we apply rule AElim to remove the pseudo-quantification on and . At this point, the abstract state of the region in the postcondition is weakened to any state that might be reached before or after the linearisation point. However, we keep record of what happened exactly at the linearisation point because of the assertions. The later application of MkAtom will be able to fetch the atomic update witness and declare the appropriate atomic update in the overall specification. Note that the overall Hoare postcondition after the application of AtomW is stable.

Finally, Figure 15 shows the proof outlines for the and operations. The only notable step of the proof of is the last application of Cons to viewshift the postcondition from to , which is possible because the interpretation of the region matches with this resource, so the reifications of the two assertions coincide.

The proof of is a straightforward lifting of the atomic reset of the cell at to the region . Neither proof involves a liveness argument.

Code. A CLH lock is an implementation of a fair lock module that guarantees fairness by queuing the threads that are waiting to take its possession. Its implementation is shown in Figure 17.

The diagram in Figure 16 describes the state of the queued threads, , waiting to take possession of the lock, as well as the module’s head and tail pointers into the queue.

As described in Section 2, this queue is represented by associating each of the threads queuing on the lock with the heap cells in memory. Each thread executing the operation to take possession of the lock then holds in its local state the address of its cell and that of its predecessor’s cell. These are held in the program variables and , respectively, in the implementation of . The local instance of these program variables for each queued threads and the cells they are pointing to can be seen in Figure 16.

The thread associated with the cell at the head of the queue is said to hold the lock, and the value stored in its cell determines the state of the lock, . When a thread first takes possession of the lock, the lock will be locked. Therefore, the initial value in these cells, when the associated threads join the queue, is 1. This can be seen in the implementation of the operation, which allocates and sets its associated cell to value 1 on line 3 before enqueuing itself. Once the thread holding the lock wishes to release it, it can do so by setting the value of its cell to 0, unlocking the lock and signalling to the next thread in the queue that it can now take possession of the lock. This can be seen in the implementation of the operation, which fetches the address of the cell associated with the lock’s owner from the queue’s head pointer and then sets its value to 0.

In Figure 16, the thread is at the head of the queue, waiting for the lock to be released. If the lock is released by its owner, then gains the exclusive permission to take possession of the lock by setting the value of the module’s head pointer to the address of its associated cell. detects the lock has been released by repeatedly reading the value of its predecessor’s cell in the loop on line 6 and then sets the head pointer to the address of its cell, , on line 7.

Once the lock is released, only the thread at the head of the queue (if any) has the permission to take possession of the lock next. Due to this, if the owners of the lock continuously eventually release it, then the threads waiting on the lock take possession of it in the order they are enqueued.

To enqueue itself, the operation performs a operation on the tail pointer, placing the cell it has allocated with value 1 at the tail of the queue and writing the address of its predecessor to the program variable. The order in which the operations are enqueued is then the order in which they executed line 4. Any weakly fair scheduler will eventually give each thread executing the operation the opportunity to execute this operation, allowing it to enqueue itself.

As long as the client then guarantees that every thread holding the lock eventually releases it, the thread will eventually take possession of the lock once it reaches the front of the queue and the operation will terminate, guaranteeing fairness.

To be able to provide the same guarantee, that every thread requesting the lock will eventually be able to take its possession as long as the lock is always eventually released, the spin lock requires that its client only call the operation concurrently a finite number of times. This is exposed in the spin lock specification via ordinals bounding the impedance on the lock.

An interesting aspect of this example is that it features a combination of internal and external blocking: The client needs to always eventually unlock the lock—external blocking, requiring the client to provide a guarantee—and the operation needs to eventually take possession of the lock once the previous thread signals its release—internal blocking, guaranteed by the implementation. This second guarantee will be enforced using obligations not exposed in the specification. The proof will therefore involve an environment liveness condition discharged using both LiveO and LiveA.

Specifications. We will prove the following fair lock module specifications:where abstractly represents the lock resource at abstract location (omitted for readability in Section 2) and concrete address , with abstract state .

To abstract the representation of a thread’s position in the queue, we will associate, through ghost state, to each thread requesting the lock, a ticket number that corresponds to the order of arrival of the implementation at line 4. Every time a thread joins the queue, it gets assigned the next available ticket.

This example shows a common proof pattern of TaDA Live: There is an inner region that exposes all the information needed for the termination argument (here, the value of the next ticket to be handed out, , so individual threads can reason about the threads queuing on the lock) and an outer one that hides enough information to make the operation abstractly atomic. This pattern nicely separates the concerns in the proof: proving atomicity is done via the outer region, termination via the inner one. Because of this, the abstract location of the lock will consist of the pair of inner and outer region identifiers. This is not a concern for modularity, however: The type of can be made opaque to the client, which just threads it through the proof unmodified.

Shared Regions. The abstract shared lock resource will be represented by a region where , , , . Here, , the region identifier of the inner region and , the address of the lock, are the fixed parameters of the region. The abstract state of the region includes , which represents the lock’s state, , which is the ticket number of the thread holding the lock, and is the address of the cell associated with the owner.

Once a operation has enqueued itself, the difference between the ticket of the lock’s owner, and the operation’s ticket, , , corresponds to the thread’s current position in the queue.

The internal region also exposes the next ticket to be handed to the next thread queuing on the lock, .

Notation. Lists will frequently be used in the ghost state for the proof of the CLH lock. We introduce notation to manipulate lists to simplify the exposition of the reasoning. Given and lists of elements of , we write , , and for prepend, append, and concatenation, respectively; is the length of , and states that the ith element (from 0) in is and ; and are the first and the last element of , respectively, and represents the list without the first element when is non-empty.

Guard algebra:. Take arbitrary. For this proof, two guards will be necessary. First , which encodes the current thread’s ticket, , once it has joined the queue, as well as , pointers to the thread’s predecessor’s cell in the queue and its own, respectively. The second guard we require is , which is used to track the overall queue, by tracking the cells associated with enqueued threads, , and the ticket number of the current owner, .

To use this as intended, a few axioms on the guard algebra will be required. First, an axiom to create new tickets, adding a new cell to the queue and associating a new, unique ticket number to the thread:This will be used to create the relevant guard resources when a lock operation enqueues itself on line 4. Similarly, an axiom to remove a thread’s predecessor from the queue once it can take possession of the lock:This will be used to update the relevant guard resources with the relevant when a lock operation takes possession of the lock on line 7, placing its associated cell, , at the head of the queue. Finally, an axiom to guarantee that a ticket guard, , is well-formed with respect to the queue in a guard :

Obligation algebra:. Take arbitrary. As mentioned above, to verify the totality of the CLH lock operation, once a thread is enqueued, if its predecessor relinquishes possession of the lock, then it must eventually take its possession. Otherwise, although the lock will be permanently unlocked, no other thread waiting for the lock can take its possession, as they are not at the head of the queue.

To encode this liveness invariant that must be fulfilled, we associate an atom obligation with the ownership of the ticket . The CLH lock’s transition system will then require that this obligation be discharged by taking possession of the lock once it is unlocked by the thread with ticket .

The layer associated with is then , so these obligations are resolved in the order the associated threads are enqueued. Finally, as with the guard algebra, we have an obligation , which will remain in the shared region’s state and track the owner’s ticket, , and the next ticket to be handed out, , associated with the obligation via the obvious axioms.

Region protocols. The interference protocol for the region is as follows:

The first transition allows a thread to place itself in the queue waiting to obtain the CLH lock, updating the next ticket to be handed out from to . While doing so, the thread acquires an obligation, , requiring it to eventually take possession of the lock once it is at the head of the queue. The second allows the thread at the head of the queue to take possession of the lock by changing the state, , incrementing the owner ticket, , to its own (tracked by the thread’s obligation) and changing the owner pointer of the lock to that of its own associated cell. This discharges the obligation , as the thread then leaves the queue to take possession of the lock. Finally, the third transition allows the lock to be unlocked.

The interference protocol for the region is then:

This hides the enqueuing step of the operation, allowing the operation to appear atomic.

Region interpretation. As explained above, the CLH lock associates a cell with each thread queuing on it, as well as its owner. The list of each of these cells in the order in which the associated threads are queued, with the owner’s cell as the head, will be denoted . is then the list of cells queueing on the lock. While threads are queuing, the associated cells must have value 1; this is represented using the predicate :The inner shared region, , holds the cells associated with each queued thread, this is represented by the resource in the region interpretation.

The shared region also holds a pointer to the tail of the queue, , as well as a pointer to its owner’s cell, whose value is the state of the lock, , as described above. This is represented by the resource:The shared region’s ghost state then comprises:

Finally, the invariant is used to guarantee that each thread that holds a ticket is associated with a cell in the queue and , associates the head of and the address of the owner’s cell. All of this ties together to give the following region interpretation:The outer shared region then holds full permission to update the inner region, , and asserts that each thread queuing on the lock, with tickets to , holds an obligation to take possession of the lock once their predecessor releases it, , where is the identifier of the inner region:

Predicates. The lock resource is then abstractly represented by the predicate:which abstracts away the CLH lock’s implementation details: the ticket and cell address associated with the lock’s current owner.

Proof of . Figure 18 gives an outline of the proof of the clh operation implementation; the definition of the loop invariant will be given later. The steps involving liveness are the operation, which enqueues the thread, hence obtaining the obligation to take possesion of the lock once the previous thread relinquishes possession of it; the while loop, which waits for the previous thread to release the lock, whose liveness depends on the previous threads in the queue taking possession and then releasing the lock in turn; and the write operation at line 7, which takes possession of the lock. We begin with the details of the operation’s proof, shown in Figure 19.

There, Step 4 is composed of the rules: FrameH, AtomW, AElim, LiftA, AElim, LiftA, AElim. The application of the FrameH rule frames off the view , the AtomW rule transfers all the remaining resources to the atomic precondition and postcondition, the AElim rule pseudo-quantifies , , and , LiftA then opens up the region , the applications of AElim and LiftA then pseudo-quantify and open the region and the final application of AElim rule pseudo-quantifies .

After using LayWH to decrease the level of the assertion to and Frame to frame off everything except the region interpretation’s tail pointer, the operation atomically updates it. After everything is framed back on, the consequence rule is then applied to the postcondition to re-establish the invariant. The axiomsare used to update the queue , by enqueuing —the local thread’s cell—at its tail, and updating the next ticket to . While doing so, the thread acquires the guard , the obligation, , which represent the thread’s position in the queue and its obligation to take possession of the lock once its predecessor reliquishes it, respectively.

As environmental obligations can always be duplicated, the thread also obtains locally. These environmental assertions will be necessary for the application of the While rule. To finish reestablishing the invariant, as the thread is retaining locally, it can leave in the region invariant. Finally, using the axiomas we hold locally, the assertion holds stably.

Next, consider the proof of the loop. The loop invariant is:which asserts that:

A thread with ticket can take possession of a CLH lock once its predecessor has taken possession of and relinquished the lock. Once the lock reaches this state, and hold stably, as all transitions from this state would set , however, we know that, .

The intent of this loop is to wait till this occurs, allowing the thread to safely take possession of the lock once the loop terminates. Hence, the goal state is:Once the lock reaches this state, a subsequent iteration of this loop will terminate with , breaking the loop. To reach the goal state, threads that come before the current thread must both take possession and then unlock the lock. The first is guaranteed due to obligations for and the second due to the pseudo-quantifier, guaranteeing that the lock must always eventually be released. The progress measureis decreased by both of these actions and, as implies , the progress measure, , is a natural number, and therefore well-founded.

The use of the difference between , the local thread’s ticket and the owner’s ticket, , to bound the number of threads that can take possession of the lock before the local thread removes the necessity for the impedance bound, , required in the proof of the spin lock module, and that must leak in the associated specification (as it imposes a restriction on any client).

To support this argument, the persistent loop invariant, , must contain the resource to make use of the liveness assumptions of the pseudo-quantifier, guaranteeing that the lock is always eventually unlocked, and the relevant environmental liveness assertions guaranteeing the threads queued before the current thread will take possession of it once their predecessor relinquishes it:

The While rule is applied as in Figure 20. The rule Elim is applied to quantify and over the antecedent. To complete the application of the rule, we need to showCondition (24) holds trivially, as seen above, all the possible operations on the module decrease the environmental metric.

To prove Condition (23), takeFirst split on :In the case , the rule LiveT applies directly. To show holds, split on the state of the lock, .