Opacity Proof for CaPR+ Algorithm

TL;DR

This paper introduces an enhanced CaPR+ algorithm for Software Transactional Memory that ensures correctness through opacity, combining automatic checkpointing, lazy versioning, and partial rollback, with empirical validation on benchmarks.

Contribution

It provides a formal proof of opacity for the CaPR+ algorithm and demonstrates its effectiveness through implementation and benchmarking.

Findings

Partial rollback outperforms pure aborts in large transactions

The algorithm maintains opacity, ensuring correctness of transactional memory

Empirical results show improved performance on benchmarks

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.