Opacity proof for CaPR+ algorithm
Opacity proof for CaPR+ algorithm
复制标题
CaPR 算法的不透明证明
DOI：
10.1145/2833312.2833445
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Sathya Peri
中科院分区：
文献类型：
--
作者：
Anshu S. Anand;R. Shyamasundar;Sathya Peri
在本文中，我们描述了一个增强的自动检查点和部分回滚算法（CAPR+），以实现基于连续冲突检测，具有自动检查点的懒惰版本和部分回滚的软件交易内存（STM）。此外，我们提供了CAPR+算法的正确性证明，尤其是不透明度，STM正确性标准，可准确捕获交易记忆所需的直觉正确性保证。该算法提供了一种自然的方式来实现纯中产品和部分回滚的混合系统。我们还实施了该算法，并参考了红色树木微基准和邮票基准表现出其有效性。获得的结果证明了部分回滚机制对纯流产机制的有效性，尤其是在由大型交易长度组成的应用中。
In this paper, we describe an enhanced Automatic Checkpointing and Partial Rollback algorithm(CaPR+) to realize Software Transactional Memory(STM) that is based on continuous conflict detection, lazy versioning with automatic checkpointing, and partial rollback. Further, we provide a proof of correctness of CaPR+ algorithm, in particular, Opacity, a STM correctness criterion, that precisely captures the intuitive correctness guarantees required of transactional memories. The algorithm provides a natural way to realize a hybrid system of pure aborts and partial rollbacks. We have also implemented the algorithm, and shown its effectiveness with reference to the Red-black tree micro-benchmark and STAMP benchmarks. The results obtained demonstrate the effectiveness of the Partial Rollback mechanism over pure abort mechanisms, particularly in applications consisting of large transaction lengths.