Theoretical Computer Science

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

Team:

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

Publications:

• Pointer Race Freedom, by Frederic Haziza, Lukas Holik, Roland Meyer, and Sebastian Wolff.
  In Proceedings of VMCAI 2016.
  PDF | DOI | BibTeX

• Lazy TSO Reachability, by Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, and Roland Meyer.
  In Proceedings of FASE 2015.
  arXiv | DOI | BibTeX

• Checking and Enforcing Robustness against Relaxed Memory Models, by Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer.
  In Proceedings of SE 2014.
  PDF

• Memory-Model-Aware Testing - a Unified Complexity Analysis, by Florian Furbach, Roland Meyer, Klaus Schneider, and Maximilian Senftleben.
  In Proceedings of ACSD 2014.
  ACSD 2014 best paper award.
  DOI | PDF

• Checking and Enforcing Robustness against TSO, by Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer.
  In Proceedings of ESOP 2013.
  PDF (full version) | DOI | BibTeX

• A Theory of Partitioned Global Address Spaces, by Georgel Calin, Egor Derevenetc, Rupak Majumdar, and Roland Meyer.
  In Proceedings of FSTTCS 2013.
  arXiv | DOI | BibTeX

• Deciding Robustness against Total Store Ordering, by Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann.
  In Proceedings of ICALP 2011.
  DOI | BibTeX

• Memory-Model-Aware Testing - a Unified Complexity Analysis, by Florian Furbach, Roland Meyer, Klaus Schneider, and Maximilian Senftleben.
  ACM Transactions on Embedded Computing Systems (TECS), 2015.
  PDF | BibTeX

• Robustness against Relaxed Memory Models, PhD thesis by Egor Derevenetc.
  University of Kaiserslautern, 2015.
  PDF | BibTeX

Funding:

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