Parameterized verification of transactional memories

ABSTRACT

We describe an automatic verification method to check whether transactional memories ensure strict serializability a key property assumed of the transactional interface. Our main contribution is a technique for effectively verifying parameterized systems. The technique merges ideas from parameterized hardware and protocol verification--verification by invisible invariants and symmetry reduction--with ideas from software verification--template-based invariant generation and satisfiability checking for quantified formulæ (modulo theories). The combination enables us to precisely model and analyze unbounded systems while taming state explosion.

Our technique enables automated proofs that two-phase locking (TPL), dynamic software transactional memory (DSTM), and transactional locking II (TL2) systems ensure strict serializability. The verification is challenging since the systems are unbounded in several dimensions: the number and length of concurrently executing transactions, and the size of the shared memory they access, have no finite limit. In contrast, state-of-the-art software model checking tools such as BLAST and TVLA are unable to validate either system, due to inherent expressiveness limitations or state explosion.

References

1. K. R. Apt and D. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22 (6): 307--309, 1986.
2. T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, pages 221--234, 2001.
3. T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, pages 1--3, 2002.
4. J. Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam, and S. Sagiv. Thread quantification for concurrent shape analysis. In CAV, pages 399--413, 2008.
5. D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Invariant synthesis for combined theories. In VMCAI, pages 378--394, 2007.
6. A. Cohen, J. W. O'Leary, A. Pnueli, M. R. Tuttle, and L. D. Zuck. Verifying correctness of transactional memories. In FMCAD, pages 37--44, 2007.
7. A. Cohen, A. Pnueli, and L. D. Zuck. Mechanical verification of transactional memories with non-transactional memory accesses. In CAV, pages 121--134, 2008.
8. S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In CAV, pages 420--432, 2003.
9. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337--340, 2008.
10. D. Dice, O. Shalev, and N. Shavit. Transactional locking II. In DISC, pages 194--208, 2006.
11. D. L. Dill, A. J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation preorders. In CAV, pages 255--265, 1991.
12. R. Guerraouić, and M. Kapalka. Dividing transactional memories by zero. In TRANSACT, 2008.
13. B. Dutertre and L. de Moura. The YICES SMT solver. http://yices.csl.sri.com.
14. M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69 (1--3): 35--45, 2007.
15. R. Guerraoui, T. A. Henzinger, B. Jobstmann, and V. Singh. Model checking transactional memories. In PLDI, pages 372--382, 2008.
16. R. Guerraoui, T. A. Henzinger, and V. Singh. Completeness and nondeterminism in model checking transactional memories. In CONCUR, pages 21--35, 2008.
17. R. Guerraoui, T. A. Henzinger, and V. Singh. Software transactional memory on relaxed memory models. In CAV, pages 321--336, 2009.
18. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pages 58--70, 2002.
19. M. Herlihy and J. E. B. Moss. Transactional memory: Architectural support for lock-free data structures. In ISCA, pages 289--300, 1993.
20. M. Herlihy, V. Luchangco, M. Moir, and W. N. S. III. Software transactional memory for dynamic-sized data structures. In PODC, pages 92--101, 2003.
21. S. Kleene. Introduction to Metamathematics. North Holland, 1980.
22. L. Lamport. Specifying concurrent program modules. ACM Trans. Program. Lang. Syst., 5 (2): 190--222, 1983.
23. J. R. Larus and R. Rajwar. Transactional Memory. Morgan & Claypool Publishers, 2006.
24. T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In SAS, pages 280--301, 2000.
25. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
26. K. L. McMillan. Verification of infinite state systems by compositional model checking. In CHARME, pages 219--234, 1999.
27. C. H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26 (4): 631--653, 1979.
28. A. Pnueli, S. Ruah, and L. D. Zuck. Automatic deductive verification with invisible invariants. In TACAS, pages 82--97, 2001.
29. J. Reineke. Shape analysis of sets. Master's thesis, Universität des Saarlandes, Germany, June 2005.
30. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002.
31. S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24 (3): 217--298, 2002.
32. S. Srivastava and S. Gulwani. Program verification using templates over predicate abstraction. In PLDI, pages 223--234, 2009.
33. S. Tasiran. A compositional method for verifying software transactional memory implementations. Technical Report MSR-TR-2008-56, Microsoft Research, April 2008.
34. C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda, and P. Wischnewski. SPASS version 3.5. In CADE, pages 140--145, 2009.
35. H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. W. O'Hearn. Scalable shape analysis for systems code. In CAV, pages 385--398, 2008.
36. K. Zee, V. Kuncak, and M. C. Rinard. Full functional verification of linked data structures. In PLDI, pages 349--361, 2008.

Index Terms

• Computing methodologies

  • Concurrent computing methodologies

    • Concurrent programming languages

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language types

        • Concurrent programming languages

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification