Proving Opacity of a Pessimistic STM
Transactional Memory (TM) is a high-level programming abstraction for concurrency control that provides programmers with the illusion of atomically executing blocks of code, called transactions. TMs come in two categories, optimistic and pessimistic, where in the latter transactions never abort. While this simplifies the programming model, high-performing pessimistic TMs can be complex. In this paper, we present the first formal verification of a pessimistic software TM algorithm, namely, an algorithm proposed by Matveev and Shavit. The correctness criterion used is opacity, formalising the transactional atomicity guarantees. We prove that this pessimistic TM is a refinement of an intermediate opaque I/O-automaton, known as TMS2. To this end, we develop a rely-guarantee approach for reducing the complexity of the proof. Proofs are mechanised in the interactive prover Isabelle.
Pessimistic STMs
Opacity
Verification
Isabelle
Simulation
TMS2
35:1-35:17
Regular Paper
Simon
Doherty
Simon Doherty
Brijesh
Dongol
Brijesh Dongol
John
Derrick
John Derrick
Gerhard
Schellhorn
Gerhard Schellhorn
Heike
Wehrheim
Heike Wehrheim
10.4230/LIPIcs.OPODIS.2016.35
Y. Afek, A. Matveev, and N. Shavit. Pessimistic software lock-elision. In M. K. Aguilera, editor, DISC, volume 7611 of LNCS, pages 297-311. Springer, 2012.
A. S. Anand, R. K. Shyamasundar, and S. Peri. Opacity proof for CaPR+ algorithm. In ICDCN, pages 16:1-16:4, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2833312.2833445.
http://dx.doi.org/10.1145/2833312.2833445
H. Attiya, A. Gotsman, S. Hans, and N. Rinetzky. A programming language perspective on transactional memory consistency. In P. Fatourou and G. Taubenfeld, editors, PODC'13, pages 309-318. ACM, 2013.
A. Cohen, J. W. O'Leary, A. Pnueli, M. R. Tuttle, and L. D. Zuck. Verifying correctness of transactional memories. In FMCAD, pages 37-44, Washington, DC, USA, 2007. IEEE Computer Society.
A. Cohen, A. Pnueli, and L. D. Zuck. Mechanical verification of transactional memories with non-transactional memory accesses. In A. Gupta and S. Malik, editors, CAV, volume 5123 of LNCS, pages 121-134. Springer, 2008.
A. Cristal, B. K. Ozkan, E. Cohen, G. Kestor, I. Kuru, O. S. Unsal, S. Tasiran, S. O. Mutluergil, and T. Elmas. Verification tools for transactional programs. In Transactional Memory, volume 8913 of LNCS, pages 283-306. Springer, 2015.
J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. Verifying opacity of a transactional mutex lock. In FM, volume 9109 of LNCS, pages 161-177. Springer, 2015.
S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim. Isabelle files for a verification of a pessimistic STM algorithm. http://www.informatik.uni-augsburg.de/swt/projects/MSPessTM.html, 2016.
http://www.informatik.uni-augsburg.de/swt/projects/MSPessTM.html
S. Doherty, L. Groves, V. Luchangco, and M. Moir. Towards formally specifying and verifying transactional memory. Formal Asp. Comput., 25(5):769-799, 2013.
B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2):19, 2015.
M. Emmi, R. Majumdar, and R. Manevich. Parameterized verification of transactional memories. SIGPLAN Not., 45(6):134-145, June 2010.
R. Guerraoui, T. A. Henzinger, and V. Singh. Completeness and nondeterminism in model checking transactional memories. In F. van Breugel and M. Chechik, editors, CONCUR, pages 21-35. Springer, 2008.
R. Guerraoui, T. A. Henzinger, and V. Singh. Model checking transactional memories. DISC, 22(3):129-145, 2010.
R. Guerraoui and M. Kapalka. On the correctness of transactional memory. In PPOPP, pages 175-184, 2008.
R. Guerraoui and M. Kapalka. Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2010.
T. Harris, J. R. Larus, and R. Rajwar. Transactional Memory, 2nd edition. Synthesis Lectures on Computer Architecture. Morgan & Claypool Publishers, 2010.
C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321-332, 1983.
M. Lesani. On the Correctness of Transactional Memory Algorithms. PhD thesis, UCLA, 2014.
M. Lesani, V. Luchangco, and M. Moir. A framework for formally verifying software transactional memory algorithms. In M. Koutny and I. Ulidowski, editors, CONCUR 2012, pages 516-530, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.
Y. Li, Y. Zhang, Y.-Y. Chen, and M. Fu. Formal reasoning about lazy-STM programs. Journal of Computer Science and Technology, 25(4):841-852, 2010.
N. Lynch and F. Vaandrager. Forward and backward simulations. Information and Computation, 121(2):214-233, 1995.
N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In PODC, pages 137-151, 1987.
V. Luchangco M. Lesani and M. Moir. Putting opacity in its place. In WTTM, 2012.
A. Matveev and N. Shavit. Towards a Fully Pessimistic STM Model. In TRANSACT, 2012.
O. MÃ¼ller. I/O Automata and beyond: Temporal logic and abstraction in Isabelle. In J. Grundy and M. Newey, editors, TPHOLs, pages 331-348. Springer, 1998.
T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.
S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6:319-340, 1976.
N. Shavit and D. Touitou. Software transactional memory. DISC, 10(2):99-116, 1997.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode