Verification of Opacity of the FastLane Algorithm

Note: The description is currently incomplete, we will update it within the next week.

This page documents the proof of opacity of the Fastlane algorithm [SEFM18]. The FastLane algorithm itself is from [Wamhoff et al 2013]. We prove that when the STM implementation switches between using a sequential implementation (SEQ) when a single thread is executing, using the FastLane algorithm for a low number of threads, and another (arbitrary) opaque implementation IMPL for a large number of threads, then under some constraints the result is opaque itself. To prove opacity of an algorithm, it is sufficient to encode it as an IO automaton (where each step of the algorithm is a transition of the automaton), and to prove that this automaton refines TMS2. The proof consists of 4 parts:

1. A proof that running FastLane alone refines TMS2 by a forward simulation

2. A proof that running a sequential algorithm (SEQ) alone (with a single thread) refines TMS2 by a forward simulation

3. A generic proof that if both C1 and C2 refines A by a forward simulation then switch(C1,C2) also refines A by a forward simulation, if certain proof obligations can be shown.

a) switch(SEQ,FastLane) refines TMS2, and

b) switch(switch(SEQ,FastLane),IMPL) also refines TMS2 under certain constraints on IMPL (one of them being that IMPL refines TMS2 by a forward simulation).

Both proofs are done by discharging (instances of) the assumptions of the generic theorem as proof obligations.

The 4 parts are organized in 4 hierarchical projects (collections of specifications and theorems). As a basis, 2 more projects are used. A generic specification of IO Automata, refinement and simulation, and a specification of TMS2 as an IO Automaton. The following subsections describe these projects.

IO Automata, Refinement and the TMS2 automaton

The project specifying IO Automata, forward simulation (see here for an overview) is quite big. The critical specifications specification of TMS2 as an automaton have already been used in an earlier project, where it is proved that TML (another STM implementation) is opaque by refining TMS2. the last section of this page. For the purpose of doing the proofs here, the specifications of TMS2 just have been placed in a separate project that does not contain TML.

Simulation proof that SEQ refines TMS2

In this project (see the overview over the specification structure) it is proved, that the trivial single-threaded (not instrumented) implementation refines TMS2.

The specification SeqSTM defines the state of SeqSTM as a tuple of its variables.
- mem is the current memory, pc the current program counter, thet the current transaction.
- ll and lv are auxiliary variables used to save the current read.
- Selecting/Updating a variable (e.g. tcntr) of the state is done with selector function '.tcntr' resp. update function '.tcntr:='. The selector is written postfix, the update is written infix. Incrementing tcntr in state ss is therefore written as 'ss.tcntr:= ss.tcntr + 1'.
- Transactions are numbered here. Tf(n) is the nth transaction. tcntr keeps track of the current transaction number.
The specification SeqPC defines the program counters of the algorithm.
- Each program counter directly corresponds to one state of TMS2
The specification SeqOP defines the behaviour of the algorithm.
- Starting a transaction in invTMBegin uses Tf(tcntr) as the new transaction and increments tcntr. Except for this bookkeeping of the running transaction which is necessary for refinement of TMS2, TMBegin is empty.
- DoRead and DoWrite directly access main memory (no instrumentation).
- SEQstart defines the initial state, starting with SS and an empty memory.
- Every step but one corresponds to the TMS2 action that is its name.
- The only tau step is tau-def which is the step from the committed PC to the initial PC.
The specification SeqFWSim defines the (straightforward) forward simulation between SeqSTM and TMS2.
- abspc defines the mapping of SeqSTM pcs to TMS2 PC
- noneStarted specifies that no transaction with an identifier greater than the current SeqSTM has been started.
- The only tau step is tau-def which is the step from the committed PC to the initial PC.
- There are two main lemmas in this specification:
  - FWsim-mainlemma Proves that given a simulation relation between a Seq state and a TMS2 state each step (except DoRead) of SeqSTM does not break the forward simulation.
  - F-DoRead Analogous to the above Lemma for the DoRead step.
The theorem base of specification SEQ-FWSim-correct contains the the main theorem FWSim for forward simulation

