Paper Info
Title
"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis
Abstract
Bounding resource usage is important for a number of areas, notably real-time embedded systems and safety-critical systems. In this paper, we present a fully automatic static type-based analysis for inferring upper bounds on resource usage for programs involving general algebraic datatypes and full recursion. Our method can easily be used to bound any countable resource, without needing to revisit proofs. We apply the analysis to the important metrics of worst-case execution time, stack- and heap-space usage. Our results from several realistic embedded control applications demonstrate good matches between our inferred bounds and measured worst-case costs for heap and stack usage. For time usage we infer good bounds for one application. Where we obtain less tight bounds, this is due to the use of software floating-point libraries.
Year
DOI
Venue
2009
10.1007/978-3-642-05089-3_23
FM
Keywords
Field
DocType
bounding resource usage,automatic static type-based analysis,heap-space usage,good bound,countable resource,amortised analysis,carbon credits,important metrics,time usage,resource-bounded computations,resource usage,real-time embedded system,good match,upper bound,worst case execution time,carbon credit,floating point
Countable set,Algebraic number,Computer science,Real-time computing,Theoretical computer science,Heap (data structure),Mathematical proof,Software,Recursion,Bounding overwatch,Bounded function
Conference
Volume
ISSN
Citations 
5850
0302-9743
20
PageRank 
References 
Authors
0.75
15
5
Name
Order
Citations
PageRank
Steffen Jost124712.36
Hans-Wolfgang Loidl234038.89
Kevin Hammond337323.36
N. Scaife428221.86
Martin Hofmann543134.48