Document Open Access Logo

Proving Opacity of a Pessimistic STM

Authors Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2016.35.pdf
  • Filesize: 0.64 MB
  • 17 pages

Document Identifiers

Author Details

Simon Doherty
Brijesh Dongol
John Derrick
Gerhard Schellhorn
Heike Wehrheim

Cite As Get BibTex

Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. Proving Opacity of a Pessimistic STM. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.OPODIS.2016.35

Abstract

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.

Subject Classification

Keywords
  • Pessimistic STMs
  • Opacity
  • Verification
  • Isabelle
  • Simulation
  • TMS2

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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. Google Scholar
  2. 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.
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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.
  9. S. Doherty, L. Groves, V. Luchangco, and M. Moir. Towards formally specifying and verifying transactional memory. Formal Asp. Comput., 25(5):769-799, 2013. Google Scholar
  10. B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2):19, 2015. Google Scholar
  11. M. Emmi, R. Majumdar, and R. Manevich. Parameterized verification of transactional memories. SIGPLAN Not., 45(6):134-145, June 2010. Google Scholar
  12. 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. Google Scholar
  13. R. Guerraoui, T. A. Henzinger, and V. Singh. Model checking transactional memories. DISC, 22(3):129-145, 2010. Google Scholar
  14. R. Guerraoui and M. Kapalka. On the correctness of transactional memory. In PPOPP, pages 175-184, 2008. Google Scholar
  15. R. Guerraoui and M. Kapalka. Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2010. Google Scholar
  16. T. Harris, J. R. Larus, and R. Rajwar. Transactional Memory, 2nd edition. Synthesis Lectures on Computer Architecture. Morgan & Claypool Publishers, 2010. Google Scholar
  17. C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321-332, 1983. Google Scholar
  18. M. Lesani. On the Correctness of Transactional Memory Algorithms. PhD thesis, UCLA, 2014. Google Scholar
  19. 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. Google Scholar
  20. 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. Google Scholar
  21. N. Lynch and F. Vaandrager. Forward and backward simulations. Information and Computation, 121(2):214-233, 1995. Google Scholar
  22. N. A. Lynch and M. R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In PODC, pages 137-151, 1987. Google Scholar
  23. V. Luchangco M. Lesani and M. Moir. Putting opacity in its place. In WTTM, 2012. Google Scholar
  24. A. Matveev and N. Shavit. Towards a Fully Pessimistic STM Model. In TRANSACT, 2012. Google Scholar
  25. 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. Google Scholar
  26. T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  27. S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6:319-340, 1976. Google Scholar
  28. N. Shavit and D. Touitou. Software transactional memory. DISC, 10(2):99-116, 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact