Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Kongresse
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Veranstaltungskalender Awards MyNewsletter Firmensuche
Kunden Login
Über Einzelzugang informieren
Über Unternehmenszugang informieren
Referenzkunden
Heavy-Duty Engines 2025 | 18. + 19. November 2025

Nutzfahrzeuge | Land- und Baumaschinen | Marine

Nehmen Sie als Referent an der 20. Internationalen MTZ-Fachtagung für Erfahrungsaustausch zu Industrie- und Nfz-Motoren teil. Reichen Sie online einen Themenvorschlag ein!
Erweiterte Suche
Anmelden
nach oben
Programming and Computer Software
Erschienen in:

01.11.2021

A Survey of Programming Language Memory Models

verfasst von: E. Moiseenko, A. Podkopaev, D. Koznov

Erschienen in: Programming and Computer Software | Ausgabe 6/2021

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

A memory model defines the semantics of concurrent programs operating on a shared memory. The most well-known and intuitive memory model, sequential consistency, is too strong for modern languages as it forbids many outcomes observable on modern hardware as a result of compiler and CPU optimizations. This gave rise to so-called weak or relaxed memory models. In recent years dozens of (weak) memory models for programming languages were proposed making different compromises with respect to programmability and the optimization potential. The goal of this paper is to survey and classify these models as well as to provide practical recommendations for language and compiler designers regarding a choice of a memory model. To achieve this goal we picked over 2000 research items from Google Scholar with keywords “Relaxed Memory Models,” “Weak Memory Models,” and “Weak Memory Consistency.” Then, we narrowed down this list to 40 papers having as a contribution a programming language memory model. We divide these models to six main classes and analyze their properties and limitations. We conclude with a discussion on how a choice of a memory model is affected by desired features of a language and suggest several possible directions for future researh in the field of weak memory models.
Vorheriger Artikel A Fast Search Algorithm for SqueeSAR Distributed Scatterers in the Problem of Calculating Displacement Velocities
Nächster Artikel Multiwindow Rendering on a Cockpit Display Using Hardware Acceleration

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
We distinguish shared variables (denoted as x, y, z) and thread local registers (denoted as r1, r2, r3, …).
 
2
From here and through the rest of the paper we assume that all variables are initialized with zeros, unless we explicitly state otherwise
 
3
This claim is supported by our data acquired from Google Scholar, see sec:methodology for details
 
7
All search queries were performed on 24 September 2020
 
8
Throughout the rest of paper, we use terms memory address and memory location interchangeably
 
9
We use terms load/stores and reads/writes interchangeably
 
10
Some architectures also provide various types of load and stores matching the access modes annotations, lda — load acquire, and stl — store release on Armv8.
 
11
On MOV instruction is used as both plain load from memory and plain store to memory instructions.
 
