Title :
Verifying Correctness of Transactional Memories
Author :
Cohen, Ariel ; O´leary, John W. ; Pnueli, Amir ; Tuttle, Mark R. ; Zuck, Lenore D.
Abstract :
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 several well-known implementations described abstractly in the TLA+ specification language.
Keywords :
Computer integrated manufacturing; Data structures; Design automation; Hardware; Memory management; Multicore processing; Specification languages; System recovery; Transaction databases; Yarn; HTM; STM; TLA+; TLC.; Verification; model checking; transactional memory;
Conference_Titel :
Formal Methods in Computer Aided Design, 2007. FMCAD '07
Conference_Location :
Austin, TX, USA
Print_ISBN :
978-0-7695-3023-9
DOI :
10.1109/FAMCAD.2007.40