Relaxed memory models must be rigorous
Francesco Zappa Nardelli, Peter Sewell, Susmit Sarkar, Luc Maranget, Mark Batty, Jade Alglave · 2009
Multiprocessors and high-level languages generally provide only relaxed (non-sequentially-consistent) memory models, to permit performance optimisations. One has to understand these models to program reliable concurrent systems — but they are typically ambiguous and incomplete informal-prose documents, sometimes give guarantees that are too weak to be useful, and are sometimes simply unsound. Based on our previous work, we review various problems with some current specifications, for x86 (Intel 64/IA32 and AMD64), and Power and ARM processors, and for the Java and C++ languages. We argue that such specifications should be rigorously defined and tested.