zbMATH — the first resource for mathematics

An operational happens-before memory model. (English) Zbl 1403.68028
Summary: Happens-before memory model (HMM) is used as the basis of Java memory model (JMM). Although HMM itself is simple, some complex axioms have to be introduced in JMM to prevent the causality loop, which causes absurd out-of-thin-air reads that may break the type safety and security guarantee of Java. The resulting JMM is complex and difficult to understand. It also has many anti-intuitive behaviors, as demonstrated by the “ugly examples” by D. Aspinall and J. Ševčík [“Java memory model examples: good, bad and ugly”, in: Proceedings of 1st international workshop on verification and analysis of multi-threaded Java-like programs, VAMP 2007, Lisbon, Portugal, September 3, 2007. 66–80 (2007), https://pdfs.semanticscholar.org/96d1/831972f10f5cda5f77944ff591073a203e9e.pdf]. Furthermore, HMM (and JMM) specifies only what execution traces are acceptable, but says nothing about how these traces are generated. This gap makes it difficult for static reasoning about programs. In this paper we present OHMM, an operational variation of HMM. The model is specified by giving an operational semantics to a language running on an abstract machine designed to simulate HMM. Thanks to its generative nature, the model naturally prevents out-of-thin-air reads. On the other hand, it uses a novel replay mechanism to allow instructions to be executed multiple times, which can be used to modelmany useful speculations and optimization. The model is weaker than JMM for lockless programs, thus can accommodate more optimization, such as the reordering of independent memory accesses that is not valid in JMM. Program behaviors are more natural in this model than in JMM, and many of the anti-intuitive examples in JMM are no longer valid here. We hope OHMM can serve as the basis for new memory models for Java-like languages.

68N15 Theory of programming languages
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI
[1] Aspinall, D.; Ševčík, J., Java memory model examples: good, bad and ugly., 66-80, (2007)
[2] Lamport, L., How to make a multiprocessor computer that correctly executes multiprocess programs., IEEE Transactions on Computers, 28, 690-691, (1979) · Zbl 0419.68045
[3] Boehm, H. J., Threads cannot be implemented as a library., 261-268, (2005)
[4] Adve, S. V.; Gharachorloo, K., Shared memory consistency models: a tutorial., IEEE Transactions on Computers, 29, 66-76, (1996)
[5] Manson, J.; Pugh, W.; Adve, S. V., The Java memory model., 378-391, (2005) · Zbl 1369.68079
[6] Cenciarelli, P.; Knapp, A.; Sibilio, E., The Java memory model: operationally, denotationally, axiomatically., 331-346, (2007) · Zbl 1187.68114
[7] Zhang, Y.; Feng, X., An operational approach to happens-before memory model., 121-128, (2013)
[8] Lamport, L., Time, clocks, and the ordering of events in a distributed system., Communications of the ACM, 21, 558-565, (1978) · Zbl 0378.68027
[9] Aspinall, D.; Ševčík, J., Formalising Java’s data race free guarantee., 22-37, (2007) · Zbl 1144.68304
[10] Huisman, M.; Petri, G., The Java memory model: a formal explanation., 81-96, (2007)
[11] Manson J. The Java Memory Model. Dissertation for the Doctoral Degree. College Park: University of Maryland, 2004
[12] Ševčík, J.; Aspinall, D., On validity of program transformations in the Java memory model., 27-51, (2008)
[13] Vafeiadis, V.; Balabonski, T.; Chakraborty, S.; Morisset, R.; Nardelli, F. Z., Common compiler optimisations are invalid in the C11 memory model and what we can do about it., 209-220, (2015) · Zbl 1345.68087
[14] Yang, Y.; Gopalakrishnan, G.; Lindstrom, G., Specifying Java thread semantics using a uniform memory model., 192-201, (2002)
[15] Lochbihler, A., Java and the Java memory model — a unified, machinechecked formalisation., 497-517, (2012) · Zbl 1352.68034
[16] Saraswat, V. A.; Jagadeesan, R.; Michael, M. M.; Praun, V. C., A theory of memory models., 161-172, (2007)
[17] Jagadeesan, R.; Pitcher, C.; Riely, J., Generative operational semantics for relaxed memory models., 307-326, (2010) · Zbl 1260.68050
[18] Sarkar, S.; Sewell, P.; Alglave, J.; Maranget, L.; Williams, D., Understanding power multiprocessors., 175-186, (2011)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.