A memory model defines the semantics of memory accesses in multithreaded programs. For programmers, sequential consistency (i.e., interleaving-based semantics) is considered as the simplest model. However, naive sequential consistency is too costly to implement, and, in fact, designing a satisfactory memory model is highly challenging, as one has to carefully balance the conflicting desiderata of programmers, compilers, and hardware.
In this talk Ori will introduce the formal underpinning of the C/C++ concurrency model from 2011 and the key ideas behind it. He will discuss some of the flaws of the model, ways of correcting it, and some remaining open problems. In particular, he will describe the notorious "out-of-thin-air" problem, and describe the "promising semantics" solution for it (appeared in POPL'17).