Value-Based or Conflict-Based? Opacity Definitions for STMs
Value-Based or Conflict-Based? Opacity Definitions for STMs
复制标题
基于价值还是基于冲突？
DOI：
10.1007/978-3-319-67729-3_8
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Heike Wehrheim
中科院分区：
文献类型：
--
作者：
Jürgen König;Heike Wehrheim
软件事务性内存（STM）算法为程序员提供了一种高级同步技术，用于并发访问共享状态。stm通常保证某种序列化性：事务的并发执行似乎按顺序发生。在Guerraoui和Kapalka 2008年的论文中，软件事务的可序列化性被称为不透明性。虽然不透明性已被接受为stm的标准正确性标准，但后来的验证方法采用了不同的公式-声称它们是不透明性。在本文中，我们研究了不同版本的不透明度，Guerraoui和Kapalka的基于价值的版本和验证友好的，无价值的基于冲突的版本之间的关系。我们表明，即使在一些合理的执行限制下，基于冲突的不透明性仍然比基于值的不透明性强，拒绝一些可序列化的执行。我们提供了基于冲突的不透明性的另一种定义，仍然不跟踪值，从而保持其验证友好的风格。这个版本，我们称之为基于约束的，被证明与基于值的不透明度是一致的。最后，我们提出了一种使用smt求解器Z3来检查执行时基于约束的不透明性的技术。
Software Transactional Memory (STM) algorithms provide programmers with a high-level synchronization technique for concurrent access to shared state. STMs typically guarantee some sort of serializability: the concurrent execution of transactions appears to occur in a sequential order. With Guerraoui and Kapalka’s 2008 paper, serializability of software transactions has been phrased asopacity. While opacity has been accepted as the standard correctness criterion for STMs, later verification approaches nevertheless adopt different formulations – claiming them to be opacity.In this paper, we study the relationships between different versions of opacity, Guerraoui and Kapalka’svalue-basedversion and the verification-friendly, value-lessconflict-basedversion. We show that even under some reasonable restrictions on executions, conflict-based remains stronger than value-based opacity, rejecting some serializable executions. We provide an alternative definition of conflict-based opacity, still not tracking values and thus keeping its verification-friendly style. This version, which we callconstraint-based, is proven to coincide with value-based opacity. Finally, we propose a technique for checking constraint-based opacity on executions, employing the SMT-solver Z3.
登录
查看更多内容
虚拟世界一致性：STM系统的一个条件（具有不可见读取操作的通用协议）
影响因子：
1.1
作者：
Damien Imbs;M. Raynal
通讯作者：
M. Raynal
影响因子：
1
作者：
Doherty, Simon;Groves, Lindsay;Moir, Mark
通讯作者：
Moir, Mark
证明悲观 STM 的不透明性
DOI：
10.4230/lipics.opodis.2016.35
发表时间：
2016
期刊：
影响因子：
--
作者：
Simon Doherty;Brijesh Dongol;John Derrick;Gerhard Schellhorn;Heike Wehrheim
通讯作者：
Heike Wehrheim
DOI：
10.1145/1152154.1152177
发表时间：
2006
期刊：
2006 International Conference on Parallel Architectures and Compilation Techniques (PACT)
影响因子：
--
作者：
Chaiyasit Manovit;Sudheendra Hangal;Hassan Chafi;Austen McDonald;Christos Kozyrakis;K. Olukotun
通讯作者：
K. Olukotun
使用 Spin 检查事务内存的模型
DOI：
10.1145/1400751.1400816
发表时间：
2008
期刊：
2009 29th IEEE International Conference on Distributed Computing Systems
影响因子：
--
作者：
J. O'Leary;Bratin Saha;M. Tuttle
通讯作者：
M. Tuttle