Cost analysis by approximation of linear operators over dioids

We present a static analysis technique for modeling and approximating the long-run resource usage of programs. We take as starting point a standard small-step operational semantics where each transition is labelled by a cost taken in a complete idempotent dioid. From such a rule-based semantics, we obtain a transition matrix, that expresses the semantics of a program as a linear operator on the moduloid of vectors of costs. Using these mathematical structures allows for defining the notion of long-run cost for a program. This cost is the maximum average of costs accumulated along a cycle of the semantics graph, and corresponds to an asymptotic average behaviour of the program. The quantitative operational semantics operates on finite, but potentially large state spaces. Hence, it is necessary to develop techniques for abstracting this semantics. Abstractions are also defined as linear operators from the set of concrete vectors into the set of abstract ones. Given such an abstraction over the semantic domains, we then have to abstract the transition matrix of the program itself into a matrix of reduced size. We give a sufficient condition for an abstraction of the semantics to be correct, i.e. to give an over-approximation of the real cost, and show how an abstract semantics that is correct by construction can be derived from the concrete one. As an application example, we have chosen a slightly unusual cost model pertaining to the analysis of cache behaviour and the number of cache misses in programs written in a simple, intermediate bytecode language (inspired by Java Card).