Citation
Liqat, Umer and Bankovíc, Zorana and López Garcia, Pedro and Hermenegildo, Manuel V.
(2018).
Inferring energy bounds via static program analysis and evolutionary modeling of basic blocks.
In: "27th International Symposium on Logic-Based Program Synthesis and Transformation ( LOPSTR 2017)", 10-12 Oct 2017, Namur, Bélgica. ISBN 978-3-319-94460-9. pp. 54-72.
https://doi.org/10.1007/978-3-319-94460-9_4.
Abstract
The ever increasing number and complexity of energy-bound
devices (such as the ones used in Internet of Things applications, smart
phones, and mission critical systems) pose an important challenge on
techniques to optimize their energy consumption and to verify that they
will perform their function within the available energy budget. In this
work we address this challenge from the software point of view and propose
a novel approach to estimating accurate parametric bounds on the
energy consumed by program executions that are practical for their application
to energy verification and optimization. Our approach divides a
program into basic (branchless) blocks and performs a best effort modeling
to estimate upper and lower bounds on the energy consumption
for each block using an evolutionary algorithm. Then it combines the
obtained values according to the program control flow, using a safe static
analysis, to infer functions that give both upper and lower bounds on the
energy consumption of the whole program and its procedures as functions
on input data sizes. We have tested our approach on (C-like) embedded
programs running on the XMOS hardware platform. However, our
method is general enough to be applied to other microprocessor architectures
and programming languages. The bounds obtained by our prototype
implementation on a set of benchmarks were always safe and quite
accurate. This supports our hypothesis that our approach offers a good
compromise between safety and accuracy, and can be applied in practice
for energy verification and optimization.