Robustness against relaxed memory models

For performance reasons, modern multiprocessors implement relaxed memory consistency models that admit out-of-program-order and non-store atomic executions. While data race-free programs are not sensitive to these relaxations, they pose a serious problem to the development of the underlying concurrency libraries. Routines that work correctly under Sequential Consistency (SC) show undesirable effects when run under relaxed memory models. These programs are not robust against the relaxations that the processor supports. To enforce robustness, the programmer has to add safety net instructions to the code that control the hardware - a task that has proven to be difficult, even for experts. We recently developed algorithms that check and, if necessary, enforce robustness against the Total Store Ordering (TSO) relaxed memory model [BDM13, BMM11]. Given a program, our procedures decide whether the TSO behavior coincides with the SC semantics. If this is not the case, they synthesize safety net instructions that enforce robustness. When built into a compiler, our algorithms thus hide the memory model from the programmer and provide the illusion of Sequential Consistency.