The standards committee of the C++ programming language defined the C11 memory model. This model provides several notions of consistency for memory reads and writes, with sequentially consistent (SC) being the strongest and most expensive. This paper shows novel examples where SC and non-SC memory accesses to the same location by different threads cause problems (race conditions) according to C11.

Although the C11 model was known to have multiple problems, none (until now) affected the correctness of compilation to the mainstream architectures. The C11 memory model is compiled into different processors using hardware fences, which provide a method to enforce SC. This paper also shows how compilation to the power processor family is broken and how programs with SC and non-SC memory accesses can go wrong.

The authors define a new memory model, called repaired C11 (RC11), and prove different properties: RC11 solves all the known problems, satisfies strong coherence properties, correctly compiles into different processor families (X86, Power, and ARM), and makes sure that different source transformations typical in compilers are still sound.

The paper formally proves, for the first time, all the properties described above, including soundness of the compilation scheme for the power processor family.

The authors follow declarative specifications of the C11 memory model and the mainstream processor architectures to provide formal proofs. They suggest mechanizing these proofs using a theorem prover as future work; that would be the strongest validation of their new RC11 memory model.

The paper uses colors for the different relations, and that should greatly help readers understand the figures with program executions.