Type-based Resource Analysis
From PUMA Graduiertenkolleg
Since several years, an increased interest in the static prediction of resource consumption of programs can be observed, in particular, in the context of mobile computing or embedded systems. The resource bounds to be respected often are amazingly small, e.g., a few kbit for embedded processors or only a few open connections for applications of ubiquitous computing.
Recently, we have substantially extended type-based analysis of object-oriented programs with arbitrary aliasing [HofmannJ06] from which several interesting and timely topics for PhD theses can be derived. The type system there assigns to each class of a Java program several types which refine the type given by the Java language, e.g., by assigning positive potential values. By summation over access paths, such a typing assigns a non-negative potential value also to every storage configuration. If we succeed to annotate classes, arrays and methods of a program with such types such that the implementing code can be proved to be type-correct by means of local type rules (these correspond to the transfer functions as known from dataflow analysis. Here, type correctness (which btw. is intricate to prove) means that the difference of the potential values of the initial and final configurations provides an upper bound to the resource consumption of a computation.