weakmemory.github.io

The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency

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.

Paper:

• 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]

Talk (20min) and Teaser (5min):

People:

• 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