Isabelle files for verification of a pessimistic STM algorithm

This page contains the Isabelle theory files that show refinement
between Matveev and Shavit's
pessimistic transactional
memory algorithm (MSPessTM) and
the TMS2 specification. Leveraging
Lesani et
al's results,
these proofs establish opacity of MSPessTM.

The tarball consists of the following:

Main files
TMS2.thy - contains the IOA specification of TMS2
MSPessTM.thy contains the I/O automata encoding of the
MSPessTM algorithm, invariants and supporting lemmas
MSPessTMCorrect.thy contains the simulation
relation and all associated proofs
proof

Supporting files
Transitions.thy and Interface.thy provide
tools for uniformly constructing automata that represent
STM implementations.

Utilities.thy and RWMemory.thy
define some concepts
that are shared between the other theories.

The proofs
require
Isabelle 2016.

If you encounter a problem loading Seq.thy,
please make sure imports is set to "../HOLCF". This is a
problem with the new Isabelle distribution.