An operational happens-before memory model

8 years 23 days ago

Download staff.ustc.edu.cn

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 diﬃcult to understand. It also has many anti-intuitive behaviors, as demonstrated by the “ugly examples” by Aspinall and ˇSevˇc´ık [3]. Furthermore, HMM (and JMM) specify only what execution traces are acceptable, but say nothing about how these traces are generated. This gap makes it diﬃcult for static reasoning about programs. In this paper we present OHMM, an operational variation of HMM. The model is speciﬁed by giving an operational semantics to a language runan 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...

Yang Zhang, Xinyu Feng

Real-time Traffic