Skip to main content

The Leaky Semicolon

JEFFREY, A, Riely, J, Batty, Mark, Cooksey, Simon, KAYSIN, I, PODKOPAEV, A (2022) The Leaky Semicolon. Principles of Programming Languages, 6 . pp. 1-30. ISSN 0743-9016. (doi:10.1145/3498716) (KAR id:95153)

PDF Publisher pdf
Language: English

Download (571kB) Preview
[thumbnail of 3498716.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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.

Item Type: Article
DOI/Identification number: 10.1145/3498716
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Batty
Date Deposited: 23 May 2022 06:52 UTC
Last Modified: 24 May 2022 15:12 UTC
Resource URI: (The current URI for this page, for reference purposes)
Batty, Mark:
  • Depositors only (login required):


Downloads per month over past year