Using Dependent Types to Define Energy Augmented Semantics of Programs

  • Bernard van GastelEmail author
  • Rody Kersten
  • Marko van Eekelen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9964)


Energy is becoming a key resource for IT systems. Hence, it can be essential for the success of a system under development to be able to derive and optimise its resource consumption. For large IT systems, compositionality is a key property in order to be applicable in practice. If such a method is hardware parametric, the effect of using different algorithms or running the same software on different hardware configurations can be studied. This article presents a hardware-parametric, compositional and precise type system to derive energy consumption functions. These energy functions describe the energy consumption behaviour of hardware controlled by the software. This type system has the potential to predict energy consumptions of algorithms and hardware configurations, which can be used on design level or for optimisation.


Dependent Type System Energy Consumption Function Called Component Functions State Update Function Time-independent Energy 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Saxe, E.: Power-efficient software. Commun. ACM 53(2), 44–48 (2010)CrossRefGoogle Scholar
  2. 2.
    Zhurikhin, D., Belevantsev, A., Avetisyan, A., Batuzov, K., Lee, S.: Evaluating power aware optimizations within GCC compiler. In: GROW-2009: International Workshop on GCC Research Opportunities (2009)Google Scholar
  3. 3.
    Jayaseelan, R., Mitra, T., Li, X.: Estimating the worst-case energy consumption of embedded software. In: Proceedings of the 12th IEEE Real-Time and Embedded Technology and Applications Symposium, pp. 81–90. IEEE (2006)Google Scholar
  4. 4.
    Ferreira, M.A., Hoekstra, E., Merkus, B., Visser, B., Visser, J.: SEFLab: A lab for measuring software energy footprints. In: 2013 2nd International Workshop on Green and Sustainable Software (GREENS), pp. 30–37. IEEE (2013)Google Scholar
  5. 5.
    Kersten, R., Toldin, P.P., Gastel, B., 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, Heidelberg (2014). doi: 10.1007/978-3-319-12466-7_6 Google Scholar
  6. 6.
    Schoolderman, M., Neutelings, J., Kersten, R., van Eekelen, M.: ECAlogic: hardware-parametric energy-consumption analysis of algorithms. In: Proceedings of the 13th Workshop on Foundations of Aspect-oriented Languages, FOAL 2014, pp. 19–22. ACM, New York (2014)Google Scholar
  7. 7.
    Parisen Toldin, P., Kersten, R., van Gastel, B., van Eekelen, M.: Soundness proof for a hoare logic for energy consumption analysis. Technical Report ICIS-R13009, Radboud University Nijmegen, October 2013Google Scholar
  8. 8.
    Albers, S.: Energy-efficient algorithms. Commun. ACM 53(5), 86–96 (2010)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Ranganathan, P.: Recipe for efficiency: principles of power-aware computing. Commun. ACM 53(4), 60–67 (2010)CrossRefGoogle Scholar
  10. 10.
    Naik, K., Wei, D.S.L.: Software implementation strategies for power-conscious systems. Mob. Netw. Appl. 6(3), 291–305 (2001)CrossRefzbMATHGoogle Scholar
  11. 11.
    Sivasubramaniam, A., Kandemir, M., Vijaykrishnan, N., Irwin, M.J.: Designing energy-efficient software. In: International Parallel and Distributed Processing Symposium, Los Alamitos, CA, USA. IEEE Computer Society (2002)Google Scholar
  12. 12.
    te Brinke, S., Malakuti, S., Bockisch, C., Bergmans, L., Akşit, M.: A design method for modular energy-aware software. In: Proceedings of the 28th Annual ACM Symposium on Applied Computing, pp. 1180–1182. ACM, New York (2013)Google Scholar
  13. 13.
    Cohen, M., Zhu, H.S., Senem, E.E., Liu, Y.D.: Energy types. SIGPLAN Not. 47(10), 831–850 (2012)CrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Kerrison, S., Liqat, U., Georgiou, K., Mena, A.S., Grech, N., Lopez-Garcia, P., Eder, K., Hermenegildo, M.V.: 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, Heidelberg (2014)Google Scholar
  16. 16.
    Gheorghita, S.V., Corporaal, H., Basten, T.: Iterative compilation for energy reduction. J. Embedded Comput. 1(4), 509–520 (2005)Google Scholar
  17. 17.
    Mehta, H., Owens, R.M., Irwin, M.J., Chen, R., Ghosh, D.: Techniques for low energy software. In: ISLPED 1997: Proceedings of the 1997 International Symposium on Low Power Electronics and Design, pp. 72–75. ACM, New York (1997)Google Scholar
  18. 18.
    Šimunić, T., Benini, L., De Micheli, G., Hans, M.: Source code optimization and profiling of energy consumption in embedded systems. In: ISSS 2000: Proceedings of the 13th International Symposium on System Synthesis, Washington, DC, pp. 193–198. IEEE Computer Society (2000)Google Scholar
  19. 19.
    Zhang, W., Kandemir, M., Vijaykrishnan, N., Irwin, M.J., De, V.: Compiler support for reducing leakage energy consumption. In: DATE 2003: Proceedings of the Conference on Design, Automation and Test in Europe, Washington, DC. IEEE Computer Society (2003)Google Scholar
  20. 20.
    You, Y.P., Lee, C., Lee, J.K.: Compilers for leakage power reduction. ACM Trans. Des. Autom. Electron. Syst. 11(1), 147–164 (2006)CrossRefGoogle Scholar
  21. 21.
    Shrivastava, A., Dutt, N.: Energy efficient code generation exploiting reduced bit-width instruction set architectures (rISA). In: ASP-DAC 2004: Proceedings of the 2004 Asia and South Pacific Design Automation Conference, Piscataway, NJ, USA, pp. 475–477. IEEE Press (2004)Google Scholar
  22. 22.
    Joo, Y., Choi, Y., Shim, H., Lee, H.G., Kim, K., Chang, N.: Energy exploration and reduction of SDRAM memory systems. In: DAC 2002: Proceedings of the 39th Annual Design Automation Conference, pp. 892–897. ACM, New York (2002)Google Scholar
  23. 23.
    Verma, M., Wehmeyer, L., Pyka, R., Marwedel, P., Benini, L.: Compilation and simulation tool chain for memory aware energy optimizations. In: SAMOS, pp. 279–288 (2006)Google Scholar
  24. 24.
    Jones, T.M., O’Boyle, M.F.P., Abella, J., González, A., Ergin, O.: Energy-efficient register caching with compiler assistance. ACM Trans. Archit. Code Optim. 6(4), 1–23 (2009)CrossRefGoogle Scholar
  25. 25.
    Lee, H.G., Chang, N.: Energy-aware memory allocation in heterogeneous non-volatile memory systems. In: ISLPED 2003: Proceedings of the 2003 International Symposium on Low Power Electronics and Design, pp. 420–423. ACM, New York (2003)Google Scholar
  26. 26.
    Okuma, T., Yasuura, H., Ishihara, T.: Software energy reduction techniques for variable-voltage processors. IEEE Des. Test 18(2), 31–41 (2001)CrossRefGoogle Scholar
  27. 27.
    Saputra, H., Kandemir, M., Vijaykrishnan, N., Irwin, M.J., Hu, J.S., Hsu, C.H., Kremer, U.: Energy-conscious compilation based on voltage scaling. LCTES/SCOPES 2002: Proceedings of the Joint Conference on Languages, Compilers and Tools for Embedded Systems, pp. 2–11. ACM, New York (2002)Google Scholar
  28. 28.
    Baek, W., Chilimbi, T.M.: Green: a framework for supporting energy-conscious programming using controlled approximation. SIGPLAN Not. 45(6), 198–209 (2010)CrossRefGoogle Scholar
  29. 29.
    te Brinke, S., Malakuti, S., Bockisch, C.M., Bergmans, L.M.J., Akşit, M., Katz, S.: A tool-supported approach for modular design of energy-aware software. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, Gyeongju, Korea, SAC 2014. ACM, March 2014Google Scholar
  30. 30.
    Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46(2), 161–203 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Ball, T., Sagiv, M. (eds.) POPL 2011, pp. 357–370. ACM (2011)Google Scholar
  32. 32.
    Atkey, R.: Amortised resource analysis with separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 85–103. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-11957-6_6 CrossRefGoogle Scholar
  33. 33.
    Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.W., Momigliano, A.: A program logic for resources. Theor. Comput. Sci. 389(3), 411–445 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    McBride, C.: Epigram: practical programming with dependent types. In: Vene, V., Uustalu, T. (eds.) AFP 2004. LNCS, vol. 3622, pp. 130–170. Springer, Heidelberg (2005). doi: 10.1007/11546382_3 CrossRefGoogle Scholar
  35. 35.
    Bove, A., Dybjer, P., Norell, U.: A brief overview of agda - a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73–78. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  36. 36.
    Condit, J., Harren, M., Anderson, Z., Gay, D., Necula, G.C.: Dependent types for low-level programming. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 520–535. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71316-6_35 CrossRefGoogle Scholar
  37. 37.
    Morgenstern, J., Licata, D.R.: Security-typed programming within dependently typed programming. Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, pp. 169–180. ACM, New York (2010)Google Scholar
  38. 38.
    Shkaravska, O., Eekelen, M., Tamalet, A.: Collected size semantics for strict functional programs over general polymorphic lists. In: Dal Lago, U., Peña, R. (eds.) FOPARA 2013. LNCS, vol. 8552, pp. 143–159. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-12466-7_9 Google Scholar
  39. 39.
    Tamalet, A., Shkaravska, O., van Eekelen, M.: Size analysis of algebraic data types. In: Achten, P., Koopman, P., Morazán, M. (eds.) Trends in Functional Programming, vol. 9 of Trends in Functional Programming, pp. 33–48. Intellect (2009)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Bernard van Gastel
    • 1
    • 2
    Email author
  • Rody Kersten
    • 3
  • Marko van Eekelen
    • 1
    • 2
  1. 1.Institute for Computing and Information SciencesRadboud UniversityNijmegenThe Netherlands
  2. 2.Faculty of Management, Science and TechnologyOpen University of the NetherlandsHeerlenThe Netherlands
  3. 3.Carnegie Mellon Silicon ValleyMoffett FieldUSA

Personalised recommendations