Institute of

Theoretical Computer Science


Technische Universität Braunschweig

Relaxed Memory Models

Relaxed Memory Models

For performance reasons, modern multiprocessors implement relaxed memory 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 show undesirable effects when run on relaxed memory models. Mutual exclusion algorithms, for example, fail if the program-order is relaxed only slightly. We study verification techniques for programs running on relaxed memory models. More


Roland Meyer, Georgel Calin, Egor Derevenetc, Florian Furbach, Sebastian Schweizer, and Sebastian Wolff



DFG: Robustness against Relaxed Memory Models (R2M2) | DAAD: Robustness under Realistic Instruction Sets (ROIS) | Carl Zeiss: Architecture-aware Verification (ArchiV) | Fraunhofer ITWM