Local Data Race Freedom with Non-Multi-Copy Atomicity
Local Data Race Freedom with Non-Multi-Copy Atomicity
复制标题
具有非多副本原子性的本地数据竞争自由
DOI：
10.1007/978-3-319-94111-0_12
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Tatsuya Abe
中科院分区：
文献类型：
--
作者：
Hirofumi Inaba;et al;鎌田裕美;鎌田裕美;Hiromi Kamata;Hiromi Kamata;Tatsuya Abe
数据竞争自由保证了松弛内存一致性模型（MCMs）下并发程序行为的顺序一致性，减少了MCMs下软件模型检测的状态爆炸问题.然而，数据竞争自由度太强，无法包括所有有趣的程序。在本文中，我们定义了一个小步骤的操作语义宽松的MCMs，定义了一个可观察的等价使用互模拟的概念，并提出了本地数据竞争自由（LDRF），这需要一种竞争自由本地，而不是全球性的属性。LDRF包括一些有趣的程序，如独立读独立写程序，这是众所周知的表现出奇怪的行为下非多副本原子MCM，和一些并发复制垃圾收集算法。在本文中，我们介绍了一种称为内存共享的LDRF程序的模型检测的优化方法，并通过实验表明，内存共享优化缓解了非多副本原子MCMs的状态爆炸问题。
Data race freedom ensures the sequentially consistent behaviors of concurrent programs under relaxed memory consistency models (MCMs), and reduces the state explosion problem for software model checking with MCMs. However, data race freedom is too strong to include all interesting programs. In this paper, we define small-step operational semantics for relaxed MCMs, define an observable equivalence using the notion of bisimulation, and propose the property of local data race freedom (LDRF), which requires a kind of race freedom locally instead of globally. LDRF includes some interesting programs, such as the independent reads independent writes program, which is well known to exhibit curious behaviors under non-multi-copy atomic MCMs, and some concurrent copying garbage collection algorithms. In this paper, we introduce an optimization method called memory sharing for model checking of LDRF programs, and show that memory sharing optimization mitigates state explosion problems with non-multi-copy atomic MCMs through experiments.