I am a...
I want to...
Sign In/Register for Account
External Research Office
A Framework for Formally Verifying Software Transactional Memory Algorithms. (May 2012)
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.
Mohsen Lesani, Victor Luchangco, Mark Moir
Oracle Labs on OTN
Want to try out some of the cool technology being built at Oracle Labs?
Email to a friend
Integrated Cloud Applications and Platform Services
Oracle RSS Feed