PhD topics

Supervisor: Robert Glück (University of Copenhagen, Denmark)
                          glueck@di.ku.dk

Objectives: The DC will advance object-oriented and functional reversible languages with a view on increasing their expressiveness and applicability to the development and construction of non-trivial reversible algorithms. It will build on the work by project members25,26,27. Algorithms of interest may be suggested by WP 2 and WP 4. The DC will also study the integration of reversible features into mainstream irreversible languages (supporting DC 6) to enable a seamless practical application including required type systems. Time-symmetric variants for computable involutions and domain-specific features will be explored to identify novel language idioms specific to reversible programming and future applications.
Expected results: 1) Formalisation and prototype of a reversible object-oriented language; 2) Language technology for and case study of a hybrid mainstream-based language; 3) Study of time-symmetric and domain-specific reversible language idioms.
Planned secondment(s): M19, TOK, S. Yuen, object-oriented feature sets; M24, CNRS, C. Di Giusto, type systems, M32, VAIRE, H. Earley, language validation.

Supervisor: Ivan Lanese (University of Bologna, Italy) 
                          ivan.lanese@gmail.com

Objectives: The DC will study extensions of reversible programming languages to support concurrency and distribution. This includes primitives to spawn processes, and for inter-process interaction, in both the shared memory (with synchronisation to avoid interferences) and the message passing setting. While such extensions can be provided as libraries, modern trends suggest to include such constructs in the core language, as in the (non-reversible) languages Go, Scala or Erlang. Initial work will build on existing reversible programming languages such as Janus, ROOPL or Joule, but the DC will then interact with DC1 to ensure compatibility of the developments.
Expected results: 1) An extension of an existing reversible programming language and of the related theory with primitives for concurrency and distribution 2) An open source implementation of the extension developed in 1)
Planned secondment(s): M14, UCPH, R. Glück, features for reversible languages; M28, AURI, C. Aubert: message passing concurrency; M36, RUG, J. Perez: types for concurrency.

Supervisor: Cinzia Di Giusto (CNRS, France) / Enrico Formenti (Université Côte d'Azur)
                          cinzia.di-giusto@univ-cotedazur.fr 

Objectives: In RC verifying forward computations equipped with distributed backtracking on non-observable actions is equivalent to verifying their causal compression which may be significantly smaller in size and therefore much more efficiently verifiable. Also, classical Linear Temporal Logic (LTL) and unfolding algorithms can be used to model check reversible systems, as an LTL formula with a past operator can be translated in terms of “future” states. This may not be the case with logics such as Computation Tree Logic (CTL) and logics for truly concurrent systems. We plan to investigate new logics for truly concurrent systems with specific operators for causality, consistency and reversible modalities. Model checking will be complemented by runtime monitoring through types. Specifically, for concurrent reversible processes, we will investigate the development of appropriate session type disciplines.
Expected results: 1) Reversible extensions of CTL and logics for true concurrency; 2) Type systems, in particular session types, for reversible languages; 3) Complexity/efficiency analysis of the developed techniques
Planned secondment(s): M19, AGH, I. Ulidowski, reversible logics; M22, UNURB, C. A. Mezzina, reversible model checking; M36, RUG, J. Perez: types and monitoring.

Supervisor: Irek Ulidowski (AGH University of Krakow, Poland)
                          irekulidowski@gmail.com

Objectives: This DC will develop reversible versions of algorithms for standard computation tasks, and deliver reversible versions of fundamental data structures and reversible operations on them. The DC will provide a notation for writing reversible algorithms taking inspiration from the reversible language Janus. The DC will then define methods for converting a traditional algorithm into its reversible version written in our notation, and then into the inverse algorithm that un-computes the result of the original algorithm. These methods will be applied in the areas of lossless compression and decompression of data, where the DC will analyse energy-efficiency as well as space and time complexity. Additionally, the DC will collaborate with DC2 and DC5 and provide support to WP 4 studentships.
Expected results: 1) Notation for reversible algorithms and data structures; 2) Method for converting standard algorithms into reversible versions, and for producing inverted versions of reversible algorithms; 3) Analysis of energy-efficiency, space and time complexity of reversible algorithms; 4) Application to lossless compression and decompression algorithms, and to algorithms from WP 4.
Planned secondment(s): M14, UCPH, R. Glück, Reversible data structures, notation for reversible algorithms; M20, UNIBO, I. Lanese, Converting standard algorithms to their reversible versions; M32, ULEIC, J. Hoey, Analysis of energy-efficiency, space and time complexity of reversible algorithms

