In previous work, Hallenberg et al. [1] have integrated region-based memory management with a Cheney-style copying garbage collection algorithm. In this talk, we prove the safety of the integration, which relies on a refinement of the region typing rules that forbid dangling pointers during evaluation.

To accommodate the triggering of garbage collection at any step in the evaluation process, we base our type-safety result for the region-based system on a small-step contextual semantics and show that whenever a well-typed expression reduces to another expression, possibly by deallocating a region, then no dangling pointers are introduced. Because there are no dangling pointers in the initial heap, no dangling pointers appears during evaluation.

The memory discipline, which combines garbage collection and region-based memory management, is implemented for Standard ML in the ML Kit compiler. Although in principle the refinement of the region typing rules lead to less flexibility and can cause worse memory behaviour than when dangling pointers are permitted, experiments show that for a range of benchmark programs, the refinement has little effect on the overall memory behaviour.

[1] Niels Hallenberg, Martin Elsman, and Mads Tofte. Combining Region Inference and Garbage Collection. In ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI'02). Berlin, Germany. June 2002.