Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption

Abstract

In many applications it is important to ensure conformance with respect to specifications that constrain the use of resources such as execution time, energy, bandwidth, etc. We present a configurable framework for static resource usage verifi cation where specifications can include data size-dependent resource usage functions, expressing both lower and upper bounds. Ensuring conformance with respect to such specifications is an undecidable problem. Therefore, our framework infers resource usage functions (of the same type as the specifications, i.e., data-size dependent, and providing upper and lower bounds), which safely approximate the actual resource usage of the program, and which are safely compared against the specification. We start by reviewing how this framework is parametric with respect to the programming language by a) translating programs to an intermediate representation based on Horn clauses, and b) using the configurability of the framework to describe the resource semantics of the input language. We then provide a more detailed formalization of the approach and extend the framework so that the outcome of the static checking of assertions can generate intervals of the input data sizes for which assertions hold or not, i.e., a given specification can be proved for some intervals but disproved for others. We also generalize the specifications to support preconditions expressing intervals within which the input data size of a program is supposed to lie. Most importantly, we provide new techniques which extend the classes of resource usage functions that can be checked, such as functions containing logarithmic or summation expressions, or some functions with multiple variables. We also report on and provide results from an implementation within the Ciao/CiaoPP framework, as well as on a practical tool built by instantiating this framework for the verification of energy consumption specifications for imperative/embedded programs written in the XC language and running on the XS1-L architecture. Finally, we illustrate with an example how embedded software developers can use this tool, in particular for determining values for program parameters that ensure meeting a given energy budget while minimizing the loss in quality of service.