Energy Consumption Analysis and Verification using CiaoPP

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