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...

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin
• Keywords: CAV 2010, Hardware, Hardware Memory Models, Memory Consistency Models, Memory Model