Energy Consumption Analysis and Verification using CiaoPP

Energy Consumption Analysis and Verification using CiaoPP

By
P. Lopez-Garcia,
M.V. Hermenegildo,
M. Klemen, and
U. Liqat

IMDEA Software Institute

Spanish Council for Scientific Research (CSIC)

Universidad Politécnica de Madrid (UPM), Departamento de Inteligencia Artificial

{pedro.lopez,manuel.hermenegildo,maximiliano.klemen,umer.liqat}@imdea.org

FULL PDF

Energy consumption and the environmental impact of computing technologies have become important concerns. There is increased demand for complex computing systems which have to operate on batteries or harvested energy, such as implantable/portable medical devices, space systems, mobile phones, and other Internet of Things devices. At the same time, energy consumption is also an important problem in high-performance computing and data centers.

Despite advances in power-efficient hardware, more energy savings can be achieved by improving the software. The estimation of the energy that program executions will consume is instrumental for program optimization and verification, and energy-aware software development in general. Performing such estimation statically (i.e., at compile-time, without running the program with concrete data) is much more useful than performing it dynamically, and is required in many interesting cases. However, this poses important challenges.

We have been developing an approach for: a) estimating such energy consumption statically in the form of functions on the input data sizes of procedures (and possibly other hardware-dependent parameters, such as clock frequency and voltage), and b) using such functions for verifying and finding errors with respect to a rich class of energy consumption specifications for programs. The approach has been implemented within the CiaoPP system. The purpose of this note is to provide a brief introduction to this work and the results obtained so far, as well as pointers to the corresponding papers, that provide the relevant details.

A fundamental observation is that determining program energy consumption requires the analysis of low-level program representations, i.e., at the level of Instruction Set Architecture (ISA), bytecodes, etc. This is because the necessary information regarding the energy-consuming operations really performed by the program is only present with sufficient accuracy at those levels. Our approach to the analysis and verification of energy consumption [22,11,16,10,8] is based on a transformation of these low-level programs into a set of Horn clauses [20,6]. These Horn clauses encode the semantics of such low-level programs through different abstractions determined by the set of abstract domains used. Such abstract domains approximate properties that are instrumental for energy analysis, such as sized types [25], determinacy [12,13], or non-failure [4,1], as well as of course the cost / energy consumption itself. An interesting aspect of our approach to energy analysis (and to cost analysis in general), and which contrasts with previous approaches to cost analysis, is that it is based directly on abstract interpretation [26].

As is usual in abstract interpretation of logic programs, given such a set of Horn clauses, the objective of our analysis is to compute their abstract minimal model for each abstract domain or combination of domains. For this purpose we use the PLAI analyzer of the CiaoPP system [7]. PLAI computes this abstract minimal model using a top-down, memo table-based fixpoint algorithm, which can be seen as an extension of a highly optimized SLDT resolution engine with the abstract domains taking the traditional role of constraint domains in the logic. This extended abstract tabling algorithm includes optimizations for fixpoint acceleration such as dependency tracking or dynamic strongly-connected component detection. It is incremental and, in contrast to bottom-up algorithms (also available in CiaoPP), multivariant (context sensitive). The result of the abstract model computation –the analysis– is a set of memo tables which store all the abstract call-success pairs that occur in the program, as well as dependencies between them. In the case of energy analysis these entries contain, for each procedure, and for each possible abstract call state and path, a function that returns the corresponding energy consumed by that procedure and class of calls, as a function of input data sizes.

This work builds on our earlier work on cost analysis, initially developed for granularity control during automatic program parallelization [2,18,17], which was later extended for inferring both upper- and lower-bound functions [3,5], and generalized for a wide class of user-definable resources [24,23]. This configurability of the system allowed us to specialize it for execution time analysis [21] (using bytecode-level models obtained by regression), and is instrumental in the energy application for representing low-level energy models.

In particular, we have applied this approach and its implementation in CiaoPP to the energy analysis of (X)C programs running on the XMOS XS1-L architecture, both specialized for embedded programs. We have also performed a set of experiments comparing the energy analysis estimations for such programs to the actual energy consumption measured on the hardware, obtaining promising results [11,10,8,9]. Embedded software developers can use this tool for determining values for program parameters that ensure meeting a given energy budget while minimizing losses in quality of service [16].

In these experiments several different energy models have been used. In [11,10] the energy models used encoded energy consumption information for each ISA or LLVM instruction. Our results confirm that energy models at lower levels (e.g. ISA) are more precise than at higher levels (e.g., LLVM), but also that at lower levels more program structure and data structure information is lost, which can imply a loss of accuracy in the analysis. In our results the LLVM level
emerges as a good compromise.

We have also explored using models of the energy consumption of whole blocks (i.e., block-level energy models) [8,9]. Our approach combines static and dynamic (profiling-based) techniques for the inference of safe energy bounds of blocks. The dynamic technique uses an evolutionary algorithm to determine bounds on the energy consumption of each basic block. The CiaoPP static analyzer is then used to combine the energy values obtained for such blocks according to the program control flow, and produce energy consumption bounds of the whole program.

Our tools also perform verification and (performance) error detection following the CiaoPP assertion model [7,15]. To this end, the inferred abstract models of energy consumption are compared to the energy specifications. This can optionally be done during the analysis or after it. In our approach specifications can include both lower and upper bounds on energy usage, and they can express intervals within which energy usage is to be certified to be within such bounds. The bounds of the intervals can be given in general as functions on input data sizes. Our verification system can prove whether such energy usage specifications are met or not. It can also infer the particular conditions under which the specifications hold. To this end, these conditions are also expressed as intervals of functions of input data sizes, such that a given specification can be proved for some intervals but disproved for others. The\ specifications themselves can also include preconditions expressing intervals for input data sizes.

Note that the type of information to be inferred by the analysis is motivated by its final use: program optimisation, verification, helping energy-aware software developers to make design decisions, etc. For example, for optimization the analysis can infer probabilistic information [27]. For verification, safe approximations (upper and lower bounds) need to be inferred [14,15,16], which poses some challenging problems. When the goal of the analysis is helping developers make resource-related design decisions, what is really needed is information that helps identify the parts (e.g., procedures) of a program responsible for highest fractions of the total resource usage of its execution, or how such total resource usage is distributed over those parts. For example, procedures which have lower costs but which are called more often may be responsible for a larger part of the overall resource usage, so that their optimization may be most profitable. We have further extended and generalized the CiaoPP resource analysis framework so that it can now be specialized for inferring such kinds of information statically [19] (i.e., for static profiling). We show that the framework is general and flexible enough to support a wide range of static cost analyses, including both “accumulated” cost and the “standard notion” of cost.

References