Formal Reasoning about the C11 Weak Memory Model
Abstract
This abstract introduces the C11 weak memory model, summarises known verification results, and discusses some open problems.
Related papers
- Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris ECOOP 2017
- Verifying C11 programs operationally PPoPP 2019
- Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it POPL 2015
- SecRSL: security separation logic for C11 release-acquire concurrency OOPSLA 2021
- Relaxed separation logic: a program logic for C11 concurrency OOPSLA 2013
- Sequential reasoning for optimizing compilers under weak memory concurrency PLDI 2022
- Correct and efficient work-stealing for weak memory models PPoPP 2013
- Verifying C11-style weak memory libraries PPoPP 2021