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.
Cat model
Not expressible in cat cited
Semantic dependency is computed from logical preconditions carried by events during composition of the program's denotation, not read off a candidate execution. Jagadeesan et al. 2020
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