Opacity proof for CaPR+ algorithm

Conference/Journal
ACM
Authors
Anshu S Anand RK Shyamasundar Sathya Peri
BibTex
Abstract
Abstract 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 ...