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.  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 controls 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 behaviour on the processor coincides with the SC semantics.  If this is not the case, they synthesise 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, we motivate the robustness problem and explain how to reduce it to a standard SC reachability query.

Speaker biography

Since July 2010, Roland Meyer has been a Professor of Theoretical Computer Science (tenure track, tenured) at the University of Kaiserslautern where he holds the Chair of Concurrency Theory.  Previously, he was a CNRS postdoc in LIAFA, University Paris 7, from March 2009 to June 2010.  From August 2004 to March 2009, he worked in the Transregional Research Center AVACS at the University of Oldenburg.  In February 2009, he obtained a PhD from the University of Oldenburg, where he was a PhD sutdent in the graduate school TrustSoft from October 2005 to September 2008.  From October 2001 to September 2005, he studied Computer Science and Mathematics in Oldenburg.