5. Week 05: Auxiliary State and Rely-Guarantee Reasoning

We continue the discussion on linearisability, moving on from the formal definitions to the proof methods.

5.1. Refinement and Simulations

Intuitively a system \(S_2\) refines a system \(S_1\) iff for any client application \(P\), all observable behaviours of \(P\) from using the system \(S_2\) are also the behaviours of using \(S_1\) (in mathematical notation \(S_2 \sqsubseteq S_1\)). In other words, the client “won’t notice a difference” if the module \(S_1\) is replaced by module of \(S_2\). In this dichotomy \(S_1\) is frequently referred to as specification, while \(S_2\) is referred to as an implementation.

The notions of refinement and linearisability are tightly connected. In essence, a linearisable object can be used as a replacement for an “atomic” object for all purposes.

Mandatory Reading

The paper Proving linearisability using forward simulations summarises basic notions connecting linearisablity, refinement and simulations — a general method of proving linearisability/refinement. Make sure to read it up to Section 4.

Highlights:

  • Refinement between concurrent libraries is stated in terms of subsets of event histories (similarly to linearisability).
  • Simulation is a relation between two labelled transition systems (think objects with operations represented by labels), which, if exists, shows that for a single step of the specification there is always a sequence of steps in the implementation, where only one of such steps is “meaningful”, and other are “administrative” ones.

Optional Reading

A general framework for proving refinement via simulations with an addition of “auxiliary” (“ghost”) and “prophecy” variables is presented in Abadi and Lamport’s seminal paper The Existence of Refinement Mappings.

5.2. Proving Simulations for Program Code

It would be nice to have a formal method to prove linearisability of our code by reasoning about implementations. As an example of a linearisable concurrent structure, let us consider Treiber’s stack, as presented in Viktor Vafeiadis’ PhD Dissertation: Figure 5.1 is a concrete implementation, and the abstract specification is given in page 87. Let us ignore the other details for now, and just think how exactly we would prove that the implementation refines the specification. Ideally, we should be able to formally justify the location of linearisation points in the code, but to tie their “effects” to the semantics of the programs, we will need some extra machinery.

5.3. Verification with Auxiliary Variables

Let us take a step back and consider an example of a simple parallel program, which is surprisingly tricky to verify using the logic rules for Hoare-style reasoning: parallel incrementation of a shared variable x. The classical 1976 paper by Susan Owicki and David Gries shows a method to deal with such problems by introducing “auxiliary” variables that record the effects of different processes. As it turns out, those auxiliary variables are also crucial for establishing forward simulations and ultimately proving linearisability. In other words, they “enrich” the state of the system under consideration with enough structure to make it possible to relate to the specification being refined.

Mandatory Reading

Verifying properties of parallel programs: An axiomatic approach, 1976.

Highlights:

  • Atomic sections of the code make it possible to make use of the invariants (similar to system invariants), which hold every time one starts an atomic operation. However, it is also one’s obligation to restore the invariant upon finishing the execution of a critical section. As an example of this reasoning, see the verification of a program add2 in Figure 2.
  • Auxiliary variables may not appear in the RHS of program statements that change non-auxiliary variables. This is to ensure that they were only used for “internal accounting” of the effect of each individual thread, and were not affecting the logic of the program (and, thus, can be safely erased).
  • That said, auxiliary variables are very useful for maintaining partial information by a thread in an interference-free way (i.e., so it couldn’t be affected by other threads) and use it for “reconciling” thread’s views upon joining them at the end of the parallel execution.

5.4. Rely-Guarantee Reasoning

But what if we cannot encapsulate the entire effect of concurrent threads into disjointly-modified auxiliary variables. In this case, we can relax the notion of a Hoare triple to incorporate the “effect” of the environment (so-called Rely-relation) and make sure that each step of our reasoning is resilient with regard to those effects. Simultaneously, in order to allow symmetric reasoning for other threads, we ensure that our own effects on the shared state are declared as well (as a so-called Guarantee relation). The reasoning method is well-known under the name Rely-Guarantee reasoning and is described in the seminal 1983 paper Tentative Steps Toward a Development Method for Interfering Programs by Cliff Jones.

Mandatory Reading

These slides (courtesy of John Wickerson) provide an excellent high-level description of the Rely-Guarantee reasoning method, as well as some examples.

Highlights:

  • In most of the rules for RG reasoning, the Rely and Guarantee take symmetric roles with regard to the parallel threads (i.e., my Guarantee is your Rely and vice versa).
  • Hoare-style reasoning is now done modulo stability: whenever shared state makes appearance in assertions (pre- and postconditions), we need to ensure that those assertions are stable. That said, if each program component is specified with stable pre/postconditions, we don’t need to perform additional checks when validating their sequential composition (do you see why?).
  • Some programs with identical effects of threads (e.g., parallel increment) are still tricky to verify using RG dure to indistinguishability of the complementary effects. Therefore, one should mix in some auxiliary variables to push the verification through.

5.5. Proving Linearisability with Auxiliaries and RG

Now, armed with Auxiliary Variables and Rely-Guarantee reasoning, we can revise the Treiber stack linearisability proof from Section 5.3.1 of Vafeiadis’ dissertation. The proof builds on the following components:

  • Definition of the abstract atomic stack structure, instantiating an auxiliary variable Abs
  • Rely/Guarantee “actions”, corresponding to push/pop in the concrete implementation
  • A state invariant, which connects the concrete state and the abstract representation.

The proof follows the standard OG/RG pattern with the only twist that the linearisation point corresponds to the “single-shot” variable AbsResult, which at some point transitions from the Undefined state to the result of the operation, signifying the execution of the corresponding transition of atomic specification. This change takes place at one of the RMW operations in the concrete implementation (compare-and-swap), which also ensure the preservation of the state invariant.

5.6. Linearisability, Refinement, and Paxos

Let us not see how the described methods work in verification of proper distributed protocols, applying them to specifying and verifying a consensus protocol.

What would be a good “sequential” specification for Paxos? This ESOP‘18 paper gives a shared-memory style specification of a single-decree Paxos and proves that a it is correctly refined by the standard distributed implementation. Also, check out the accompanying slides.