Model checking transactional memories

ABSTRACT

Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memory. We show that, under certain conditions, the verification problem can be reduced to a finite-state problem, and we illustrate the use of the method by proving the correctness of several STMs, including two-phase locking, DSTM, TL2, and optimistic concurrency control. The safety properties we consider include strict serializability and opacity; the liveness properties include obstruction freedom, livelock freedom, and wait freedom.

Our main contribution lies in the structure of the proofs, which are largely automated and not restricted to the STMs mentioned above. In a first step we show that every STM that enjoys certain structural properties either violates a safety or liveness requirement on some program with two threads and two shared variables, or satisfies the requirement on all programs. In the second step we use a model checker to prove the requirement for the STM applied to a most general program with two threads and two variables. In the safety case, the model checker constructs a simulation relation between two carefully constructed finite-state transition systems, one representing the given STM applied to a most general program, and the other representing a most liberal safe STM applied to the same program. In the liveness case, the model checker analyzes fairness conditions on the given STM transition system.

REFERENCES

• 1: James H. Anderson , Yong-Jik Kim , Ted Herman, Shared-memory mutual exclusion: major research trends since 1986, Distributed Computing, v.16 n.2-3, p.75-110, September 2003 [doi>10.1007/s00446-003-0088-6]
• 2: Rajeev Alur , Ken McMillan , Doron Peled, Model-checking of correctness conditions for concurrent objects, Information and Computation, v.160 n.1-2, p.167-188, July 10/Aug. 1, 2000 [doi>10.1006/inco.1999.2847]
• 3: Sebastian Burckhardt , Rajeev Alur , Milo M. K. Martin, CheckFence: checking consistency of concurrent data types on relaxed memory models, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 4: M. C. Browne , E. M. Clarke , O. Grumberg, Reasoning about networks with many identical finite state processes, Information and Computation, v.81 n.1, p.13-31, April 1989 [doi>10.1016/0890-5401(89)90026-6]
• 5: Jerry R. Burch , David L. Dill, Automatic verification of Pipelined Microprocessor Control, Proceedings of the 6th International Conference on Computer Aided Verification, p.68-80, June 21-23, 1994
• 6: 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]
• 7: D. Dice, O. Shalev, and N. Shavit. Transactional locking II. In International Symposium on Distributed Computing (DISC), pages 194--208. Springer, 2006.
• 8: K. P. Eswaran , J. N. Gray , R. A. Lorie , I. L. Traiger, The notions of consistency and predicate locks in a database system, Communications of the ACM, v.19 n.11, p.624-633, Nov. 1976 [doi>10.1145/360363.360369]
• 9: Keir Fraser , Tim Harris, Concurrent programming without locks, ACM Transactions on Computer Systems (TOCS), v.25 n.2, p.5-es, May 2007 [doi>10.1145/1233307.1233309]
• 10: M. Flé and G. Roucairol. Maximal serializability of iterated transactions. Theoretical Computer Science, pages 1--16, 1985.
• 11: Rachid Guerraoui , Michal Kapalka, On the correctness of transactional memory, Proceedings of the 13th ACM SIGPLAN Symposium on Principles and practice of parallel programming, February 20-23, 2008, Salt Lake City, UT, USA [doi>10.1145/1345206.1345233]
• 12: G. Gopalakrishnan, Y. Yang, and H. Sivaraj. QB or Not QB: An efficient execution verification tool for memory orderings. In International Conference on Computer Aided Verification (CAV), pages 401--413. Springer, 2004.
• 13: Maurice Herlihy, Wait-free synchronization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.1, p.124-149, Jan. 1991 [doi>10.1145/114005.102808]
• 14: M. R. Henzinger , T. A. Henzinger , P. W. Kopke, Computing simulations on finite and infinite graphs, Proceedings of the 36th Annual Symposium on Foundations of Computer Science (FOCS'95), p.453, October 23-25, 1995
• 15: Maurice Herlihy , Victor Luchangco , Mark Moir, Obstruction-Free Synchronization: Double-Ended Queues as an Example, Proceedings of the 23rd International Conference on Distributed Computing Systems, p.522, May 19-22, 2003
• 16: Maurice Herlihy , Victor Luchangco , Mark Moir , William N. Scherer, III, Software transactional memory for dynamic-sized data structures, Proceedings of the twenty-second annual symposium on Principles of distributed computing, p.92-101, July 13-16, 2003, Boston, Massachusetts [doi>10.1145/872035.872048]
• 17: Maurice Herlihy , J. Eliot B. Moss, Transactional memory: architectural support for lock-free data structures, Proceedings of the 20th annual international symposium on Computer architecture, p.289-300, May 16-19, 1993, San Diego, California, United States
• 18: Thomas A. Henzinger , Shaz Qadeer , Sriram K. Rajamani, Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems, Proceedings of the 11th International Conference on Computer Aided Verification, p.301-315, July 06-10, 1999
• 19: H. T. Kung , John T. Robinson, On optimistic methods for concurrency control, ACM Transactions on Database Systems (TODS), v.6 n.2, p.213-226, June 1981 [doi>10.1145/319566.319567]
• 20: Jim Larus , Ravi Rajwar, Transactional Memory (Synthesis Lectures on Computer Architecture), Morgan & Claypool Publishers, 2007
• 21: R. Milner. An algebraic definition of simulation between programs. In International Joint Conference on Artificial Intelligence (IJCAI), pages 481--489. William Kaufmann, 1971.
• 22: Christos H. Papadimitriou, The serializability of concurrent database updates, Journal of the ACM (JACM), v.26 n.4, p.631-653, Oct. 1979 [doi>10.1145/322154.322158]
• 23: Shaz Qadeer, Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking, IEEE Transactions on Parallel and Distributed Systems, v.14 n.8, p.730-741, August 2003 [doi>10.1109/TPDS.2003.1225053]
• 24: M. L. Scott. Sequential specification of transactional memory semantics. In ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT), 2006.
• 25: William N. Scherer, III , Michael L. Scott, Advanced contention management for dynamic software transactional memory, Proceedings of the twenty-fourth annual ACM symposium on Principles of distributed computing, July 17-20, 2005, Las Vegas, NV, USA [doi>10.1145/1073814.1073861]
• 26: Nir Shavit , Dan Touitou, Software transactional memory, Proceedings of the fourteenth annual ACM symposium on Principles of distributed computing, p.204-213, August 20-23, 1995, Ottowa, Ontario, Canada [doi>10.1145/224964.224987]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Languages, Verification

Keywords:
model checking, transactional memories