The proof uses the FWsim-F lemma.
FWsim-F splits into the proof that the starting states are related by F and the proof that the forward simulation is preserved each step.
The first part is proven using mainly the nonStarted axiom.
The second part contains a further case distinction if DoRead or another action has happened. The cases are prove using FWSim-mainlemma and F-DoRead.

Simulation proof that FastLane refines the TMS2

In this project (see the overview over the specification structure) it is proved, that the FastLane algorithm refines TMS2. The PC values used here differ from the line numbers used in the paper Instead PC values starting with S refer to the START program, those with HR/MR to HELPERREAD/MASTERREAD etc.)

Specification FLpc describes the program counters of FastLane which in the paper are the code lines but here are named after their corresponding part of the program. The mapping of PCs to code lines can be found below.
START
S1: if (masterID = pid)
S2: then ttas-lock (master)
S3: if(masterID = pid)
MSNT: then MASTERSTART
S4: else ttas-unlock(master)
HSNT: HELPERSTART
else if(pessimistic)
S5: ttas-lock (master)
S6: masterID := pid
MSNT: MASTERSTART
HSNT: else HELPERSTART

MASTERSTART
MSNT:
MS: return

MASTERREAD
MR1: val = mem(addr)
MR2: return val

MASTERWRITE
MW1: if even(cntr)
MW2: then cntr := cntr +1
MW3: dirty[hash(addr)] := cntr
MW4: mem(addr) := val
MW5: return

MASTERCOMMIT
MC1: if odd(cntr)
MC3: then cntr := cntr + 1
MC3: ttas-unlock(master)
C: return

HELPERSTART
HSNT
HS: start := cntr &~1
HI: return

HELPERREAD
HR1: if CONTAINS(write-set, addr)
HR2 + HR21: then return GET(write-set, addr)
HR3: val := mem(addr)
HR4: if (dirty[hash(addr)] > start)
A1: then ABORT
HR5: ADD(read-set, addr)
HR6: return val

HELPERWRITE
HW1: if (dirty[hash(addr)] > start)
A1: then ABORT
HW2: PUT(write-set, addr, val)
HW3: return

HELPERCOMMIT
HC1: if EMPTY(write-set)
then return
HC2: mcs-lock(helpers)
HC3: ttas-lock (master)
HC4: if ¬(VALIDATE)
HC6: then ttas-unlock (master)
HC7: mcs-unlock (helpers)
A1: ABORT
HC8: cntr := cntr + 1
HC9: foreach(addr,val) in write-set
HC9a: do dirty[hash(addr)] := cntr
mem(addr) := val
HC10: cntr := cntr + 1
HC11: ttas-unlock(master)
HC12: mcs-unlock (helpers)
C: return

VALIDATE
HC4: if(cntr ≤ start)
HC8: then return true
HC5: foreach addr in(read-set ∪ write-set)
HC4: do if(dirty[hash(addr)] > start)
HC6: then return false
HC8: return true

ABORT
A1: CLEAR(read-set, write-set)
A2: return
The specification FLState defines the state of FastLane as a tuple of its variables.
- The partial map "pidf" used in the paper is represented here as a total map from PID to TorNONE of the same name. TorNONE is either a transaction identifier or a placeholder for no transaction.
The specification LocalOP specifies the transitions of FastLane with the program counters being the action.
- Predicates LOP, LSOP divide the different sections for being in a write read or commit, starting and transit. These predicates are defined over the state variables of one local state before and after the transition (primed variables store the value after the step).
- Predicates write0,read0 represent the steps entering a transactional write or read
- Axioms GSInit and LSInit describe the initial state of the algorithm or a transaction respectively.
- For each predicate axioms defines the pre and post conditions for each action.
The specification FLOP lifts the steps defined in LocalOP to (internal or external) to functions over the full state (the local state function is modified at t/pid to store the new value computed by the local operation. Function f(t;v) is the function f modified at t to be v). Also the TMS2 actions (or an empty τ action) are specified for each step.

