A Transactional Correctness Tool for Abstract Data Types
A Transactional Correctness Tool for Abstract Data Types
复制标题
抽象数据类型的事务正确性工具
DOI：
10.1145/3148964
复制
发表时间：
2017
影响因子：
1.6
通讯作者：
Dechev, Damian
中科院分区：
文献类型：
--
作者：
Peterson, Christina;Dechev, Damian
事务内存通过保证事务形式的顺序代码块将表现出原子性和隔离性来简化多处理器编程。transmittance数据结构通过支持操作组合的原子执行，为并发数据结构提供了相同的保证。事务存储系统的并发控制通过检测多个并发事务之间的读/写冲突来保持原子性和隔离性。最先进的事务数据结构通过仅为非交换操作提供显式事务级同步来改进此并发控制协议。由于读/写冲突是由线程级并发控制来处理的，因此不能根据读/写历史来评估事务数据结构的正确性。这对现有的事务存储器的正确性验证技术提出了挑战，因为正确性是根据事务在存在读/写confliction.In本文中，我们提出了transmittance正确性工具抽象数据类型（TxC-ADT），第一个工具，可以检查事务数据结构的正确性。TxC-ADT将事务正确性的标准定义提升为抽象数据类型，这是检查仅同步高级语义冲突的事务正确性的一个重要方面。为了适应各种各样的事务正确性条件，我们提出了一种技术，用于将正确性定义为一个happens-before关系。以这种方式定义正确性条件实现了一种自动化方法，在该方法中，通过在模型检查期间生成和分析事务性发生前图来评估正确性。事务发生前图是在每个线程的基础上维护的，使我们的方法适用于不强制执行事务执行总顺序的事务正确性条件。我们展示了TxC-ADT的实际应用，通过检查锁自由transmittance转换和transmittance数据结构库的可串行化，严格的可串行化，不透明性和因果一致性。
Transactional memory simplifies multiprocessor programming by providing the guarantee that a sequential block of code in the form of a transaction will exhibit atomicity and isolation. Transactional data structures offer the same guarantee to concurrent data structures by enabling the atomic execution of a composition of operations. The concurrency control of transactional memory systems preserves atomicity and isolation by detecting read/write conflicts among multiple concurrent transactions. State-of-the-art transactional data structures improve on this concurrency control protocol by providing explicit transaction-level synchronization for only non-commutative operations. Since read/write conflicts are handled by thread-level concurrency control, the correctness of transactional data structures cannot be evaluated according to the read/write histories. This presents a challenge for existing correctness verification techniques for transactional memory, because correctness is determined according to the transitions taken by the transactions in the presence of read/write conflicts.In this article, we present Transactional Correctness tool for Abstract Data Types (TxC-ADT), the first tool that can check the correctness of transactional data structures. TxC-ADT elevates the standard definitions of transactional correctness to be in terms of an abstract data type, an essential aspect for checking correctness of transactions that synchronize only for high-level semantic conflicts. To accommodate a diverse assortment of transactional correctness conditions, we present a technique for defining correctness as a happens-before relation. Defining a correctness condition in this manner enables an automated approach in which correctness is evaluated by generating and analyzing a transactional happens-before graph during model checking. A transactional happens-before graph is maintained on a per-thread basis, making our approach applicable to transactional correctness conditions that do not enforce a total order on a transactional execution. We demonstrate the practical applications of TxC-ADT by checking Lock Free Transactional Transformation and Transactional Data Structure Libraries for serializability, strict serializability, opacity, and causal consistency.
登录
查看更多内容
宽松内存模型上的软件事务内存
DOI：
--
发表时间：
2009
期刊：
International Conference on Computer Aided Verification
影响因子：
--
作者：
R. Guerraoui;T. Henzinger;Vasu Singh
通讯作者：
Vasu Singh
同步共享抽象类型
DOI：
--
发表时间：
1984
期刊：
TOCS
影响因子：
--
作者：
P. Schwarz;A. Spector
通讯作者：
A. Spector
面向对象数据库系统中的语义并发控制
DOI：
--
发表时间：
1993
期刊：
Proceedings of IEEE 9th International Conference on Data Engineering
影响因子：
--
作者：
Peter Muth;T. Rakow;G. Weikum;Peter Brössler;Christof Hasse
通讯作者：
Christof Hasse
DOI：
--
发表时间：
2011
期刊：
European Symposium on Programming
影响因子：
--
作者：
Annette Bieniusa;Peter Thiemann
通讯作者：
Peter Thiemann
DOI：
10.1145/1806596.1806613
发表时间：
2010
期刊：
Formal Methods in Computer Aided Design (FMCAD'07)
影响因子：
--
作者：
M. Emmi;R. Majumdar;R. Manevich
通讯作者：
R. Manevich