The semantics of progress in lock-based transactional memory

ABSTRACT

Transactional memory (TM) is a promising paradigm for concurrent programming. Whereas the number of TM implementations is growing, however, little research has been conducted to precisely define TM semantics, especially their progress guarantees. This paper is the first to formally define the progress semantics of lockbased TMs, which are considered the most effective in practice.

We use our semantics to reduce the problems of reasoning about the correctness and computability power of lock-based TMs to those of simple try-lock objects. More specifically, we prove that checking the progress of any set of transactions accessing an arbitrarily large set of shared variables can be reduced to verifying a simple property of each individual (logical) try-lock used by those transactions. We use this theorem to determine the correctness of state-of-the-art lock-based TMs and highlight various configuration ambiguities. We also prove that lock-based TMs have consensus number 2. This means that, on the one hand, a lock-based TM cannot be implemented using only read-write memory, but, on the other hand, it does not need very powerful instructions such as the commonly used compare-and-swap.

We finally use our semantics to formally capture an inherent trade-off in the performance of lock-based TM implementations. Namely, we show that the space complexity of every lock-based software TM implementation that uses invisible reads is at least exponential in the number of objects accessible to transactions.

REFERENCES

• 1: Martín Abadi , Andrew Birrell , Tim Harris , Michael Isard, Semantics of transactional memory and automatic mutual exclusion, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 2: 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
• 3: Milo Martin , Colin Blundell , E. Lewis, Subtleties of Transactional Memory Atomicity Semantics, IEEE Computer Architecture Letters, v.5 n.2, p.17, July 2006 [doi>10.1109/L-CA.2006.18]
• 4: Dave Dice, Ori Shalev, and Nir Shavit. Transactional locking II. In Proceedings of the 20th International Symposium on Distributed Computing (DISC), 2006.
• 5: Robert Ennals. Software transactional memory should not be obstruction-free. Technical Report IRC-TR-06-052, Intel Research Cambridge Tech Report, Jan 2006.
• 6: 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]
• 7: Pascal Felber , Christof Fetzer , Torvald Riegel, Dynamic performance tuning of word-based software 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.1345241]
• 8: 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]
• 9: Rachid Guerraoui and Michał Kapałka. The semantics of progress in lock-based transactional memory. Technical Report LPD-REPORT-2008-015, EPFL, October 2008.
• 10: Rachid Guerraoui , Michal Kapalka, On obstruction-free transactions, Proceedings of the twentieth annual symposium on Parallelism in algorithms and architectures, June 14-16, 2008, Munich, Germany [doi>10.1145/1378533.1378587]
• 11: Rachid Guerraoui , Thomas A. Henzinger , Barbara Jobstmann , Vasu Singh, Model checking transactional memories, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 12: Vassos Hadzilacos, A theory of reliability in database systems, Journal of the ACM (JACM), v.35 n.1, p.121-145, Jan. 1988 [doi>10.1145/42267.42272]
• 13: Tim Harris , Mark Plesko , Avraham Shinnar , David Tarditi, Optimizing memory transactions, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 14: 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]
• 15: 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
• 16: Maurice P. Herlihy , Jeannette M. Wing, Linearizability: a correctness condition for concurrent objects, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.3, p.463-492, July 1990 [doi>10.1145/78969.78972]
• 17: Suresh Jagannathan , Jan Vitek , Adam Welc , Antony Hosking, A transactional object calculus, Science of Computer Programming, v.57 n.2, p.164-186, August 2005 [doi>10.1016/j.scico.2005.03.001]
• 18: Prasad Jayanti, Adaptive and efficient abortable mutual exclusion, Proceedings of the twenty-second annual symposium on Principles of distributed computing, p.295-304, July 13-16, 2003, Boston, Massachusetts [doi>10.1145/872035.872079]
• 19: Leslie Lamport, The mutual exclusion problem: partII—statement and solutions, Journal of the ACM (JACM), v.33 n.2, p.327-348, April 1986 [doi>10.1145/5383.5385]
• 20: Leslie Lamport. On interprocess communication-part II: Algorithms. Distributed Computing, 1 (2), 1986.
• 21: Virendra J. Marathe, Michael F. Spear, Christopher Heriot, Athul Acharya, David Eisenstat, William N. Scherer III, and Michael L. Scott. Lowering the overhead of software transactional memory. In 1st ACM SIGPLAN Workshop on Transactional Computing (TRANSACT), Jun 2006.
• 22: Vijay Menon , Steven Balensiefer , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Richard L. Hudson , Bratin Saha , Adam Welc, Practical weak-atomicity semantics for java stm, Proceedings of the twentieth annual symposium on Parallelism in algorithms and architectures, June 14-16, 2008, Munich, Germany [doi>10.1145/1378533.1378588]
• 23: Katherine F. Moore , Dan Grossman, High-level small-step operational semantics for transactions, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 24: 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]
• 25: M. Raynal , D. Beeson, Algorithms for mutual exclusion, MIT Press, Cambridge, MA, 1986
• 26: Michael L. Scott. Sequential specification of transactional memory semantics. In 1st ACM SIGPLAN Workshop on Transactional Computing (TRANSACT), 2006.
• 27: Michael L. Scott , William N. Scherer, Scalable queue-based spin locks with timeout, Proceedings of the eighth ACM SIGPLAN symposium on Principles and practices of parallel programming, p.44-52, June 2001, Snowbird, Utah, United States
• 28: Jan Vitek, Suresh Jagannathan, Adam Welc, and Antony Hosking. A semantic framework for designer transactions. In Proceedings of the European Symposium on Programming (ESOP), March 2004.

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems

General Terms:
Algorithms, Theory, Verification

Keywords:
consensus number, impossibility, lock, lower bound, reduction, semantics, transactional memory, try-lock