Abstract
Concurrent garbage collection algorithms are an emblematic challenge in the area of concurrent program verification. In this paper, we address this problem by proposing a mechanized proof methodology based on the popular Rely-Guarantee (RG) proof technique. We design a specific compiler intermediate representation (IR) with strong type guarantees, dedicated support for abstract concurrent data structures, and high-level iterators on runtime internals. In addition, we define an RG program logic supporting an incremental proof methodology where annotations and invariants can be progressively enriched.
We formalize the IR, the proof system, and prove the soundness of the methodology in the Coq proof assistant. Equipped with this IR, we prove a fully concurrent garbage collector where mutators never have to wait for the collector.
This material is based upon work supported by grants ANR 14-CE28-0004, NSF CCF-1318227, CCF-1544542, SHF-1518844 and ONR N00014-15-1-2332.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
We present a simplified pseudo-code of the MGC, with variable x, field f, and value v assumed non-deterministically chosen from the thread environment. The actual definition in Coq is an operational characterization of this thread system.
- 2.
The write barrier in [5] avoids marking old in some cases. We drop this optimization.
References
Demange, D., Laporte, V., Zhao, L., Jagannathan, S., Pichardie, D., Vitek, J., Plan, B.: a buffered memory model for java. In: POPL 2013, pp. 329–342 (2013)
Dijkstra, E.W., Lamport, L., Martin, A.J., Scholten, C.S., Steffens, E.F.M.: On-the-fly garbage collection: an exercise in cooperation. Commun. ACM 21(11), 966–975 (1978)
Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Proceedings POPL 1994, pp. 70–83 (1994)
Doligez, D., Leroy, X.: A concurrent, generational garbage collector for a multithreaded implementation of ML. In: Proceedings of POPL 1993, pp. 113–123 (1993)
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: Proceedings of ISMM 2000, pp. 155–166 (2000)
Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Proceedings of POPL 2009, pp. 2–15 (2009)
Zakowski, Y., et al.: Verifying a concurrent garbage collector using an RG methodology (2017). http://www.irisa.fr/celtique/ext/cgc/
Gammie, P., Hosking, A.L., Engelhardt, K.: Relaxing safely: verified on-the-fly garbage collection for x86-TSO. In: Proceedings of PLDI 2015, pp. 99–109 (2015)
Gonthier, G.: Verifying the safety of a practical concurrent garbage collector. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 462–465. Springer, Heidelberg (1996). doi:10.1007/3-540-61474-5_103
Havelund, K.: Mechanical verification of a garbage collector. In: Rolim, J., et al. (eds.) IPPS 1999. LNCS, vol. 1586, pp. 1258–1283. Springer, Heidelberg (1999). doi:10.1007/BFb0098007
Hawblitzel, C., Petrank, E.: Automated verification of practical garbage collectors. In: Proceedings of POPL 2009, pp. 441–453 (2009)
Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 449–465. Springer, Cham (2015). doi:10.1007/978-3-319-21668-3_26
Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Jagannathan, S., Laporte, V., Petri, G., Pichardie, D., Vitek, J.: Atomicity refinement for verified compilation. ACM Trans. Program. Lang. Syst. 36(2), 6:1–6:30 (2014)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)
Jones, R., Hosking, A., Moss, E.: Handbook, The Garbage Collection: The Art of Automatic Memory Management, 1st edn. Chapman & Hall/CRC, Boca Raton (2011)
Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst. 36, 3 (2014)
McCreight, A., Chevalier, T., Tolmach, A.P.: A certified framework for compiling and executing garbage-collected languages. In: Proceedings of ICFP 2010, pp. 273–284 (2010)
Myreen, M.O.: Reusable Verification of a Copying Collector. In: VSTTE 2010 (2010)
Pizlo, F., Ziarek, L., Maj, P., Hosking, A.L., Blanton, E., Vitek, J.: Schism: fragmentation-tolerant real-time garbage collection. In: Proceedings of PLDI (2010)
Nieto, L.P.: The rely-guarantee method in Isabelle/HOL. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 348–362. Springer, Heidelberg (2003). doi:10.1007/3-540-36575-3_24
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS 2002, pp. 55–74 (2002)
Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: Proceedings of PLDI 2015, pp. 77–87. ACM (2015)
Vafeiadis, V.: Concurrent separation logic and operational semantics. Electron. Notes Theor. Comput. Sci. 276, 335–351 (2011)
Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74407-8_18
Zakowski, Y., Cachera, D., Demange, D., Pichardie, D.: Compilation of linearizable data structures - a mechanised RG logic for semantic refinement. Technical report (2017). https://hal.archives-ouvertes.fr/hal-01538128
Acknowledgement
We thank the anonymous reviewers and Peter Gammie for their thorough comments and suggestions on how to improve the final version of the paper. We also thank Vincent Laporte for his work earlier in this project, and his help on implementing parts of the garbage collector presented here.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Zakowski, Y. et al. (2017). Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-66107-0_31
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66106-3
Online ISBN: 978-3-319-66107-0
eBook Packages: Computer ScienceComputer Science (R0)