Modern processors and compilers aggressively optimise programs. Effects of theese optimisations are not observed in single-threaded applications, but can lead to counter-intuitive behaviors in multi-threaded setting. Memory models that allow for such behavors arise are called `weak`.
It could be hard to reason about `weak` behaviors for ordinary programmers. In order to cope with that, many memory models provides a so-called DRF guaratee. DRF guaratee states, that if the programm has no races under SC memory model, then it has no weak behaviors under given memory model.
Unfortunately, DRF guaratee is `global`. One single data-race in program completely violates it.In this talk more strong Local DRF guarantee will be presented, along with the new memory model that provides this guarantee.
Stephen Dolan, KC Sivaramakrishnan, Anil Madhavapeddy. Bounding Data Races in Space and Time // PLDI 2018.
Presenter: Eugene Moiseenko
Date: March 5, 2018
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28