Reversible Computation with Stacks and "Reversible Management of Failures"
Matteo Palazzo, Luca Roversi
TL;DR
This paper investigates how to reinterpret imperative programming models as fully reversible by refining their semantic state. It introduces S-CORE, an extension of SRL with stacks, and develops three semantic layers: an irreversible naive semantics, an assertion-based PIF-reversibilized semantics (A-semantics), and an assertion-free TIF-reversibilized semantics (R-semantics). The key result is that R-semantics yields total bijections on a richly structured state space $(v,s,c)$, enabling reversible computation even when A-semantics would abort. The work demonstrates, via Coq-verified push/pop inverses, that refining the internal state suffices to obtain strong reversibility without relying on program-wide assertions, illustrating a pathway from PIF to TIF reversibilization and highlighting practical implications for debugging, checkpointing, and energy-efficient computing.
Abstract
This work focuses on making certain computational models reversible. We start with the idea that "reversibilizing" should mean a process that gives a computational model an operational semantics capable of interpreting each term as a bijection. The most commonly used method of reversibilization creates operational semantics that halt computation when it is not possible to uniquely determine the starting state from a produced computational state; thus, terms are interpreted as partial bijective functions. We introduce $\textsf{S-CORE}$, a language of terms that allows manipulation of variables and stacks. For $\textsf{S-CORE}$, we define the operational semantics $\textsf{R-semantics}$. With the help of a proof assistant, we certify that $\textsf{R-semantics}$ makes $\textsf{S-CORE}$ a reversible imperative computational model where all terms are interpreted as total bijections on an appropriate state space.