nach oben

2015 | Buch

Kapitel lesen Erstes Kapitel lesen

Reversible Computation

7th International Conference, RC 2015, Grenoble, France, July 16-17, 2015, Proceedings

herausgegeben von: Jean Krivine, Jean-Bernard Stefani

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 7th International Conference on Reversible Computation, RC 2015, held in Grenoble, France in July 2015. The 19 papers presented together with 1 invited talk were carefully reviewed and selected from 30 submissions. The Conference on Reversible Computation particularly includes the following topics: reversible machines, reversible languages, design and verification of quantum circuits, design of reversible circuits and circuit synthesis.

Inhaltsverzeichnis

Frontmatter

Invited Paper

Frontmatter

Moment Semantics for Reversible Rule-Based Systems

Abstract

We develop a notion of stochastic rewriting over marked graphs – i.e. directed multigraphs with degree constraints. The approach is based on double-pushout (DPO) graph rewriting. Marked graphs are expressive enough to internalize the ‘no-dangling-edge’ condition inherent in DPO rewriting. Our main result is that the linear span of marked graph occurrence-counting functions – or motif functions – form an algebra which is closed under the infinitesimal generator of (the Markov chain associated with) any such rewriting system. This gives a general procedure to derive the moment semantics of any such rewriting system, as a countable (and recursively enumerable) system of differential equations indexed by motif functions. The differential system describes the time evolution of moments (of any order) of these motif functions under the rewriting system. We illustrate the semantics using the example of preferential attachment networks; a well-studied complex system, which meshes well with our notion of marked graph rewriting. We show how in this case our procedure obtains a finite description of all moments of degree counts for a fixed degree.

Vincent Danos, Tobias Heindel, Ricardo Honorato-Zimmer, Sandro Stucki

Reversible Machines

Frontmatter

A Hierarchy of Fast Reversible Turing Machines

Abstract

Reversible Turing machines with a working tape and a one-way or two-way read-only input tape are considered. We investigate the classes of languages acceptable by such devices with small time bounds in the range between real time and linear time, i.e., time bounds of the form \(n+r(n)\) where \(r\in o(n)\) is a sublinear function. It is shown that there exist infinite time hierarchies of separated complexity classes in that range. We then turn to the question of whether reversible Turing machines in the range of interest are weaker than general ones or not. This is answered in the affirmative by proving that there are languages accepted by irreversible one-way Turing machines in real time that cannot be accepted by any reversible one-way machine in less than linear time.

Holger Bock Axelsen, Sebastian Jakobi, Martin Kutrib, Andreas Malcher

Real-Time Methods in Reversible Computation

Abstract

Bennett has shown how to simulate arbitrary forwards-only computations by fully reversible computation. In particular he has given a space-efficient linear time simulation. After describing a different linear-time reversible simulation with improved space efficiency, we initiate the study of real-time simulations. In addition to being linear-time, these must offer continuous progress, meaning that the delay between successive forward events must be bounded by a constant.

Tommi Pesu, Iain Phillips

Reversible Ordered Restarting Automata

Abstract

Stateless deterministic ordered restarting automata characterize the class of regular languages. Here we introduce a notion of reversibility for these automata and show that each regular language is accepted by such a reversible stateless deterministic ordered restarting automaton. We study the descriptional complexity of these automata, showing that they are exponentially more succinct than nondeterministic finite-state acceptors. We also look at the case of unary input alphabets.

Friedrich Otto, Matthias Wendlandt, Kent Kwee

Reversible Languages

Frontmatter

Garbage Collection for Reversible Functional Languages

Abstract

Reversible languages are programming languages where all programs can run both forwards and backwards. Reversible functional languages have been proposed that use symmetric pattern matching and data construction. To be reversible, these languages require linearity: Every variable must be used exactly once, so no references are copied and all references are followed exactly once. Copying of values must use deep copying. Similarly, equality testing requires deep comparison of trees.

A previous paper describes reversible treatment of reference counts, which allows sharing of structures without deep copying, but there are limitations. Applying a constructor to arguments creates a new node with reference count 1, so pattern matching is by symmetry restricted to nodes with reference count 1. A variant pattern that does not change the reference count of the root node is introduced to allow manipulation of shared data. Having two distinct patterns for shared and unshared data, however, adds a burden on the programmer.

