arXiv · 1510.06967
Opacity Proof for CaPR+ Algorithm
Abstract
In this paper, we describe an enhanced Automatic Check- pointing and Partial Rollback algorithm(CaP R + ) to realize Software Transactional Memory(STM) that is based on con- tinuous conflict detection, lazy versioning with automatic checkpointing, and partial rollback. Further, we provide a proof of correctness of CaP R+ 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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Anshu S Anand, R K Shyamasundar, Sathya Peri. 2015-10-23. Opacity Proof for CaPR+ Algorithm. https://arxiv.org/abs/1510.06967
Cite the original work for its findings. Save a collection to share your selection of sources.