3:00 pm on Monday, February 25, 2013
5:00 pm on Monday, February 25, 2013
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)