Decomposing Opacity
Decomposing Opacity
复制标题
分解不透明度
DOI：
10.1007/978-3-662-45174-8_27
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
J. Palsberg
中科院分区：
文献类型：
--
作者：
M. Lesani;J. Palsberg
交易记忆（TM）算法是微妙的，TM正确性条件很复杂。正确性条件的分解可以为TM算法设计和验证带来模块化。我们提出了一种被称为标记的不透明度分解，称为单独的直觉不变性。我们证明了不透明度和标志性的等效性。 TM算法的标志性证明可以通过并反映算法设计直觉。例如，我们证明了TL2算法的标记性和不透明性。另外，基于其中一个不变性，我们为TM算法的时间复杂性提供了下限结果。
Transactional memory (TM) algorithms are subtle and the TM correctness conditions are intricate. Decomposition of the correctness condition can bring modularity to TM algorithm design and verification. We present a decomposition of opacity called markability as a conjunction of separate intuitive invariants. We prove the equivalence of opacity and markability. The proofs of markability of TM algorithms can be aided by and mirror the algorithm design intuitions. As an example, we prove the markability and hence opacity of the TL2 algorithm. In addition, based on one of the invariants, we present lower bound results for the time complexity of TM algorithms.