Supervisors: Rajeev Raman (University of Leicester,UK) / James Hoey (University of Leicester,UK)
                            jbh13@leicester.ac.uk

Objectives: The aim of this PhD research is twofold. First, the DC will study what it means to reverse and how to reverse concurrent (e.g., non-blocking algorithms with compare-and-swap) and distributed algorithms (e.g., atomic commit and leader election). The DC will first work with DC 2 to develop a notation for reversible concurrent and distributed programs, and then focus on the algorithmic aspects. A toolbox of concurrent and distributed algorithms for both the message passing and shared memory approach will be assembled, and example algorithms will be implemented in the reversible language with concurrency and distribution developed by DC 2.
Expected results: 1) Notation for concurrency and distribution features of reversible algorithms; 2) Reversible versions of relevant concurrent and distributed algorithms; 3) Library of implemented concurrent and distributed algorithms.
Planned secondment(s): M15, UNIBO, I. Lanese, language extension with shared memory concurrency; M22, AGH, I. Ulidowski, extend the algorithm notation of DC 4 with concurrency and distribution; M28, TOK, S. Yuen, concurrency and distribution support.

Supervisor: Ivan Lanese (University of Bologna, Italy)
                          ivan.lanese@gmail.com

Objectives: The DC will study the trade-off between lost information, time complexity and space complexity in reversible algorithms. The work will build on the framework and technique used in the literature 29 to study many specific algorithms and data structures. First, the framework will be implemented and further algorithms and data structures will be considered, e.g., hashing, dynamic programming and geometric algorithms. Then the DC will look for general methodologies and theories to understand the trade-off for given algorithms as well as finding concrete solutions given the desired preferences. Specific algorithms of interest, possibly suggested by WP4 DCs, will be considered to exercise the framework and test its effectiveness. The DC will interact with WP 1 and WP 3 DCs to study the support needed at language and architecture level to enable the execution of partially reversible algorithms.
Expected results: 1) An implementation of a framework in the literature 29 to enable experimentation 2); Analysis of lost information/time/space trade-offs for algorithms of interest; 3) A theory and methodology to study the trade-offs in 1).
Planned secondment(s): M14, UCPH, R. Glück, extended notation for partially reversible algorithms; M33, AGH, I. Ulidowski, reversible and partially-reversible algorithms; M36, UoM, M. Lujan, architectural support for partially reversible algorithms.

Supervisor: Robert Glück (University of Copenhagen, Denmark)
                          glueck@di.ku.dk

Objectives: The DC will study techniques for translating high-level reversible languages to efficient low-level reversible and irreversible representations. Initially the work will build on and develop the prototype compilers for Janus-like and object-oriented reversible languages. The main objective is the development of optimisation techniques for compilation specific to reversible programs, both to reversible and irreversible computer architectures. This includes the development of a benchmark suit specific for reversible compilation.
Expected results: 1) Foundations and novel techniques for optimising compilers comprising program analysis and code generation; 2) Prototype compiler for a Janus-like and an object-oriented reversible language; 3) Benchmark suits and empirical evaluation.
Planned secondment(s): M16, THM, U. Meyer, compilers and optimisation; M21, UoM, M. Lujan, instruction set architecture

Supervisor: Mikel Lujan (University of Manchester, UK)
                            Mikel.Lujan@manchester.ac.uk
                            

