Towards Formally Specifying and Verifying Transactional Memory

We describe ongoing work in which we aim to formally specify a correctness condition for transactional memory (TM) called Weakest Reasonable Condition (WRC), and to facilitate fully formal and machine-checked proofs that TM implementations satisfy the condition. To precisely define the WRC condition, we express it using an I/O automaton. We similarly present another condition, called PRAG, which is more restrictive, but more closely reflects intuition about common TM implementation techniques. We sketch a simulation proof that PRAG implements WRC, allowing ourselves and others to focus more pragmatically on proofs of such implementations. We are working on modeling these conditions in the PVS language so that we can construct and check such proofs precisely and mechanically. We are also working towards proving that some popular TM implementations satisfy the PRAG condition, starting with simple coarse-grained versions and refining them to model realistic implementations.