Programming Languages and Tools Lab

PwT: Compositional Semantics for Relaxed-Memory Concurrency

Pomsets with Preconditions, PwT, is aimed to provide a denotational memory model for programming languages which solves the Out-Of-Thin-Air problem without sacrificing performance on modern CPUs. This could be used to replace the C++ memory model.

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 fail to address sequential composition directly, or overly restrict processors and compilers, or permit nonsense thin-air behaviors that 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.

Participants

Anton Podkopaev