Document Open Access Logo

Owicki-Gries Reasoning for C11 RAR

Authors Sadegh Dalvandi , Simon Doherty , Brijesh Dongol , Heike Wehrheim

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.11.pdf
  • Filesize: 0.78 MB
  • 26 pages

Document Identifiers

Author Details

Sadegh Dalvandi
  • University of Surrey, United Kingdom
Simon Doherty
  • University of Sheffield, United Kingdom
Brijesh Dongol
  • University of Surrey, United Kingdom
Heike Wehrheim
  • Paderborn University, Germany

Funding

  • Dalvandi, Sadegh: Supported by EPSRC Grant EP/R032556/1.
  • Doherty, Simon: Supported by EPSRC Grant EP/R032351/1.
  • Dongol, Brijesh: Supported by EPSRC Grant EP/R032556/1.
  • Wehrheim, Heike: Supported by DFG grant WE 2290/12-1.

Cite AsGet BibTex

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. Owicki-Gries Reasoning for C11 RAR. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 11:1-11:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.11

Abstract

Owicki-Gries reasoning for concurrent programs uses Hoare logic together with an interference freedom rule for concurrency. In this paper, we develop a new proof calculus for the C11 RAR memory model (a fragment of C11 with both relaxed and release-acquire accesses) that allows all Owicki-Gries proof rules for compound statements, including non-interference, to remain unchanged. Our proof method features novel assertions specifying thread-specific views on the state of programs. This is combined with a set of Hoare logic rules that describe how these assertions are affected by atomic program steps. We demonstrate the utility of our proof calculus by verifying a number of standard C11 litmus tests and Peterson’s algorithm adapted for C11. Our proof calculus and its application to program verification have been fully mechanised in the theorem prover Isabelle.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Hoare logic
  • Theory of computation → Concurrency
  • Theory of computation → Operational semantics
  • Theory of computation → Program reasoning
Keywords
  • C11
  • Verification
  • Hoare logic
  • Owicki-Gries
  • Isabelle

Metrics

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

Supplementary Materials

