Model checking transactional memory with spin

ABSTRACT

We used the Spin model checker to show that Intel's implementation of software transactional memory is correct, and built a preprocessor to accelerate the performance of Spin on parameterized models of shared-memory protocols.

REFERENCES

• 1: Ali-Reza Adl-Tabatabai , Brian T. Lewis , Vijay Menon , Brian R. Murphy , Bratin Saha , Tatiana Shpeisman, Compiler and runtime support for efficient software transactional memory, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 2: Rajeev Alur , Ken McMillan , Doron Peled, Model-checking of correctness conditions for concurrent objects, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.219, July 27-30, 1996
• 3: Ariel Cohen , John W. O'Leary , Amir Pnueli , Mark R. Tuttle , Lenore D. Zuck, Verifying Correctness of Transactional Memories, Proceedings of the Formal Methods in Computer Aided Design, p.37-44, November 11-14, 2007 [doi>10.1109/FMCAD.2007.39]
• 4: Gerard Holzmann, Spin model checker, the: primer and reference manual, Addison-Wesley Professional, 2003

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Design, Verification

Keywords:
model checking, spin, transactional memory