Opacity proof for CaPR+ algorithm

Software Transactional Memory(STM) is a new programming paradigm that can be an effective alternative to the conventional parallel programming models and languages. It absolves the programmer of having to synchronize and coordinate parallel computations, and instead delegates these to the compiler and run-time systems. In this paper, we describe an enhanced Automatic Checkpointing and Partial Rollback algorithm(CaPR+ ) to realize STMs 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 refernce to the Red-black tree microbenchmark and STAM...

• Type: Journal
• Year: 2016
• Where: ICDCN
• Authors: Anshu S. Anand, R. K. Shyamasundar, Sathya Peri
• Keywords: Distributed And Parallel Computing, ICDCN 2016