A Compositional Proof Method for Linearizability applied to a Wait-Free Multiset

This presentation accompanies our article submitted to iFM '14. The paper presents a compositional proof method for linearizability that goes beyond existing local approaches (including our own [15]). It illustrates its expressivenes using a novel wait-free multiset example with intricate potential linearization points that change the abstract representation and linearize several other processes. The example is comparable to the Herlihy Wing queue that is considered one of the most intricate examples for proving linearizability. To our knowledge, it can not be shown with existing local techniques, since these are typically restricted to potential linearization points that do not alter the abstract representation.

This site directs the interested reader to the mechanized specifications/derivations that are indicated in the paper. The presentation is structured in three parts: First, the formalization and the soundness proofs of the underlying logic RGITL are described on this extra page formalization of RGITL (corresponding to the brief description in Section 3.1 from the paper; a version of our recent journal article [13] can also be downloaded there). The second and third part are given below. The second part introduces the formalization and correctness proofs of our proof method for linearizability (Theorem 1 in the paper), and the third part describes the application to verify the wait-free multiset correct.

Linearizability and Possibilities:

• We specify linearizability using a predicate "linearizable" on lists of invoke and return events (i.e., histories). Several auxiliary predicates (legal histories that corresond to our histories H in the paper, sequential histories that correspond to Hs in the paper, matching pairs of invokes and returns, pending invokes pi, ...) are used, too. On top of that theory, we define possibilities. Possibilities were also defined in [5]. Instead of the original notation "<v,P,R> in Poss(H)" we write "Poss(H,R,v)" (parameter P is redundant, since it is just the pending invokes in H, that have not linearized, i.e., for which there is no corresponding return in R). Parameter R is written "es" (event set) in all of the proofs; parameter v is AS in the paper. The specification also defines possibility steps as either HBInv (corresponding to "Invoke" in the paper), HBLin ("Linearize) and HBRet (abstract return). The reflexive and transitive closure of the union of HBInv, HBLin and HBRet is defined as HBOp*.
• In our proof method we use an equivalent definition of possibility steps: DPoss(H,as,R,HS,H',as',R') holds if there is a derivation from Poss(H,As,R) to Poss(H',As',R'). Compared with the paper, predicate DPoss has an extra parameter HS, which is the abstract (sequential) history that can be constructed from the executions of linearization points (see second disjunct in the definition).
• Our paper implicitly claims that possibilities are equivalent to linearizability: In addition to the proof of Theorem 9 in [5], which says that the existence of a possibility guarantees linearizability, we also prove Theorem 10, which is the other direction. These two proofs are rather complex and require lots of lemmas about the auxiliary predicates involved.

Proof Method (Theorem 1):

• The history enhanced concurrent system model according to Section 2.1/2.2 of our paper is defined in specification HSPAWN. The system state "S" from the paper is "LSF,GS" in KIV where LSF is the local state function and GS is the shared part of the state.
• The pre-conditions of Theorem 1 are given as axioms in specification HRG-Lin-Conds: The central proof obligation (3) from the paper corresponds to axioms "HCOP-invoke", "HCOP-lin" and "HCOP-ret" for the invocation, the internal steps and the return event, respectively. The central guarantee G^{poss} corresponds to predicate "HDPoss-bw" and the rely R^{poss} is defined here as the two relies HRPi and NoPi' -> NoPi''. Whenever we instantiate this specification (e.g., to verify the multiset correct), its axioms become proof obligations that we must verify for the given instantiation. The RG restrictions such as reflexivity of guarantee conditions, transitivity of rely conditions... correspond to axioms "hg-refl", "hr-trans" and so on.
• The conclusion of Theorem 1 corresponds to theorem HSPAWN-is-linearizable in the theorem base of specification HRG-Linearizability-Theorem. The non-trivial proof of this theorem essentially uses i) the axioms of specification HRG-Lin-Conds, ii) the conclusion of the RG decomposition rule (2) from the paper which corresponds to theorem HSPAWN-sust-hrg-main and requires various lemmas about the underlying RG conditions, iii) theorem HSPAWN-alw-poss-strng that shows that HSPAWN always preserves possibilities and iv) Theorem 9 above. (Mechanizing a completeness proof for our method, using Theorem 10 above, is possible future work.)

Verifying the Wait-Free Multiset:

• The algorithms from Figure 1 of the paper are formalized in KIV specification DELMSET-COP. The insert/delete operations increment an auxiliary counter variable (Ix) atomically with their failing if*-test (CAS). The original counter variable of the algorithm (Jx) is incremented in an extra step afterwards. The abstract multiset operations are specified in DELMSET-AOP.
• The abstraction relation is defined in specification DELMSET-ABS as axiom "habs-def" where function "Linsf" from the paper is "outs" in KIV. The simple required RG conditions are defined in specification DELMSET-HINV. The invariant properties (as stated in the paper) are directly encoded in predicate exPi. The number of running processes is formalized based on the number (#pi) of pending invocations in the history (in DELMSET-ABS).
• The central proof for proof obligation (3) from the paper, corresponds to theorem HCOP-Lin-Dia.
  Side note: RG assertions <: VL | R,G,Inv,COP> in KIV (and program assertions in general) have an explicit list of frame variables VL. Variables from VL are unchanged during a transition of the program COP, unless they are assigned in the transition. Frame variables are left implicit in the paper. While proof obligation (3) in the paper, requires a proof of partial correctness only (using the [.] operator), we can even prove total correctness (using <.>) for the multiset with the variant # Ar - Jx for well-founded induction, since the operations are wait-free.
• The verification of a corresponding RG assertion for each of the three multiset operations leads to three central predicate logic lemmas that prove the step-local backward simulation: For the RG assertion HCOP-Dia-Delete, the central lemma is habs-del-lastx for the transition that removes the last occurrence of the searched element from the considered abstract multiset. For the RG assertion HCOP-Dia-LookUp, the central lemma is habs-lkp-true for the transition that finds the searched element. Finally, for the RG assertion HCOP-Dia-Insert, the central lemma is habs-ins-true for the transition that inserts the input element.