Relaxed Memory Model Zoo

Memory model
← Back to the map

Generative Operational Semantics GOS

2010 · Jagadeesan, Pitcher, Riely · language, formal, operational

A generative operational semantics that attempts to fix the JMM by constraining speculative execution with stratification conditions to rule out thin-air values. The authors prove the external DRF theorem and verify a few program transformations (store→store reordering, load/load elimination, and roach-motel reordering), though the overall study of transformations is not systematic.

Ordering relationships

Incomparable with
  • C11/C++11 Memory Model — GOS gives a generative operational semantics with stratification constraints on speculation to rule out thin-air values and prove external DRF; it forbids thin-air reads C11 permits but is not a strict subset.

References

  • Radha Jagadeesan, Corin Pitcher, James Riely. Generative Operational Semantics for Relaxed Memory Models. ESOP 2010, 2010. doi:10.1007/978-3-642-11957-6_17
  • Evgenii Moiseenko, Anton Podkopaev, Dmitrii Koznov. A Survey of Programming Language Memory Models. Programming and Computer Software 47(6), pp. 439–456, 2021. doi:10.1134/S0361768821060050

Open GOS in the interactive map →