Weak memory model semantics of a high-level programming language should allow behaviors of a concurrent program obtained due to compiler optimizations. Several previously proposed semantics are either too strong or too weak. Later could lead to the so called `out-of-thin-air read` problem. That is a counterintuitive behavior of a program not observed in practice, but allowed by formal semantics.
Recently Chakraborty & Vafeiadis have proposed a new weak memory semantics based on event structures. This semantics solves `OOTA` problem. Moreover, it is more declarative compared to alternative solutions. In this talk we will present `event structure` memory model. We will also compare it to the alternative approach based on `promise` machine. Also an overview of the proof of compilation correctness from `event structure` model to the `Intermediate Memory Model` will be given.
1. Soham Chakraborty and Viktor Vafeiadis. Grounding Thin-Air Reads with Event Structures \\ POPL'19
2. Anton Podkopaev, Ori Lahav, Viktor Vafeiadis. Bridging the Gap Between Programming Languages and Hardware Weak Memory Models \\ POPL'19
Presenter: Evgeny Moiseenko
Date: November 12, 2018
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28