2012 | OriginalPaper | Buchkapitel
A Framework for Formally Verifying Software Transactional Memory Algorithms
verfasst von : Mohsen Lesani, Victor Luchangco, Mark Moir
Erschienen in: CONCUR 2012 – Concurrency Theory
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.