International Training School on Reversible Computation

Abstract: Computing models that have a read-only input tape, may be equipped with further resources, and evolve in discrete time are considered from the viewpoint of logical reversibility. Since such abstract models may serve as prototypes of machines which can be physically constructed it is interesting to study their capabilities to perform computations reversible. In essence, the reversibility of a deterministic computation means that every configuration has a unique successor configuration and a unique predecessor configuration. The talk covers the notion of reversibility and its possible definitions. In which way is the predecessor configuration computed? Do we have to consider all possible configurations as potential predecessors? Or only configurations that are reachable from some initial configurations? We present some selected aspects as gradual reversibility, time-symmetry, and decidability as well as results on the computational and descriptional capacity of several logical reversible devices.

Biography: Martin Kutrib received the Diploma in informatics from the University of Braunschweig in 1989, and the Dr.\ degree from the Department of Mathematics, University of Giessen, in 1993. From 1994 to 1995 he was a Visiting Researcher at the University of Siegen. Since 1997 he has been with the Institute of Informatics at the University of Giessen, where he received the postdoctoral lecture qualification (Habilitation) in 1999. Currently he holds the position of a professor for theoretical computer science. His current research interests include automata theory, formal languages and grammars, reversibility, parallel automata and their algorithms, complexity and descriptional complexity. He is co-editor-in-chief of Journal of Automata, Languages, and Combinatorics, a member of the editorial boards of International Journal of Unconventional Computing and Journal of Cellular Automata, co-editor of special issues of several journals, member of the IFIP WG Cellular Automata and Discrete Complex Systems and member of the IFIP WG Descriptional Complexity, and SC and PC member of several international conferences. He is author and co-author of more than 200 publications in international journals and conference proceedings and gave scientific talks at conferences and workshops in 35 countries on 5 continents.

Abstract: We introduce the main concepts related to reversibility for concurrent interacting systems, with particular emphasis on causal-consistent reversibility. We first consider an uncontrolled setting, useful to study the kind of history and causal information needed to enable reversibility. We then discuss different ways for controlling reversibility, namely to decide which actions can be undone and when. We also discuss how to avoid undesired loops using alternatives. We illustrate our presentation with examples on the process calculus CCS.

An overview of the main topics we will consider is available in:
Ivan Lanese, Claudio Antares Mezzina, Francesco Tiezzi: Causal-Consistent Reversibility. Bulletin of the EATCS 114 (2014)

Biography: Ivan Lanese got the PhD degree in Computer Science in 2006 at University of Pisa (Italy). After his PhD he worked first as a post-doc and then as a researcher in the Department of Computer Science and Engineering of University of Bologna (Italy). He is currently a member of the FOCUS team, a joint team between University of Bologna and INRIA (France). Ivan Lanese research interests are in the field of formal models for concurrent and distributed systems. He studies reversibility for such systems since 2009. Other research interests include process calculi and semantics, service-oriented systems, long running transactions, and choreographic programming. Ivan Lanese has many ongoing collaborations in Italy (Lucca, Padova, Torino, ...) and abroad (Lisbona, Grenoble, Leicester, Oslo, Buenos Aires, ...). Ivan Lanese activity has been performed in the framework on many Italian, French and European projects, including the European COST Action on "Reversible computation - extending horizons of computing" where he is vice-chair, and the French project REVER on "Programming reversible recoverable systems". As a result of his work, Ivan Lanese published about 40 research papers in international conferences and journals.

Abstract: Cellular automata are massively parallel and homogeneous systems of simple processors, called the cells, that update their states synchronously using a local update rule that gives the new state of a cell based on the previous states of its neighbors. A cellular automaton is reversible if there is an inverse cellular automaton that retraces the evolution step-by-step back in time. We explain the classical results by Hedlund, Moore and Myhill that link injectivity, surjectivity and reversibility. We discuss computational universality by reversible cellular automata and some decidability questions. We also discuss aspects of local reversibility vs. global reversibility in cellular automata.

