PDF

Description

We introduce a new region-based memory management technique that allows flexible memory usage patterns and is provably safe. Our technique is explicit and manual like C's malloc and free, and it allows programmers to exert a similar degree of control over the program behavior. Our method is quite simple in spite of this expressiveness and safety.

We apply the technique to a small functional language to formally describe the core concepts, prove its safety, and argue its usability and efficiency analytically. In particular, we show that the system can efficiently encode more rigid, traditional regions whose lifetime is bounded by that of a stack frame. We also show that the technique works nicely with multi-threaded and imperative programs.

Details

Files

Statistics

from
to
Export
Download Full History