Ph.D. Thesis

SIMPLE, SAFE, AND EFFICIENT MEMORY MANAGEMENT
USING LINEAR POINTERS
by

LIKAI LIU

B.A., Boston University, 2004

Submitted in partial fulfillment of the
requirements for the degree of
Doctor of Philosophy
2014

Abstract

Efficient and safe memory management is a hard problem. Garbage collection promises automatic memory management but comes with the cost of increased memory foot- print, reduced parallelism in multi-threaded programs, unpredictable pause time, and intricate tuning parameters balancing the program’s workload and designated mem- ory usage in order for an application to perform reasonably well. Existing research mitigates the above problems to some extent, but programmer error could still cause memory leak by erroneously keeping memory references when they are no longer needed. We need a methodology for programmers to become resource aware, so that efficient, scalable, predictable and high performance programs may be written without the fear of resource leak.

Linear logic has been recognized as the formalism of choice for resource tracking. It requires explicit introduction and elimination of resources and guarantees that a resource cannot be implicitly shared or abandoned, hence must be linear. Early languages based on linear logic focused on Curry-Howard correspondence. They began by limiting the expressive powers of the language and then reintroduced them by allowing controlled sharing which is necessary for recursive functions. However, only by deviating from Curry-Howard correspondence could later development actually address programming errors in resource usage.

The contribution of this dissertation is a simple, safe, and efficient approach in- troducing linear resource ownership semantics into C++ (which is still a widely used language after 30 years since inception) through linear pointer, a smart pointer in- spired by linear logic. By implementing various linear data structures and a parallel, multi-threaded memory allocator based on these data structures, this work shows that linear pointer is practical and efficient in the real world, and that it is possible to build a memory management stack that is entirely leak free. The dissertation offers some closing remarks on the difficulties that must be addressed in order to support formal reasoning about a concurrent linear data algorithm.

View as PDF (962kb)