A theory of memory models

ABSTRACT

A memory model for a concurrent imperative programming language specifies which writes to shared variables may be seen by reads performed by other threads. We present a simple mathematical framework for relaxed memory models for programming languages. To instantiate this framework for a specific language, the designer must choose the notion of atomic steps supported by the language (e.g. 32-bit reads and writes) and specify how a composite step may be broken into a sequence of atomic steps (the decomposition rule). This rule determines which sequence of intermediate writes (if any) are visible to concurrent reads by other threads. Different choices of the rule lead to models which permit a read to return any value if there is a concurrent write (race), or models which satisfy a "No Thin Air Read"property. The former is suitable for languages such as C++(programs with races have undefined behavior), and the latter for Java. Other intermediate models are possible, useful and interesting.

We establish that all models in the framework satisfy the Fundamental Property of relaxed memory models: programs whose sequentially consistent (SC) executions have no races must have have only SC executions. We show how to define synchronization constructs (such as volatiles of various kinds) in the framework, and discuss the causality test cases from the Java Memory Model.

REFERENCES

• 1: Arvind Arvind , Jan-Willem Maessen, Memory Model = Instruction Reordering + Store Atomicity, Proceedings of the 33rd annual international symposium on Computer Architecture, p.29-40, June 17-21, 2006
• 2: Hans-J. Boehm, Threads cannot be implemented as a library, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 3: Philippe Charles , Christian Grothoff , Vijay Saraswat , Christopher Donawa , Allan Kielstra , Kemal Ebcioglu , Christoph von Praun , Vivek Sarkar, X10: an object-oriented approach to non-uniform cluster computing, Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
• 4: Guang R. Gao , Vivek Sarkar, Location Consistency-A New Memory Model and Cache Consistency Protocol, IEEE Transactions on Computers, v.49 n.8, p.798-813, August 2000 [doi>10.1109/12.868026]
• 5: Kourosh Gharachorloo , Daniel Lenoski , James Laudon , Phillip Gibbons , Anoop Gupta , John Hennessy, Memory consistency and event ordering in scalable shared-memory multiprocessors, Proceedings of the 17th annual international symposium on Computer Architecture, p.15-26, May 28-31, 1990, Seattle, Washington, United States
• 6: James Gosling , Bill Joy , Guy Steele , Gilad Bracha, Java(TM) Language Specification, The (3rd Edition) (Java (Addison-Wesley)), Addison-Wesley Professional, 2005
• 7: J. Hoeflinger and B. de Supinsky. The OpenMP memory model. June 2005.
• 8: L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, 28(9), 1979.
• 9: D. Lea. Alternatives to SC. Message to C++ threads standardization list, Thu Jan 11 2007.
• 10: Jeremy Manson , William Pugh , Sarita V. Adve, The Java memory model, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.378-391, January 12-14, 2005, Long Beach, California, USA
• 11: Maged M. Michael , Michael L. Scott, Simple, fast, and practical non-blocking and blocking concurrent queue algorithms, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, p.267-275, May 23-26, 1996, Philadelphia, Pennsylvania, United States [doi>10.1145/248052.248106]
• 12: W. Pugh. Java Memory Model Causality Test Cases. Technical report, U Maryland, 2004. On www.cs.umd.edu, as~pugh/java/memoryModel/.
• 13: V. Saraswat. Concurrent Constraint-Based Memory Machines: A Framework for Java Memory Models. In ASIAN, pages 494--508, 2004.
• 14: Vijay Saraswat , Radha Jagadeesan, Concurrent clustered programming, Lecture Notes in Computer Science, Springer-Verlag, London, 2005 [doi>10.1007/11539452_28]
• 15: Dennis Shasha , Marc Snir, Efficient and correct execution of parallel programs that share memory, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.282-312, April 1988 [doi>10.1145/42190.42277]
• 16: Zehra Sura , Xing Fang , Chi-Leung Wong , Samuel P. Midkiff , Jaejin Lee , David Padua, Compiler techniques for high performance sequentially consistent java programs, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065947]
• 17: Jean Etienne Vuillemin, Proof-techniques for recursive programs., 1974
• 18: C. Wallace, G. Tremblay, and J. Amaral. The Tamability of the Location Consistency Memory Model, 2002.
• 19: K. Yelick, D. Bonachea, and C. Wallace. A Proposal for a UPC Memory Consistency Model, v1.1. Technical Report LBNL Technical Report (draft), 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

General Terms:
Languages, Theory

Keywords:
memory model, sequential consistency, weak model