FLStart and the corresponding axiom define the starting state of the algorithm.
FLastep defines transitions corresponding to a step in TMS2.
FLstep specifies all transitions of the FL automaton, meaning .
FLstep splits into FLstepnoT and FLstepT. FLstepnoT defines steps of the algorithm where no transaction is assigned (these have no counterpart in TMS2). FLstept specifies steps of the code while it is executing transition t.
For each predicate axioms define the pre and post condition for each action.

The specification FL-FWSim specifies the forward simulation between FastLane and TMS2 as the Predicate F.
- F contains the invariant that the abstract memory sequence is never empty on the top level
- The predicate MemR defined in the paper corresponds to the second part of the conjunction.
- F uses predicate FW which describes propertoes of the forward simulation for individual threads (pid's) together with several invariants.
- abspc maps the concrete program counters to the abstract program counters of TMS2.
- The theorem base of specification FWsim-F contains the main lemmas needed for the forward simulation. The interesting ones are that
- the steps implementing DoRead step preserves F, which splits into three lemmas for the three pcs HR2, HR5 and MR1, which all implement DoRead.
- steps outside of running a transaction (FLstepnoT) preserve F as well as that steps running transaction t (FLstepT).
- The latter lemma has two important sublemmas: steps executed by pid preserve FW for the same pid and for a different pid.
The specification FL-FWSim-correct is an instance of IOforward-is-leqrefine, which proves that a forward simulation implies refinement. It contains the main correctness theorem, that FastLane refines TMS2 with forward simulation F

Generic proof for: if C1 <=_F1 A and C2 <=_F2 A, then switch(C1,C2) <=_F A

See the project overview.

The main specification is Switch-IOAut. It contains the assumptions of the main theorem as axioms:
- Axiom fw1 states, that an automaton C1 (with CStart1 for initialitization, and CStep1 as step relation) refines A (with AStart, AStep) by a forward simulation F1 (C1 <=_F1 A in the paper).
- Similarly, axiom fw2 states C2 <=_F2 A.
- The Axiom CStart-def corresponds to the criterion for initial states of C = switch(C1,C2) of Def. 2 in the paper.
- The axioms CStep-def, Cstep1-preserves-INV1, Cstep2-preserves-INV2, Cstep-preserves-INV, CStep3-preserves-F0 correspond to the requirements of Def. 2 of splitting CStep into CStep1, CStep2, CStep3 with suitable properties and to the preconditions of Theorem 2.
- We allow to specify an invariant AINV (that satisfies Astart-AINV and Astep-AInv) of the abstract specification here. AINV is not mentioned in the paper, and simply conjoined to the forward simulation. In the instantiation (where A is TMS2), this simply avoids having to prove a TMS2 invariant in every refinement.
- The axioms F-def and F0-def specify the forward simulation for C as in the paper.
That Theorem 2 of the paper holds, i.e. that that C <=_F A is implied by the axioms is shown over specification Switch-IOAut-fwrefines-A.
The two projects below that instantiate the theory given here (with concrete states, steps, invariants and simulations) have to prove the (instantiated) axioms of Switch-IOAut as proof obligations. They then inherit the theorem C <=_F A for the instance.

Proof that switch(SEQ,FastLane) <= TMS2 and switch(switch(SEQ,FastLane), IMPL) <= TMS2

See the project overview.

Specifications RestIMPLstate and IMPLOP specify the required types and operations for the (unknown) implementation IMPL. For a concrete implementation these could be instantiated with concrete tuples. No constraints are given (for technical reasons predicate ext must be defined). Since we want to have all internal actions of TMS2 available, when defining steps, but the refinement theory has only a single internal action τ, we define both TMS2step and TMS2astep (like for Fastlane), two accomodate for the difference.
Specification CombState contains the specification of the state used in both switch(SEQ,FastLane) and switch(switch(SEQ,FastLane), IMPL). Variable combs is typically used for such states. The tuple contains
- the union of the components of the sequential state and the fastlane state
- some unspecified remainder combs.ri (of type restIMPLstate) for the non-overlapping part of IMPLstate.
- combs.mode, which is one of "seq", "fastlane" and "impl", which indicates the running implementation
- combs.regset, the set of registered threads,
- combs.runmap, a finite map that maps those pid's (identifiers for threads) which run a transaction, to the corresponding transaction identifier. Since FastLane is currently verified with a function that maps pid's to a Transaction(tid) or None, a conversion function .topids is defined.
CombOP defines the operations of both switch(SEQ,FastLane) and switch(switch(SEQ,FastLane), IMPL).
- The initial states of both are those satisfying COMBstart. The steps are PCombStep resp. CombStep.
- PCombstep has steps of SEQ, when mode = seq, steps of Fastlane otherwise (when mode = fastlane or impl), that leave components of the other implementation unchanged (e.g. SEQ leaves dirty unchanged, Fastlane leaves the sequential pc unchanged). It also has Register, Unregister and SwitchSteps (predicates RegisterStep, UnregisterStep and PSwitchStep).
- CombStep is similar, but has Fastlane steps only, when mode = fastlane. When mode = impl, then IMPLsteps are done. Switching (predicate SwitchStep) is now between three implementations.
- runmapPred contrains steps to correctly allocate/deallocate transactions: steps implementing invTMBegin(t) must use some registered pid, that allocates t = Tf(tcntr), adds (pid,t) to runmap and increments tcntr; steps implementing respTMEnd(t) and RespAbort(t) must remove the pair (pid,t) in the runmap; all other steps must leave runmap and tcntr unchanged.
- RegisterStep adds an new pid to regset, Unregisterstep removes one, that currently runs no transaction (which is not in the domain of runmap, checked with pID ∈ combs.runmap)
- Invariant PINV1 holds in switch(SEQ,FastLane) while SEQ is running. It asserts properties that hold for the FastLane components (like master lock being free). PINV2 would be dual, but is not needed.
- Invariant PINV holds at all times for switch(SEQ,FastLane). It asserts that runmap never contains any transaction with a higher number than tcntr (predicate unused), and that all read/writesets for transaction with a higher number than tcntr (predicate keepempty) are still empty (as in the initial state).
- Predicates INV1, INV2, INV are used in switch(switch(SEQ,FastLane), IMPL). They have the same role as PINV, PINV1, PINV2 in switch(SEQ,FastLane). Since IMPL is not known, the three predicates are left unspecified (we give constraints on them being invariant later on)
- Switching to IMPL may have to reset some implementation state (e.g. reset some pc-values). Therefore an unspecified predicate SwitchtoI is used there (which is later on constrained to at least set mode to impl).
- Switching from IMPL to Seq or FastLane might have some additional constraints than "no transaction running" (similar to fastlane, which runs the decision to call helperstart of masterstart, before running a transaction). These are given as an unspecified predicate preSwitchfromI (which can be instantiated for any concrete implementation).
The theorems of specification Instance-SEQ-FL are instances of the axioms of specification Switch-IOAut (and some trivial ones, that ensure we have a match). Discharging them as proof obligations gives switch(SEQ,FastLane) <= TMS2 as a theorem (not visible; the instantiation mechanism makes instances of all theorems proven in Switch-IOAut-fwrefines-A (here: the instance switch(SEQ,FastLane) <= TMS2 of theorem switch(C1,C2) <= A) available in all superspecifications of the current one). The hard part here is getting all invariants right; once they are, proofs are not difficult.
The theorems of specification Instance-SEQFL-IMPL discharge the proof obligations for switch(switch(SEQ,FastLane),IMPL) <= TMS2. Since the implementation IMPL is not known, these can only be proven under assumptions on IMPL. These are collected as axioms in specification IMPL-assumptions. The comments in the specification give explanations for each assumption. For a concrete implementation these would have to be discharged as proof obligations.

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

[SEFM18]	G. Schellhorn, M. Wedel, O. Travkin, J. König, H. Wehrheim. Fastlane is Opaque - A Case Study in Mechanized Proofs of Opacity. (submitted to SEFM 2018)
[Wamhoff et al 2013]	G. J. Wamhoff, C. Fetzer, P. Felber, E. Riviere, G. Muller. Fastlane: improving performance of software transactional memory for low thread counts. (PPoPP, pp. 113-122, ACM)