A Framework for Formally Verifying Software Transactional Memory Algorithms


Mohsen Lesani, Victor Luchangco, Mark Moir


We present a framework for verifying transactional memory (TM) algorithms. Specifications and algorithms are specified using I/O automata, enabling hierarchical proofs that the algorithms implement the specifications. We have used this framework to develop what we believe is the first fully formal machine-checked verification of a practical TM algorithm: the NOrec algorithm of Dalessandro, Spear and Scott. Our framework is available for others to use and extend. New proofs can leverage existing ones, eliminating significant work and complexity.


[Getting Started Tutorial]
[PVS Framework]