Data Independence for Software Transactional Memory
Data Independence for Software Transactional Memory
复制标题
DOI：
10.1007/978-3-030-20652-9_18
复制
发表时间：
2019-05
期刊：
影响因子：
--
通讯作者：
J. König;H. Wehrheim
中科院分区：
文献类型：
--
作者：
J. König;H. Wehrheim
软件事务存储器（STM）算法为程序员提供了一种同步机制，用于并发访问共享变量。基本上，程序员可以指定事务（阅读和写入共享状态），然后以“表面上”的原子性执行。这个属性在正确性标准calledopacity中捕获。对于STM算法的不透明度模型检查，原则上，我们需要检查所有可能的交易组合的不透明度，所有可能的值都要写入。这将导致模型检查过程中的无穷大的几个来源：无限多的数据值，无限多的可能访问的transactions，和无限多transactions正在执行。在本文中，我们提出了一种技术，以避免无限的第一个来源：无限多个不同的数据值。为此，我们采用了数据独立的概念，并提供了两个结果。首先，我们证明了不透明度作为正确性标准是数据无关的。其次，我们开发的条件检查STM算法的数据独立性，并显示其合理性。总之，这些结果允许将模型检查（数据独立STM）减少到具有写入值的单一选择的事务。
Software Transactional Memory (STM) algorithms provide programmers with a synchronisation mechanism for concurrent access to shared variables. Basically, programmers can specifytransactions(reading from and writing to shared state) which then execute in a “seeming” atomicity. This property is captured in a correctness criterion calledopacity. For model checking the opacity of an STM algorithm, we – in principle – need to check opacity for all possible combinations of transactions with all possible values to be written. This leads to several sources of infinity during model checking: infinitely many data values, infinitely many possible accesses in transactions, and unboundedly many transactions being executed.In this paper, we propose a technique for avoiding the first source of infinity: infinitely many different data values. To this end, we employ a notion ofdata independenceand provide two results. First, we prove that opacity as a correctness criterion is data independent. Second, we develop conditions for checking data independence of STM algorithms and show their soundness. Together, these results allow to reduce model checking (of data independent STMs) to transactions with a single choice for values written.