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 IO-Automata 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 bottom-up explanation of the KIV proof.