-
Greening AI-enabled Systems with Software Engineering: A Research Agenda for Environmentally Sustainable AI Practices
Authors:
Luís Cruz,
João Paulo Fernandes,
Maja H. Kirkeby,
Silverio Martínez-Fernández,
June Sallou,
Hina Anwar,
Enrique Barba Roque,
Justus Bogner,
Joel Castaño,
Fernando Castor,
Aadil Chasmawala,
Simão Cunha,
Daniel Feitosa,
Alexandra González,
Andreas Jedlitschka,
Patricia Lago,
Henry Muccini,
Ana Oprescu,
Pooja Rani,
João Saraiva,
Federica Sarro,
Raghavendra Selvan,
Karthik Vaidhyanathan,
Roberto Verdecchia,
Ivan P. Yamshchikov
Abstract:
The environmental impact of Artificial Intelligence (AI)-enabled systems is increasing rapidly, and software engineering plays a critical role in developing sustainable solutions. The "Greening AI with Software Engineering" CECAM-Lorentz workshop (no. 1358, 2025) funded by the Centre Européen de Calcul Atomique et Moléculaire and the Lorentz Center, provided an interdisciplinary forum for 29 parti…
▽ More
The environmental impact of Artificial Intelligence (AI)-enabled systems is increasing rapidly, and software engineering plays a critical role in developing sustainable solutions. The "Greening AI with Software Engineering" CECAM-Lorentz workshop (no. 1358, 2025) funded by the Centre Européen de Calcul Atomique et Moléculaire and the Lorentz Center, provided an interdisciplinary forum for 29 participants, from practitioners to academics, to share knowledge, ideas, practices, and current results dedicated to advancing green software and AI research. The workshop was held February 3-7, 2025, in Lausanne, Switzerland. Through keynotes, flash talks, and collaborative discussions, participants identified and prioritized key challenges for the field. These included energy assessment and standardization, benchmarking practices, sustainability-aware architectures, runtime adaptation, empirical methodologies, and education. This report presents a research agenda emerging from the workshop, outlining open research directions and practical recommendations to guide the development of environmentally sustainable AI-enabled systems rooted in software engineering principles.
△ Less
Submitted 3 June, 2025; v1 submitted 2 June, 2025;
originally announced June 2025.
-
Static Communication Analysis for Hardware Design
Authors:
Mads Rosendahl,
Maja H. Kirkeby
Abstract:
Hardware acceleration of algorithms is an effective method for improving performance in high-demand computational tasks. However, developing hardware designs for such acceleration fundamentally differs from software development, as it requires a deep understanding of the highly parallel nature of the hardware architecture. In this paper, we present a framework for the static analysis of communicat…
▽ More
Hardware acceleration of algorithms is an effective method for improving performance in high-demand computational tasks. However, developing hardware designs for such acceleration fundamentally differs from software development, as it requires a deep understanding of the highly parallel nature of the hardware architecture. In this paper, we present a framework for the static analysis of communication within datapath architectures designed for field-programmable gate arrays (FPGAs). Our framework aims to enhance hardware design and optimization by providing insights into communication patterns within the architecture, which are essential for ensuring efficient data handling.
△ Less
Submitted 27 May, 2025;
originally announced May 2025.
-
Teaching Energy-Efficient Software -- An Experience Report
Authors:
Henrik Bærbak Christensen,
Maja Hanne Kirkeby,
Bent Thomsen,
Lone Leth Thomsen
Abstract:
Environmental sustainability is a major and relevant challenge facing computing. Therefore, we must start teaching theory, techniques, and practices that both increase an awareness in our student population as well a provide concrete advice to be applied in practical software development. In this experience report, we focus on energy consumption of executing software, and describe teaching approac…
▽ More
Environmental sustainability is a major and relevant challenge facing computing. Therefore, we must start teaching theory, techniques, and practices that both increase an awareness in our student population as well a provide concrete advice to be applied in practical software development. In this experience report, we focus on energy consumption of executing software, and describe teaching approaches from three different universities that all address software energy consumption in various ways. Our main contribution is reporting lessons learned from these experiences and sketching some issues that teachers must be aware of when designing learning goals, teaching material and exercises.
△ Less
Submitted 28 April, 2025;
originally announced April 2025.
-
Energy and Time Complexity for Sorting Algorithms in Java
Authors:
Kristina Carter,
Su Mei Gwen Ho,
Mathias Marquar Arhipenko Larsen,
Martin Sundman,
Maja H. Kirkeby
Abstract:
The article investigates the relationship between time complexity and energy consumption in sorting algorithms, focusing on commonly-used algorithms implemented in Java: Bubble Sort, Counting Sort, Merge Sort, and Quick Sort. The significance of understanding this relationship is driven by the increasing energy demands of Information and Communication Technology systems and the potential for softw…
▽ More
The article investigates the relationship between time complexity and energy consumption in sorting algorithms, focusing on commonly-used algorithms implemented in Java: Bubble Sort, Counting Sort, Merge Sort, and Quick Sort. The significance of understanding this relationship is driven by the increasing energy demands of Information and Communication Technology systems and the potential for software optimization to contribute to energy efficiency. If we find a strong correlation between time complexity and energy usage, it would enhance the ability of software developers to create energy-efficient applications.
This quantitative study researches the execution of four selected sorting algorithms with input varying over input sizes (25000 to 1 million) and input order types (best, worst, and random cases) on a single kernel in a Java-enabled system. The input size is adjusted according to the type's maximum execution time, resulting in 136 combinations, totalling 12960 measurements. Wall time and the CPU energy consumption is measured using Intel's RAPL. Statistical analysis are used to examine the correlations between time complexity, wall time, and energy consumption.
The study finds a strong correlation between time complexity and energy consumption for the sorting algorithms tested. More than 99% of the variance in energy consumption for Counting Sort, Merge Sort, and Quick Sort depend on their time complexities. More than 94% of the variance in energy consumption for Bubble Sort depends on its time complexity. The results affirm that time complexity can serve as a reliable predictor of energy consumption in sequential sorting algorithms. This discovery could guide software developers in choosing energy-efficient algorithms by considering time complexities.
△ Less
Submitted 8 May, 2024; v1 submitted 13 November, 2023;
originally announced November 2023.
-
Energy Consumption and Performance of Heapsort in Hardware and Software
Authors:
Maja H. Kirkeby,
Thomas Krabben,
Mathias Larsen,
Maria B. Mikkelsen,
Tjark Petersen,
Mads Rosendahl,
Martin Schoeberl,
Martin Sundman
Abstract:
In this poster abstract we will report on a case study on implementing the Heapsort algorithm in hardware and software and comparing their time and energy consumption. Our experiment shows that the Hardware implementation is more energy efficient, but slower than the Software implementation due to a low clock frequency. It also indicate that the optimal degree of parallelization differs when optim…
▽ More
In this poster abstract we will report on a case study on implementing the Heapsort algorithm in hardware and software and comparing their time and energy consumption. Our experiment shows that the Hardware implementation is more energy efficient, but slower than the Software implementation due to a low clock frequency. It also indicate that the optimal degree of parallelization differs when optimizing for time compared to optimizing for time.
△ Less
Submitted 7 April, 2022;
originally announced April 2022.
-
Towards Comparing Performance of Algorithms in Hardware and Software
Authors:
Maja H. Kirkeby,
Martin Schoeberl
Abstract:
In this paper, we report on a preliminary investigation of the potential performance gain of programs implemented in field-programmable gate arrays (FPGAs) using a high-level language Chisel compared to ordinary high-level software implementations executed on general-purpose computers and small and cheap computers. FPGAs inherently support parallel evaluations, while sequential computers do not. F…
▽ More
In this paper, we report on a preliminary investigation of the potential performance gain of programs implemented in field-programmable gate arrays (FPGAs) using a high-level language Chisel compared to ordinary high-level software implementations executed on general-purpose computers and small and cheap computers. FPGAs inherently support parallel evaluations, while sequential computers do not. For this preliminary investigation, we have chosen a highly parallelizable program as a case study to show an upper bound of performance gain. The purpose is to demonstrate whether or not programming FPGAs has the potential for performance optimizations of ordinary programs. We have developed and evaluated Conway's Game of Life for an FPGA, a small and cheap computer Raspberry Pi 4, and a MacBook Pro Laptop. We have compared the performance of programs over different input sizes to decide the relative increase in runtime.
△ Less
Submitted 25 May, 2022; v1 submitted 7 April, 2022;
originally announced April 2022.
-
An Inversion Tool for Conditional Term Rewriting Systems -- A Case Study of Ackermann Inversion
Authors:
Maria Bendix Mikkelsen,
Robert Glück,
Maja H. Kirkeby
Abstract:
We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting systems are theoretically well founded and can model functional and non-functional rewrite relations. We illustrate the inversion by experiments with full and partial…
▽ More
We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting systems are theoretically well founded and can model functional and non-functional rewrite relations. We illustrate the inversion by experiments with full and partial inversions of the Ackermann function. The case study demonstrates, among others, that polyvariant inversion and input-output set propagation can reduce the search space of the generated inverse systems.
△ Less
Submitted 6 September, 2021;
originally announced September 2021.
-
Probabilistic Output Analyses for Deterministic Programs --- Reusing Existing Non-probabilistic Analyses
Authors:
Maja Hanne Kirkeby
Abstract:
We consider reusing established non-probabilistic output analyses (either forward or backwards) that yield over-approximations of a program's pre-image or image relation, e.g., interval analyses. We assume a probability measure over the program input and present two techniques (one for forward and one for backward analyses) that both derive upper and lower probability bounds for the output events.…
▽ More
We consider reusing established non-probabilistic output analyses (either forward or backwards) that yield over-approximations of a program's pre-image or image relation, e.g., interval analyses. We assume a probability measure over the program input and present two techniques (one for forward and one for backward analyses) that both derive upper and lower probability bounds for the output events. We demonstrate the most involved technique, namely the forward technique, for two examples and compare their results to a cutting-edge probabilistic output analysis.
△ Less
Submitted 19 January, 2020;
originally announced January 2020.
-
Confluence of CHR revisited: invariants and modulo equivalence
Authors:
Henning Christiansen,
Maja H. Kirkeby
Abstract:
Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constrain…
▽ More
Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.
△ Less
Submitted 2 October, 2018; v1 submitted 26 May, 2018;
originally announced May 2018.
-
Confluence and Convergence in Probabilistically Terminating Reduction Systems
Authors:
Maja H. Kirkeby,
Henning Christiansen
Abstract:
Convergence of an abstract reduction system (ARS) is the property that any derivation from an initial state will end in the same final state, a.k.a. normal form. We generalize this for probabilistic ARS as almost-sure convergence, meaning that the normal form is reached with probability one, even if diverging derivations may exist. We show and exemplify properties that can be used for proving almo…
▽ More
Convergence of an abstract reduction system (ARS) is the property that any derivation from an initial state will end in the same final state, a.k.a. normal form. We generalize this for probabilistic ARS as almost-sure convergence, meaning that the normal form is reached with probability one, even if diverging derivations may exist. We show and exemplify properties that can be used for proving almost-sure convergence of probabilistic ARS, generalizing known results from ARS.
△ Less
Submitted 3 October, 2017; v1 submitted 15 September, 2017;
originally announced September 2017.
-
On Proving Confluence Modulo Equivalence for Constraint Handling Rules
Authors:
Henning Christiansen,
Maja H. Kirkeby
Abstract:
Previous results on proving confluence for Constraint Handling Rules are extended in two ways in order to allow a larger and more realistic class of CHR programs to be considered confluent. Firstly, we introduce the relaxed notion of confluence modulo equivalence into the context of CHR: while confluence for a terminating program means that all alternative derivations for a query lead to the exact…
▽ More
Previous results on proving confluence for Constraint Handling Rules are extended in two ways in order to allow a larger and more realistic class of CHR programs to be considered confluent. Firstly, we introduce the relaxed notion of confluence modulo equivalence into the context of CHR: while confluence for a terminating program means that all alternative derivations for a query lead to the exact same final state, confluence modulo equivalence only requires the final states to be equivalent with respect to an equivalence relation tailored for the given program. Secondly, we allow non-logical built-in predicates such as var/1 and incomplete ones such as is/2, that are ignored in previous work on confluence.
To this end, a new operational semantics for CHR is developed which includes such predicates. In addition, this semantics differs from earlier approaches by its simplicity without loss of generality, and it may also be recommended for future studies of CHR.
For the purely logical subset of CHR, proofs can be expressed in first-order logic, that we show is not sufficient in the present case. We have introduced a formal meta-language that allows reasoning about abstract states and derivations with meta-level restrictions that reflect the non-logical and incomplete predicates. This language represents subproofs as diagrams, which facilitates a systematic enumeration of proof cases, pointing forward to a mechanical support for such proofs.
△ Less
Submitted 11 November, 2016;
originally announced November 2016.
-
Probabilistic Resource Analysis by Program Transformation
Authors:
Maja H. Kirkeby,
Mads Rosendahl
Abstract:
The aim of a probabilistic resource analysis is to derive a probability distribution of possible resource usage for a program from a probability distribution of its input. We present an automated multi- phase rewriting based method to analyze programs written in a subset of C. It generates a probability distribution of the resource usage as a possibly uncomputable expression and then transforms it…
▽ More
The aim of a probabilistic resource analysis is to derive a probability distribution of possible resource usage for a program from a probability distribution of its input. We present an automated multi- phase rewriting based method to analyze programs written in a subset of C. It generates a probability distribution of the resource usage as a possibly uncomputable expression and then transforms it into a closed form expression using over-approximations. We present the technique, outline the implementation and show results from experiments with the system.
△ Less
Submitted 15 December, 2016; v1 submitted 3 August, 2016;
originally announced August 2016.
-
Probabilistic Output Analysis by Program Manipulation
Authors:
Mads Rosendahl,
Maja H. Kirkeby
Abstract:
The aim of a probabilistic output analysis is to derive a probability distribution of possible output values for a program from a probability distribution of its input. We present a method for performing static output analysis, based on program transformation techniques. It generates a probability function as a possibly uncomputable expression in an intermediate language. This program is then an…
▽ More
The aim of a probabilistic output analysis is to derive a probability distribution of possible output values for a program from a probability distribution of its input. We present a method for performing static output analysis, based on program transformation techniques. It generates a probability function as a possibly uncomputable expression in an intermediate language. This program is then analyzed, transformed, and approximated. The result is a closed form expression that computes an over approximation of the output probability distribution for the program. We focus on programs where the possible input follows a known probability distribution. Tests in programs are not assumed to satisfy the Markov property of having fixed branching probabilities independently of previous history.
△ Less
Submitted 28 September, 2015;
originally announced September 2015.