Objectives: This DC will start surveying the state-of-the-art RC architectures, their instruction sets, and their main implementations. The DC will then first work on developing a software simulation platform for reversible architectures. He/she will follow the concept of chiplets, with an energy-efficient chiplet dedicated to traditional processing (e.g. Arm-based processing cores). These cores would provide I/O, bootup, configuration and, if needed, would be Linux capable. A second chiplet would be dedicated to general purpose computing using RC adiabatic architectures. The simulation and novel reversible architectures on the second chiplet would be the main research topic. Additionally, the DC will investigate the interaction between standard processors and RC architectures.
Expected results: 1) Simulation platform for general purpose architecture based on RC; 2) Energy simulation platform for general purpose RC architecture; 3) Novel insights in combining standard processing cores with new RC architectures
Planned secondment(s): M14, UCPH, R. Glück, requirements from compilation; M25, SDU, U. P. Schultz, simulation of drones architectures

Supervisors: Luca Peres (University of Manchester, UK) / Oliver Rhodes (University of Manchester, UK)
                            luca.peres-2@manchester.ac.uk

Objectives: This DC will study the applicability of RC to non-von Neumann architectures, namely neuromorphic systems. In conjunction with DC 8, the DC will start surveying the state-of-the-art reversible architectures, but this will focus on neural simulations and will target neuromorphic computing. Neuromorphic computing aims to develop unconventional low energy architectures inspired by biological neural networks with emphasis on connectivity, recurrence and higher time resolutions. These platforms can in principle require less energy and target ML and AI. This DC will collaborate on developing the fundamentals of the simulation platform for RC architectures accelerating neural networks simulations and ML applications. The interaction between the standard chiplet and novel reversible neuromorphic accelerators would be the main research topic. This DC will work on architectures that will be beneficial for cyber-physical systems (collaborating with DC 12 on RC algorithms for aerial robots) and for ML applications (targeting platforms which can accelerate techniques developed by DC 13), enabling reversible on-chip online learning paradigms and efficient neural networks simulations.

Expected results: 1) Simulation platform for RC neuromorphic systems; 2) Energy simulation platform for RC neuromorphic architectures; 3) Novel insights in combining standard processing with new reversible computing-based neuromorphic systems.
Planned secondment(s): M14, SDU, U. P. Schultz, requirements for neuromorphic architectures for cyber-physical systems; M31, AGH, I. Ulidowski, neuromorphic architectures and neural networks

Supervisor: Rodolfo Rosini
                          rodolfo@vaire.co

Objectives: The DC will work on designing and realizing resonant adiabatic reversible circuits targeting specific computations of interest, such as matrix multiplications and other algorithms used for Large Language Models and Multimodal ones. The circuits will be first designed and then realised using custom EDA tooling provided by VAIRE. Measurements of energy consumption will be performed and contrasted against irreversible circuits computing the same function, to check that the expected energy savings take place. They will also be contrasted against results of simulations of the same circuits to validate the simulation models of DC 8.
Expected results: 1) Design of circuits to accelerate inference in various neural networks 2) Practical realisation of circuits in collaboration with the VAIRE layout team 3) Energy measurements of the circuits
Planned secondment(s): M26, UoM, M. Lujan, assessing the results of simulation, M39, AGH, I. Ulidowski, application to ML, M41, SDU, U. P. Schultz, application to drones

Supervisor: Claudio Sacerdoti Coen (University of Bologna, Italy)
                          claudio.sacerdoticoen@unibo.it

