Isabelle files for a verification of pessimistic STM algorithm

Authors: Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn and Heike Wehrheim

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.

Download the theory files here. The tarball consists of the following:

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.

[Imprint] [Data Privacy Statement] [E-Mail]