Proving opacity of transactional memory with early release

• Autorzy: Siek K. , Wojciechowski P. T.

Identyfikatory

DOI

10.1515/fcds-2015-0018

• Języki publikacji: EN

Abstrakty

EN

Transactional Memory (TM) is an alternative way of synchronizing concurrent accesses to shared memory by adopting the bstraction 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.

Słowa kluczowe

EN

Concurrency; Parallel Programming; Software Transactional Memory; safety; Early Release

• Wydawca: Wydawnictwo Politechniki Poznańskiej
• Czasopismo: Foundations of Computing and Decision Sciences
• Rocznik: 2015
• Tom: Vol. 40, No. 4
• Strony: 317--335
• Opis fizyczny: Bibliogr. 28 poz.

Twórcy

autor

Siek K.

autor

Wojciechowski P. T.

Bibliografia

• [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.
• [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.
• [7] Dziuma, D., Fatourou, P., and Kanellou, E. Consistency for transactional memory computing. Bulletin of the EATCS, 113, 2014.
• [8] Felber, P., Gramoli, V., and Guerraoui, R. Elastic Transactions. In Proc. DISC’09, Sept. 2009.
• [9] Guerraoui, R. and Kapałka, M. On the correctness of transactional memory. In Proc. PPoPP’08, Feb. 2008.
• [10] Guerraoui, R. and Kapałka, M. Principles of Transactional Memory. Morgan & Claypool, 2010.
• [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.
• [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.
• [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.
• [22] Shavit, N. and Touitou, D. Software Transactional Memory. In Proc. PODC’95, Aug. 1995.
• [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.