The key problem is program transformation, and in particular optimizations. Different CPUs/ISAs, and compilers, might want to transform your program to make it

The key problem is program transformation, and in particular optimizations. Different CPUs/ISAs, and compilers, might want to transform your program to make it run faster. However, in the multi-core setting, data races pose bounds and limits on how much you can trigger those optimizations. The program doesn't generally execute sequentially in a way that can be entirely reasoned about. Instructions might be reordered for the sake of the program to run faster. Programmers can't work with that. So one proposes a memory model. Follow these rules, and our optimizations won't alter the behavior of the program. They kind-of describes what happens "in between" the critical sections of the program, hence the lack of a mutex mention. The paper presents a local property and then shows, formally, that this property is enough to guarantee an efficient memory model. That is, a model in which you can perform optimizations, while programmers can still reason about the programs behavior. The crux of the paper is that the property is local. This is new, because memory models which came before it are global: to reason about correctness, you have to consider the whole program, rather than consider a small (local) subset. OCaml requires more safety than most programming languages, so this is good for the fact that you can now compose local fragments of OCaml programs, without having to worry about a global safety property. The property is also simpler for programmers to reason about. The way you "use" the paper is that you adapt your optimizations to follow the property, and you make sure that the virtual memory model is implemented the same way on different architectures. Finally, the examples: they explore the idea of a local reasoning. In particular, they show why the (existing) global properties fail if you view them under the stronger requirement of local reasoning. It's the setup for the paper, since it means you can't just use the existing models. They need to be adapted if you want a more localized property.