Abstract
Energy consumption in embedded systems plays a large role as it has implications for the power supply and the batteries used. Programmers of these systems should consider how their programs control external devices, and where energy consumption hotspots lie. We present a static analysis to predict and visualize energy consumption of external devices controlled by programs written in a simple imperative programming language. Currently available energy consumption analysis techniques generate graphs over time, which makes it difficult to see from where in the source code the consumption originates. Our method generates graphs over source locations, called skyline diagrams, showing the maximum power draw for each line of source code.
Our method harnesses symbolic execution extended with support for controlling external devices. This gives accurate predictions and complete code path coverage, as far as the limits of computability allow. To make the diagrams easier to understand, we introduce a merge algorithm that condenses all skylines into a concise overview. We demonstrate the potential by analysing various example programs with our prototype implementation. We envision this approach being used to identify energy consumption hotspots of embedded systems during the design and development phase, in a less involved way than traditional approaches.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Arduino project hub. https://create.arduino.cc/projecthub. Accessed 01 May 2020
SECA project wiki. https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/-/wikis/home. Accessed 06 Feb 2020
SECA source code repository. https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution. Accessed 29 Jan 2020
Albers, S.: Energy-efficient algorithms. Commun. ACM 53(5), 86–96 (2010)
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: Design and implementation of a cost and termination analyzer for Java bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 113–132. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92188-2_5
Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.W., Momigliano, A.: A program logic for resources. Theor. Comput. Sci. 389(3), 411–445 (2007). https://doi.org/10.1016/j.tcs.2007.09.003
Atkey, R.: Amortised resource analysis with separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 85–103. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_6
Brooks, D., Tiwari, V., Martonosi, M.: Wattch: a framework for architectural-level power analysis and optimizations. SIGARCH Comput. Arch. News 28(2), 83–94 (2000)
Cohen, M., Zhu, H.S., Senem, E.E., Liu, Y.D.: Energy types. SIGPLAN Not. 47(10), 831–850 (2012)
van Gastel, B.: Assessing sustainability of software - analysing correctness, memory and energy consumption. Ph.D. thesis, Open University (2016)
van Gastel, B., Kersten, R., van Eekelen, M.: Using dependent types to define energy augmented semantics of programs. In: van Eekelen, M., Dal Lago, U. (eds.) FOPARA 2015. LNCS, vol. 9964, pp. 20–39. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46559-3_2
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Ball, T., Sagiv, M. (eds.) POPL 2011, pp. 357–370. ACM (2011)
Jayaseelan, R., Mitra, T., Li, X.: Estimating the worst-case energy consumption of embedded software. In: Proceedings of RTAS 2006, pp. 81–90. IEEE (2006). https://doi.org/10.1109/RTAS.2006.17
Junior, M.N.O., et al.: Analyzing software performance and energy consumption of embedded systems by probabilistic modeling: an approach based on coloured petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 261–281. Springer, Heidelberg (2006). https://doi.org/10.1007/11767589_15
Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., Lopez-Garcia, P., Grech, N., Hermenegildo, M.V., 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, Cham (2014). https://doi.org/10.1007/978-3-319-14125-1_5
Kersten, R., Toldin, P.P., van Gastel, B., van Eekelen, M.: A hoare logic for energy consumption analysis. In: Dal Lago, U., Peña, R. (eds.) FOPARA 2013. LNCS, vol. 8552, pp. 93–109. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12466-7_6
Kersten, R., Shkaravska, O., van Gastel, B., Montenegro, M., Eekelenvan Eekelen, M.: Making resource analysis practical for real-time Java. In: Proceedings of JTRES 2012, pp. 135–144. ACM (2012). https://doi.org/10.1145/2388936.2388959
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Klinik, M., van Gastel, B., Kop, C., Eekelenvan Eekelen, M.: Skylines for symbolic energy consumption analysis - technical report. Technical report, Radboud University (2020). https://gitlab.science.ru.nl/mklinik/eca-symbolic-execution/blob/master/paper/techreport.pdf
Klinik, M., Jansen, J.M., Plasmeijer, R.: The sky is the limit: analysing resource consumption over time using skylines. In: Proceedings of the 29th Symposium on Implementation and Application of Functional Programming Languages, IFL 2017. ACM (2017)
Microchip Technology Inc.: ATmega48A/PA/88A/PA/168A/PA/328/P Data Sheet (2018)
Nielson, H.R., Nielson, F.: Semantics With Applications: A Formal Introduction. Wiley, Hoboken (1992)
Nogueira, B., Maciel, P., Tavares, E., Andrade, E., Massa, R., Callou, G., Ferraz, R.: A formal model for performance and energy evaluation of embedded systems. EURASIP J. Embed. Syst. 2011(1), 1–12 (2011). https://doi.org/10.1155/2011/316510
Ranganathan, P.: Recipe for efficiency: principles of power-aware computing. Commun. ACM 53(4), 60–67 (2010)
Sampson, A., Dietl, W., Fortuna, E., Gnanapragasam, D., Ceze, L., Grossman, D.: EnerJ: approximate data types for safe and general low-power computation. SIGPLAN Not. 46(6), 164–174 (2011)
Saxe, E.: Power-efficient software. Commun. ACM 53(2), 44–48 (2010). https://doi.org/10.1145/1646353.1646370
Sinha, A., Chandrakasan, A.P.: JouleTrack: a web based tool for software energy profiling. In: Proceedings of DAC 2001, pp. 220–225. ACM (2001)
Acknowledgements
We would like to thank Rinus Plasmeijer, Olha Shkaravska, Tim Steenvoorden, and Nico Naus for many hours of fruitful discussion. Special thanks goes to Ralf Hinze, who created an exam question, the grading of which eventually led to the idea of resource skylines. Thanks also to Pieter Koopman who provided funding for this project.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Klinik, M., Gastel, B.v., Kop, C., Eekelen, M.v. (2020). Skylines for Symbolic Energy Consumption Analysis. In: ter Beek, M.H., Ničković, D. (eds) Formal Methods for Industrial Critical Systems. FMICS 2020. Lecture Notes in Computer Science(), vol 12327. Springer, Cham. https://doi.org/10.1007/978-3-030-58298-2_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-58298-2_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-58297-5
Online ISBN: 978-3-030-58298-2
eBook Packages: Computer ScienceComputer Science (R0)