We observe that we can allow pattern matching on nodes with arbitrary reference count if we also allow constructor application to return nodes with arbitrary reference counts. We do this by using maximal sharing: If a newly constructed node is identical to an already existing node, we return a pointer to the existing node (increasing its reference count) instead of allocating a new node with reference count 1.

To avoid searching the entire heap for an identical node, we use hash-consing to restrict the search to a small segment of the heap. We estimate how large this segment needs to be to give a very low probability of allocation failure when the heap is less than half full. Experimentally, we find that overlapping segments gives dramatically better results than disjoint segments.

Torben Ægidius Mogensen

Reverse Code Generation for Parallel Discrete Event Simulation

Abstract

Reverse computation has become a central notion in discrete event simulation over the last decade. It is not just a theoretical line of research, but an immensely practical one that is necessary to achieve high performance for large parallel discrete event simulations (PDES). The models that are implemented for PDES are of increasing complexity and size and require various language features to support abstraction, encapsulation, and composition when building a simulation model. In this paper we focus on parallel simulation models that are written in C++ and present an approach for automatically generating reverse code for C++. The strategy we have adopted for our approach is to first assure that we can correctly handle event methods that use the entire C++ language. Although a significant runtime overhead is introduced with our technique, the assurance that the reverse code is always generated fully automatically is an enormous win that can open the door to routine optimistic simulation with models that can be implemented using the entire C++ language.

Markus Schordan, David Jefferson, Peter Barnes, Tomas Oppelstrup, Daniel Quinlan

Towards a Domain-Specific Language for Reversible Assembly Sequences

Abstract

Programming industrial robots for small-sized batch production of assembly operations is challenging due to the difficulty of precisely specifying general yet robust assembly operations. We observe that as the complexity of assembly increases, so does the likelihood of errors. We propose that certain classes of errors during assembly operations can be addressed using reverse execution, allowing the robot to temporarily back out of an erroneous situation, after which the assembly operation can be automatically retried. Moreover, reversibility can be used to automatically derive a disassembly sequence from a given assembly sequence, or vice versa.

This paper presents the initial design of the RASQ domain-specific language (DSL) for specifying such assembly sequences, based on initial experiments using an industrial case study. The language is defined in terms of a formal semantics corresponding to a realistic execution model currently under implementation. The DSL is used as part of a software framework that aims at tackling uncertainties through a combination of reverse and probabilistic execution.

Ulrik Pagh Schultz, Johan Sund Laursen, Lars-Peter Ellekilde, Holger Bock Axelsen

Design and Verification of Quantum Circuits

Frontmatter

Reversibility in Extended Measurement-Based Quantum Computation

Abstract

When applied on some particular quantum entangled states, measurements are universal for quantum computing. In particular, despite the fondamental probabilistic evolution of quantum measurements, any unitary evolution can be simulated by a measurement-based quantum computer (MBQC). We consider the extended version of the MBQC where each measurement can occur not only in the \(\{X,Y\}\)-plane of the Bloch sphere but also in the \(\{X,Z\}\)- and \(\{Y,Z\}\)-planes. The existence of a gflow in the underlying graph of the computation is a necessary and sufficient condition for a certain kind of determinism. We extend the focused gflow (a gflow in a particular normal form) defined for the \(\{X,Y\}\)-plane to the extended case, and we provide necessary and sufficient conditions for the existence of such normal forms.

Nidhal Hamrit, Simon Perdrix

A Fully Fault-Tolerant Representation of Quantum Circuits

Abstract

We present a quantum circuit representation consisting entirely of qubit initialisations (I), a network of controlled-NOT gates (C) and measurements with respect to different bases (M). The ICM representation is useful for optimisation of quantum circuits that include teleportation, which is required for fault-tolerant, error corrected quantum computation. The non-deterministic nature of teleportation necessitates the conditional introduction of corrective quantum gates and additional ancillae during circuit execution. Therefore, the standard optimisation objectives, gate count and number of wires, are not well-defined for general teleportation-based circuits. The transformation of a circuit into the ICM representation provides a canonical form for an exact fault-tolerant, error corrected circuit needed for optimisation prior to the final implementation in a realistic hardware model.

Alexandru Paler, Ilia Polian, Kae Nemoto, Simon J. Devitt

Equational Reasoning About Quantum Protocols

Abstract

