Reversible Computing and Programming

PhD defence by Holger Bock Axelsen


Reversible computing is the study of computation models that are both forward and backward deterministic, without any logical information loss. This has profound implications on the theory, analysis and application of these computation models. Historically, work on reversible computing has focused on reversible simulations of irreversible computations. Such simulations incur computational overheads, in particular in the form of extraneous garbage information left in the computational state at halting. In this work, we take the viewpoint that the property of reversibility itself should be the starting point of a computational theory of reversible computing. In particular, we study how garbage-free reversible computing works in the theoretical setting of Turing machines, and at the various abstraction levels of a reversible programmable system, ranging from high-level programming languages to low-level circuit designs.

We develop a semantical framework to study the properties of reversible Turing machines, including, but not limited to, those resulting from reversible simulations. In this framework we construct a universal reversible Turing machine from first principles, prove robustness under various resource reductions, and establish the time complexity of multitape simulation. We further show that reversible logspace is characterized by reversible multi-head finite automata.

For practical reversible programming we formalize an abstract reversible machine for low-level languages. We extend the high-level imperative language Janus, and describe a programming methodology for its use. We give efficient garbage-free compilation schemes from Janus to the abstract reversible machine. We also propose a novel reversible flowchart computation model, and use it to show that structured and unstructured reversible programming are equally powerful.

Going deeper in the programming stack, we propose new reversible logic designs for a ripple-carry block adder; and an ALU providing a wider array of functionalities at comparatively low cost. The ALU is used in the proposal of the Bob architecture, which binds our language, logic and theoretical results together in a compact reversible logic design for a simple machine with a universal reversible instruction set architecture.

We believe that these contributions provide evidence that garbage-free reversible computing is feasible and practical at all abstraction levels of the programming stack, and that this also holds for the underlying abstract computation models.

Academic Committee:

Chairman: Associate Professor Torben Ægidius Mogensen, DIKU, University of Copenhagen, Denmark
Professor Kenichi Morita, Department of Information Engineering, Hiroshima University, Japan
Junior Professor Janis Voigtländer, Institute for Computer Science, University of Bonn, Germany

Academic Advisor:

Associate Professor Robert Glück, DIKU, University of Copenhagen, Denmark