Program logics and semantics tell a pleasant story about sequential
composition: when executing (S1; S2), we first execute S1 then S2. To
improve performance, however, processors execute instructions out of order,
and compilers reorder programs even more dramatically. By design,
single-threaded systems cannot observe these reorderings; however,
multiple-threaded systems can, making the story considerably less pleasant.
A formal attempt to understand the resulting mess is known as a ``relaxed
memory model.'' Prior models either fail to address sequential composition
directly, or overly restrict processors and compilers, or permit nonsense
thin-air behaviors which are unobservable in practice.
To support sequential composition while targeting modern hardware, we enrich
the standard event-based approach with preconditions and families of
predicate transformers. When calculating the meaning of (S1;S2), the
predicate transformer applied to the precondition of an event e from S2
is chosen based on the set of events in S1 upon which e depends. We
apply this approach to two existing memory models.
- 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), January 2022.
[Paper | Paper with Draft Appendices | Artifact @Zenodo]
- Alan Jeffrey, Roblox
- James Riely, DePaul University
- Mark Batty, University of Kent
- Simon Cooksey, University of Kent
- Ilya Kaysin, JetBrains Research and University of Cambridge
- Anton Podkopaev, HSE University