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. Library routines that work correctly under Sequential Consistency (SC) show undesirable effects when run under a relaxed memory model. These routines 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 prominent relaxed memory models like TSO implemented in x86 processors and Power implemented in IBM architectures. Given a program, our algorithms decide whether the actual behavior on the processor 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 relaxed memory model from the programmer and provide the illusion of Sequential Consistency. In this talk, I will give an introduction to relaxed memory models, motivate the robustness problem, and explain how to reduce it to a language emptiness problem.