Sciweavers

CAV
2010
Springer

Generating Litmus Tests for Contrasting Memory Consistency Models

14 years 4 months ago
Generating Litmus Tests for Contrasting Memory Consistency Models
Well-defined memory consistency models are necessary for writing correct parallel software. Developing and understanding formal specifications of hardware memory models is a challenge due to the subtle differences in allowed reorderings and different specification styles. To facilitate exploration of memory model specifications, we have developed a technique for systematically comparing hardware memory models specified using both operational and axiomatic styles. Given two specifications, our approach generates all possible multi-threaded programs up to a specified bound, and for each such program, checks if one of the models can lead to an observable behavior not possible in the other model. When the models differs, the tool finds a minimal “litmus test” program that demonstrates the difference. A number of optimizations reduce the number of programs that need to be examined. Our prototype implementation has successfully compared both axiomatic and operational specifi...
Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin
Comments (0)