[jmm-dev] Pomsets with Preconditions: A Simple Model of Relaxed Memory

[James Riely]

Hi everyone,

We're pleased to announce our latest attempt to provide a model of relaxed
memory that is compositional, supports common compiler optimizations, can
be compiled to hardware*, and above all is simple enough to be understood
by humans. It's been accepted to appear at this year's OOPSLA:

https://2020.splashcon.org/details/splash-2020-oopsla/70/Pomsets-with-Preconditions-A-Simple-Model-of-Relaxed-Memory

The * is because it turns out multi-copy atomic architectures have a
simpler model than non-MCA. So we have fence-free compilation to ARM but
not Power.

The model is surprisingly straightforward, avoids OOTA, but doesn't require
alternate universes (in the style of speculative or promising operational
semantics or the JMM).

Best wishes,
James (on behalf of Alan and Radha)