The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency

Program logics and semantics tell a pleasant story about sequential composition: when executing (𝑆 1 ; 𝑆 2 ), we first execute 𝑆 1 then 𝑆 2 . 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 (𝑆 1 ; 𝑆 2 ), the predicate transformer applied to the precondition of an event 𝑒 from 𝑆 2 is chosen based on the set of events in 𝑆 1 upon which 𝑒 depends. We apply this approach to two existing memory models.