Long-Run Cost Analysis by Approximation of Linear Operators over Dioids

Abstract. We present a static analysis technique for modeling and approximating the long-run resource usage of programs. The approach is based on a quantitative semantic framework where programs are repres linear operators over dioids. We provide abstraction techniques for such linear operators which make it feasible to compute safe overapproximations of the long-run cost of a program. A theorem is proved stating that such abstractions yield correct approximations of the program's long-run cost. These approximations are effectively computed as nvalue of the matrix representation of the abstract semantics. The theoretical developments are illustrated on a concrete example taken from the analysis of the cache behaviour of a simple bytecode language.

• Type: Conference
• Year: 2008
• Where: AMAST
• Authors: David Cachera, Thomas P. Jensen, Arnaud Jobin, Pascal Sotin
• Keywords: AMAST 2008, Linear Operators, Long-run Cost, Long-run Resource Usage, Software Engineering