Document Open Access Logo

Privatization-Safe Transactional Memories

Authors Artem Khyzha, Hagit Attiya, Alexey Gotsman

PDF
Thumbnail PDF

File

LIPIcs.DISC.2019.24.pdf
  • Filesize: 0.54 MB
  • 17 pages

Document Identifiers

Author Details

Artem Khyzha
  • Tel Aviv University, Tel Aviv, Israel
Hagit Attiya
  • Technion - Israel Institute of Technology, Haifa, Israel
Alexey Gotsman
  • IMDEA Software Institute, Madrid, Spain

Funding

This research was funded in part by the Israel Science Foundation (grants 2005/17, 1749/14 and 380/18) and the European Research Council (Starting Grant RACCOON).

Cite AsGet BibTex

Artem Khyzha, Hagit Attiya, and Alexey Gotsman. Privatization-Safe Transactional Memories. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.DISC.2019.24

Abstract

Transactional memory (TM) facilitates the development of concurrent applications by letting the programmer designate certain code blocks as atomic. Programmers using a TM often would like to access the same data both inside and outside transactions, and would prefer their programs to have a strongly atomic semantics, which allows transactions to be viewed as executing atomically with respect to non-transactional accesses. Since guaranteeing such semantics for arbitrary programs is prohibitively expensive, researchers have suggested guaranteeing it only for certain data-race free (DRF) programs, particularly those that follow the privatization idiom: from some point on, threads agree that a given object can be accessed non-transactionally. In this paper we show that a variant of Transactional DRF (TDRF) by Dalessandro et al. is appropriate for a class of privatization-safe TMs, which allow using privatization idioms. We prove that, if such a TM satisfies a condition we call privatization-safe opacity and a program using the TM is TDRF under strongly atomic semantics, then the program indeed has such semantics. We also present a method for proving privatization-safe opacity that reduces proving this generalization to proving the usual opacity, and apply the method to a TM based on two-phase locking and a privatization-safe version of TL2. Finally, we establish the inherent cost of privatization-safety: we prove that a TM cannot be progressive and have invisible reads if it guarantees strongly atomic semantics for TDRF programs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Program semantics
  • Software and its engineering → Software verification
Keywords
  • Transactional memory
  • privatization
  • observational refinement

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. ISO/IEC. Technical Specification for C++ Extensions for Transactional Memory, 19841:2015, 2015. Google Scholar
  2. ISO/IEC. Programming Languages - C++, 14882:2017, 2017. Google Scholar
  3. Martín Abadi, Andrew Birrell, Tim Harris, Johnson Hsieh, and Michael Isard. Implementation and Use of Transactional Memory with Dynamic Separation. In International Conference on Compiler Construction (CC), pages 63-77, 2009. Google Scholar
  4. Martín Abadi, Andrew Birrell, Tim Harris, and Michael Isard. Semantics of transactional memory and automatic mutual exclusion. ACM Trans. Program. Lang. Syst., 33:2:1-2:50, 2011. Google Scholar
  5. Martín Abadi, Tim Harris, and Katherine F. Moore. A Model of Dynamic Separation for Transactional Memory. In International Conference on Concurrency Theory (CONCUR), pages 6-20, 2008. URL: https://doi.org/10.1007/978-3-540-85361-9_5.
  6. Hagit Attiya, Alexey Gotsman, Sandeep Hans, and Noam Rinetzky. A programming language perspective on transactional memory consistency. In Symposium on Principles of Distributed Computing (PODC), pages 309-318, 2013. URL: https://doi.org/10.1145/2484239.2484267.
  7. Hagit Attiya and Eshcar Hillel. The Cost of Privatization in Software Transactional Memory. IEEE Transactions on Computers, 62(12):2531-2543, 2013. Google Scholar
  8. Colin Blundell, E. Christopher Lewis, and Milo M. K. Martin. Subtleties of Transactional Memory Atomicity Semantics. Computer Architecture Letters, 5(2), 2006. Google Scholar
  9. Nathan Chong, Tyler Sorensen, and John Wickerson. The semantics of transactions and weak memory in x86, Power, ARM, and C++. In Conference on Programming Language Design and Implementation (PLDI), pages 211-225, 2018. Google Scholar
  10. Luke Dalessandro and Michael L. Scott. Strong Isolation is a Weak Idea. In Workshop on Transactional Computing (TRANSACT), 2009. Google Scholar
  11. Luke Dalessandro, Michael L. Scott, and Michael F. Spear. Transactions as the Foundation of a Memory Consistency Model. In International Symposium on Distributed Computing (DISC), pages 20-34, 2010. Google Scholar
  12. Luke Dalessandro, Michael F. Spear, and Michael L. Scott. NOrec: streamlining STM by abolishing ownership records. In Symposium on Principles and Practice of Parallel Programming (PPOPP), pages 67-78, 2010. URL: https://doi.org/10.1145/1693453.1693464.
  13. Peter Damron, Alexandra Fedorova, Yossi Lev, Victor Luchangco, Mark Moir, and Daniel Nussbaum. Hybrid Transactional Memory. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 336-346, 2006. Google Scholar
  14. David Dice, Ori Shalev, and Nir Shavit. Transactional Locking II. In International Symposium on Distributed Computing (DISC), pages 194-208, 2006. URL: https://doi.org/10.1007/11864219_14.
  15. David Dice and Nir Shavit. TLRW: return of the read-write lock. In Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 284-293, 2010. URL: https://doi.org/10.1145/1810479.1810531.
  16. P. Felber, C. Fetzer, P. Marlier, and T. Riegel. Time-Based Software Transactional Memory. IEEE Transactions on Parallel and Distributed Systems, 21(12):1793-1807, 2010. Google Scholar
  17. Ivana Filipovic, Peter O'Hearn, Noam Rinetzky, and Hongseok Yang. Abstraction for concurrent objects. Theoretical Computer Science, 411(51-52):4379-4398, 2010. Google Scholar
  18. Free Software Foundation. Transactional Memory in GCC. URL: http://gcc.gnu.org/wiki/TransactionalMemory.
  19. Rachid Guerraoui, Thomas A. Henzinger, Michal Kapalka, and Vasu Singh. Transactions in the jungle. In Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 263-272, 2010. Google Scholar
  20. Rachid Guerraoui and Michal Kapalka. On the correctness of transactional memory. In Symposium on Principles and Practice of Parallel Programming (PPOPP), pages 175-184, 2008. Google Scholar
  21. Rachid Guerraoui and Michal Kapalka. Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2010. URL: https://doi.org/10.2200/S00253ED1V01Y201009DCT004.
  22. Maurice Herlihy, Victor Luchangco, and Mark Moir. Obstruction-Free Synchronization: Double-Ended Queues as an Example. In International Conference on Distributed Computing Systems (ICDCS), pages 522-529, 2003. Google Scholar
  23. Maurice Herlihy and J. Eliot B. Moss. Transactional Memory: Architectural Support for Lock-Free Data Structures. In International Symposium on Computer Architecture (ISCA), pages 289-300, 1993. URL: https://doi.org/10.1145/165123.165164.
  24. Intel Corporation. Intel architecture instruction set extensions programming reference. Chapter 8: Intel transactional synchronization extensions, 2012. Google Scholar
  25. Gokcen Kestor, Osman S. Unsal, Adrián Cristal, and Serdar Tasiran. T-Rex: a dynamic race detection tool for C/C++ transactional memory applications. In European Systems Conference (EuroSys), pages 20:1-20:12, 2014. Google Scholar
  26. Artem Khyzha, Hagit Attiya, and Alexey Gotsman. Privatization-Safe Transactional Memories (Extended Version). arXiv CoRR, 1908.03179, 2019. URL: http://arxiv.org/abs/1908.03179.
  27. Artem Khyzha, Hagit Attiya, Alexey Gotsman, and Noam Rinetzky. Safe privatization in transactional memory. In Symposium on Principles and Practice of Parallel Programming (PPoPP), pages pages 233-245, 2018. Extended version available at URL: https://arxiv.org/abs/1801.04249.
  28. Sanjeev Kumar, Michael Chu, Christopher J Hughes, Partha Kundu, and Anthony Nguyen. Hybrid transactional memory. In Symposium on Principles and Practice of Parallel Programming (PPOPP), pages 209-220, 2006. Google Scholar
  29. H. Q. Le, G. L. Guthrie, D. E. Williams, M. M. Michael, B. G. Frey, W. J. Starke, C. May, R. Odaira, and T. Nakaike. Transactional memory support in the IBM POWER8 processor. IBM Journal of Research and Development, 59(1):8:1-8:14, 2015. Google Scholar
  30. Mohsen Lesani, Victor Luchangco, and Mark Moir. Specifying Transactional Memories with Nontransactional Operations. In Workshop on the Theory of Transactional Memory (WTTM), 2013. Google Scholar
  31. Virendra J. Marathe, Michael F. Spear, and Michael L. Scott. Scalable Techniques for Transparent Privatization in Software Transactional Memory. In International Conference on Parallel Processing (ICPP), pages 67-74, 2008. Google Scholar
  32. Paul E. McKenney. Exploiting Deferred Destruction: An Analysis of Read-Copy-Update Techniques in Operating System Kernels. PhD thesis, OGI School of Science and Engineering at Oregon Health and Sciences University, 2004. Google Scholar
  33. Katherine F. Moore and Dan Grossman. High-level small-step operational semantics for transactions. In Symposium on Principles of Programming Languages (POPL), pages 51-62, 2008. URL: https://doi.org/10.1145/1328438.1328448.
  34. Nir Shavit and Dan Touitou. Software transactional memory. Distributed Computing, 10(2):99-116, 1997. Google Scholar
  35. Michael F. Spear, Virendra J. Marathe, Luke Dalessandro, and Michael L. Scott. Privatization techniques for software transactional memory. In Symposium on Principles of Distributed Computing (PODC), pages 338-339, 2007. Extended version appears as Technical Report 915, Computer Science Department, University of Rochester. Google Scholar
  36. Richard M. Yoo, Yang Ni, Adam Welc, Bratin Saha, Ali-Reza Adl-Tabatabai, and Hsien-Hsin S. Lee. Kicking the tires of software transactional memory: why the going gets tough. In Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 265-274, 2008. URL: https://doi.org/10.1145/1378533.1378582.
  37. Tingzhe Zhou, Pantea Zardoshti, and Michael F. Spear. Practical Experience with Transactional Lock Elision. In International Conference on Parallel Processing (ICPP), pages 81-90, 2017. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact