Verification of Durable Linearizability of a Persistent Queue

DMSQ, Assertions and Invariants

The formal proofs make use of a library (specifications with orange color) that contains a formalization of much of the refinement theory of IO-Automata from [LV95]. The specifications imported from this library contain

• the definitions of an IO-Automaton as a pair of a start- and and step-function.
• the definition of IO-Automata refinement.
• the definition of a forward simulation together with a proof that it implies refinement.
• the definition of an image finite backward simulation (named t; with invariants cINV and aINV) together with a proof that it implies refinement (in the strong sense; even infinite traces of the concrete autmaton are a subset of the abstract ones).

The proofs of the case study benefit from an automated transformation of programs to a standard IO-Automaton, and the generation of thread-local proof obligations, as described in [FAoC20] that is programmed in KIV. The main specification DMSQ contains the programs annotated with assertions. The data types and axioms for the step relation that are generated from these programs can be found after the separator.

The theorem base of specification DMSQ-proofs contains the generated thread-local proof obligations and the definition of the invariant generated from the assertions as described in [FAoC20]. Most of the effort of mechanizing the case study went into getting the assertions right, and proving all the proof obligations required. The syntax of both specifications is similar to the one of the paper. Here is a rough description and some remarks about small technical differences.

• All programs can refer to the global variables specified under "state variables" and to the auxiliary variables specified under "ghost variables". It is checked that program variables do not depend on ghost variables.
• Accessing the value stored under a reference r in volatile/persistent store is explicitly given as vs[r]/ps[r]. vs and ps map a finite number of allocated references to nodes, that contain three elements. A value stored in the queue is stored under vs[r].val, an optional threadid under vs[r].deqID, the pointer to the next cell is vs[r].nxt.
• Thread Ids are an abstract type in the specification, while the paper has positive integers for better readability. The deqID stored in a cell is therefore from an option type: it is either Some(tid) or None, which corresponds to -1 in [FAoC20].
• Queue-references are stored in vs and rs. All other references are stored separately. The volatile/persistent head is stored in vhead/phead, The return value for a thread with identifier tid are stored in two separate heaps vrvHp and prvHp. They store optional values, which can be either The value stored can either be Some(value) or None. The array with refererences itself is accessed as vretRefs(tid) and pretRefs(tid).
• The programs specified include the (nonatomic) enqueue and dequeue program, that generate steps of one thread. An atomic program RUN starts a thread by changing its program counter pc from idle to ready. The flushes and the crash are specified as global steps.
• Assertions are given either directly in the program as comments in "/* ... */" or explictly for (ranges of) labels in the "assertions" section.
• The rely predicate is specified under "rely condition"
• The atomic steps of the program are parallel assignments (the individual assignments are separated with a comma, while statements are separated with a semicolon), the evaluation of tests, allocating a new cell (by choosing an arbitrary one not yet allocated at line E2). Instead of a "while(true)"-loop with return statements in the middle of the code a "while (not success)"-loop is used, where success is a boolean variable, that starts as false and is set to true by CAS instructions. A "CAS(old, global, new)" is encoded as "if* old=global then success:=true, global := new else success := false". The test of an "if*" is evaluated together with the following assignment in one atomic step.
• The programs specify custom actions using a with-clause at persistence points.
• KIV generates a theorem that the invariant is indeed invariant for steps of the automaton. Formally this is generated as an axiom that does not need a proof (its definition is marked to depend on the proof obligations, to ensure that it cannot be used in the proofs for proof obligations). To ensure that the generated proof obligations are correct, the generic proof given in [FAoC20] has been done for copies of the theorem, and the four lemmas step-lemma rely-lemma, stable-lemma and otherstep-lemma.
• The references used in vrvHp and prvHp are of type rvRef, which is a copy of the type Ref. Since variables of different types have different names, using a copy of the type allows to identify, whether a reference points to a Node or a return value just by its name. It has no other consequences.
• Two small discrepancies to the notation in [FAoC20] are, that the notation for updating the heap "vs" at reference "r" with a node "nd" is "vs[r,nd]", while the paper writes "vs[r := nd]". Function "lsf", updated at "tid" to be "ls" is written "lsf(tid;ls)" instead of "lsf(tid := ls)".
• Variable "last" is named "lst" here, since "last" is a keyword in KIV's temporal logic.

Intermediate Automaton DQ and Abstract Automaton DurQ

• The actions of each step are given using a "with" clause They are as in [FAoC20], except for notation: "res_t(Deq,v)" is written "retDeq(tid, Val(v))" or "retDeq(tid, Empty)", "do_t(Deq)" is written "DoDeq(t)" and "DoDeqEmpty(t)" etc..
• In this automaton all programs (steps of one thread) are atomic. pc(t) before the step is given before the program, the return label specifies the updated pc(t).
• All other conditions under "Pre" are given as a precondition, the effect ("Eff") is the body of the program.
• Variables under "local variables" are available for all threads, they survive individual calls.
• Each of the three automata generates its own action type (DMSQAction, DQaction, and DurQAction). The 1:1 mapping between the actions of DMSQ and DQ is given by a renaming function "ren" in specification abs.

Refinement proof from DMSQ to DQ

• The case of a crash is proved using the main theorem about the effect of crash and recovery.
• fwsim-step-invenq, fwsim-step-invdeq, fwsim-step-retenq, fwsim-step-retdeq are the proofs for invoking and response steps.
• fwsim-step-doenq, fwsim-step-dodeq and fwsim-step-dodeqempty are the proofs for the steps that are persistence points. For the first two cases the step is a flush that may be done by the process running enqueue/dequeue, by another thread or by the system.
• fwsim-step-checkemp and fwsim-step-run are the two remaining steps that have a non-tau action, and finally fwsim-step-abstau are all other steps of DMSQ where the step refines an empty sequence of steps of DQ. The last proof is broken up into proving that the local abstraction (absls and abspc) is preserved for the thread doing the step and for other threads.

Refinement proof from DQ to DurQ

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.

Bibliography

[Imprint] [Data Privacy Statement] [E-Mail]