Literatur
1.
Dijkstra, E.W., Cooperating sequential processes, in The Origin of Concurrent Programming, Springer, 1968, pp. 65–138.
2.
Lamport, L., How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Trans. Comput., 1979, vol. 28, no. 9, pp. 690–691.CrossRef
3.
Manson, J., Pugh, W., and Adve, S.V., The Java memory model, Conference Record of the Annual ACM Symposium on Principles of Programming Languages, Jan. 12–14, 2005, pp. 378–391.
4.
Bender, J. and Palsberg, J., A formalization of Java’s concurrent access modes, Proc. ACM Program. Lang., 2019, vol. 3, no. OOPSLA, pp. 1–28.
5.
Batty, M., Owens, S., Sarkar, S., Sewell, P., and Weber, T., Mathematizing C++ concurrency, Proc. POPL’2011, Jan. 26–28, 2011, pp. 55–66.
6.
Chakraborty, S. and Vafeiadis, V., Formalizing the concurrency semantics of an LLVM fragment, Proc. IEEE/ACM Int. Symp. on Code Generation and Optimization (CGO), Feb. 4–8, 2017, pp. 100–110.
7.
Watt, C., Pulte, C., Podkopaev, A., Barbier, G., Dolan, S., Flur, S., Pichon-Pharabod, J., and Guo, S.-Y., Repairing and mechanising the JavaScript relaxed memory model, in Proc. 41st ACM SIGPLAN Conf. on Programming Language Design and Implementation, New York: Association for Computing Machinery, 2020, pp. 346–361.
8.
Vollmer, M., Scott, R.G., Musuvathi, M., and Newton, R.R., SC-Haskell: sequential consistency in languages that minimize mutable shared heap, ACM SIGPLAN Not., 2017, vol. 52, no. 8, pp. 283–298.CrossRef
9.
Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., and Myreen, M.O., x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors, Commun. ACM, 2010, vol. 53, no. 7, pp. 89–97.CrossRef
10.
Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., and Nardelli, F.Z., The semantics of power and ARM multiprocessor machine code, Proc. 4th Workshop on Declarative Aspects of Multicore Programming, 2009, pp. 13–24.
11.
Sarkar, S., Sewell, P., Alglave, J., Maranget, L., and Williams, D., Understanding POWER multiprocessors, Proc. 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI’11, 2011, pp. 175–186.
12.
Alglave, J., Maranget, L., and Tautschnig, M., Herding cats: modelling, simulation, testing, and data mining for weak memory, ACM Trans. Program. Lang. Syst., 2014, vol. 36, no. 2, pp. 7:1–7:74.
13.
Chong, N. and Ishtiaq, S., Reasoning about the ARM weakly consistent memory model, Proc. ACM SIGPLAN Workshop on Memory Systems Performance and Correctness: Held in Conjunction with the 13th Int. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS’08), Seattle, 2008, pp. 16–19.
14.
Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., and Sewell, P., Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8, Proc. ACM Program. Lang., 2018, vol. 2, no. POPL, pp. 1–29.
15.
Flur, S., Gray, K.E., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W., and Sewell, P., Modelling the ARMv8 architecture, operationally: concurrency and ISA, ACM SIGPLAN Not., 2016, vol. 51, no. 1, pp. 608–621.CrossRef
16.
Boehm, H.-J. and Demsky, B., Outlawing ghosts: avoiding out-of-thin-air results, Proc. Workshop on Memory Systems Performance and Correctness MSPC’14, Edinburgh, 2014, pp. 7:1–7:6.
17.
Kang, J., Hur, C.-K., Lahav, O., Vafeiadis, V., and Dreyer, D., A promising semantics for relaxed-memory concurrency, Proc. 44th ACM SIGPLAN Symp. on Principles of Programming Languages POPL 2017, Paris, 2017.
18.
Lee, S.-H., Cho, M., Podkopaev, A., Chakraborty, S., Hur, C.-K., Lahav, O., and Vafeiadis, V., Promising 2.0: global optimizations in relaxed memory concurrency, Proc. 41st ACM SIGPLAN Conf. on Programming Language Design and Implementation, 2020, pp. 362–376.
19.
Chakraborty, S. and Vafeiadis, V., Grounding thin-air reads with event structures, Proc. ACM Program. Lang., 2019, vol. 3, no. POPL, pp. 1–28.
20.
Paviotti, M., Cooksey, S., Paradis, A., Wright, D., Owens, S., and Batty, M., Modular relaxed dependencies in weak memory concurrency, in Proc. European Symp. on Programming, Cham: Springer, 2020, pp. 599–625.
21.
Lahav, O., Vafeiadis, V., Kang, J., Hur, C.-K., and Dreyer, D., Repairing sequential consistency in C/C++11, Proc. 38th ACM SIGPLAN Conf. on Programming Language Design and Implementation PLDI 2017, Barcelona, 2017.
22.
Dolan, S., Sivaramakrishnan, K., and Madhavapeddy, A., Bounding data races in space and time, ACM SIGPLAN Not., 2018, vol. 53, no. 4, pp. 242–255.CrossRef
23.
Ou, P. and Demsky, B., Towards understanding the costs of avoiding out-of-thin-air results, Proc. ACM Program. Lang., 2018, vol. 2, no. OOPSLA, pp. 1–29.
24.
Jeffrey, A. andRiely, J., On thin air reads: towards an event structures model of relaxed memory, Proc. 31st Annu. ACM/IEEE Symp. on Logic in Computer Science LICS’16, New York, 2016.
25.
Pichon-Pharabod, J. and Sewell, P., A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions, ACM SIGPLAN Not., 2016, vol. 51, no. 1, pp. 622–633.CrossRef
26.
Marlow, S., et al., Haskell 2010 language report, 2010. https://​www.​ haskell.org/onlinereport/haskell2010.
27.
Klabnik, S. and Nichols, C., The Rust Programming Language (Covers Rust 2018), No Starch Press, 2019.
28.
Boehm, H.-J. and Adve, S.V., Foundations of the C++ concurrency memory model, ACM SIGPLAN Not., 2008, vol. 43, no. 6, pp. 68–78.CrossRef
29.
Lahav, O., Giannarakis, N., and Vafeiadis, V., Taming release-acquire consistency, ACM SIGPLAN Not., 2016, vol. 51, no. 1, pp. 649–662.CrossRef
30.
Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K.E., Sezgin, A., Batty, M., and Sewell, P., Mixed-size concurrency: ARM, Power, C/C++ 11, and SC, ACM SIGPLAN Not., 2017, vol. 52, no. 1, pp. 429–442.CrossRef
31.
C/C++11 mappings to processors, 2011. https://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html. Accessed Apr. 26, 2021.
32.
Marino, D., Singh, A., Millstein, T., Musuvathi, M., and Narayanasamy, S., A case for an SC-preserving compiler, ACM SIGPLAN Not., 2011, vol. 46, no. 6, pp. 199–210.CrossRef
33.
Liu, L., Millstein, T., and Musuvathi, M., A volatile-by-default JVM for server applications, Proc. ACM Program. Lang., 2017, vol. 1, no. OOPSLA, pp. 1–25.
34.
Muchnick, S., Advanced Compiler Design and Implementation, Morgan Kaufmann, 1997.
35.
Lahav, O., Namakonov, E., Oberhauser, J., Podkopaev, A., and Vafeiadis, V., Making weak memory models fair, 2020. arXiv:2012.01067.
36.
Ševčík, J. and Aspinall, D., On validity of program transformations in the Java memory model, in Proc. European Conf. on Object-Oriented Programming, Springer, 2008, pp. 27–51.
37.
Wegman, M.N. and Zadeck, F.K., Constant propagation with conditional branches, ACM Trans. Program. Lang. Syst., 1991, vol. 13, no. 2, pp. 181–210.CrossRef
38.
Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., and Sewell, P., The problem of programming language concurrency semantics, in Proc. European Symp. on Programming Languages and Systems ESOP 2015, Springer, 2015, pp. 283–307.
39.
Maranget, L., Sarkar, S., and Sewell, P., A tutorial introduction to the ARM and POWER relaxed memory models, 2012. https://​www.​cl.​cam.​ac.​uk/​~pes20/​ppc-supplemental/​test7.​pdf.​ Accessed Apr. 30, 2021.
40.
Boudol, G. and Petri, G., A theory of speculative computation, in Proc. European Symp. on Programming, Springer, 2010, pp. 165–184.
41.
Singh, A., Narayanasamy, S., Marino, D., Millstein, T., and Musuvathi, M., End-toend sequential consistency, Proc. 39th IEEE Annu. Int. Symp. on Computer Architecture (ISCA), Portland, 2012, pp. 524–535.
42.
Liu, L., Millstein, T., and Musuvathi, M., Accelerating sequential consistency for Java with speculative compilation, Proc. 40th ACM SIGPLAN Conf. on Programming Language Design and Implementation, 2019, pp. 16–30.
43.
Marino, D., Singh, A., Millstein, T., Musuvathi, M., and Narayanasamy, S., DRFx: a simple and efficient memory model for concurrent programming languages, Proc. 31st ACM SIGPLAN Conf. on Programming Language Design and Implementation, Toronto, 2010, pp. 351–362.
44.
Demange, D., Laporte, V., Zhao, L., Jagannathan, S., Pichardie, D., and Vitek, J., Plan B: a buffered memory model for Java, Proc. 40th Annu. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Rome, 2013, pp. 329–342.
45.
Boudol, G. and Petri, G., Relaxed memory models: an operational approach, ACM SIGPLAN Not., 2009, vol. 44, no. 1, pp. 392–403.CrossRef
46.
Dodds, M., Batty, M., and Gotsman, A., Compositional verification of compiler optimisations on relaxed memory, in Proc. European Symp. on Programming, Springer, 2018, pp. 1027–1055.
47.
Doherty, S., Dongol, B., Wehrheim, H., and Derrick, J., Verifying C11 programs operationally, Proc. 24th Symp. on Principles and Practice of Parallel Programming, Washington, 2019, pp. 355–365.
48.
Dang, H.-H., Jourdan, J.-H., Kaiser, J.-O., and Dreyer, D., RustBelt meets relaxed memory, Proc. ACM Program. Lang., 2020, vol. 4, no. POPL, art. no. 34, pp. 1–29.
49.
Alglave, J., Maranget, L., McKenney, P.E., Parri, A., and Stern, A., Frightening small children and disconcerting grownups: concurrency in the Linux kernel, Proc. 23rd Int. Conf. on Architectural Support for Programming Languages and Operating Systems, 2018, pp. 405–418.
50.
Zhang, Y. and Feng, X., An operational happens-before memory model, Front. Comput. Sci., 2016, vol. 10, no. 1, pp. 54–81.CrossRef
51.
Huisman, M. and Petri, G., The Java memory model: a formal explanation, Proc. Workshop on Verification and Analysis of Multi-Threaded Java-Like Programs VAMP’07, Lisbon, 2007, vol. 7, pp. 81–96.
52.
Jagadeesan, R., Pitcher, C., and Riely, J., Generative operational semantics for relaxed memory models, in Proc. European Symp. on Programming, Springer, 2010, pp. 307–326.
53.
Sarkar, S., Memarian, K., Owens, S., Batty, M., Sewell, P., Maranget, L., Alglave, J., and Williams, D., Synchronising C/C++ and POWER, Proc. 33rd ACM SIGPLAN Conf. on Programming Language Design and Implementation, Beijing, 2012, pp. 311–322.
54.
Batty, M., Memarian, K., Owens, S., Sarkar, S., and Sewell, P., Clarifying and compiling C/C++ concurrency: from C++ 11 to POWER, ACM SIGPLAN Not., 2012, vol. 47, no. 1, pp. 509–520.CrossRef
55.
Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., and Nardelli, F.Z., Common compiler optimisations are invalid in the C11 memory model and what we can do about it, Proc. 42nd Ann. ACM SIGPLAN-SIGACT Symp. on Principles of Programming POPL’15, Mumbai, 2015, pp. 209–220.
56.
Batty, M., Donaldson, A.F., and Wickerson, J., Overhauling SC atomics in C11 and OpenCL, Proc. 43rd Annu. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, St. Petersburg, FL, 2016, pp. 634–648.
57.
Nienhuis, K., Memarian, K., and Sewell, P., An operational semantics for C/C++ 11 concurrency, Proc. ACM SIGPLAN Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications, Amsterdam, 2016, pp. 111–128.
58.
Crary, K. and Sullivan, M.J., A calculus for relaxed memory, Proc. 42nd Annu. ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Mumbai, 2015, pp. 623–636.
59.
Saraswat, V.A., Jagadeesan, R., Michael, M., andvon Praun, C., A theory of memory models, Proc. 12th ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming, San Jose, 2007, pp. 161–172.
60.
Inc, S.I. and Weaver, D.L., The SPARC Architecture Manual, Prentice-Hall, 1994.
61.
Lustig, D., Trippel, C., Pellauer, M., and Martonosi, M., ArMOR: defending against memory consistency model mismatches in heterogeneous architectures, Proc. 42nd Annu. Int. Symp. on Computer Architecture, Portland, 2015, pp. 388–400.
62.
Podkopaev, A., Lahav, O., and Vafeiadis, V., Bridging the gap between programming languages and hardware weak memory models, Proc. ACM Program. Lang., 2019, vol. 3, no. POPL, pp. 1–31.
63.
Pugh, W., Fixing the Java memory model, Proc. ACM Conf. on Java Grande, San Francisco, 1999, pp. 89–98.
64.
Diwan, A., McKinley, K.S., and Moss, J.E.B., Type-based alias analysis, ACM SIGPLAN Not., 1998, vol. 33, no. 5, pp. 106–117.CrossRef
65.
Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., and Vafeiadis, V., A separation logic for a promising semantics, in Programming Languages and Systems, Ahmed, A., Ed., Cham: Springer Int. Publ., 2018, pp. 357–384.
66.
Choi, J.-D., Gupta, M., Serrano, M., Sreedhar, V.C., and Midkiff, S., Escape analysis for Java, ACM SIGPLAN Not., 1999, vol. 34, no. 10, pp. 1–19.CrossRef
67.
Jagadeesan, R., Jeffrey, A., and Riely, J., Pomsets with preconditions: a simple model of relaxed memory, Proc. ACM Program. Lang., 2020, vol. 4, no. OOPSLA, art. no. 194, pp. 1–30.
68.
Cho, M., Lee, S.-H., Hur, C.-K., and Lahav, O., Modular data-race-freedom guarantees in the promising semantics, Proc. 42st ACM SIGPLAN Conf. on Programming Language Design and Implementation, 2021.
Metadaten
Titel
A Survey of Programming Language Memory Models
verfasst von
E. Moiseenko
A. Podkopaev
D. Koznov
Publikationsdatum
01.11.2021
Verlag
Pleiades Publishing
Erschienen in
Programming and Computer Software / Ausgabe 6/2021
Print ISSN: 0361-7688
Elektronische ISSN: 1608-3261
DOI
https://doi.org/10.1134/S0361768821060050

Weitere Artikel der Ausgabe 6/2021

Searching for Taint Vulnerabilities with Svace Static Analysis Tool

A Fast Search Algorithm for SqueeSAR Distributed Scatterers in the Problem of Calculating Displacement Velocities

Multiwindow Rendering on a Cockpit Display Using Hardware Acceleration

Controlling and Restoring the Integrity of Multi-Dimensional Data Arrays through Cryptocode Constructs

Premium Partner

    Bildnachweise