Inferring Parametric Energy Consumption Functions at Different Software Levels: ISA vs. LLVM IR

  • U. Liqat
  • K. Georgiou
  • S. Kerrison
  • P. Lopez-GarciaEmail author
  • John P. Gallagher
  • M. V. Hermenegildo
  • K. Eder
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9964)


The static estimation of the energy consumed by program executions is an important challenge, which has applications in program optimization and verification, and is instrumental in energy-aware software development. Our objective is to estimate such energy consumption in the form of functions on the input data sizes of programs. We have developed a tool for experimentation with static analysis which infers such energy functions at two levels, the instruction set architecture (ISA) and the intermediate code (LLVM IR) levels, and reflects it upwards to the higher source code level. This required the development of a translation from LLVM IR to an intermediate representation and its integration with existing components, a translation from ISA to the same representation, a resource analyzer, an ISA-level energy model, and a mapping from this model to LLVM IR. The approach has been applied to programs written in the XC language running on XCore architectures, but is general enough to be applied to other languages. Experimental results show that our LLVM IR level analysis is reasonably accurate (less than \(6.4\,\%\) average error vs. hardware measurements) and more powerful than analysis at the ISA level. This paper provides insights into the trade-off of precision versus analyzability at these levels.


Energy consumption analysis Resource usage analysis Static analysis Embedded systems 



