kirancodes.me
To Proof Maintenance & Beyond!

Memory, an elusive abstraction

Peter Sewell

Abstract

Multiprocessors are now ubiquitous. They provide an abstraction of shared memory, accessible by concurrently executing threads, which supports a wide range of software. However, exactly what this key abstraction is -- what the hardware designers implement, and what programmers can depend on -- is surprisingly elusive. In 1979, when articulating the notion of sequential consistency (SC), Lamport wrote "For some applications, achieving sequential consistency may not be worth the price of slowing down the processors." [7], and indeed most major multiprocessor families, including Alpha, ARM, Itanium, Power, Sparc, and x86, do not provide the abstraction of SC memory. Internally, they incorporate a range of sophisticated optimisations which have various programmer-visible effects. For some (such as Sparc) these effects are captured in a well-defined relaxed memory model, making it possible (if challenging) to reason with confidence about the behaviour of concurrent programs. For others, however, it has been very unclear what a reasonable model is, despite extensive research over the last three decades. In this talk, I will reflect on the experience of my colleagues and I in trying to establish usable models for x86 multiprocessors, where it appears that our x86-TSO model suffices for common-case code [1-4], and for Power and ARM multiprocessors, where we have models that capture some but not all aspects of their behaviour [5,6]. The underlying causes of these difficulties are complex, including:

Related papers