Using Dependent Types to Define Energy Augmented Semantics of Programs

Bernard van Gastel; Rody Kersten; Marko van Eekelen

doi:10.1007/978-3-319-46559-3_2

Using Dependent Types to Define Energy Augmented Semantics of Programs

Bernard van Gastel^*, Rody Kersten, Marko van Eekelen

^*Corresponding author for this work

Research Line Resilience (part of LIRS program)

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

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.

Original language	English
Title of host publication	Foundational and Practical Aspects of Resource Analysis
Subtitle of host publication	4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers
Editors	Marko van Eekelen, Ugo Dal Lago
Place of Publication	Cham
Publisher	Springer International Publishing AG
Chapter	2
Pages	20-39
Number of pages	20
ISBN (Electronic)	9783319465593
ISBN (Print)	9783319465586
DOIs	https://doi.org/10.1007/978-3-319-46559-3_2
Publication status	Published - 2016
Event	Foundational and Practical Aspects of Resource Analysis - London, United Kingdom Duration: 11 Apr 2015 → 11 Apr 2015 Conference number: 4 http://resourceanalysis.cs.ru.nl/fopara/fopara-dice-2015-programme.pdf

Publication series

Series	Lecture Notes in Computer Science (LNCS) series
Volume	9964
ISSN	0302-9743

Workshop

Workshop	Foundational and Practical Aspects of Resource Analysis
Abbreviated title	FOPARA 2015
Country/Territory	United Kingdom
City	London
Period	11/04/15 → 11/04/15
Internet address	http://resourceanalysis.cs.ru.nl/fopara/fopara-dice-2015-programme.pdf

Access to Document

10.1007/978-3-319-46559-3_2Licence: Unspecified

Cite this

van Gastel, B., Kersten, R., & van Eekelen, M. (2016). Using Dependent Types to Define Energy Augmented Semantics of Programs. In M. van Eekelen, & U. Dal Lago (Eds.), Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers (pp. 20-39). Springer International Publishing AG. https://doi.org/10.1007/978-3-319-46559-3_2

van Gastel, Bernard ; Kersten, Rody ; van Eekelen, Marko. / Using Dependent Types to Define Energy Augmented Semantics of Programs. Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. editor / Marko van Eekelen ; Ugo Dal Lago. Cham : Springer International Publishing AG, 2016. pp. 20-39 (Lecture Notes in Computer Science (LNCS) series, Vol. 9964).

@inproceedings{3401b4cc24174b85b9e7b227ec577daa,

title = "Using Dependent Types to Define Energy Augmented Semantics of Programs",

abstract = "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.",

author = "{van Gastel}, Bernard and Rody Kersten and {van Eekelen}, Marko",

year = "2016",

doi = "10.1007/978-3-319-46559-3_2",

language = "English",

isbn = "9783319465586",

series = "Lecture Notes in Computer Science (LNCS) series",

publisher = "Springer International Publishing AG",

pages = "20--39",

editor = "{van Eekelen}, Marko and {Dal Lago}, Ugo",

booktitle = "Foundational and Practical Aspects of Resource Analysis",

address = "Switzerland",

note = "Foundational and Practical Aspects of Resource Analysis, FOPARA 2015 ; Conference date: 11-04-2015 Through 11-04-2015",

url = "http://resourceanalysis.cs.ru.nl/fopara/fopara-dice-2015-programme.pdf",

}

van Gastel, B, Kersten, R & van Eekelen, M 2016, Using Dependent Types to Define Energy Augmented Semantics of Programs. in M van Eekelen & U Dal Lago (eds), Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. Springer International Publishing AG, Cham, Lecture Notes in Computer Science (LNCS) series, vol. 9964, pp. 20-39, Foundational and Practical Aspects of Resource Analysis, London, United Kingdom, 11/04/15. https://doi.org/10.1007/978-3-319-46559-3_2

Using Dependent Types to Define Energy Augmented Semantics of Programs. / van Gastel, Bernard; Kersten, Rody; van Eekelen, Marko.
Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. ed. / Marko van Eekelen; Ugo Dal Lago. Cham: Springer International Publishing AG, 2016. p. 20-39 (Lecture Notes in Computer Science (LNCS) series, Vol. 9964).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Using Dependent Types to Define Energy Augmented Semantics of Programs

AU - van Gastel, Bernard

AU - Kersten, Rody

AU - van Eekelen, Marko

N1 - Conference code: 4

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-46559-3_2

DO - 10.1007/978-3-319-46559-3_2

M3 - Conference Article in proceeding

SN - 9783319465586

T3 - Lecture Notes in Computer Science (LNCS) series

SP - 20

EP - 39

BT - Foundational and Practical Aspects of Resource Analysis

A2 - van Eekelen, Marko

A2 - Dal Lago, Ugo

PB - Springer International Publishing AG

CY - Cham

T2 - Foundational and Practical Aspects of Resource Analysis

Y2 - 11 April 2015 through 11 April 2015

ER -

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, editors, Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, April 11, 2015. Revised Selected Papers. Cham: Springer International Publishing AG. 2016. p. 20-39. (Lecture Notes in Computer Science (LNCS) series, Vol. 9964). Epub 2016 Sept 25. doi: 10.1007/978-3-319-46559-3_2

Using Dependent Types to Define Energy Augmented Semantics of Programs

Abstract

Publication series

Workshop

Access to Document

Fingerprint

Cite this