Reversing an Imperative Concurrent Programming Language

TL;DR

This paper presents a novel method for reversing imperative concurrent programs by creating forward and reverse versions, ensuring correctness and garbage-free reversal using identifiers.

Contribution

It introduces a systematic approach to reverse imperative concurrent programs, including the use of identifiers and formal correctness proofs.

Findings

Reversible execution is achieved with two program versions.

The method guarantees the initial state is restored.

Reversibility is proven to be correct and garbage-free.

Abstract

We introduce a method of reversing the execution of imperative concurrent programs. Given an irreversible program, we describe the process of producing two versions. The first performs forward execution and saves information necessary for reversal. The second uses this saved information to simulate reversal. We propose using identifiers to overcome challenges of reversing concurrent programs. We prove this reversibility to be correct, showing that the initial program state is restored and that all saved information is used (garbage-free).