The notion of a relaxed (aka weak) memory model is well known, given that such models are implemented by almost all hardware vendors and embedded within the concurrency semantics of many ma jor programming languages. However, given the sheer volume of work on consistency models, formalisations and tools, the area can be both confusing (and intimidating) for newcomers to get into, with even experts missing new developments. In this paper, we coalesce a recent line of work that has focussed on developing reasoning principles for relaxed memory into a single reference, extrapolating their key ideas. This line of work aims to reuse (standard) verification techniques for concurrent programs such as Owicki-Gries, rely-guarantee and refinement that were established in the 1970s and 80s, which are well known to most formal methods researchers. We aim to explain these ideas in simple terms, explain some of the main developments and discuss open problems and opportunities for further research. Throughout the paper, we will focus on the RC11 memory model, but discuss how these reasoning principles apply to other models. Instead of focussing on relaxed memory litmus tests (which non-experts may not appreciate), we use a novel proof of a non-trivial buffer developed by Lamport as a running example.

Resources

• Tutorial webpage: https://brijeshdongol.github.io/FM26/tutorial.html
• Tutorial paper: https://brijeshdongol.github.io/FM26/paper.pdf
• Slides: https://brijeshdongol.github.io/FM26/slides.pdf
• Isabelle/HOL files: https://brijeshdongol.github.io/FM26/Isabelle.zip
• Link to download the Isabelle proof assistant: https://isabelle.in.tum.de