Amortised Memory Analysis Using the Depth of Data Structures

Amortised Memory Analysis Using the Depth of Data Structures

2009 | Brian Campbell
This paper presents a type-based amortized analysis for bounding stack space requirements in functional programs, extending Hofmann and Jost's heap space analysis. The analysis uses the depth of data structures and expresses potential in terms of maxima and sums. It introduces a type system with structured contexts to represent bounds and an inference procedure based on linear programming. The system allows precise bounds for tree-structured data, using max-plus expressions on depth. The type system includes structural rules to manipulate contexts and ensures that the potential assigned to the input is an upper bound on the required stack space. The analysis is sound, as proven by Theorem 1, and can be used to certify bounds in a proof-carrying code system. The paper also discusses limitations when analyzing nested data structures and presents extensions to the analysis, including handling containers and resource polymorphism. The system is implemented in Standard ML and available online. The work relates to other analyses based on sized types and recurrence solvers for cost estimation.This paper presents a type-based amortized analysis for bounding stack space requirements in functional programs, extending Hofmann and Jost's heap space analysis. The analysis uses the depth of data structures and expresses potential in terms of maxima and sums. It introduces a type system with structured contexts to represent bounds and an inference procedure based on linear programming. The system allows precise bounds for tree-structured data, using max-plus expressions on depth. The type system includes structural rules to manipulate contexts and ensures that the potential assigned to the input is an upper bound on the required stack space. The analysis is sound, as proven by Theorem 1, and can be used to certify bounds in a proof-carrying code system. The paper also discusses limitations when analyzing nested data structures and presents extensions to the analysis, including handling containers and resource polymorphism. The system is implemented in Standard ML and available online. The work relates to other analyses based on sized types and recurrence solvers for cost estimation.
Reach us at info@study.space
[slides] Amortised Memory Analysis Using the Depth of Data Structures | StudySpace