Analysis of Computer Systems Group

Department of Computer Science, New York University

Verifying Transactional Memory with TLPVS

Transactional memory is a programming abstraction intended to simplify the synchronization of conflicting memory accesses (by concurrent threads) without the difficulties associated with locks. In previous work we showed how to specify transactional memory in terms of the admissible interchange of transaction operations, and give proof rules for showing that an implementation satisfies such a specification. This notion of an admissible interchange is a key to our ability to use a model checker, and lets us capture the various notions of transaction conflict as characterized by Scott. However, automatic proofs according to the new proof rules is well beyond the capabilities of current model checking techniques, both in terms of the data structures needed and the nature of the proof rule itself. We propose to use TLPVS to overcome the difficulties and to produce a machine checkable, deductive proof for the correctness of implementations of transactional memory systems.

Download

A proof of LTM
(Last updated on June 14, 2008 – use framework v1.2):

ltm.pvs – specification and implementation of LTM;
ltm.prf – the proof (search for 'proof-of-abstraction');

A variation of TCC that supports non-transactional accesses
(Last updated on January 27, 2008 – use framework v1.1):

abs_tm_nontr.pvs – specification and implementation of Transactional Memory that supports non-transactional accesses;
abs_tm_nontr.prf – the proof (search for 'abstraction-complete-proof');

A proof of TCC
(Last updated on November 18, 2007 – use framework v1.1):

abs_tm_inter.pvs – specification and implementation of TCC;
abs_tm_inter.prf – the proof;

Formal Framework (v1.3):

tm.pvs – a framework for verifying transactional memory implementations (v1.1,v1.2);
SYSTEM.pvs – includes the rule ABS_REL (v1.1,v1.2);
SYSTEM.prf – the proof (v1.1,v1.2);
special_list.pvs – the non-standard list (v1.1,v1.2);
special_list.prf – the proof (v1.1);
queue.pvs – uses special_list to construct the queue if the specification (v1.1,v1.2);
event.pvs – defines events (v1.1,v1.2);
EPFS.pvs – defines observable parameterized fair systems (v1.1,v1.2);

Related Publications

Ariel Cohen, Amir Pnueli and Lenore Zuck. Mechanical verification of transactional memories with non-transactional memory accesses. To appear in CAV’08.
Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck. Verifying Correctness of Transactional Memories. In Proceedings of the 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 2007.

Links

   TLPVS – PVS implementation of a linear temporal logic verification system;

   PVS – A verification system;

   Transactional Memory Online – A resource for researchers and practitioners in Transactional Memory;

   ACSys – Formal Methods group (NYU);

LAST UPDATED: 8/1/2008
Maintained by Ariel Cohen (arielc at cs.nyu.edu)