Verification of Opacity of a Transactional Mutex Lock

Simulation proof that TML refines the TMS2 automaton with Isabelle

• Utilities.thy
• RWMemory.thy
• Transitions.thy
• Interface.thy
• TML.thy
• TMS2.thy
• TMLCorrect.thy

Proof that TML is opaque via Linearizability with KIV

• The project is based on KIV's library of data types. Several types of lists are used, where [] denotes the empty list, a ' is the one element list of a, and + is used to concatenate lists. # x is the length of x, and x[n] is its nth element (zero-based). x.first and x.rest are the first element, and the list without the first element, x.last and x.butlast are the last element resp. the list without the last.
• Free data types are defined using a notation similar to functional languages. A typical one is specification run events. It gives several cases for run events (separated by |). Each case gives a constructor first (here e.g. Write), and then in brackets selectors and types for its components. In the example Write(p,a,v) constructs a run event, when p, a, v are arguments of type Proc, address, int respectively. The given selectors are written postfix, so Write(p,a,v).p gives p. Optionally each case of the data type has a `with clause defining a predicate. Here, e.g. write?(Write(p,a,v)) is true, while write?(Begin(p)) is false. Special cases of data types are enumerations (e.g. program counters) and tuples (e.g. CState).
• Specification CState gives the states that the algorithms work on. The state is a tuple consisting of the global state, consisting of two values glb and mem, and local states for each process, given as functions from process ids (specification Proc defines process ids as an arbitrary parameter type) to values. The values are
  • glb, a counter (natural number)
  • mem, a memory specified as a function from L to V (where both L and V are parameter types).
    The empty memory, which maps all addresses to an unspecified constant O of type V is denoted as ∅.

  For each process the local state consists of

  • pc, a program counter of type PC. pc = N is used to denote a process that is not currently executing a transaction, pc = T means, the process is executing a transaction, but currently runs none of the algorithms.
  • loc, a local copy of the glb counter
  • a, an address and v, an integer value. These two are used to store an adress and a value as used in the TMRead and TMWrite algorithm.

• Specification LCOP gives the individual steps of the algorithms, which can be informally written as follows:

  TMBegin(None)
  B1 do loc := glb
  B2 while odd(loc)
  B3 return None
  

  TMRead(mkL(l))
  R1 v = mem(l)
  R2 if (glb = loc)
  R3    return mkV(v)
  R4 return Aborted
  

  TMWrite(mkLV(l,v))
  W1 if even(loc)
  W2    if ! CAS(glb, loc, loc +1)
  W3        return Aborted
  W4     else loc := loc + 1
  W5 mem(l) := v
  W6 return None
  

  TMEnd(None)
  E1 if odd(loc)
  E2    glb := glb+1
  E3 return None
  

  The individual steps of the algorithms are written as operations, which modify the global state mem and glb, and one local state (four values pc, loc, l, v). Primed values (glb' etc.) denote the values after the step. The individual steps are written as indexed operations. They fall into 3 categories.

  • Invoking steps INVOP. These start with pc = N (TMBegin) and with pc = T (the other three operations). They have an input, which for uniformity is chosen as one specific summand (as given in the pseudocode) from free datatype INPUT. (e.g. TMRead accepts only an input of the form mkL(l)). The input is copied (where necessary) to the local variables l and v.
  • Internal steps COP. They have neither inputs nor outputs.
  • Returning steps RETOP. These end with pc = N (TMEnd and aborts of TMRead and TWrite) or pc = T. They have an additional return value. Again for uniformity, the return value is always of type OUTPUT.
  Finally, the specification also gives criteria for initial local states (predicate LSInit) and initial global state (GSInit).

• Specification COP promotes the steps to steps INVOp, COp, RETOp which now work on the full state cs:CState plus an auxiliary variable r of type run.
  • The operations are now indexed with a process p, to indicate which process executes them, so the appropriate local state is modified.
  • A run is a list of run events.
  • Each run event is an abstract representation of a pair of events of an alternating history required for linearizability of operations (in linearizability, such a history is usually called sequential, but we use the term here for transaction-sequential histories only).
  • Since linearizability provides the illusion, that the algorithms can be viewed from the outside as if executing atomically, the events of the run can be viewed as the sequence of atomic executions: Begin(p) executes a TMBegin, Read(p,l,v) and Write(p,l,v) are successful executions of TMRead and TMWrite, Commit(p) is the (successful) execution of TMEnd. Finally Abort(p) denotes aborting executions of TMRead and TMWrite.
  • The promoted COp operation adds one run event at every linearization point (see the paper for code annotated with all LPs). E.g. when pcf(p) = W5 a run event Write(p, lf(p),vf(p)) is added, since W5 is the linearization point of TMWrite.
  • In the formulas, f(x;v) denotes function f modified at x to be v.
  • (p ⊃ v1;v2) is KIV's if-then-else operator: The value denoted is v1 if the test p holds, otherwise v2.
  • Over the specification a number of simple validation lemmas are proved. These show, that when one process executes alone, the operations (except TMBegin, when glb is odd) terminate.

• Specification transaction defines predicates that characterize transactions in a run.
  • All predicates use two natural numbers m and n to characterize the positions in a run r where a transaction begins and ends.
  • All transactions are required to begin with r[m] = Begin(p) (where r[m] is selection of an element from a list).
  • Committed transactions (predicate ctrans(m,n,p,r)) end with r[n] = Commit(p).
  • Aborted transactions (atrans) end with r[n] = Abort(p).
  • Together these are finished transactions (ftrans).
  • A transaction (trans) that is not finished is live (ltrans).
  • For a live transaction r[n] is required to be the last event of the run that is executed by p.
  • The ranges of transactions are required to be mininal, i.e. between positions m and n other Begin(p), Commit(p) or Abort(p) events are disallowed.
  • The specification also defines predicates ctr, atr, ftr, ltr, tr that existentially quantify over the process executing the transaction.
  • A run is wellformed (predicate wf) if every event is part of a transaction (implying e.g., that there is no Read(p) event in the run without a prior Begin(p) etc.).
  • Given, that trans(m,n,p,r) holds, the events of which this transaction consists are all events executed by p in the range from m to n. They are computed as runevs(m,n,r).
  • The definition of runevs uses m .. n to denote the pair of m and n with the idea of using it as a range. Selection of a range m .. n of elements from a list x is denoted as x[m .. n].
  • In the following a range m .. n that satisfies tr(m,n,r) will be viewed as being the transaction in r.

• To define opacity a run r must be reordered to a sequential run rs.
  • An important concept to do this elegantly (without resorting to complex permutation functions) are transaction sequences. For a run r a transaction sequence ts = [m0 .. n0, m1 .. n1, ... ,mk .. nk] is a list of pairs mi .. ni, such that the pairs are all transactions of r: Each pair satisfies tr(mi,ni,r), the list is duplicate free and contains all pairs m .. n that satisfy tr(m,n,r). This is what predicate transseq(r,ts) specifies.
  • A sequential run (called rs in the paper) can be computed from a transaction sequence ts by concatenating all runevs(mi,ni,r) (in that order!).
  • Two transactions m .. n and m0 .. n0 are in real-time order (<rt) iff the first transaction is finished and n < m0. A transaction sequence ts preserves real time order (predicate presrt), if in this case m .. n is earlier in the transaction sequence than m0 .. n0 (predicate pos(a,x) computes the position of element a in list x).
  • A sequence of memories (denoted as σ) is a proper semantics of a run r, denoted as 〚r〚(σ), if it fits to the semantics 〚re〚(mem, mem') of every run event re in the sequence.
  • Opacity (predicate opaque(r,ts)) requires that the sequential run rs (as encoded by the transaction sequence ts) preserves real-time order, and that every transaction (in rs, or equivalently, in ts) has correct semantics.
  • A transaction mi .. ni in ts has correct semantics if the sequential run consisting of the events of the committed transactions in the sequence tsi = [m0 .. n0 ... m(i-1) .. n(i-1)] (function firstn(i,ts) computes the subsequence, function cp(tsi, r) already defined in specification transaction removes the ones that are not committed) plus the events in the transaction mi .. ni itself admit a proper semantics (which starts with an empty memory).
  • Over the specification a few lemmas are proved. The most interesting ones are that the semantics is deterministic, and that starting a new transaction preserves opacity.
• Specification INV contains the main definitions and theorems that form the proof of opacity.
  • The proof first has to show that every operation properly linearizes once, and that the run properly records (an abstraction of the) alternating history (with the right input/output values). This is done by proving two lemmas for every operation, see here and here for TMBegin, here and here for TMRead, here and here for TMWrite, here and here for TMEnd. We explain the lemmas for TMWrite, the others are similar.
  • The first lemma shows, that any incomplete run of TMWrite will linearize at most once (note, that linearizability requires that even infinite runs do not linearize more than once, so the second lemma below is not sufficient). Formally: if pc(p) = T, an invoke of write is executed and then any sequence of operations, even of other processes (AnyOps), but no return operation of p, then the run events of process p at the end (r1 | p) at the end are either the same as at the start, or one Abort(p) event has been added, or a single Write(p,a,v) event has been added, where a and v were the inputs of the invoke. To make the lemma inductively provable, it is strengthened to state specific pc-values for which each case is possible. The lemma also states, that the case of an added Write(p,a,v) only occurs, when the pc is W6 and when the local values cs1.a(p) and cs1.v(p) at that point agrees with the inputs a and v. This implies that the write that occured in the last step from W5 to W6 has indeed updated memory correctly (since it uses cs1.a(p) and cs1.v(p)).
  • The second lemma shows, that any terminated run properly linearizes once: if after a run as in the first lemma a return happens, exactly one event of process p has been added to r, and the output is the correct result: If an Abort(p) was added to r then the algorithm returns Aborted. If a Write(p,a,v) was added then the output is None. Also the pc has been set correctly (after an abort it is N, so a new transaction must be started, otherwise it is T and the transaction can continue).
  • The second lemma is always easy to prove from the first, the first lemma requires a simple induction over the number of steps done.
  • Together the lemmas imply that the algorithms properly linearize to the abstract events recorded in the run.
  • The main proof now must show that the run r constructed can always be reordered to an opaque sequential run rs. This is done by proving that ∃ ts. INV(cs,r,ts) is an invariant of all the steps of all algorithms, where INV(cs,r,ts) trivially implies opaque(r,ts).
  • The invariant INV is a conjunction of several predicates, the first one strengthens the opaque predicate. The other auxiliary invariants describe the possible transaction sequences, that the algorithms may generate.
    • opaque+(r,ts,mem) strenghthens opaque(r,ts) by the additional requirement, that the last memory of the memory sequence needed for the proper semantics of the last transaction in ts is the current memory of the algorithm. This strengthening is necessary, such that an actual read of the algorithm, and the corresponding read/write events in the transaction sequence read from/write to the same memory.
    • predicate evenlocnowrites states, that transactions for which loc(p) is even have not performed any writes.
    • predicate oddlocatend states, that any live transaction with odd loc(p) is the last transaction, and loc(p) = glb. This implicitly implies that there is at most one live transaction with an odd value for loc(p).
    • predicate curlocnofinishedafter states, that a live transaction with loc(p) = glb is never ordered before a finished transaction in ts.
    • predicate livesortednolocs states, that live transactions are ordered (non-strictly) by their loc values.
    • predicate abortnowrites states, that aborted transactions contain no write operations.
  • Before proving the main invariant that implies opacity, a number of simpler invariants is proved first:
    • predicate LINV states some simple properties of the algorithms, that hold for one algorithm (with its one local state consisting of pc, loc, a and v) .e.g. that loc is always less or equal to glb, or that loc is even when pc = W4.
    • predicate D states a disjointness property for the pc and loc values of two processes: no two processes can ever store both an odd loc value, when actively using it (note that in TMBegin an odd loc value may be loaded, but it is then not used).
    • predicate GINV promotes these properties to an invariant of the full state.
    • That GINV is invariant in all steps of the algorithm is shown by proving six simple lemmas about LINV and D (two lemmas for invoking operations, here and here, two for internal operations here and here, and finally two for return operations here and here). From these we get three lemmas for GINV, here, here and here.
    • Knowing that GINV is invariant, we can then assume GINV as a precondition in a proof, that the operations preserve wellformedness of the run r. This proof uses an auxiliary invariant livenonidle, that states, that the run contains a live transaction for p iff the process p has a pc that indicates, that it is after the linearization point of TMBegin, but before the linearization point of TMEnd, and has not excuted the aborting linearization point of either TMRead (pc = R4) or TMWrite (pc = W3). Again the invariance proof is done separately for invoking, internal and returning operations.
  • The main proof for INV then already assumes GINV, wf, and livenonidle as preconditions. Most of the steps of the algorithm do not linearize. These steps do not change r, so there is no need to change the quantified transaction sequence either. The proof for these steps, as well as the ones for invoking and returning operations are trivial.
  • The difficult proofs are for the steps that modify r, and require to modify the transaction sequence. Several of the proofs require to first rotate the transaction sequence. That this is possible for two live transactions which both have the same even loc (so both have not done any writes) is proved as a lemma first. This implies (Lemma INV-switch-evenloc-to-minpos) that a specific live transaction can be moved to the minimal position with the same loc value in the transaction sequence.
  • The proofs for each of the linearization steps then are (if an auxiliary lemma is present this indicates that Lemma INV-switch-evenloc-to-minpos is used. In this case the auxiliary lemma is the main proof):
    • Theorem for pc=B1 when glb is even
    • Theorem for pc=R2 when glb is not loc(p) and the read aborts with auxiliary lemma.
    • Theorem for pc=R2 when glb is loc(p) and the read succeeds. This proof has two subcases. The case for odd loc(p) is proved directly, the case where loc(p) is even requires again an auxiliary lemma.
    • Theorem for pc=W2 when the write aborts with auxiliary lemma.
    • Theorem for pc=W4. This step is no linearization point, but loc becomes odd in this step so the transaction must be swapped to the last position of the transaction sequence.
    • Theorem for pc=W5.
    • Theorem for pc=E1 and even loc with auxiliary lemma.
    • Theorem for pc=E2.
  • All proofs except the one for B1 crucially rely on lemmas that say how properties change when another event re of a process p with a live transaction is attached to a run r (r' = r + re). Assuming the transaction sequence is not rotated this implies that the range m .. n for the live transaction of p in the transaction sequence must be replaced by m .. # r (since the new event re = r'[# r] is now the last one of the live transaction). Predicate transseq is preserved according to this lemma, and real-time order is preserved too according to this lemma. The most difficult lemma proved is that under certain preconditions semantics is preserved too.
  • Finally the individual proofs are collected together to prove that all of the invariants are indeed invariant in invoking, internal and returning operations. Since the invariant implies opacity, and trivially holds in all initial states, this finishes the opacity proof.

Simulation proof that TML refines the TMS2 automaton with KIV

The overview over the specification structure therefore shows a quite big development graph, but almost all of it is irrelevant for the proof of the case study. The only interesting specifications are the one of an IO Automaton as a pair of a start and a step predicate with the constraint, that the start states must not be empty, and the definition of a forward simulation ≤F(cioaut,aiout) between two IO Automata (which is proven to imply refinement).

The refinement theory is imported into the project of the case study. The overview over the specification structure shows the following main specifications:

• TML is now specified as the two predicates TMLstart and TMLastep (which form an IO Automaton).
  • The local transitions LOP from the linearizability approach above have been reused (which has not paid off; in retrospect it would have been somewhat shorter to define the steps directly, though this would not change the proofs).
  • The state of the TML automaton is the same as before, except that we added an auxiliary writer-component, which is either "Some(t)" if there is a writing transaction t with odd loc-value or "None". This change would have simplified linearizability proofs a bit too, since the need to talk via a quantifier about the "existing" writing transaction goes away.
  • The lifting to the full state is similar to the lineariability approach, instead of 'process identifiers' (Proc) we now have 'transactions identifiers' (T). While a process can execute several transactions, a transaction can only be executed once, so the program counter values now distinguish the start state (pc = S) from the committed (pc = C) and the aborted state (pc = A), instead of having pc = N for all three.
  • Instead of input/output we now have actions. Note that the standard refinement theory used forces us to use the same actions, and there is only one internal action "τ" (even though many steps of TML and also many of the steps of TMS2 (e.g. DoRead) are internal) . It would be nicer to have more flexibility in the theory, e.g. by allowing a mapping between actions that must be identity only for external ones. Since in the simulation we want to map steps of TML to a step of TMS2 (without a distinction on internal/external; an internal step of TML may be mapped to "τ") we use the full set of TMS2 actions in the definition of TMLstep. The actions DoRead, DoWrite are placed exactly at the linearization points used earlier. Only when defining the transitional relation TMLastep we abstract to the external invoke/response actions + "τ".
• The definition of the TMS2 automaton (with functions TMS2start, TMS2astep) uses the same construction as above to get from TMS2step to TMS2astep. Otherwise it follows the definitions of the forthcoming paper, but the parameters of internal actions have been found to be bad for our proof, so they have been dropped. Most of the parameters are redundant anyway, except that the parameter "n" of DoRead encodes a nondeterministic choice. For this reason DoRead has not been specified (like all other transitions) using a TMS2stepp predicate specifying the precondition, and a TMS2stepf function that describes the effect.
• The forward simulation F consists of two parts: A relation between the concrete memory "mem" and "memories.last", the last in the sequence of memories of TMS2, and a relation FW(t) between the two states (projected to the t-component) for every transaction t, predicate FW defines the following properties:
  • if there is a writer, then the writeset of TMS2 is subset of current memory of TML, and the loc value is odd, except when pc= W4.
  • A number of local invariants (copied over from the linearizability approach of TML),.e.g. that at pc = W2 the loc value must be even.
  • the pc value of TMS2 can be computed from the one of TML with function "abspc".
  • An even loc-value implies an empty writeset, except for pc = B1 and B2.
  • An odd loc-value implies loc=glb, except when pc is one of {B1, B2, E3, A, C}.
  • If the transaction is not (almost) finished (i.e. pc is not E3, A or C), then glb = loc (or the exceptional case pc = W4) implies that the readset is subset of memories.last. Otherwise, loc < glb and the readset is valid for memories[n] with beginIdx ≤ n (see the definition of ∃valid in TMS2).
• The main proof is first reduced (proving the simple initialization condition) to the main lemma, that verifies a commuting diagram for all actions except DoRead. Note that the lemma already uses the concrete actions, and that a concrete step is mapped to a single or no abstract action (if is an internal step), while the generic theory would allow any sequence of abstract steps with the correct external action. The lemma also exploits that steps of TMS2 (TMS2step) can be split into TMSstepp and TMSstepf. This avoids the quantifier for the post-state of the abstract step. A separate lemma is necessary for DoRead, where the quantifier over the post-state is still present and must be instantiated manually, depending on the case. This lemma is reduced similar to the others, but without defining the three sublemmas.
• The main lemma is then reduced to three sublemmas:
  • The first shows that the memory correspondence is preserved by each step.
  • The second shows that the simulation relation FW(t) is preserved by every step of t.
  • The third shows that the simulation relation FW(t0) is preserved by every step of t, when t and t0 are different transactions.
  Note that all three lemmas exploit, that we know, which instances of FW will be needed as precondition: All three sublemmas need the instance of the transaction t executing the step and the instance for the writing transaction (if there is one), the last lemmas also needs the one for t0. Compared to the linearizability approach, the lemmas are extremely easy to prove, as they involve almost no quantified definitions. The only exceptions are "∃valid" and "⊆", which need a few simplifierrules defined in here.

Update: KIV simulation proof with thread-local, step-local proof obligations

In recent work [ABZ23], we have further improved the support of KIV for (refinements of) IO Automata. KIV can now natively generate all required data structures and functions/predicates for defining an IOA from algorithms given in KIV's imperative programming language. Furthermore, invariants and refinements can now be proven using thread- and step-local proof obligations, reducing the verification effort significantly.

The project has been enhanced with the new automaton specifications and refinement proofs.

• The automaton of TMS2 is now generated from the definition of atomic invoke, do, and response actions in this specification.
• TML is generated from the non-atomic programs given in this specification.
• Local and global invariants are proven for TMS2 and TML using thread- and step-local proof obligations.
• Two variants for proving the refinement of TMS2 with TML were added:
  • By proving the standard (non-step-local) forward simulation conditions directly.
  • By proving the local refinement obligations and lifting these to the forward simulation conditions.

For more details on the alternative proof technique, see [ABZ23] and the web presentation of the associated case study.

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]