A Better x86 Memory Model: x86-TSO (Extended Version)
A Better x86 Memory Model: x86-TSO (Extended Version)
复制标题
更好的 x86 内存模型：x86-TSO（扩展版本）
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Peter Sewell
中科院分区：
文献类型：
--
作者：
Scott Owens;Susmit Sarkar;Peter Sewell
真实的多处理器不提供大多数语义上的工作和验证的依据，它们具有放松的记忆模型，通常在模棱两可的散文中描述，这是导致宽度的混淆我们的工作制作了一个严格的X86-CC模型，格式化了当时的英特尔和AMD架构规范，但事实证明，这些模型对实际硬件而言是不合适的，并且可以说是太弱了，以至于我们讨论了这些问题。一个新的X86-TSO模型遇到了HOL4中的正式，我们认为对实际处理器是正确的，可以更好地反映供应商的意图，并且更适合编程。 ：基于本地写入缓冲区的直观操作模型，类似于SPARCV8的公理储物订单模型。所有有效的测试程序的有效执行的集合，并为了更大的信心，直接验证了此类执行的证人，并从第三个，更算法的，等效版本的定义中提取了代码。
Real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, typically described in ambiguous prose, which lead to widespread confusion. These are prime targets for mechanized formalization. In previous work we produced a rigorous x86-CC model, formalizing the Intel and AMD architecture specifications of the time, but those turned out to be unsound with respect to actual hardware, as well as arguably too weak to program above. We discuss these issues and present a new x86-TSO model that suffers from neither problem, formalized in HOL4. We believe it is sound with respect to real processors, reflects better the vendor’s intentions, and is also better suited for programming. We give two equivalent definitions of x86-TSO: an intuitive operational model based on local write buffers, and an axiomatic total store ordering model, similar to that of the SPARCv8. Both are adapted to handle x86-specific features. We have implemented the axiomatic model in our memevents tool, which calculates the set of all valid executions of test programs, and, for greater confidence, verify the witnesses of such executions directly, with code extracted from a third, more algorithmic, equivalent version of the definition.