PRACTICAL LINEAR OBJECT OWNERSHIP SEMANTICS WITH APPLICATION IN PARALLEL MEMORY ALLOCATION: Likai Liu PhD Proposal
- Starts:
- 3:00 pm on Monday, February 25, 2013
- Ends:
- 5:00 pm on Monday, February 25, 2013
- Location:
- Hariri Institute
Abstract
Efficient and robust memory management is a hard problem. Garbage
collection promises automatic memory management but comes with the
cost of increased memory footprint, reduced parallelism in shared
memory multiprogramming, unpredictable pause time, and fickle tuning
parameters that must be optimized according to a combination of the
program's workload and the underlying hardware's capability in order
for an application to perform reasonably well. A wealth of research
mitigates all of the above problems to a certain extent, but
programmer error could still cause memory leak by erroneously keeping
memory references when they are no longer needed. What we need is a
methodology to encourage programmers to become resource aware, so that
efficient, scalable, predictable and high performance programs may be
written without the fear of resource leak.
Abstract Linear logic has been recognized as the formalism of choice
for resource tracking. The formalism requires explicit introduction
and elimination of resources, and otherwise 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 reintroduces 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.
Abstract This dissertation documents my research work that introduces
linear resource ownership semantics into C++, which is the fourth most
widely used programming language. The work is a library-based approach
by implementing linear pointer as a smart pointer object and checking
for linearity violations during runtime in debug builds. In release
builds, runtime checks are turned off, and the program incurs no
overhead. No other smart pointer enjoys this property of erasure like
linear pointers. Various linear data structures are implemented.
Parallel computing and non-blocking algorithms are also explored in
the context of linear pointers. And finally, a memory allocator is
implemented on top of linear data structures, thus proving the
feasibility of this approach in the real world and guaranteeing that
the memory management subsystem itself would not leak memory.
Ph.D. Thesis Committee:
Hongwei Xi (Advisor)
Richard West
Mark Crovella
Jonathan Appavoo (Chair)
