Verifying Correctness of Transactional Memories

—We show how to verify the correctness of transactional memory implementations with a model checker. We show how to specify transactional memory in terms of the admissible interchange of transaction operations, and give proof rules for showing that an implementation satisfies this 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. We demonstrate our work using the TLC model checker to verify well-known implementations described abstractly in the TLA+ specification language.

• Type: Conference
• Year: 2007
• Where: FMCAD
• Authors: Ariel Cohen 0002, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck
• Keywords: Admissible Interchange, FMCAD 2007, Model Checker, Transactional Memory