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

Alan Jeffrey ajeffrey at servo.org
Wed Oct 28 21:04:49 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'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)

More information about the jmm-dev mailing list