Advertisement
Published in:
2012 | OriginalPaper | Chapter
A Framework for Formally Verifying Software Transactional Memory Algorithms
Authors : Mohsen Lesani, Victor Luchangco, Mark Moir
Published in: CONCUR 2012 – Concurrency Theory
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.