Pomsets with Predicate Transformers (The Leaky Semicolon) PwT
A compositional, denotational relaxed-memory model based on pomsets with predicate transformers (PwT), extending Pomsets with Preconditions (Jagadeesan, Jeffrey & Riely, POPL 2020) with families of predicate transformers so that the denotation of a sequential composition S1;S2 is computed directly from those of S1 and S2. It bans out-of-thin-air behaviour (verified in Coq) while permitting common compiler and hardware reorderings, and defines two instances: PwT-C11 (inherits RC11's top-level axioms; lowers to any C11-supported architecture) and PwT-mca (fully compositional, with optimal lowering to multi-copy-atomic architectures such as Arm8). Despite the overlapping author set, this is the pomsets/preconditions lineage rather than the Well-Justified Event Structures (Jeffrey & Riely 2016) event-structures line; the paper states no formal ordering to WJES.
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 Armv8
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
Ordering relationships
- Strictly weaker than
- Pomsets with Preconditions (PwP) — 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.
- Incomparable with
- Repaired C11 (RC11) — Leaky Semicolon §9: 'PwT-mca is incomparable to both RC11 ... and the promising semantics'. RC11 allows non-multi-copy-atomic behaviours that PwT-mca disallows, while PwT-mca allows optimisations that RC11's No-Thin-Air axiom forbids.
- Promising Semantics (PS) — Leaky Semicolon §9: 'PwT-mca is incomparable to both RC11 ... and the promising semantics [Kang et al. 2017] ... PwT-mca has a weaker notion of coherence than the promising semantics.'
References
- Alan Jeffrey, James Riely, Mark Batty, Simon Cooksey, Ilya Kaysin, Anton Podkopaev. The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency. Proc. ACM Program. Lang. 6(POPL), Article 54, 2022. doi:10.1145/3498716