Verification of Opacity of a Transactional Mutex Lock
We have proved opacity of a transactional mutex lock
using two different approaches with the proof assistants KIV and Isabelle.
The first proof was based on linearizability and was done with KIV only.
The second approach proves IOAutomata refinement to the TMS2 automaton.
Earlier work [LLM12] shows this is sufficient to prove opacity.
The second approach was first proved using Isabelle, then independently a slightly
different proof was done with KIV.
A description of all proofs, and a comparison of the two methods will
appear in a forthcoming publication.
Simulation proof that TML refines the TMS2 automaton with Isabelle
The Isabelle proof can be found in the following files:
The main theorem, that TML is trace included in TMS2, is in
TMLCorrect.thy. TML.thy and TMS2.thy contain the TML and TMS2
automata, respectively. The files Transitions.thy and Interface.thy
provide tools for uniformly constructing automata that represent STM
implementations. The files Utilities.thy and RWMemory.thy define some
concepts that are shared between the other theories. A tarball
containing all files can be found
here.
Proof that TML is opaque via Linearizability with KIV
The KIV proofs are based on (and assume the reader is familiar with)
the explanations given in
[FM15].
They are almost identical to the ones given
here
for [FM15], except that the type of memory has been changed from 'address > int'
to 'L > V' (with typical values l and v) to be compatible with the definitions of
the new publication.
The
overview over the specification structure can be used to browse
through specifications, theorems and proofs.
Here is a bottomup explanation of the KIV proof.
 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 (zerobased).
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 transactionsequential 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 ifthenelse 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 realtime
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 realtime
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(i1) .. n(i1)]
(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 pcvalues 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 (nonstrictly) 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
INVswitchevenloctominpos)
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
INVswitchevenloctominpos is used. In this case the auxiliary lemma is the main proof):
 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 realtime 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 KIV proofs are based on a framework of IO Automata refinement theory.
This was originally created to compare to ASM refinement,
a new completeness result for ASM refinement that also gives a
completeness result for IO automata can be found
here.
The specifications were revised to have IOAutomata as specification
objects. A lot of the theory given in [LynVaa95] is mechanised in this framework,
and also some more results e.g. on normed simulations [GrifVaa98].
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 writercomponent, which is
either
"Some(t)" if there is a writing transaction t with odd locvalue 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 tcomponent)
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 locvalue implies an empty writeset, except for pc = B1 and B2.
 An odd locvalue 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 poststate of the abstract step.
A separate lemma
is
necessary for
DoRead, where the quantifier over the poststate 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 threadlocal, steplocal 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 steplocal 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 nonatomic programs given in
this specification.

Local and global invariants are proven for TMS2
and TML using thread
and steplocal proof obligations.

Two variants for proving the refinement of TMS2 with TML were added:
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
[FM15]

J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, H. Wehrheim.
Verifying Opacity of a Transactional Mutex Lock.
(FM 2015, Springer LNCS 9109, p. 161177)

[ABZ23] 
G. Schellhorn, S. Bodenmüller, W. Reif
ThreadLocal, StepLocal Proof Obligations for Refinement of StateBased Concurrent
Systems.
(submitted to ABZ 2023)

[LynVaa95] 
N. Lynch and F.W. Vaandrager
Forward and Backward Simulations  Part I: Untimed systems.
(Information and Computation 1995, vol. 121(2), p. 214233)

[LLM12] 
M. Lesani, V. Luchangco, M. Moir
Workshop on Transactional Memory.
(2012)

[GrifVaa98] 
W.O.D. Griffioen and F.W. Vaandrager
Normed Simulations.
(CAV 1998, Springer LNCS 1427, p. 332344)

[Imprint]
[Data Privacy Statement]
[EMail]