×

Proving opacity of transactional memory with early release. (English) Zbl 1328.68034

Summary: Transactional Memory (TM) is an alternative way of synchronizing concurrent accesses to shared memory by adopting the abstraction of transactions in place of low-level mechanisms like locks and barriers. TMs usually apply optimistic concurrency control to provide a universal and easy-to-use method of maintaining correctness. However, this approach performs a high number of aborts in high contention workloads, which can adversely affect performance. Optimistic TMs can cause problems when transactions contain irrevocable operations. Hence, pessimistic TMs were proposed to solve some of these problems. However, an important way of achieving efficiency in pessimistic TMs is to use early release. On the other hand, early release is seemingly at odds with opacity, the gold standard of TM safety properties, which does not allow transactions to make their state visible until they commit. In this paper we propose a proof technique that makes it possible to demonstrate that a TM with early release can be opaque as long as it prevents inconsistent views.

MSC:

68M14 Distributed systems
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

Software:

AtomCaml; SAMOA
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Afek, Y., Morrison, A., and Tzafrir, M. Brief announcement: View Transactions: Transactional Model with Relaxed Consistency Checks. In Proc. PODC’10, 2010.;
[2] Attiya, H., Gotsman, A., Hans, S., and Rinetzky, N. A programming language perspective on transactional memory consistency. In Proc. PODC’13, 2013.; · Zbl 1323.68061
[3] Bernstein, P. A., Hadzilacos, V., and Goodman, N. Concurrency control and recovery in database systems. Addison-Wesley, 1987.;
[4] Bieniusa, A., Middelkoop, A., and Thiemann, P. Brief announcement: actions in the twilight-concurrent irrevocable transactions and inconsistency repair. In PODC ’10, 2010.;
[5] Dice, D., Shalev, O., and Shavit, N. Transactional Locking II. In Proc. DISC’06, 2006.;
[6] Doherty, S., Groves, L., Luchangco, V., and Moir, M. Towards formally specifying and verifying transactional memory. Formal Aspects of Computing, 25, Sept. 2013.; · Zbl 1298.68168
[7] Dziuma, D., Fatourou, P., and Kanellou, E. Consistency for transactional memory computing. Bulletin of the EATCS, 113, 2014.; · Zbl 1409.68070
[8] Felber, P., Gramoli, V., and Guerraoui, R. Elastic Transactions. In Proc. DISC’09, Sept. 2009.; · Zbl 1261.68024
[9] Guerraoui, R. and Kapałka, M. On the correctness of transactional memory. In Proc. PPoPP’08, Feb. 2008.; · Zbl 1315.68065
[10] Guerraoui, R. and Kapałka, M. Principles of Transactional Memory. Morgan & Claypool, 2010.; · Zbl 1242.68056
[11] Harris, T. and Fraser, K. Language Support for Lightweight Transactions. In Proc. OOPSLA’03, Oct. 2003.;
[12] Harris, T., Marlow, S., Peyton Jones, S., and Herlihy, M. Composable memory transactions. In Proc. PPoPP’05, June 2005.;
[13] He, J., Hoare, C. A. R., and Sanders, J. W. Data refinement refined. In Proc. ESOP’86, 1986.; · Zbl 0587.68018
[14] Herlihy, M., Luchangco, V., Moir, M., and William N. Scherer, I. Software transactional memory for dynamic-sized data structures. In Proc. PODC’03, 2003.;
[15] Herlihy, M. and Moss, J. E. B. Transactional memory: Architectural support for lock-free data structures. In Proc. ISCA’93, May 1993.;
[16] Imbs, D., de Mendivil, J. R., and Raynal, M. On the Consistency Conditions or Transactional Memories. Technical report, Dec. 2008.;
[17] Lesani, M. and Palsberg, J. Decomposing opacity. In Proc. DISC’14, Oct. 2014.;
[18] Ni, Y., Welc, A., Adl-Tabatabai, A.-R., Bach, M., Berkowits, S., Cownie, J., Geva, R., Kozhukow, S., Narayanaswamy, R., Olivier, J., Preis, S., Saha, B., Tal, A., and Tian, X. Design and implementation of transactional constructs for C/C++. In Proc. OOPSLA’08, 2008.;
[19] Papadimitrou, C. H. The Serializability of Concurrent Database Updates. Journal of the ACM, 26(4):631-653, 1979.; · Zbl 0419.68036
[20] Ramadan, H. E., Roy, I., Herlihy, M., and Witchel, E. Committing Conflicting Transactions in an STM. In Proc. PPoPP’09, Feb. 2009.;
[21] Ringenburg, M. F. and Grossman, D. AtomCaml: first-class atomicity via rollback. In Proc. ICFP’05, Sept. 2005.; · Zbl 1302.68052
[22] Shavit, N. and Touitou, D. Software Transactional Memory. In Proc. PODC’95, Aug. 1995.; · Zbl 1373.68178
[23] Siek, K. and Wojciechowski, P. T. Atomic RMI: a Distributed Transactional Memory Framework. In Proc. HLPP’14, July 2014.;
[24] Siek, K. and Wojciechowski, P. T. Brief announcement: Relaxing opacity in pessimistic transactional memory. In Proc. DISC’14, 2014.;
[25] Siek, K. and Wojciechowski, P. T. Zen and the Art of Concurrency Control: An Exploration of TM Safety Property Space with Early Release in Mind. In Proc. WTTM’14, July 2014.;
[26] Siek, K. and Wojciechowski, P. T. Atomic RMI: A Distributed Transactional Memory Framework. International Journal of Parallel Programming, 2015.;
[27] Wojciechowski, P. T. Isolation-only Transactions by Typing and Versioning. In Proc. PPDP’05, July 2005.;
[28] Wojciechowski, P. T., Rütti, O., and Schiper, A. SAMOA: A Framework for a Synchronisation-Augmented Microprotocol Approach. In Proc. IPDPS’04, Apr. 2004.;
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.