-
Design of Reversible Computing Systems; Large Logic, Languages, and Circuits
Authors:
Michael Kirkedal Thomsen
Abstract:
This PhD dissertation investigates garbage-free reversible computing systems from abstract design to physical gate-level implementation. Designed in reversible logic, we propose a ripple-block carry adder and work towards a reversible circuit for general multiplication. At a higher-level, abstract designs are proposed for reversible systems, such as a small von Neumann architecture that can execut…
▽ More
This PhD dissertation investigates garbage-free reversible computing systems from abstract design to physical gate-level implementation. Designed in reversible logic, we propose a ripple-block carry adder and work towards a reversible circuit for general multiplication. At a higher-level, abstract designs are proposed for reversible systems, such as a small von Neumann architecture that can execute programs written in a simple reversible two-address instruction set, a novel reversible arithmetic logic unit, and a linear cosine transform. To aid the design of reversible logic circuits we have designed two reversible functional hardware description languages: a linear-typed higher-level language and a gate-level point-free combinator language. We suggest a garbage-free design flow, where circuits are described in the higher-level language and then translated to the combinator language, from which methods to place-and-route of CMOS gates can be applied. We have also made standard cell layouts of the reversible gates in complementary pass-gate CMOS logic and used these to fabricate the ALU design. In total, this dissertation has shown that it is possible to design non-trivial reversible computing systems without garbage and that support from languages (computer aided design) can make this process easier.
△ Less
Submitted 21 September, 2023;
originally announced September 2023.
-
pun: Fun with Properties; Towards a Programming Language With Built-in Facilities for Program Validation
Authors:
Triera Gashi,
Sophie Adeline Solheim Bosio,
Joachim Tilsted Kristensen,
Michael Kirkedal Thomsen
Abstract:
Property-based testing is a powerful method to validate program correctness. It is, however, not widely use in industry as the barrier of entry can be very high. One of the hindrances is to write the generators that are needed to generate randomised input data. Program properties often take complicated data structures as inputs and, it requires a significant amount of effort to write generators fo…
▽ More
Property-based testing is a powerful method to validate program correctness. It is, however, not widely use in industry as the barrier of entry can be very high. One of the hindrances is to write the generators that are needed to generate randomised input data. Program properties often take complicated data structures as inputs and, it requires a significant amount of effort to write generators for such structures in a invariant preserving way.
In this paper, we suggest and formalise a new programming language \textsf{pun}; a simple functional programming with properties as a built-in mechanism for program validation. We show how to generate input for \textsf{pun} properties automatically, thus, providing the programmer with a low barrier of entry for using property-based testing. We evaluate our work a on library for binary search trees and compare the test results to a similar library in Haskell.
△ Less
Submitted 12 September, 2023; v1 submitted 9 September, 2023;
originally announced September 2023.
-
Tail recursion transformation for invertible functions
Authors:
Joachim Tilsted Kristensen,
Robin Kaarsgaard,
Michael Kirkedal Thomsen
Abstract:
Tail recursive functions allow for a wider range of optimisations than general recursive functions. For this reason, much research has gone into the transformation and optimisation of this family of functions, in particular those written in continuation passing style (CPS).
Though the CPS transformation, capable of transforming any recursive function to an equivalent tail recursive one, is deepl…
▽ More
Tail recursive functions allow for a wider range of optimisations than general recursive functions. For this reason, much research has gone into the transformation and optimisation of this family of functions, in particular those written in continuation passing style (CPS).
Though the CPS transformation, capable of transforming any recursive function to an equivalent tail recursive one, is deeply problematic in the context of reversible programming (as it relies on troublesome features such as higher-order functions), we argue that relaxing (local) reversibility to (global) invertibility drastically improves the situation. On this basis, we present an algorithm for tail recursion conversion specifically for invertible functions. The key insight is that functions introduced by program transformations that preserve invertibility, need only be invertible in the context in which the functions subject of transformation calls them. We show how a bespoke data type, corresponding to such a context, can be used to transform invertible recursive functions into a pair of tail recursive function acting on this context, in a way where calls are highlighted, and from which a tail recursive inverse can be straightforwardly extracted.
△ Less
Submitted 28 February, 2023; v1 submitted 20 February, 2023;
originally announced February 2023.
-
Branching execution symmetry in Jeopardy by available implicit arguments analysis
Authors:
Joachim Tilsted Kristensen,
Robin Kaarsgaard,
Michael Kirkedal Thomsen
Abstract:
When the inverse of an algorithm is well-defined -- that is, when its output can be deterministically transformed into the input producing it -- we say that the algorithm is invertible. While one can describe an invertible algorithm using a general-purpose programming language, it is generally not possible to guarantee that its inverse is well-defined without additional argument. Reversible langua…
▽ More
When the inverse of an algorithm is well-defined -- that is, when its output can be deterministically transformed into the input producing it -- we say that the algorithm is invertible. While one can describe an invertible algorithm using a general-purpose programming language, it is generally not possible to guarantee that its inverse is well-defined without additional argument. Reversible languages enforce deterministic inverse interpretation at the cost of expressibility, by restricting the building blocks from which an algorithm may be constructed.
Jeopardy is a functional programming language designed for writing invertible algorithms \emph{without} the syntactic restrictions of reversible programming. In particular, Jeopardy allows the limited use of locally non-invertible operations, provided that they are used in a way that can be statically determined to be globally invertible. However, guaranteeing invertibility in Jeopardy is not obvious.
One of the central problems in guaranteeing invertibility is that of deciding whether a program is symmetric in the face of branching control flow. In this paper, we show how Jeopardy can solve this problem, using a program analysis called available implicit arguments analysis, to approximate branching symmetries.
△ Less
Submitted 6 December, 2022;
originally announced December 2022.
-
Jeopardy: An Invertible Functional Programming Language
Authors:
Joachim Tilsted Kristensen,
Robin Kaarsgaard,
Michael Kirkedal Thomsen
Abstract:
Algorithms are ways of map** problems to solutions. An algorithm is invertible precisely when this map** is injective, such that the initial problem can be uniquely inferred from its solution.
While invertible algorithms can be described in general-purpose languages, no guarantees are generally made by such languages as regards invertibility, so ensuring invertibility requires additional (an…
▽ More
Algorithms are ways of map** problems to solutions. An algorithm is invertible precisely when this map** is injective, such that the initial problem can be uniquely inferred from its solution.
While invertible algorithms can be described in general-purpose languages, no guarantees are generally made by such languages as regards invertibility, so ensuring invertibility requires additional (and often non-trivial) proof. On the other hand, while reversible programming languages guarantee that their programs are invertible by restricting the permissible operations to those which are locally invertible, writing programs in the reversible style can be cumbersome, and may differ significantly from conventional implementations even when the implemented algorithm is, in fact, invertible.
In this paper we introduce Jeopardy, a functional programming language that guarantees program invertibility without imposing local reversibility. In particular, Jeopardy allows the limited use of uninvertible -- and even nondeterministic! -- operations, provided that they are used in a way that can be statically determined to be invertible. To this end, we outline an \emph{implicitly available arguments analysis} and three further approaches that can give a partial static guarantee to the (generally difficult) problem of guaranteeing invertibility.
△ Less
Submitted 7 December, 2022; v1 submitted 6 September, 2022;
originally announced September 2022.
-
Self-Inverse Functions and Palindromic Circuits
Authors:
Mathias Soeken,
Michael Kirkedal Thomsen,
Gerhard W. Dueck,
D. Michael Miller
Abstract:
We investigate the subclass of reversible functions that are self-inverse and relate them to reversible circuits that are equal to their reverse circuit, which are called palindromic circuits. We precisely determine which self-inverse functions can be realized as a palindromic circuit. For those functions that cannot be realized as a palindromic circuit, we find alternative palindromic representat…
▽ More
We investigate the subclass of reversible functions that are self-inverse and relate them to reversible circuits that are equal to their reverse circuit, which are called palindromic circuits. We precisely determine which self-inverse functions can be realized as a palindromic circuit. For those functions that cannot be realized as a palindromic circuit, we find alternative palindromic representations that require an extra circuit line or quantum gates in their construction. Our analyses make use of involutions in the symmetric group $S_{2^n}$ which are isomorphic to self-inverse reversible function on $n$ variables.
△ Less
Submitted 20 February, 2015;
originally announced February 2015.
