FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings
复制标题
FM 2015：形式化方法 - 第 20 届国际研讨会，挪威奥斯陆，2015 年 6 月 24-26 日，会议记录
DOI：
10.1007/978-3-319-19249-9_12
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Derrick J
中科院分区：
文献类型：
--
作者：
Derrick J
弱（或宽松）内存模型的实现是现代多处理器硬件中的标准实践。为了提高效率，这些内存模型允许操作在共享内存中以与它们在程序中发生的顺序不同的顺序生效。已经提出了一些正确性的标准，并发对象在这样的内存模型上操作，每个反映不同的约束的对象，可以证明是正确的。在本文中，我们提供了一个框架，其中的正确性标准定义在两个组成部分：第一个定义特定的标准（因为它将被定义在没有一个弱记忆模型），第二个定义特定的弱记忆模型。该框架促进了正确性标准的定义和比较，并鼓励重用现有的定义。后者使属性的标准，以证明使用现有的证据。我们说明的框架，通过定义的正确性标准的TSO（总存储顺序）弱记忆模型。
The implementation of weak (or relaxed) memory models is standard practice in modern multiprocessor hardware. For efficiency, these memory models allow operations to take effect in shared memory in a different order from that which they occur in a program. A number of correctness criteria have been proposed for concurrent objects operating on such memory models, each reflecting different constraints on the objects which can be proved correct. In this paper, we provide a framework in which correctness criteria are defined in terms of two components: the first defining the particular criterion (as it would be defined in the absence of a weak memory model), and the second defining the particular weak memory model. The framework facilitates the definition and comparison of correctness criteria, and encourages reuse of existing definitions. The latter enables properties of the criteria to be proved using existing proofs. We illustrate the framework via the definition of correctness criteria on the TSO (Total Store Order) weak memory model.