×

Verifying a concurrent garbage collector with a rely-guarantee methodology. (English) Zbl 1468.68068

Summary: Concurrent garbage collection algorithms are a challenge for program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the Rely-Guarantee proof technique. We design a compiler intermediate representation with strong type guarantees, dedicated support for abstract concurrent data structures, and high-level iterators on runtime internals. In addition, we define an Rely-Guarantee program logic supporting an incremental proof methodology where annotations and invariants can be progressively enriched. We formalize the intermediate representation, the proof system, and prove the soundness of the methodology in the Coq proof assistant. Equipped with this, we prove a fully concurrent garbage collector where mutators never have to wait for the collector.

MSC:

68N20 Theory of compilers and interpreters
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI HAL

References:

[1] Brookes, S., A semantics for concurrent separation logic, Theor. Comput. Sci., 375, 227-270, (2007) · Zbl 1111.68021
[2] Davis, J.; Myreen, MO, The reflective Milawa theorem prover is sound (down to the machine code that runs it), J. Autom. Reason., 55, 117-183, (2015) · Zbl 1356.68186
[3] De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software (TACAS) (2008)
[4] Demange, D., Laporte, V., Zhao, L., Jagannathan, S., Pichardie, D., Vitek, J.: Plan B: a buffered memory model for Java. In: Symposium on Principles of Programming Languages (POPL) (2013) · Zbl 1301.68098
[5] Dijkstra, EW; Lamport, L.; Martin, AJ; Scholten, CS; Steffens, EFM, On-the-fly garbage collection: an exercise in cooperation, Commun. ACM, 21, 966-975, (1978) · Zbl 0386.68024
[6] Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Symposium on Principles of Programming Languages (POPL) (1994)
[7] Doligez, D., Leroy, X.: A concurrent, generational garbage collector for a multithreaded implementation of ML. In: Symposium on Principles of Programming Languages (POPL) (1993)
[8] Domani, T., Kolodner, E.K., Lewis, E., Salant, E.E., Barabash, K., Lahan, I., Levanoni, Y., Petrank, E., Yanover, I.: Implementing an on-the-fly garbage collector for Java. In: International Symposium on Memory Management (ISMM) (2000)
[9] Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Symposium on Principles of Programming Languages (POPL) (2009) · Zbl 1315.68087
[10] Gammie, P., Hosking, A.L., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Programming Language Design and Implementation (PLDI) (2015)
[11] Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: International Conference on Computer Aided Verification (CAV) (1996)
[12] Havelund, K.: Mechanical verification of a garbage collector. In: International Parallel Processing Symposium and Symposium on Parallel and Distributed Processing (IPPS/SPDP) (1999)
[13] Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: Conference on Operating Systems Design and Implementation (OSDI) (2014)
[14] Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. In: Symposium on Principles of Programming Languages (POPL) (2009) · Zbl 1315.68096
[15] Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: International Conference on Computer Aided Verification (CAV) (2015)
[16] Herlihy, M.; Wing, JM, Linearizability: a correctness condition for concurrent objects, Trans. Program. Lang. Syst. (TOPLAS), 12, 463-492, (1990)
[17] Jagannathan, S.; Laporte, V.; Petri, G.; Pichardie, D.; Vitek, J., Atomicity refinement for verified compilation, Trans. Program. Lang. Syst. (TOPLAS), 36, 6, (2014)
[18] Jones, CB, Tentative steps toward a development method for interfering programs, Trans. Program. Lang. Syst. (TOPLAS), 5, 596-619, (1983) · Zbl 0517.68032
[19] Jones, R., Hosking, A., Moss, E.: The Garbage Collection Handbook. Chapman & Hall, London (2011)
[20] Leino, R.: This is boogie 2 (2008). https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/
[21] Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: Symposium on Principles of Programming Languages (POPL) (2012) · Zbl 1321.68201
[22] Liang, H.; Feng, X.; Fu, M., Rely-guarantee-based simulation for compositional verification of concurrent program transformations, Trans. Program. Lang. Syst. (TOPLAS), 36, 3, (2014)
[23] McCreight, A., Chevalier, T., Tolmach, A.: A certified framework for compiling and executing garbage-collected languages. In: International Conference on Functional Programming (ICFP) (2010) · Zbl 1323.68136
[24] McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: Programming Language Design and Implementation (PLDI) (2007)
[25] Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Symposium on Principles of Distributed Computing (PODC) (1996)
[26] Myreen, M.O.: Reusable verification of a copying collector. In: Conference on Verified Software: Theories, Tools, Experiments (VSTTE) (2010)
[27] O’Hearn, P.W.: Separation logic and concurrent resource management. In: International Symposium on Memory Management (ISMM) (2007)
[28] Owicki, S.; Gries, D., An axiomatic proof technique for parallel programs I, Acta Inform., 6, 319-340, (1976) · Zbl 0312.68011
[29] Pavlovic, D., Pepper, P., Smith, D.R.: Formal derivation of concurrent garbage collectors. In: International Conference on Mathematics of Program Construction (MPC) (2010) · Zbl 1286.68090
[30] Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Programming Language Design and Implementation (PLDI) (1988)
[31] Pizlo, F., Ziarek, L., Maj, P., Hosking, A.L., Blanton, E., Vitek, J.: Schism: fragmentation-tolerant real-time garbage collection. In: Programming Language Design and Implementation (PLDI) (2010)
[32] Prensa Nieto, L.: the rely-guarantee method in Isabelle/HOL. In: European Conference on Programming (ESOP) (2003) · Zbl 1032.68130
[33] Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS) (2002)
[34] Sandberg Ericsson, A.; Myreen, MO; Åman Pohjola, J.; Ayala-Rincón, M. (ed.); Muñoz, C. (ed.), A verified generational garbage collector for CakeML, 444-461, (2017), Cham · Zbl 1468.68065
[35] Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Programming Language Design and Implementation (PLDI) (2015)
[36] Ševčík, J.; Vafeiadis, V.; Nardelli, FZ; Jagannathan, S.; Sewell, P., CompcertTSO: a verified compiler for relaxed-memory concurrency, J. ACM, 60, 22, (2013) · Zbl 1281.68072
[37] Torp-Smith, N.; Birkedal, L.; Reynolds, JC, Local reasoning about a copying garbage collector, Trans. Program. Lang. Syst. (TOPLAS), 30, 24, (2008) · Zbl 1325.68041
[38] Treiber, R.K.: Systems programming: coping with parallelism. Technical report, IBM Almaden Research Center (1986)
[39] Vafeiadis, V., Concurrent separation logic and operational semantics, Electron. Notes Theor. Comput. Sci., 276, 335-351, (2011) · Zbl 1342.68104
[40] Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guarantee and separation logic. In: International Conference on Concurrency Theory (CONCUR) (2007) · Zbl 1151.68556
[41] Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Programming Language Design and Implementation (PLDI) (2010)
[42] Zakowski, Y., Cachera, D., Demange, D., Petri, G., Pichardie, D., Jagannathan, S., Vitek, J.: Verifying a concurrent garbage collector using a rely-guarantee methodology—companion website (2017). http://www.irisa.fr/celtique/ext/cgc/. Accessed 31 Oct 2018 · Zbl 1468.68067
[43] Zakowski, Y., Cachera, D., Demange, D., Pichardie, D.: Compilation of linearizable data structures—a mechanised RG logic for semantic refinement. In: Symposium on Applied Computing (SAC) (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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.