This research has received funding from the European Union 7th Framework Program agreement no 318337, ENTRA, Spanish MINECO TIN’12-39391 StrongSoft project, and the Madrid M141047003 N-GREENS program.


  1. 1.
    Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reasoning 46(2), 161–203 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71316-6_12 CrossRefGoogle Scholar
  3. 3.
    Bjørner, N., Fioravanti, F., Rybalchenko, A., Senni, V. (eds.) Proceedings of First Workshop on Horn Clauses for Verification and Synthesis, vol. 169. EPTCS, July 2014Google Scholar
  4. 4.
    Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  5. 5.
    Debray, S.K., Lin, N.-W., Hermenegildo, M.: Task granularity analysis in logic programs. In: Proceeding of the 1990 ACM Conference on Programming Language Design and Implementation, pp. 174–188. ACM Press, June 1990Google Scholar
  6. 6.
    Debray, S.K., López-García, P., Hermenegildo, M., Lin, N.-W.: Lower bound cost estimation for logic programs. In: 1997 International Logic Programming Symposium, pp. 291–305. MIT Press, Cambridge, October 1997Google Scholar
  7. 7.
    Georgiou, K., Kerrison, S., Eder, K.: On the Value, Limits of Multi-level Energy Consumption Static Analysis for Deeply Embedded Single, Multi-threaded Programs. ArXiv e-prints: arXiv:1510.07095, October 2015
  8. 8.
    Grebenshchikov, S., Gupta, A., Lopes, N.P., Popeea, C., Rybalchenko, A.: HSF(C): a software verifier based on horn clauses. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 549–551. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28756-5_46 CrossRefGoogle Scholar
  9. 9.
    Grech, N., Georgiou, K., Pallister, J., Kerrison, S., Morse, J., Eder, K.: Static analysis of energy consumption for LLVM IR programs. In: Proceedings of the 18th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2015. ACM, New York (2015)Google Scholar
  10. 10.
    Gurfinkel, A., Kahsai, T., Navas, J.A.: SeaHorn: a framework for verifying C programs (Competition Contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 447–450. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46681-0_41 Google Scholar
  11. 11.
    Henriksen, K.S., Gallagher, J.P.: Abstract interpretation of PIC programs through logic programming. In: Sixth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM 2006), pp. 184–196. IEEE Computer Society (2006)Google Scholar
  12. 12.
    Hermenegildo, M., Puebla, G., Bueno, F., Lopez-Garcia, P.: Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Sci. Comput. Program. 58(1–2), 115–140 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Hermenegildo, M.V., Bueno, F., Carro, M., López, P., Mera, E., Morales, J., Puebla, G.: An overview of Ciao and its design philosophy. Theory Pract. Logic Program. 12(1–2), 219–252 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Herrmann, C., Bonenfant, A., Hammond, K., Jost, S., Loidl, H.-W., Pointon, R.: Automatic amortised worst-case execution time analysis. In: 7th International Workshop on Worst-Case Execution Time Analysis (WCET 2007), vol. 6. OASIcs. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2007)Google Scholar
  15. 15.
    Hojjat, H., Konečný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 247–251. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32759-9_21 CrossRefGoogle Scholar
  16. 16.
    Jayaseelan, R., Mitra, T., Li, X.: Estimating the worst-case energy consumption of embedded software. In: IEEE Real Time Technology and Applications Symposium, pp. 81–90. IEEE Computer Society (2006)Google Scholar
  17. 17.
    Kerrison, S., Eder, K.: Energy modeling of software for a hardware multithreaded embedded microprocessor. ACM Trans. Embed. Comput. Syst. 14(3), 1–25 (2015)CrossRefGoogle Scholar
  18. 18.
    Lafond, S., Lilius, J.: Energy consumption analysis for two embedded Java virtual machines. J. Syst. Archit. 53(5–6), 328–337 (2007)CrossRefGoogle Scholar
  19. 19.
    Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: Proceeding of the 2004 International Symposium on Code Generation and Optimization (CGO), pp. 75–88. IEEE Computer Society, March 2004Google Scholar
  20. 20.
    Liqat, U., Georgiou, K., Kerrison, S., Lopez-Garcia, P., Hermenegildo, M.V., Gallagher, J.P., Eder, K., Consumption, I.E.: At Different Software Levels: ISA vs. LLVM IR. Technical report, FET 318337 ENTRA Project, Appendix D3.2.4 of Deliverable D3.2.
  21. 21.
    Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., Lopez-Garcia, P., Grech, N., Hermenegildo, M., Eder, K.: Energy Consumption analysis of programs based on XMOS ISA-level models. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 72–90. Springer, Switzerland (2014). doi: 10.1007/978-3-319-14125-1_5 Google Scholar
  22. 22.
    Méndez-Lojo, M., Navas, J., Hermenegildo, M.V.: A flexible, (C)LP-based approach to the analysis of object-oriented programs. In: King, A. (ed.) LOPSTR 2007. LNCS, vol. 4915, pp. 154–168. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78769-3_11 CrossRefGoogle Scholar
  23. 23.
    Mera, E., López-García, P., Carro, M., Hermenegildo, M.: Towards execution time estimation in abstract machine-based languages. In: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2008), pp. 174–184. ACM Press, July 2008Google Scholar
  24. 24.
    Navas, J., Méndez-Lojo, M., Hermenegildo, M.: Safe upper-bounds inference of energy consumption for Java bytecode applications. In: The Sixth NASA Langley Formal Methods Workshop (LFM 2008), Extended Abstract, April 2008Google Scholar
  25. 25.
    Navas, J., Mera, E., Lopez-Garcia, P., Hermenegildo, M.V.: User-definable resource bounds analysis for logic programs. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 348–363. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-74610-2_24 CrossRefGoogle Scholar
  26. 26.
    Pallister, J., Kerrison, S., Morse, J., Eder, K.: Data dependent energy modeling for worst case energy consumption analysis. arXiv preprint arXiv:1505.03374 (2015)
  27. 27.
    Rosendahl, M.: Automatic complexity analysis. In: 4th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA 1989). ACM Press (1989)Google Scholar
  28. 28.
    Serrano, A., Lopez-Garcia, P., Hermenegildo, M.: Resource usage analysis of logic programs via abstract interpretation using sized types. In: Theory and Practice of Logic Programming, 30th International Conference on Logic Programming (ICLP 2014) Special Issue, vol. 14, no. 4–5, pp. 739–754 (2014)Google Scholar
  29. 29.
    Seshia, S.A., Kotker, J.: Gametime: a toolkit for timing analysis of software. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 388–392. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-19835-9_34 CrossRefGoogle Scholar
  30. 30.
    Vasconcelos, P.B., Hammond, K.: Inferring Cost Equations for Recursive, Polymorphic and Higher-Order Functional Programs. In: Trinder, P., Michaelson, G.J., Peña, R. (eds.) IFL 2003. LNCS, vol. 3145, pp. 86–101. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27861-0_6 CrossRefGoogle Scholar
  31. 31.
    Watt, D.: Programming XC on XMOS Devices. XMOS Limited (2009)Google Scholar
  32. 32.
    Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528–539 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenström, P.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embedded Comput. Syst. 7(3), 36 (2008)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • U. Liqat
    • 1
  • K. Georgiou
    • 2
  • S. Kerrison
    • 2
  • P. Lopez-Garcia
    • 1
    • 3
    Email author
  • John P. Gallagher
    • 5
  • M. V. Hermenegildo
    • 1
    • 4
  • K. Eder
    • 2
  1. 1.IMDEA Software InstituteMadridSpain
  2. 2.University of BristolBristolUK
  3. 3.Spanish Council for Scientific Research (CSIC)MadridSpain
  4. 4.Universidad Politécnica de Madrid (UPM)MadridSpain
  5. 5.Roskilde UniversityRoskildeDenmark

Personalised recommendations