References

  1. P. A. Abdulla, J. Arora, M. F. Atig, and S. N. Krishna. Verification of programs under the release-acquire semantics. In K. S. McKinley and K. Fisher, editors, PLDI, pages 1117-1132. ACM, 2019. Google Scholar
  2. P. Aziz Abdulla, S. Aronis, M. Faouzi Atig, B. Jonsson, C. Leonardsson, and K. Sagonas. Stateless model checking for TSO and PSO. Acta Inf., 54(8):789-818, 2017. URL: https://doi.org/10.1007/s00236-016-0275-0.
  3. J. Alglave and P. Cousot. Ogre and Pythia: an invariance proof method for weak consistency models. In G. Castagna and A. D. Gordon, editors, POPL, pages 3-18. ACM, 2017. Google Scholar
  4. J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig. Software verification for weak memory via program transformation. In M. Felleisen and P. Gardner, editors, ESOP, volume 7792 of LNCS, pages 512-532. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_28.
  5. J. Alglave, D. Kroening, and M. Tautschnig. Partial orders for efficient bounded model checking of concurrent software. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of LNCS, pages 141-157. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_9.
  6. J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1-7:74, 2014. Google Scholar
  7. K. R. Apt, F. S. de Boer, and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Texts in Computer Science. Springer, 2009. URL: https://doi.org/10.1007/978-1-84882-745-5.
  8. M. Batty, A. F. Donaldson, and J. Wickerson. Overhauling SC atomics in C11 and OpenCL. In POPL, pages 634-648. ACM, 2016. Google Scholar
  9. M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. Mathematizing C++ concurrency. In T. Ball and M. Sagiv, editors, POPL, pages 55-66. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926394.
  10. S. Böhme and T. Nipkow. Sledgehammer: Judgement day. In IJCAR, volume 6173 of Lecture Notes in Computer Science, pages 107-121. Springer, 2010. Google Scholar
  11. S. Dalvandi, B. Dongol, and S. Doherty. Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL. CoRR, abs/2004.02983, 2020. URL: http://arxiv.org/abs/2004.02983.
  12. S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Verifying C11 programs operationally. In J. K. Hollingsworth and I. Keidar, editors, PPoPP, pages 355-365. ACM, 2019. URL: https://doi.org/10.1145/3293883.3295702.
  13. S. Dolan, K. C. Sivaramakrishnan, and A. Madhavapeddy. Bounding data races in space and time. In PLDI, PLDI 2018, pages 242-255, New York, NY, USA, 2018. ACM. Google Scholar
  14. N. Gavrilenko, H. Ponce de Le'on, F. Furbach, K. Heljanko, and R. Meyer. BMC for weak memory models: Relation analysis for compact SMT encodings. In I. Dillig and S. Tasiran, editors, CAV, volume 11561 of LNCS, pages 355-365. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_19.
  15. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576-580, 1969. URL: https://doi.org/10.1145/363235.363259.
  16. J.-O. Kaiser, H.-H. Dang, D. Dreyer, O. Lahav, and V. Vafeiadis. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In P. Müller, editor, ECOOP, volume 74 of LIPIcs, pages 17:1-17:29. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2017.17.
  17. J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer. A promising semantics for relaxed-memory concurrency. In G. Castagna and A. D. Gordon, editors, POPL, pages 175-189. ACM, 2017. Google Scholar
  18. M. Kokologiannakis, O. Lahav, K. Sagonas, and V. Vafeiadis. Effective stateless model checking for C/C++ concurrency. PACMPL, 2(POPL):17:1-17:32, 2018. URL: https://doi.org/10.1145/3158105.
  19. M. Kokologiannakis, A. Raad, and V. Vafeiadis. Model checking for weakly consistent libraries. In K. S. McKinley and K. Fisher, editors, PLDI, pages 96-110. ACM, 2019. Google Scholar
  20. O. Lahav. Verification under causally consistent shared memory. SIGLOG News, 6(2):43-56, 2019. URL: https://doi.org/10.1145/3326938.3326942.
  21. O. Lahav and V. Vafeiadis. Owicki-Gries reasoning for weak memory models. In M. M. Halldórsson, K. Iwama, N. Kobayashi, and B. Speckmann, editors, ICALP, volume 9135 of LNCS, pages 311-323. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_25.
  22. O. Lahav, V. Vafeiadis, J. Kang, C.-K. Hur, and D. Dreyer. Repairing sequential consistency in C/C++11. In PLDI, pages 618-632. ACM, 2017. Google Scholar
  23. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers, 28(9):690-691, 1979. URL: https://doi.org/10.1109/TC.1979.1675439.
  24. T. Nipkow and L. P. Nieto. Owicki/Gries in Isabelle/HOL. In FASE, volume 1577 of Lecture Notes in Computer Science, pages 188-203. Springer, 1999. Google Scholar
  25. S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6:319-340, 1976. URL: https://doi.org/10.1007/BF00268134.
  26. L. C. Paulson. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow), volume 828 of LNCS. Springer, 1994. URL: https://doi.org/10.1007/BFb0030541.
  27. A. Podkopaev, I. Sergey, and A. Nanevski. Operational aspects of C/C++ concurrency. CoRR, abs/1606.01400, 2016. URL: http://arxiv.org/abs/1606.01400.
  28. H. Ponce de León, F. Furbach, K. Heljanko, and R. Meyer. BMC with memory models as modules. In N. Bjørner and A. Gurfinkel, editors, FMCAD, pages 1-9. IEEE, 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603021.
  29. A. J. Summers and P. Müller. Automating deductive verification for weak-memory programs. In D. Beyer and M. Huisman, editors, TACAS, volume 10805 of LNCS, pages 190-209. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89960-2_11.
  30. K. Svendsen, J. Pichon-Pharabod, M. Doko, O. Lahav, and V. Vafeiadis. A separation logic for a promising semantics. In A. Ahmed, editor, ESOP, volume 10801 of LNCS, pages 357-384. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_13.
  31. O. Travkin, A. Mütze, and H. Wehrheim. SPIN as a linearizability checker under weak memory models. In V. Bertacco and A. Legay, editors, HVC, volume 8244 of LNCS, pages 311-326. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03077-7_21.
  32. A. Turon, V. Vafeiadis, and D. Dreyer. GPS: navigating weak memory with ghosts, protocols, and separation. In A. P. Black and T. D. Millstein, editors, OOPSLA, pages 691-707. ACM, 2014. URL: https://doi.org/10.1145/2660193.2660243.
  33. J. Wickerson, M. Batty, T. Sorensen, and G. A. Constantinides. Automatically comparing memory consistency models. In G. Castagna and A. D. Gordon, editors, POPL, pages 190-204. ACM, 2017. Google Scholar
  34. A. Williams. https://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_C++0x_atomics.html, 2018. Accessed: 2018-06-20.
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 Imprint Privacy Contact