Biography: Jarkko Kari received a PhD in mathematics in 1990 at the University of Turku, Finland. He has worked for the Academy of Finland, Iterated Systems Inc., the University of Iowa, and the University of Turku, where he has a position as a professor of mathematics since year 2000. Jarkko Kari has supervised eight PhD theses, and published over one hundred research articles on automata theory, cellular automata and image processing. He currently serves in the editorial boards of eight international journals.

Abstract: The semantics of reversible processes is a current topic of research. Whatever eventual solutions may be proposed, it seems clear that they will have to take into account (1) concurrency between events and (2) reverse transitions as well as forward transitions. Moreover it seems likely that true concurrency models will be used. We describe a hierarchy of bisimulation-based equivalences on configuration structures, a particular model of true concurrency closely related to event structures and Petri nets. These equivalences are obtained using forward and reverse transitions, where a transition may involve multiple events. We furthermore discuss how these equivalences can be characterised by logics with forward and reverse modalities. These logics can be used to characterise individual configuration structures up to a given equivalence.

Biography: Iain Phillips received a DPhil in mathematical logic from the University of Oxford. After spending a year as a lecturer at the University of Minnesota, he became a research assistant in the Department of Computing at Imperial College, London, where he is now a Senior Lecturer. His research is on the theory of concurrency, most recently in the context of reversible computation.

Abstract: This course introduces the principles and methods of programming using reversible while-languages. We illustrate clean reversible programming with examples, and show how static and dynamic data structures can be used in reversible programming. We discuss concrete tools such as program inverters, and introduce the syntax and semantics of Janus. The course will be complemented with practical exercises.

Biography: Robert Glück is an Associate Professor of Computer Science at the University of Copenhagen, Denmark. He received his PhD degree and Habilitation in Austria. He is a member of the Steering Committee of the Reversible Computing Conferences. His main research interests are programming languages and software systems. His recent research is related to reversible computing, partial evaluation, and metacomputation.

Abstract: RFun is a simple first-order reversible functional programming language. This training session will introduce RFun and its typesystem, and detail how linearity and the “first-match policy” ensures reversibility of programs. In general this can only be guaranteed at run-time, but we will see that with a clever implementation and correct usage of the typesystem this can often be done statically. We will give reversible implementations of many of the classical functions including map, zip, and right- and left-scan. We will also introduce the interpreter and help you to implement your own functional program.

Biography: Michael Kirkedal Thomsen is assistant professor at DIKU, Department of Computer Science, University of Copenhagen, Denmark. At DIKU and while being Marie Curie fellow at the University of Bremen, Germany he has worked on the topic of Reversible Computations with in in relations to hardware description languages, models describing reversible logic and reversible logic circuits, and computer architectures. Recently he has focused on designing languages general-propose reversible programming languages and applications of reversibility to optimistic execution, testing, reliability and security.

Abstract: This lecture describes the motivation and application areas for reversible computation with incremental state saving. We discuss how program state can be maintained and restored in the presence of memory allocation, destructive updates (assignments), and floating point computation. The discussed methods are applicable to arbitrary C++11 programs, which are in general irreversible programs. We will also discuss the forward-reverse-commit paradigm and performance aspects of the respective forward/reverse/commit functions with incremental state saving. The open-source tool Backstroke for generating reversible C++11 code and its runtime library for maintaining the state information is discussed in detail. For one selected application area of reverse code generation, parallel computing and synchronization, we discuss the time warp algorithm for optimistic parallel discrete event simulation (PDES). The time warp algorithm is a very good example for the importance of reversible execution, because its roll back mechanism requires reversibility. Performance results of PDES simulations using incremental state saving and an overview of possible further enhancements and concepts for the combination with reversible languages conclude the lecture.

