nach oben

Tipp

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

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

We distinguish shared variables (denoted as x, y, z) and thread local registers (denoted as r₁, r₂, r₃, …).

From here and through the rest of the paper we assume that all variables are initialized with zeros, unless we explicitly state otherwise

This claim is supported by our data acquired from Google Scholar, see sec:methodology for details

https://kotlinlang.org/

https://riscv.org/

https://scholar.google.com/

All search queries were performed on 24 September 2020

Throughout the rest of paper, we use terms memory address and memory location interchangeably

We use terms load/stores and reads/writes interchangeably

Some architectures also provide various types of load and stores matching the access modes annotations, lda — load acquire, and stl — store release on Armv8.

On MOV instruction is used as both plain load from memory and plain store to memory instructions.

https://kotlinlang.org/

Dijkstra, E.W., Cooperating sequential processes, in The Origin of Concurrent Programming, Springer, 1968, pp. 65–138.

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

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.

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.

Batty, M., Owens, S., Sarkar, S., Sewell, P., and Weber, T., Mathematizing C++ concurrency, Proc. POPL’2011, Jan. 26–28, 2011, pp. 55–66.

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.

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.

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

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.

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

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

A Survey of Programming Language Memory Models

Abstract

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

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Premium Partner

Springer Professional

Tipp

Weitere Artikel dieser Ausgabe durch Wischen aufrufen

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Technik"

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 6/2021

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

Searching for Taint Vulnerabilities with Svace Static Analysis Tool

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

Multiwindow Rendering on a Cockpit Display Using Hardware Acceleration

Premium Partner