Reversible programming is an unconventional paradigm that offers new ways to construct software. When programs have inherent inverse counterparts, such as compression/decompression, the invertibility of reversible implementations enables a “write once, verify once” approach. The nature of today’s computers is, however, irreversible. This work-in-progress contribution explores the dereversibilization of reversible source programs into irreversible target programs. As a first step into this space, we explore the use of state-of-the-art Satisfiability-Modulo-Theories (SMT) solvers to statically remove redundant assertions. We divide the problem space into two parts: High-level dereversibilization of Janus-like source programs and classical compilation to machine code. In this contribution, we focus on the semantics-preserving removal of assertions from reversible control-flow statements. Our prototype reduces the size of the assembly code and marks the first step towards automatic dereversibilization and new opportunities of using reversible programs.
Reversible Computation (RC)
2023
2024-08-22