Biography: Markus Schordan joined the Center for Applied Scientific Computing (CASC) at Lawrence Livermore National Laboratory in April 2013 as a senior computer scientist. His research interests include program analysis and formal software verification, reversible computation, and compiler construction. He is co-author of the software verification tool CodeThorn, the tool Backstroke for reversible computation, and the ROSE compiler infrastructure. He received a Diploma Degree in computer science from TU Vienna in 1997, and a PhD degree from University Klagernfurt in 2001 (with distinction). He is author or co-author of 35+ peer-reviewed publications. He is a member of the IFIP Working group 2.4 Software Technology, the ACM, and IEEE. In 2009 he received an R&D 100 AWARD (ROSE), in 2011 a Best Paper Award at the 11th IEEE Source-Code and Manipulation Conference (SCAM 2011), and in 2012 and 2013 the Method Combination Award in the RERS Challenges (an international software verification competition). In 2014 and 2015 he won the RERS Challenge (Team Markus Schordan and Marc Jasper). He has served as co-organizer of the ISoLA 2016 track "Evaluation and Reproducibility of Program Analysis and Verification", the ISoLA 2014 track "Evaluation and Reproducibility of Program Analysis", the workshops GPUScA 2011 and GPUScA 2010, the Dagstuhl Seminar No. 08161, and the ISoLA'08 Track: Formal Methods for Analysing and Verifying Very Large Systems, and the EuroPar'03 Topic 04: Compilers for High-Performance. He served as program committee member of several conferences, most recently ISoLA 2016, RC 2016, Euro-Par 2015, SYNASC 2015, SOFSEM 2015, ISoLA 2014, SYNASC 2014, SYNASC 2013, ARW 2013, SYNASC 2012, GPGPU-5 2012.

Abstract: Reverse debugging is the ability of a debugger to stop after a failure in a program has been observed and go back into the history of the execution to uncover the reason for the failure. The implications behind this simple definition are very deep, and not easy to achieve especially when dealing with distributed programs. Nowadays we can witness a huge effort from the software industry to provide tools such as reversible debuggers to ease software development.
In this lecture will overview the existing techniques related to reversible debugging and re-execution of concurrent distributed systems with a particular focus on industrial solutions. We then introduce a novel debugging approach based on causal-consistent reversibility.

References: [1] Jakob Engblom: A review of reverse debugging. In System, Software, SoC and Silicon Debug Conference (S4D), 2012
[2] Elena Giachino, Ivan Lanese, Claudio Antares Mezzina: Causal-Consistent Reversible Debugging. FASE 2014: 370-384

Biography: Dr. Claudio Antares Mezzina is an assistant professor of IMT Institute for Advanced studies Lucca (Italy). He received his PhD in Computer Science and Engineering, from both Université Joseph Fourier (France) and University of Bologna (Italy) in February 2012, under the supervision of Jean-Bernard Stefani and Davide Sangiorgi. During his PhD he focused on the interplay between concurrency and reversibility in the setting of Higher-Order Pi. Before, he received a Laurea Degree cum laude from the University of Bologna (October 2007). Since February 2008 he has been a member of the SARDES team at INRIA Rhone Alpes in Grenoble. Before joining the SysMA research unit at IMT in December 2014, he has been researcher within the SOA team at FBK in Trento working on adaptable business processes, goal models and smart cities.
Claudio Mezzina research interests lie in the area of semantics of programming languages and concurrency theory, with a particular focus on programming abstractions for faults-tolerant systems. Since 2008 he studies reversibility as a means to build reliable distributed systems.

Abstract: Reversible circuits realize bijective functions and are usually comprised as a cascade of reversible gates where fanout and feedback are not directly allowed. Accordingly, the synthesis of this kind of circuits significantly differs from approaches known for synthesis of conventional circuits. In the past, several approaches have been introduced which synthesize a reversible circuit from a given function. This lecture provides an introduction into reversible circuits and corresponding descriptions as well as gives an overview on the proposed synthesis schemes. This provides the basis for the following lectures that cover the respective solutions in more detail.

Biography: Robert Wille is Professor for Integrated Circuit and System Design at the Johannes Kepler University, Linz, Austria. He received the Diploma and Dr.-Ing. degrees in computer science from the University of Bremen, Germany, in 2006 and 2009, respectively. He has been with the Group of Computer Architecture, University of Bremen, Bremen, Germany, from 2006 to 2015 and with the German Research Center for Artificial Intelligence (DFKI), Bremen, Germany, from 2013 onwards. Additionally, he worked as Lecturer at the University of Applied Science, Bremen, Bremen, Germany, and as Visiting Professor at the University of Potsdam, Potsdam, Germany, and the Technical University Dresden, Dresden, Germany. His research interests are in the design of circuits and systems for both conventional and emerging technologies.

