Last modified: Wed Nov 25 05:59:26 2015 GMT.
Languages such as Java, C-sharp, Standard ML and Haskell use automated memory management to simplify development and improve reliability by eliminating the need for programmers to manually free unused objects. The cost of this improved programmer experience is that the implementation of the language becomes more complex, requiring a garbage collector (GC). Garbage collectors are becoming increasingly sophisticated to adapt them to high-performance, concurrent and real-time applications, making internal collector invariants and the interface with user programs (mutators in garbage collector parlance) subtle and difficult to implement correctly.
My thesis is that treating the garbage collected heap as an abstract data type allows the specification and verification of flexible and expressive garbage collector-mutator interfaces, and that the mechanized verification of garbage collector implementations using Hoare-style logic is both practical and effective. The mutator-garbage collector interface I describe in this paper is expressive enough to be used with verified mutators, while being abstract enough that a single interface can be used with both stop-the-world and incremental collectors. It is also powerful enough to be used with collectors that require read or write barriers.
In this dissertation, I describe my framework for the mechanized also describe the specification and verification of the Cheney and Baker copying collectors. The Baker collector is an incremental collector that requires a read barrier. Finally, I discuss some practical tools I developed for program verification using separation logic in the Coq proof assistant.