Automated Verification of Practical Garbage Collectors

TL;DR

This paper presents two practically verified garbage collectors for real-world C# applications, using formal methods and automated theorem proving to ensure correctness and performance.

Contribution

It introduces two mechanically verified garbage collectors implemented in assembly, verified with Boogie and Z3, suitable for real-world use and benchmarked against standard collectors.

Findings

Verified collectors are competitive in performance.

Use of formal verification ensures correctness.

Applicable to real-world C# benchmarks.

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.