Static prediction of heap space usage for first-order functional programs

We show how to efficiently obtain linear a priori bounds on the heap space consumption of first-order functional programs. The analysis takes space reuse by explicit deallocation into account and also furnishes an upper bound on the heap usage in the presence of garbage collection. It covers a wide variety of examples including, for instance, the familiar sorting algorithms for lists, including quicksort. The analysis relies on a type system with resource annotations. Linear programming (LP) is used to automatically infer derivations in this enriched type system. We also show that integral solutions to the linear programs derived correspond to programs that can be evaluated without any operating system support for memory management. The particular integer linear programs arising in this way are shown to be feasibly solvable under mild assumptions. Categories and Subject Descriptors F.3.2 [Logics and Meanings of Programs]: Seman

• Type: Conference
• Year: 2003
• Where: POPL
• Authors: Martin Hofmann, Steffen Jost
• Keywords: Enriched Type System, Familiar Sorting Algorithms, Particular Integer Linear, POPL 2003, Programming Languages