DocumentCode :
2372097
Title :
Verifying Correctness of Transactional Memories
Author :
Cohen, Ariel ; O´leary, John W. ; Pnueli, Amir ; Tuttle, Mark R. ; Zuck, Lenore D.
fYear :
2007
fDate :
11-14 Nov. 2007
Firstpage :
37
Lastpage :
44
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Formal Methods in Computer Aided Design, 2007. FMCAD '07
Conference_Location :
Austin, TX, USA
Print_ISBN :
978-0-7695-3023-9
Type :
conf
DOI :
10.1109/FAMCAD.2007.40
Filename :
4401980
Link To Document :
بازگشت