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

[Alan Jeffrey]

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's turns out multi-copy atomic architectures have a
simpler model than non-MCA. So we have a lock-free compilation to ARM8 but
not ARM7.

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,

Alan (on behalf of James and Radha)