x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors
x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors
复制标题
DOI：
10.1145/1785414.1785443
复制
发表时间：
2010-07
期刊：
影响因子：
--
通讯作者：
Peter Sewell;Susmit Sarkar;Scott Owens;Francesco Zappa Nardelli;Magnus O. Myreen
中科院分区：
文献类型：
--
作者：
Peter Sewell;Susmit Sarkar;Scott Owens;Francesco Zappa Nardelli;Magnus O. Myreen
开发最近变得无处不在的多处理器需要高性能和可靠的并发系统代码，用于并发数据结构，操作系统内核，同步库，编译器等。首先，真实的多处理器通常不提供顺序一致的内存，这是大多数工作的语义和验证。相反，它们有宽松的内存模型，在处理器家族之间以微妙的方式变化，其中不同的硬件线程可能只有松散一致的共享内存视图。第二，公共供应商架构，理应规定程序员可以依赖什么，通常是模糊的非正式散文（一个特别差的媒介松散的规范），导致广泛的混乱。在本文中，我们将重点介绍x86处理器。我们回顾了几个最近的英特尔和AMD的规格，显示所有包含严重的模糊性，有些可以说是太弱的程序以上，有些只是不健全的实际硬件。我们提出了一个新的x86-TSO程序员的模型，据我们所知，没有这些问题。它在数学上是精确的（在HOL 4中有严格的定义），但可以作为一个直观的抽象机器呈现，应该被工作的程序员广泛使用。我们说明了如何可以用来推理的正确性的Linux自旋锁实现，并描述了一般理论的x86-TSO的数据竞争自由。这将使x86多处理器系统的构建建立在一个更坚实的基础上;它还将为将来验证此类系统的工作提供基础。
Exploiting the multiprocessors that have recently become ubiquitous requires high-performance and reliable concurrent systems code, for concurrent data structures, operating system kernels, synchronization 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 semantics 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 programmers 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 several 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 programmer's model that, to the best of our knowledge, suffers from none of these problems. It is mathematically precise (rigorously defined in HOL4) but can be presented as an intuitive 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 implementation and describe a general theory of data-race freedom for x86-TSO. This should put x86 multiprocessor system building on a more solid foundation; it should also provide a basis for future work on verification of such systems.