Automated verification of practical garbage collectors

DOI10.1145/1480881.1480935MaRDI QIDQ5261539zbMATH OpenOpenAlexFDO

Authors Chris Hawblitzel, Erez Petrank

Publication date 3 July 2015

Published in Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1004.3808

zbMATH Keywords

garbage collectionverification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the proofs were hand-written or the collectors were too simplistic to use on practical applications. In this work, we present two mechanically verified garbage collectors, both practical enough to use for real-world C# benchmarks. The collectors and their associated allocators consist of x86 assembly language instructions and macro instructions, annotated with preconditions, postconditions, invariants, and assertions. We used the Boogie verification generator and the Z3 automated theorem prover to verify this assembly language code mechanically. We provide measurements comparing the performance of the verified collector with that of the standard Bartok collectors on off-the-shelf C# benchmarks, demonstrating their competitiveness.

Recommendations

• Automated verification of practical garbage collectors
• A verified generational garbage collector for CakeML
• A verified generational garbage collector for CakeML
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Formal Verification of an Incremental Garbage Collector

Cited in

(9)

• Verifying a concurrent garbage collector using a rely-guarantee methodology
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• scientific article; zbMATH DE number 1670550 (Why is no real title available?)
• Automated verification of practical garbage collectors
• Practical Tactics for Separation Logic
• A verified generational garbage collector for CakeML
• A verified generational garbage collector for CakeML
• Reasoning about memory layouts
• A mechanically verified garbage collector for OCaml

Describes a project that uses

Uses Software

• z3
• Boogie

This page was built for publication: Automated verification of practical garbage collectors

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5261539)