Proof-Carrying Garbage Collection

Safe programming languages such as Java and C# is capable of producing software systems that are free from some pitfalls often seen in software developed with traditional programming languages. However, all the existing safe languages rely on garbage collection mechanism for dynamic memory management. And some of their safety-related features, including the prevention of dangling pointer dereference and memory leak, are provided by garbage collection. Thus, the correctness of the underlying garbage collection is the key to the safety of these languages. Unfortunately, garbage collectors are extremely hard to implement correctly, and their interactions with mutators are often complex and error-prone. For increasing the safety of languages such as Java and C#, it is necessary to rigorously reason about the safety and correctness of garbage collection.This paper presents the Proof-Carrying Code style formal verification of two garbage collectors against their safety and correctness specifications, as well as the safe interaction between garbage collectors and various mutators, including codes constructed with Typed Assembly Language. The verification work presented is implemented as COQ proofs, and is thus machine-checkable and ready to be distributed in the form of Proof-Carrying Code.The work presented in this paper includes three major parts. The first part of work verifies two garbage collectors, namely stop-the-world mark-sweep and Yuasa incremental, against their safety and correctness specifications. The specifications, including some intricate invariants like the Weak Tri-color Invariant, are constructed using Separation-Logic style specification language. And the proof is constructed in a Hoare-style program logic.The second part of work introduces a new uniform approach to verify the safety of the interaction between mutator and garbage collector in Hoare-style program logic. Based on techniques like Abstract Data Type, this approach specifies garbage collector interfaces in an abstract way. Thus the verification of mutator is freed from reason- ing about the details of garbage collector. And the linking of the mutator verification against the verification of garbage collector is easier and more flexible.The final part of work studies the issue of type-safe garbage collection. It offers an approach of combining Typed Assembly Language with verified garbage collection. Using an open Proof-Carrying Code framework and the ideas in the second part of work, this approach successfully links the code constructed in a Typed Assembly Language with a proved conservative garbage collector, which includes showing that the collector's interface specifications are compatible with the typing rules of the Typed Assembly Language.Besides, this paper also discusses the COQ implementation issues of the work above, and introduces some ideas and techniques for improving productivity in proof construction.The work presented in this paper may effectively reduced the Trusted Computing Base of languages like Java and C#, as well as other safe programming systems using garbage collection. And the successful verification of complex garbage collector algorithms is also a valuable experience for Proof-Carrying Code style verification.