An operational happens-before memory model

作者：Zhang, Yang^*; Feng, Xinyu

来源：Frontiers of Computer Science, 2016, 10(1): 54-81.

DOI：10.1007/s11704-015-4492-4

• relaxed memory model
• happens-before
• operatonal semantics
• DRF-Guarantee
• JMM

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 Aspinall and Sevcik [1]. 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 model many 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.

• 出版日期2016-2
• 单位中国科学技术大学苏州研究院; 中国科学技术大学