x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors

Exploiting the multiprocessors that have recently become ubiquitous requires high-performance and reliable concur-rent systems code, for concurrent data structures, operat-ing system kernels, synchronisation libraries, compilers, and so on. However, concurrent programming, which is always challenging, is made much more so by two problems. First, real multiprocessors typically do not provide the sequentially consistent memory that is assumed by most work on seman-tics and verification. Instead, they have relaxed memory models, varying in subtle ways between processor families, in which different hardware threads may have only loosely consistent views of a shared memory. Second, the public vendor architectures, supposedly specifying what program-mers can rely on, are often in ambiguous informal prose (a particularly poor medium for loose specifications), leading to widespread confusion. In this paper we focus on x86 processors. We review sev-eral recent Intel and AMD specifications, showing that all contain serious ambiguities, some are arguably too weak to program above, and some are simply unsound with respect to actual hardware. We present a new x86-TSO program-mer’s model that, to the best of our knowledge, suffers from none of these problems. It is mathematically precise (rig-orously defined in HOL4) but can be presented as an intu-itive abstract machine which should be widely accessible to working programmers. We illustrate how this can be used to reason about the correctness of a Linux spinlock implemen-tation and describe a general theory of data-race-freedom for x86-TSO. This should put x86 multiprocessor system build-ing on a more solid foundation; it should also provide a basis for future work on verification of such systems. 1