Objectives: The DC will study how to make algorithms used in blockchains reversible or partially reversible. He/she will first focus or one or more blockchains (e.g. Bitcoin and Ethereum) and their implementations to identify the parts of the code that are more responsible for energy consumption unrelated to packet transmission in a few scenarios (proof-of-work vs proof-of-stake, chain validation vs mining). More likely, one such part will be the implementation of the SHA-256 algorithm used at the base of the proof-of-work algorithm of Bitcoin. Then, the DC will try to rephrase those parts as partially reversible algorithms exploiting existing reversible programming languages such as Janus, RFun or Joule, but the DC will then interact with DC1 to exploit languages developed by the latter. It will also interact with DC4 and DC6 to exploit advances in reversible and partially reversible algorithms. Finally, the DC will focus on decentralised applications (DAPPS), also called smart contracts. DAPPS are usually written in high-level, resource aware languages that are later compiled into bytecodes that are interpreted by the nodes of the blockchain during chain validation and mining. All these languages allow rollbacks to abort computations for various reasons and restore the initial state. The natural research question here is to which extent the high-level and the bytecode languages can be made reversible, and whether a reversible interpreter for them can benefit from their reversibility, e.g. during rollback, ultimately also mitigating energy consumption.
Expected results: 1) Identification of energy-critical algorithms and their implementation in standard blockchains, including SHA-256, 2) A reversible or partially reversible implementation of SHA-256 algorithm, 3) A proposal for reversible bytecode and high-level languages for distributed applications, together with reversible compilers and interpreters.
Planned secondment(s): M19, AGH, I. Ulidowski, reversible algorithms; M33, UNICA, M. Bartoletti, reversibility in smart contracts; M38, UCPH, R. Glück, smart code compilation.

Supervisor: Ulrik Pagh Schultz (University of Southern Denmark, Denmark)
                          ups@mmmi.sdu.dk

Objectives: The DC will study the use of RC for programming low-energy cyber-physical systems, such as fixed-wing aerial robots or IoT devices, where a large proportion of the energy consumption can be from computation rather than actuation or communication. Reversible programming languages will be used to implement relevant algorithms, and they will be integrated into a simulated implementation of each cyber-physical system. Algorithms are expected to include both fully and partially reversible algorithms, for example compression of data collected from sensors and image analysis algorithms. Energy consumption of the cyber-physical system as a whole will be estimated by a dual approach combining energy estimates of the RC hardware and of the cyber-physical system as a
whole. A key research question lies in determining the extent to which energy savings depend on the I/O properties of the system, e.g., lossless compression of sensor data in an IoT device versus extracting information from an input image for control of an aerial robot.
Expected results: 1) Identification of energy-critical fully or partially reversible algorithms relevant for use in low-energy cyber-physical systems; 2) Modelling framework for estimating the energy impact of reversibility on cyber-physical systems; 3) Proof of concept implementation of aerial robot and IoT systems using reversible algorithms.
Planned secondment(s): M15, UNIBO, I. Lanese, partially reversible algorithms; M32, UoM, M. Lujan, modelling framework

Supervisors: Irek Ulidowski (AGH University of Krakow, Poland) / Crefeda Rodrigues (ARM limited, UK)
                            irekulidowski@gmail.com / Crefeda.Rodrigues@arm.com

Objectives: This DC aims at applying reversible computation techniques (in collaboration with DC4 and DC6) as well as other energy saving approaches to enhance energy efficiency in ML, and more specifically in Deep Neural Networks (DNN). Energy consumption will be estimated using approaches from the literature. We will re-design algorithms and re-develop software components used in the training phase of DNN layers by applying reversibility and other energy saving approaches. Concurrently, we will create modelling frameworks for estimation of energy consumption that are appropriate for experimenting with software at instruction and application levels. We will then carry out measurements and analysis work to empirically evaluate suitability of (a) the energy modelling frameworks, and of (b) the proposed energy reducing techniques.
Expected results: 1) Development of reversible versions of DNN layer learning algorithms, also enhanced with other energy saving features; and their implementations; 2) Formulation of suitable models for estimation of energy consumption of software, called the energy models; 3) Measurement of energy consumption of the developed software, and evaluation of the energy models; 4) Analysis of the effect of reversible computation techniques and other approaches on energy efficiency, as well as on time and space complexity.
Planned secondment(s): ULEIC, M16, R. Raman, reversing algorithms for DNNs, developing their implementations; M21, UoM, M. Lujan, models to estimate energy consumption of software, experiments to measure it; M32, VAIRE, H. Earley, language validation.