Verification of FLIT Refinements

This page documents the KIV formalization of

Stefan Bodenmüller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim:
A Fully Verified Persistence Library.
Submitted to VMCAI 2024

Project Overview gives an overview of the entire specification hierarchy.

KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.

• The project verifies two refinements: one from PLib to FLIT[wPSC] and one from FLIT[wPSC] to FLIT[PTSO]
• The three automata are given in the specifications PLIB , FLITPSCweak and FLIT. Each of the last two are directly given as a single automaton that combines the state of FLIT( flit counter, program counter + local variables) with the state of wPSC (persistence buffer "p" ("P" in the paper) + persistent memory "mem" ("m" in the paper)) and PTSO (persistence buffer "pq" ("P" in the paper) + store buffer "bq" ("B" in the paper) + persistent memory "pmem" ("m" in the paper)) respectively. PLIB uses "h, "vm" and "pm" for the log and for volatile and persistent memory ("log", "vmem" and "pmem" in the paper).
• Auxiliary functions and predicates used in each automaton are specified in PLIB-preds, FLITPSC-preds and FLIT-preds. In particular, PLIB-preds defines the function "persistDependentReads" ("pdr" in the paper) and the predicate "h.lastPersistedOrElse(il, true)" ("lwp" in the paper). The theorembases of PLIB-preds, FLITPSC-preds and FLIT-preds contain basic lemmas about the predicates that are used as rewrite rules.
• All automata use KIV's program notation for atomic global steps (keyword "global"; used for e.g. the persist-steps of the memory model and crashes), atomic steps of threads (keyword "atomic"; e.g. the "complete" step), and nonatomic programs (no keyword; used for the flit algorithms). They are automatically translated by KIV to predicate logic transitions of the automaton according to [FAoC2021]. The predicate logic specification resulting from the translation is given after the "END" keyword. Nonatomic programs are labelled, they are translated to a sequence of transitions, each from one one label to the next. A "with" clause after a label indicates the action of the step (if none is given, the default "τ"-action is used). For automaton X, the translation results in a program counter for each thread "pcf(t)" of type "XPC", a local state "lsf(t): XLState" per thread and a global (shared) state "gs: XGState". Together these form the states of type "XState" of the automaton. The actions are of type "XAction". "lstep" is the step relation of one thread, "xStep" is the full transition relation of the automaton that includes global steps, "xInit" describes initial states.
• FLIT[wPSC] and FLIT[PTSO] both use two auxiliary variables "(f)readers" and "(f)writers". "(f)readers" stores those threads that are in between the read instruction and issuing an FO marker with flush_opt. "(f)writers" stores those threads that are in between incrementing and decrementing the flit_counter ("flit_ctr(τ)" from the paper is written "ctr(t)" and "fctr(t)").
• The automata specify global and local invariants under "assertions". Assertions without a range of pc-values hold globally, those with a range (or several) of program counters are thread-local, they hold for specific lines in the code. The invariants are collected in predicates "XLinv" (local invariants) "XGinv" (global invariants) and "XInv" (their combination). The proof strategy described in [FAoC2021] verifies that local invariants are stable with respects to steps of other threads by using a rely condition.
• The proofs for the thread-local proof obligations for the invariants can be found specifications PLIB-proofs, FLITPSCweak-proofs and FLIT-proofs.
• The two refinements each use an abstraction relation (that is a forward simulation) based on predicates "reorder" and "abs" defined in abs-FLIT-FLITPSCweak and abs-FLITPSCweak-PLIB. Again, a number of lemmas are proved in the two theorembases.
• The full abstraction relation is given in specifications FLIT-refines-FLITPSCweak and FLITPSCweak-refines-PLIB under the keywords "abstraction" and "local abstraction" (like for the invariant we have a part for the global (shared) state and a part for the local state of one thread). The specification also defines an "action mapping", that specifies which actions of the concrete automaton are mapped to which action of the abstract one. All concrete actions that do not appear explicitly in the mapping are mapped to an empty sequence.
• The theorem bases FLIT-refines-FLITPSCweak and FLITPSCweak-refines-PLIB for each refinement contain proofs of the thread-local proof obligations for a forward simulation that result from the approach described in [ABZ2023].

Used basic libraries:

• The basic KIV library with basic data types.

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]