Amortised Memory Analysis Using the Depth of Data Structures

Amortised Memory Analysis Using the Depth of Data Structures

2009 | Brian Campbell
The paper presents a new stack space analysis for functional programs, inspired by Hofmann and Jost's heap space analysis. The analysis uses the depth of data structures to bound stack space requirements, allowing for more precise bounds compared to linear bounds. The key innovation is the introduction of structured typing contexts, which represent the form of the bounds (maxima and sums) and enable the use of max-plus expressions. The type system ensures that the assigned potential is sufficient to cover all stack space requirements, and an inference procedure based on Linear Programming is used to determine the exact bounds. The paper includes examples, a soundness proof, and discussions on extensions and related work. The analysis is implemented in Standard ML and has been applied to infer bounds for functional heap sort and other programs.The paper presents a new stack space analysis for functional programs, inspired by Hofmann and Jost's heap space analysis. The analysis uses the depth of data structures to bound stack space requirements, allowing for more precise bounds compared to linear bounds. The key innovation is the introduction of structured typing contexts, which represent the form of the bounds (maxima and sums) and enable the use of max-plus expressions. The type system ensures that the assigned potential is sufficient to cover all stack space requirements, and an inference procedure based on Linear Programming is used to determine the exact bounds. The paper includes examples, a soundness proof, and discussions on extensions and related work. The analysis is implemented in Standard ML and has been applied to infer bounds for functional heap sort and other programs.
Reach us at info@study.space