Pomsets with Preconditions PwP
A denotational relaxed-memory model for a Java-like language that combines pomsets (Gischer 1988) with preconditions (Hoare-style logical formulae labelling events) to calculate semantic dependencies. It bans out-of-thin-air reads while supporting temporal-safety reasoning, all expected sequential compiler optimizations (including common subexpression elimination, unlike C11 relaxed atomics), and the sc-drf criterion. The model realizes multi-copy atomicity and compiles to x64 and Arm8 without extra fences on relaxed accesses, but is deliberately not implementable on non-MCA processors such as POWER and Armv7. It is the base model that Pomsets with Predicate Transformers / 'The Leaky Semicolon' (Jeffrey et al. 2022) extends to give a direct, compositional account of sequential composition; that later work's PwT-mca1 imposes the same reads-from-implies-order requirement (m7c) as PwP and is thus close to it, while its PwT-mca2 drops m7c and is a strictly weaker model new to the 2022 paper.
Properties
Property vector author-extrapolated — set only where the model’s definition pins the cell down (unknown cells are omitted); cells citing a specific source are marked.
- Compilation optimal mapping to
- yes x86
- no POWER
- no Armv7
- yes Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Other local transformations
- yes Common subexpr. elim.
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- yes Multicopy atomic
Ordering relationships
- Strictly stronger than
- Pomsets with Predicate Transformers (The Leaky Semicolon) (PwT) — Leaky Semicolon §9/App. E: 'PwT-mca generalizes PwP to account for sequential composition'; PwP imposes m7c (reads-from implies pomset order) and 'is similar to PwT-mca1', whereas 'PwT-mca2 ... drops ... m7c' and 'is a weaker model new to this paper' (§4.2). Dropping m7c admits behaviours PwP forbids: the Arm8 execution of §4.2 is allowed by PwT-mca2 but 'disallowed by PwT-mca1', witnessing that the LeakySemi/PwT-mca model is strictly weaker (more permissive) than PwP. Since PwP is roughly PwT-mca1 rather than exactly it (§9: 'PwT is based on PwP, [but] there are many differences'), no equivalence is claimed.
References
- Radha Jagadeesan, Alan Jeffrey, James Riely. Pomsets with Preconditions: A Simple Model of Relaxed Memory. Proc. ACM Program. Lang. 4(OOPSLA), Article 194, 2020. doi:10.1145/3428262