Abstract: RevKit is an open source framework for logic synthesis and has been actively developed since 2009. Several reversible synthesis algorithms, particularly many of those being introduced in the lectures at the training school, have an implementation in RevKit. This introductory lecture will show the basic usage of RevKit, how to read and write files, how to inspect files, and the general functionality of the program. A second lecture will show how to invoke the synthesis algorithms after they have been introduced in the lecture.

Biography: Mathias Soeken works as a researcher at the Integrated Systems Laboratory at EPFL, Lausanne, Switzerland. From 2009 to 2015 he worked at the University of Bremen, Germany. Since 2014, he is a regularly visiting post doc at UC Berkeley, CA, USA in the group of Robert K. Brayton. He holds a Ph.D. degree (Dr.-Ing.) in Computer Science from University of Bremen, Germany (2013). He is in active collaboration UC Berkeley, Microsoft Research, and imec, and maintaining the widely used logic synthesis frameworks RevKit and CirKit. His research interests are logic synthesis, reverse engineering, formal verification, and quantum computing.

Abstract: Today's rapid advances in the physical implementation of quantum computers demand for scalable synthesis methods in order to map practical logic designs to quantum architectures. In the lecture, we level hierarchical synthesis algorithms. Hierarchical synthesis algorithms are scalable while allowing reasonable space/time tradeoffs at the same time. Several hierarchical synthesis algorithms have been presented in the past, e.g., based on binary decision diagrams and logic networks. We show how they work and how they are employed today’s design flows for quantum computing.

Abstract: In this lecture, selected approaches to synthesis of reversible circuits will be presented. First, the development of different cycle-based synthesis algorithms will be described in a chronological order. It is worth to mention that they are among those considered as the most successful ones. Next, synthesis of exact optimal circuits for all 4-variable reversible functions will be introduced. The lecture will conclude with a brief presentation of another interesting approaches to synthesis and discussions on current state-of-the-art.

Abstract: This lecture covers further directions of reversible circuit design. We outline and discuss currently discussed solutions towards the design of reversible circuits by means of hardware description languages. Besides that, we review how the methods proposed thus far already help in various applications such as encoder design, interconnects, adiabatic circuits, etc. and how they may even provide benefits in further applications beyond that.

Abstract: Quantum computers have the potential to perform certain computations significantly faster than any classical computers. However, to achieve such performance, quantum algorithms need to be designed and implemented to execute efficiently on a quantum computer. The reversibility of operations is essential for the implementation of these quantum algorithms. For instance, testing logical expressions is an important building block of several quantum algorithms such as the Grover’s search algorithm. The need for operations reversibility has made quantum computing one of the main applications of reversible logic synthesis.

When synthesising reversible quantum circuits, several parameters such as the number of qubits, the number of quantum operations and their types, are critical for the management of the quantum computer resources and the fault-tolerance of the quantum operations. Therefore, the selection of the appropriate logic synthesis technique is important for implementing efficiently the quantum algorithms.

In this training session:
i) We will introduce quantum computing and its applications.
ii) We will see how we can use the QX Quantum Computer Simulator to simulate the execution of quantum algorithms on a realistic quantum computer.
ii) We will use reversible logic synthesis techniques to build quantum circuits, simulate their executions and compare different synthesis techniques.
iii) Finally, we will use reversible logic synthesis to implement a practical quantum application : the Grover’s search algorithm.

Biography: After getting his Electrical Engineering degree from the National School of Engineering of Brest (ENIB) in France, Nader Khammassi pursued his PhD at the National Engineering School of Advanced Technology (ENSTA) in Brittany, the focus of his research was on High Performance Computing (HPC) and more particularly on parallel programming for multicore architectures. During his PhD, Nader worked as a research engineer at Thales Airborne Systems on the implementation of several high performance signal processing algorithms for electronic warfare applications and obtained his doctorate in 2014. In 2015, he joined the Quantum Computing Lab of QuTech at the Delft University of Technology in the Netherlands. The current topic of Nader's research is the design of a scalable quantum computer architecture, in particular he is focusing is on designing high performance simulation tools for quantum computers and the compilation of quantum algorithms for different quantum computing devices.