×

Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL. (English) Zbl 07498610

Summary: Weak memory presents a new challenge for program verification and has resulted in the development of a variety of specialised logics. For C11-style memory models, our previous work has shown that it is possible to extend Hoare logic and Owicki-Gries reasoning to verify correctness of weak memory programs. The technique introduces a set of high-level assertions over C11 states together with a set of basic Hoare-style axioms over atomic weak memory statements (e.g. reads/writes), but retains all other standard proof obligations for compound statements. This paper takes this line of work further by introducing the first deductive verification environment in Isabelle/HOL for C11-like weak memory programs. This verification environment is built on the Nipkow and Nieto’s encoding of Owicki-Gries in the Isabelle theorem prover. We exemplify our techniques over several litmus tests from the literature and two non-trivial examples: Peterson’s algorithm and a read-copy-update algorithm adapted for C11. For the examples we consider, the proof outlines can be automatically discharged using the existing Isabelle tactics developed by Nipkow and Nieto. The benefit here is that programs can be written using a familiar pseudocode syntax with assertions embedded directly into the program.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abdulla, PA; Aronis, S.; Atig, MF; Jonsson, B.; Leonardsson, C.; Sagonas, K., Stateless model checking for TSO and PSO, Acta Inf., 54, 8, 789-818 (2017) · Zbl 1380.68265 · doi:10.1007/s00236-016-0275-0
[2] Alglave, J., Cousot, P.: Ogre and Pythia: an invariance proof method for weak consistency models. In: Castagna, G., Gordon, A.D. (eds.) POPL, pp. 3-18. ACM (2017) · Zbl 1380.68101
[3] Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M. Gardner, P. (eds.) ESOP, LNCS, vol. 7792, pp. 512-532. Springer (2013) · Zbl 1381.68143
[4] Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV, LNCS, vol. 8044, pp. 141-157. Springer (2013)
[5] Apt, KR; de Boer, FS; Olderog, E., Verification of Sequential and Concurrent Programs. Texts in Computer Science (2009), Berlin: Springer, Berlin · Zbl 1183.68361 · doi:10.1007/978-1-84882-745-5
[6] Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 55-66. ACM (2011) · Zbl 1284.68165
[7] Böhme, S., Nipkow, T.: Sledgehammer: judgement day. In: IJCAR, Lecture Notes in Computer Science, vol. 6173, pp. 107-121. Springer (2010) · Zbl 1291.68327
[8] Dalvandi, M., Dongol, B.: Towards deductive verification of C11 programs with Event-B and ProB. In: Proceedings of the 21st Workshop on Formal Techniques for Java-like Programs, p. 4. ACM (2019)
[9] Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Owicki-Gries reasoning for C11 RAR. In: Hirschfeld, R., Pape, T. (eds.) ECOOP, LIPIcs, vol. 166, pp. 11:1-11:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). doi:10.4230/LIPIcs.ECOOP.2020.11
[10] Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Isabelle files for “Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL” (2021). doi:10.6084/m9.figshare.14387201.v1. https://figshare.com/articles/software/Isabelle_Files_for_Integrating_Owicki-Gries_for_C11-Style_Memory_Models_into_Isabelle_HOL_/14387201
[11] Dan, A.; Meshman, Y.; Vechev, M.; Yahav, E., Effective abstractions for verification under relaxed memory models, Comput. Lang. Syst. Struct., 47, 62-76 (2017) · Zbl 1379.68237
[12] de Roever, WP; de Boer, FS; Hannemann, U.; Hooman, J.; Lakhnech, Y.; Poel, M.; Zwiers, J., Concurrency Verification: Introduction to Compositional and Noncompositional Methods, Cambridge Tracts in Theoretical Computer Science (2001), Cambridge: Cambridge University Press, Cambridge · Zbl 1009.68020
[13] Desnoyers, M.; McKenney, PE; Stern, AS; Dagenais, MR; Walpole, J., User-level implementations of read-copy update, IEEE Trans. Parallel Distrib. Syst., 23, 2, 375-382 (2012) · doi:10.1109/TPDS.2011.159
[14] Doherty, S., Dongol, B., Wehrheim, H., Derrick, J.: Verifying C11 programs operationally. In: Hollingsworth, J.K., Keidar, I. (eds.) PPoPP, pp. 355-365. ACM (2019)
[15] Doko, M., Vafeiadis, V.: A program logic for C11 memory fences. In: VMCAI, LNCS, vol. 9583, pp. 413-430. Springer (2016) · Zbl 1475.68083
[16] Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: ESOP, pp. 448-475 (2017) · Zbl 1485.68061
[17] Dolan, S., Sivaramakrishnan, K., Madhavapeddy, A.: Bounding data races in space and time. In: PLDI, PLDI 2018, pp. 242-255. ACM, New York, NY, USA (2018)
[18] Gavrilenko, N., Ponce de Le’on, H., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) CAV, LNCS, vol. 11561, pp. 355-365. Springer (2019). doi:10.1007/978-3-030-25540-4_19
[19] Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[20] Jeannet, B., Relational interprocedural verification of concurrent programs, Softw. Syst. Model., 12, 2, 285-306 (2013) · doi:10.1007/s10270-012-0230-7
[21] Kaiser, J., Dang, H., Dreyer, D., Lahav, O., Vafeiadis, V.: Strong logic for weak memory: reasoning about release-acquire consistency in Iris. In: Müller, P. (ed.) ECOOP, LIPIcs, vol. 74, pp. 17:1-17:29. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)
[22] Kang, J., Hur, C., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL, pp. 175-189. ACM (2017) · Zbl 1380.68103
[23] Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C/C++ concurrency. PACMPL 2(POPL), 17:1-17:32 (2018)
[24] Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: McKinley, K.S., Fisher, K. (eds.) PLDI, pp. 96-110. ACM (2019)
[25] Lahav, O., Verification under causally consistent shared memory, SIGLOG News, 6, 2, 43-56 (2019) · doi:10.1145/3326938.3326942
[26] Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP, LNCS, vol. 9135, pp. 311-323. Springer (2015) · Zbl 1440.68046
[27] Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing sequential consistency in C/C++11. In: PLDI, pp. 618-632. ACM (2017)
[28] Lamport, L., How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Trans. Comput., 28, 9, 690-691 (1979) · Zbl 0419.68045 · doi:10.1109/TC.1979.1675439
[29] Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 41-62. Springer (2016) · Zbl 1475.68191
[30] Nipkow, T., Nieto, L.P.: Owicki/Gries in Isabelle/HOL. In: FASE, Lecture Notes in Computer Science, vol. 1577, pp. 188-203. Springer (1999)
[31] Owicki, SS; Gries, D., An axiomatic proof technique for parallel programs I, Acta Inf., 6, 319-340 (1976) · Zbl 0312.68011 · doi:10.1007/BF00268134
[32] Paulson, L.C.: Isabelle—A Generic Theorem Prover (with a contribution by T. Nipkow), LNCS, vol. 828. Springer (1994) · Zbl 0825.68059
[33] Paviotti, M., Cooksey, S., Paradis, A., Wright, D., Owens, S., Batty, M.: Modular relaxed dependencies in weak memory concurrency. In: Müller, P. (ed.) ESOP, LNCS, vol. 12075, pp. 599-625. Springer (2020). doi:10.1007/978-3-030-44914-8_22 · Zbl 1508.68045
[34] Podkopaev, A., Sergey, I., Nanevski, A.: Operational aspects of C/C++ concurrency. CoRR abs/1606.01400 (2016) . https://arxiv.org/abs/1606.01400
[35] Ponce de León, H., Furbach, F., Heljanko, K., Meyer, R.: BMC with memory models as modules. In: Bjørner, N., Gurfinkel, A. (eds.) FMCAD, pp. 1-9. IEEE (2018)
[36] Summers, A.J., Müller, P.: Automating deductive verification for weak-memory programs. In: Beyer, D., Huisman, M. (eds.) TACAS, LNCS, vol. 10805, pp. 190-209. Springer (2018) · Zbl 1423.68111
[37] Svendsen, K., Pichon-Pharabod, J., Doko, M., Lahav, O., Vafeiadis, V.: A separation logic for a promising semantics. In: Ahmed, A. (ed.) ESOP, LNCS, vol. 10801, pp. 357-384. Springer (2018) · Zbl 1422.68037
[38] Travkin, O., Mütze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V. Legay, A. (eds.) HVC, LNCS, vol. 8244, pp. 311-326. Springer (2013)
[39] Turon, A., Vafeiadis, V., Dreyer, D.: GPS: navigating weak memory with ghosts, protocols, and separation. In: Black, A.P., Millstein, T.D. (eds.) OOPSLA, pp. 691-707. ACM (2014)
[40] Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, pp. 867-884 (2013)
[41] Williams, A.: https://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_C++0x_atomics.html (2018). Accessed 20 June 2018
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.