Distributed Computing
Distributed Computing
复制标题
分布式计算
DOI：
10.1007/978-3-642-33651-5_3
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Gotsman A
中科院分区：
文献类型：
--
作者：
Gotsman A
现代编程语言，如c++和Java，为遵循某种同步规则的行为良好的程序提供了顺序一致（SC）内存模型，例如，对于那些无数据争用（DRF）的程序。然而，性能关键型库经常使用语义较弱的低级硬件原语，从而违反这一原则。在这种情况下，对于这些库来说，保护它们本来表现良好的客户机不受较弱内存模型的影响是很重要的。在本文中，我们证明了线性化的一个变体可以用来正式地推理高级DRF客户端和为总存储顺序（TSO）内存模型编写的低级库之间的互操作性，该模型由x86处理器实现。也就是说，我们提出了线性化的概念，将运行在TSO上的具体库实现与运行在SC机器上的抽象规范联系起来。如果调用抽象库规范的SC执行不包含数据竞争，则此库的客户端称为DRF。然后，我们将展示如何将DRF客户端编译为TSO，以便它只显示SC行为，尽管调用了一个racy库。
Modern programming languages, such as C++ and Java, provide a sequentially consistent (SC) memory model for well-behaved programs that follow a certain synchronisation discipline, e.g., for those that are data-race free (DRF). However, performance-critical libraries often violate the discipline by using low-level hardware primitives, which have a weaker semantics. In such scenarios, it is important for these libraries to protect their otherwise well-behaved clients from the weaker memory model.In this paper, we demonstrate that a variant of linearizability can be used to reason formally about the interoperability between a high-level DRF client and a low-level library written for the Total Store Order (TSO) memory model, which is implemented by x86 processors. Namely, we present a notion of linearizability that relates a concrete library implementation running on TSO to an abstract specification running on an SC machine. A client of this library is said to be DRF if its SC executions calling the abstract library specification do not contain data races. We then show how to compile a DRF client to TSO such that it only exhibits SC behaviours, despite calling into a racy library.