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

James Riely jriely at gmail.com
Sat Oct 31 14:27:37 UTC 2020

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:


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)

More information about the jmm-dev mailing list