Cited By
View all- Svyatlovskiy MMermelstein SLahav O(2024)Compositional Semantics for Shared-Variable ConcurrencyProceedings of the ACM on Programming Languages10.1145/36563998:PLDI(543-566)Online publication date: 20-Jun-2024
Memory Consistency Models for Program Transformations: An Intellectual Abstract
Pages 30 - 42
Abstract
Memory consistency models traditionally specify the behavior of shared memory concurrent hardware. Hardware behavior drifts away from traditional sequential reasoning, thus exhibiting behaviors that are termed as "weak". Weaker consistency models allow for more concurrent behaviors, thus justifying hardware optimizations such as read/write buffers. In parallel, weaker memory models for software allow more compiler optimizations (transformations). However, this "more" may not be strict: certain safe optimizations in stronger models are rendered unsafe in ones weaker than them. We identify properties that must hold among a pair of weak and strong memory models to guarantee this. We propose a framework using which we could build such models, showcasing our results in allowing Read Read reordering over Sequential Consistency (SC). We also show how to partially retain our desired property for a pair of models, placing constraints on the set of transformations or equivalently, on program structure. Lastly, we discuss the potential advantage of designing models satisfying such properties.
Supplementary Material
Appendix for full proofs of the paper.
- Download
- 445.63 KB
References
[1]
Sarita V. Adve and Kourosh Gharachorloo. 1996. Shared Memory Consistency Models: A Tutorial. Computer, 29, 12 (1996), 66–76. https://doi.org/10.1109/2.546611
[2]
Alfred Aho, Monica, Ravi Sethi, and Jeffrey Ullman. 1986. Compilers: Principles, Techniques and Tools.
[3]
Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, and Michael Tautschnig. 2011. Soundness of Data Flow Analyses for Weak Memory Models. In Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings, Hongseok Yang (Ed.) (Lecture Notes in Computer Science, Vol. 7078). Springer, 272–288. https://doi.org/10.1007/978-3-642-25318-8_21
[4]
Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst., 36, 2 (2014), 7:1–7:74. https://doi.org/10.1145/2627752
[5]
Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Jan Vitek (Ed.) (Lecture Notes in Computer Science, Vol. 9032). Springer, 283–307. https://doi.org/10.1007/978-3-662-46669-8_12
[6]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, Thomas Ball and Mooly Sagiv (Eds.). ACM, 55–66. https://doi.org/10.1145/1926385.1926394
[7]
cppreference. 2022. Memory Consistency. https://en.cppreference.com/w/cpp/language/memory_model
[8]
java. 2022. Memory Consistency Model. https://docs.oracle.com/javase/specs/jls/se17/html/jls-17.html##jls-17.4
[9]
Ori Lahav and Viktor Vafeiadis. 2016. Explaining Relaxed Memory Models with Program Transformations. In FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings, John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.) (Lecture Notes in Computer Science, Vol. 9995). 479–495. https://doi.org/10.1007/978-3-319-48989-6_29
[10]
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing sequential consistency in C/C++11. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, Albert Cohen and Martin T. Vechev (Eds.). ACM, 618–632. https://doi.org/10.1145/3062341.3062352
[11]
Leslie Lamport. 1997. How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor. IEEE Trans. Computers, 46, 7 (1997), 779–782. https://doi.org/10.1109/12.599898
[12]
Jeremy Manson, William W. Pugh, and Sarita V. Adve. 2005. The Java memory model. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, Jens Palsberg and Martín Abadi (Eds.). ACM, 378–391. https://doi.org/10.1145/1040305.1040336
[13]
Evgenii Moiseenko, Anton Podkopaev, and Dmitrij V. Koznov. 2021. A Survey of Programming Language Memory Models. Program. Comput. Softw., 47, 6 (2021), 439–456. https://doi.org/10.1134/S0361768821060050
[14]
Robin Morisset, Pankaj Pawan, and Francesco Zappa Nardelli. 2013. Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 187–196. https://doi.org/10.1145/2491956.2491967
[15]
Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A Better x86 Memory Model: x86-TSO. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.) (Lecture Notes in Computer Science, Vol. 5674). Springer, 391–407. https://doi.org/10.1007/978-3-642-03359-9_27
[16]
Marco Paviotti, Simon Cooksey, Anouk Paradis, Daniel Wright, Scott Owens, and Mark Batty. 2020. Modular Relaxed Dependencies in Weak Memory Concurrency. In Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Peter Müller (Ed.) (Lecture Notes in Computer Science, Vol. 12075). Springer, 599–625. https://doi.org/10.1007/978-3-030-44914-8_22
[17]
William W. Pugh. 1999. Fixing the Java Memory Model. In Proceedings of the ACM 1999 Conference on Java Grande, JAVA ’99, San Francisco, CA, USA, June 12-14, 1999, Geoffrey C. Fox, Klaus E. Schauser, and Marc Snir (Eds.). ACM, 89–98. https://doi.org/10.1145/304065.304106
[18]
Jaroslav Ševcík and David Aspinall. 2008. On Validity of Program Transformations in the Java Memory Model. In ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings, Jan Vitek (Ed.) (Lecture Notes in Computer Science, Vol. 5142). Springer, 27–51. https://doi.org/10.1007/978-3-540-70592-5_3
[19]
Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. 2015. Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 209–220. https://doi.org/10.1145/2676726.2676995
Index Terms
- Memory Consistency Models for Program Transformations: An Intellectual Abstract
Recommendations
Litmus tests for comparing memory consistency models: how long do they need to be?
DAC '11: Proceedings of the 48th Design Automation ConferenceMemory consistency litmus tests are small parallel programs that are designed to illustrate subtle differences between memory consistency models by exhibiting different outcomes for different models. In this paper, we show that for a class of memory ...
Location Consistency-A New Memory Model and Cache Consistency Protocol
Existing memory models and cache consistency protocols assume the memory coherence property which requires that all processors observe the same ordering of write operations to the same location. In this paper, we address the problem of defining a memory ...
Virtual world consistency: A condition for STM systems (with a versatile protocol with invisible read operations)
The aim of a Software Transactional Memory (STM) is to discharge the programmers from the management of synchronization in multiprocess programs that access concurrent objects. To that end, an STM system provides the programmer with the concept of a ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2023
175 pages
ISBN:9798400701795
DOI:10.1145/3591195
- General Chair:
- Stephen M. Blackburn,
- Program Chair:
- Erez Petrank
Copyright © 2023 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 06 June 2023
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- NSERC COHESA Strategic Networks
- Mitacs
- EPSRC UK grant
Conference
ISMM '23
Sponsor:
ISMM '23: 2023 ACM SIGPLAN International Symposium on Memory Management
June 18, 2023
FL, Orlando, USA
Acceptance Rates
Overall Acceptance Rate 72 of 156 submissions, 46%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 106Total Downloads
- Downloads (Last 12 months)40
- Downloads (Last 6 weeks)3
Reflects downloads up to 09 Jan 2025
Other Metrics
Citations
Cited By
View all- Svyatlovskiy MMermelstein SLahav O(2024)Compositional Semantics for Shared-Variable ConcurrencyProceedings of the ACM on Programming Languages10.1145/36563998:PLDI(543-566)Online publication date: 20-Jun-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in