Communicating Quantum Processes (CQP) is a quantum process calculus that applies formal techniques from classical computer science to concurrent and communicating systems that combine quantum and classical computation. By employing the theory of behavioural equivalence between processes, it is possible to verify the correctness of a system in CQP. The equational theory of CQP helps us to analyse quantum systems by reducing the need to explicitly construct bisimulation relations. We add three new equational axioms to the existing equational theory of CQP, which helps us to analyse various quantum protocols by proving that the implementation and specification are equivalent. We summarise the necessary theory and demonstrate its application in the analysis of quantum secret sharing. Also, we illustrate the approach by verifying other interesting and important practical quantum protocols such as superdense coding, quantum error correction and remote CNOT.

Simon J. Gay, Ittoop V. Puthoor

Design of Reversible Circuits

Frontmatter

Design and Fabrication of a Microprocessor Using Adiabatic CMOS and Bennett Clocking

Abstract

This paper will describe the design and implementation of a MIPS-based microprocessor using Bennett clocking to implement reversible logic. In Bennett clocking the clock signals form a “cascade” that moves information forward through logic gates in the compute phase, and then recovers energy during a decompute phase, forming a reversible logic circuit. New logic design and verification tools were developed, using structural Verilog and extensions to ModelSim to address the issues of adiabatic clocking, tools that are currently unavailable in commercial packages. The microprocessor is based on a simplified version of the MIPS architecture. After verification by our design tools it was then implemented using CMOS standard cells based on split-level charge recovery logic. The final design contains approximately 5700 transistors, and is currently being fabricated at MOSIS.

Ismo K. Hänninen, César O. Campos-Aguillón, Rene Celis-Cordova, Gregory L. Snider

Improved Algorithms for Debugging Problems on Erroneous Reversible Circuits

Abstract

Reversible circuits and their synthesis methods have been actively studied in order to realize reversible computation. However, there are few known ways to debug erroneous reversible circuits. In this paper, we propose new algorithms for debugging problems. For single gate error, we improve the theoretical efficiency of previous methods, which use worst case exponential time algorithms such as SAT or decision diagrams. We also propose an algorithm debugging multiple gate error circuits by using \(\pi \)DDs, decision diagrams for permutation sets. We evaluate our algorithms theoretically and experimentally, and confirm significant improvement.

Yuma Inoue, Shin-ichi Minato

Ricercar: A Language for Describing and Rewriting Reversible Circuits with Ancillae and Its Permutation Semantics

Abstract

Previously, Soeken and Thomsen presented six basic semantics-preserving rules for rewriting reversible logic circuits, defined using the well-known diagrammatic notation of Feynman. While this notation is both useful and intuitive for describing reversible circuits, its shortcomings in generality complicates the specification of more sophisticated and abstract rewriting rules.

In this paper, we introduce Ricercar, a general textual description language for reversible logic circuits designed explicitly to support rewriting.

Taking the not gate and the identity gate as primitives, this language allows circuits to be constructed using control gates, sequential composition, and ancillae, through a notion of ancilla scope. We show how the above-mentioned rewriting rules are defined in this language, and extend the rewriting system with five additional rules to introduce and modify ancilla scope. This treatment of ancillae addresses the limitations of the original rewriting system in rewriting circuits with ancillae in the general case.

To set Ricercar on a theoretical foundation, we also define a permutation semantics over symmetric groups and show how the operations over permutations as transposition relate to the semantics of the language.

Michael Kirkedal Thomsen, Robin Kaarsgaard, Mathias Soeken

Circuit Synthesis

Frontmatter

Technology Mapping for Single Target Gate Based Circuits Using Boolean Functional Decomposition

Abstract

Quantum computing offers a promising emerging technology due to the potential theoretical capacity of solving many important problems with exponentially less complexity. Since most of the known quantum algorithms include Boolean components, the design of quantum computers is often conducted by a two-stage approach. In a first step, the Boolean component is realized in reversible logic and then mapped to quantum gates in a second step. This paper describes a new mapping flow for determining quantum gate realizations for single-target gates (ST). Since each ST gate contains a Boolean control function, our method attempts to find a decomposition based on its BDD representation. It consists on breaking large ST gate into smaller ones using additional lines. Experiments show that we obtain smaller realizations when comparing to standard mapping.

Nabila Abdessaied, Mathias Soeken, Rolf Drechsler

Towards Line-Aware Realizations of Expressions for HDL-Based Synthesis of Reversible Circuits

Abstract

Hardware Description Languages (HDLs) allow for the efficient synthesis of large and complex circuits. Consequently, researchers also investigated their potential in the domain of reversible logic. Here, existing HDL-based synthesis approaches suffer from the significant drawback of employing additional circuit lines in order to buffer intermediate results. In this work, we investigate the possibility of reducing this overhead. For this purpose, an alternative synthesis scheme is proposed and evaluated which aims at a more efficient realization of expressions. The general idea is to re-compute (i.e to undo) sub-expressions as soon as the respective intermediate results are not needed anymore. The observations and discussions result in initial guidelines on how to realize expressions more efficiently as well as a better understanding of the potential of HDL-based synthesis.

Zaid Al-Wardi, Robert Wille, Rolf Drechsler

Synthesis of Quantum Circuits for Dedicated Physical Machine Descriptions

Abstract

Quantum computing has been attracting increasing attention in recent years because of the rapid advancements that have been made in quantum algorithms and quantum system design. Quantum algorithms are implemented with the help of quantum circuits. These circuits are inherently reversible in nature and often contain a sizeable Boolean part that needs to be synthesized. Consequently, a large body of research has focused on the synthesis of corresponding reversible circuits and their mapping to the quantum operations supported by the quantum system. However, reversible circuit synthesis has usually not been performed with any particular target technology in mind, but with respect to an abstract cost metric. When targeting actual physical implementations of the circuits, the adequateness of such an approach is unclear. In this paper, we explicitly target synthesis of quantum circuits at selected quantum technologies described through their Physical Machine Descriptions (PMDs). We extend the state-of-the-art synthesis flow in order to realize quantum circuits based on just the primitive quantum operations supported by the respective PMDs. Using this extended flow, we evaluate whether the established reversible circuit synthesis methods and metrics are still applicable and adequate for PMD-specific implementations.

Philipp Niemann, Saikat Basu, Amlan Chakrabarti, Niraj K. Jha, Robert Wille

Short Papers

Frontmatter

Power-Clock Generator Impact on the Performance of NEM-Based Quasi-Adiabatic Logic Circuits

Abstract

The influence of the power-clock generator on the global energy-performance relationship of nanoelectromechanical (NEM) switch-based quasi-adiabatic logic circuits is investigated in this paper. This investigation is undertaken the capacitor bank type generator, it is found that the leakage current of the MOSFET switching devices used within the generator constitutes an important source of performance degradation. Capacitor type generators are found to be most efficient for low operating frequencies (less than a MHz).

Samer Houri, Gerard Billiot, Marc Belleville, Alexandre Valentian, Herve Fanet

Towards a Cost Metric for Nearest Neighbor Constraints in Reversible Circuits

Abstract

This work in progress report proposes a new metric for estimating nearest neighbor cost at the reversible circuit level. This is in contrast to existing literature where nearest neighbor constraints are usually considered at the quantum circuit level. In order to define the metric, investigations on a state-of-the-art reversible to quantum mapping scheme have been conducted. From the retrieved information, a proper estimation to be used as a cost metric has been obtained. Using the metric, it becomes possible for the first time to optimize a reversible circuit with respect to nearest neighbor constraints.

Abhoy Kole, Kamalika Datta, Indranil Sengupta, Robert Wille

Towards Modelling of Local Reversibility

Abstract

We describe a new operator for reversible process calculi that allows us to model locally controlled reversibility. In our setting, actions can be undone spontaneously or as a part of pairs of so-called concerted actions, where performing forwards a weak action forces undoing of another action, without the need of a global control or a memory. We model an example from chemistry, the simple interaction of two water molecules, and give an informal explanation of the role of the new operator.

Stefan Kuhn, Irek Ulidowski

Application of Functional Decomposition in Synthesis of Reversible Circuits

Abstract

The design of reversible circuits differs significantly from the design of conventional circuits. Although many methods to synthesize reversible functions have been developed, most of them are not scalable. In this paper an application of the divide and conquer paradigm is proposed that adopts for reversible logic synthesis the concept of functional decomposition developed for conventional logic synthesis. The initial function is decomposed into a network of smaller sub-functions that are easier to analyze and synthesize into reversible blocks. The final circuit is then composed of these blocks. The results of experiments reported here demonstrate the potential of the proposed approach.

Mariusz Rawski

Backmatter

Titel: Reversible Computation
herausgegeben von: Jean Krivine
Jean-Bernard Stefani
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-20860-2
Print ISBN: 978-3-319-20859-6
DOI: https://doi.org/10.1007/978-3-319-20860-2