Abstract

Despite many years of research, it has proven very difficult to develop a model for relaxed-memory concurency that satisfies all the requirements of programmers, compilers, and hardware.

In this talk, I will introduce the first relaxed-memory model, called “promising semantics”, that fulfills (most of) the requirements. It (1) accounts for a broad spectrum of features from the C++11 concurrency model, (2) is implementable, in the sense that it provably validates many standard compiler optimizations and reorderings, as well as standard compilation schemes to x86-TSO and Power, (3) justifies simple invariant-based reasoning, thus demonstrating the absence of bad “out-of-thin-air” behaviors, (4) supports “DRF” guarantees, ensuring that programmers who use sufficient synchronization need not understand the full complexities of relaxed-memory semantics, and (5) defines the semantics of racy programs without relying on undefined behaviors, which is a prerequisite for applicability to type-safe languages like Java. To establish confidence in our model, we have formalized most of our key results in Coq.

Also, in this talk, no prior knowledge of relaxed memory concurrency (in particular, existing axiomatic semantics) is assumed. This is particularly because the promising semantics is a standard interleaving operational semantics with just two new notions: “view” and “promise”.