nach oben

Erschienen in:

01.11.2018

Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology

verfasst von: Yannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Vorheriger Artikel A Verified Generational Garbage Collector for CakeML

Nächster Artikel Formalization of the Fundamental Group in Untyped Set Theory Using Auto2

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

We present a simplified pseudo-code of the MGC, with variable

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9489-x/MediaObjects/10817_2018_9489_Figco_HTML.gif

, field

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9489-x/MediaObjects/10817_2018_9489_Figcp_HTML.gif

, and value

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9489-x/MediaObjects/10817_2018_9489_Figcq_HTML.gif

assumed non-deterministically chosen from the thread environment. The actual definition in Coq is an operational characterization of this thread system.

The write barrier in [8] avoids marking old in some cases. We drop this optimization.

Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1–3), 227–270 (2007)MathSciNetCrossRefMATH

Davis, J., Myreen, M.O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it). J. Autom. Reason. 55(2), 117–183 (2015)MathSciNetCrossRefMATH

De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software (TACAS) (2008)

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)

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)CrossRefMATH

Doligez, D., Gonthier, G.: Portable, unobtrusive garbage collection for multiprocessor systems. In: Symposium on Principles of Programming Languages (POPL) (1994)

Doligez, D., Leroy, X.: A concurrent, generational garbage collector for a multithreaded implementation of ML. In: Symposium on Principles of Programming Languages (POPL) (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: International Symposium on Memory Management (ISMM) (2000)

Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: Symposium on Principles of Programming Languages (POPL) (2009)

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)

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, J.M.: Linearizability: a correctness condition for concurrent objects. Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463–492 (1990)CrossRef

17.

Jagannathan, S., Laporte, V., Petri, G., Pichardie, D., Vitek, J.: Atomicity refinement for verified compilation. Trans. Program. Lang. Syst. (TOPLAS) 36(2), 6 (2014)

18.

Jones, C.B.: Tentative steps toward a development method for interfering programs. Trans. Program. Lang. Syst. (TOPLAS) 5(4), 596–619 (1983)CrossRefMATH

19.

Jones, R., Hosking, A., Moss, E.: The Garbage Collection Handbook. Chapman & Hall, London (2011)CrossRef

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)

22.

Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. Trans. Program. Lang. Syst. (TOPLAS) 36(1), 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)

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(4), 319–340 (1976)MathSciNetCrossRefMATH

29.

Pavlovic, D., Pepper, P., Smith, D.R.: Formal derivation of concurrent garbage collectors. In: International Conference on Mathematics of Program Construction (MPC) (2010)

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)

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, M.O., Åman Pohjola, J.: A verified generational garbage collector for CakeML. In: Ayala-Rincón, M., Muñoz, C. (eds.) Interactive Theorem Proving, pp. 444–461. Springer, Cham (2017)CrossRef

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, F.Z., Jagannathan, S., Sewell, P.: CompcertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22 (2013)MathSciNetMATH

37.

Torp-Smith, N., Birkedal, L., Reynolds, J.C.: Local reasoning about a copying garbage collector. Trans. Program. Lang. Syst. (TOPLAS) 30(4), 24 (2008)MATH

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)MathSciNetCrossRefMATH

40.

Vafeiadis, V., Parkinson, M.J.: A marriage of rely/guarantee and separation logic. In: International Conference on Concurrency Theory (CONCUR) (2007)

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

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)

Titel: Verifying a Concurrent Garbage Collector with a Rely-Guarantee Methodology
verfasst von: Yannick Zakowski
David Cachera
Delphine Demange
Gustavo Petri
David Pichardie
Suresh Jagannathan
Jan Vitek
Publikationsdatum: 01.11.2018
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 2/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9489-x

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2019

Call-by-Value Lambda Calculus as a Model of Computation in Coq

Effect Polymorphism in Higher-Order Logic (Proof Pearl)

Formalization of the Fundamental Group in Untyped Set Theory Using Auto2

Guarded Cubical Type Theory

CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory