Abstract: “In this dissertation, we study memory management strategies with an eye out for fitness to system programming.
First, we establish a framework to study memory management strategies. Often perceived as distinct categories, we argue that memory management approaches are actually part of a single design space. To this end, we establish a precise and powerful lexicon to describe memory management strategies of any kind. Using our newly established vocabulary, we further argue that this design space has not been exhaustively explored. We argue that one of the unexplored portion of this space, the static-automatic gap, contributes to the persistence of C in system programming.
Second, we develop asap: a new memory management technique that fits in the static-automatic gap. Asap is fully automatic (not even annotations are required) and makes heavy use of static analysis. At compile time it inserts, in the original program, code that deallocates memory blocks as they becomes useless. We then show how asap interacts with various, advanced language features. Specifically, we extend asap to support polymorphism and mutability.
Third, we compare asap with existing approaches. One of the points of comparison we use is the behavioural suitability to system programming. We also explore how the ideas from asap can be combined with other memory management strategies. We then show how asap handles programs satisfying the linear or region constraints. Finally, we explore the insights gained whilst developing and studying asap.”
@nickpsecurity, very interesting thesis. The caveats are on page 67:
I think mutation and separate compilation are only ones that would be potential problems for most coders in system setting. The mutation could be isolated with a different mechanism to check it. The separate compilation might be handled with a special linker. I’ve always thought a better linker was necessary anyway to prevent linker errors. Still extra work for anyone building on these techniques, though.
Mutation is addressed later in the thesis (chapter 6) in a refinement of the original model. Seems to make the analysis much more complex, particularly if you also want polymorphism.
The extra complexity seems to be a general problem we just covered here. ;) Of course, there’s more research all the time into automated methods for separation logic and other methods for handling that stuff. So, the question becomes whether one could mix that with the models having trouble with mutation. I didn’t dig into the paper enough to attempt to answer that.