Reversing Imperative Parallel Programs

TL;DR

This paper introduces a method for reversing imperative programs by augmenting and inverting them, including extensions to handle parallelism and execution interleaving, ensuring accurate rollback of program states.

Contribution

It presents a novel approach for program reversal with augmentation and inversion, extended to support non-communicating parallelism and deterministic interleaving.

Findings

Successfully reverses imperative programs with preserved data integrity.

Extends reversal technique to parallel programs with interleaving.

Proves correctness of augmentation and inversion methods.

Abstract

We propose an approach and a subsequent extension for reversing imperative programs. Firstly, we produce both an augmented version and a corresponding inverted version of the original program. Augmentation saves reversal information into an auxiliary data store, maintaining segregation between this and the program state, while never altering the data store in any other way than that of the original program. Inversion uses this information to revert the final program state to the state as it was before execution. We prove that augmentation and inversion work as intended, and illustrate our approach with several examples. We also suggest a modification to our first approach to support non-communicating parallelism. Execution interleaving introduces a number of challenges, each of which our extended approach considers. We define annotation and redefine inversion to use a sequence of statement identifiers, making the interleaving order deterministic in reverse.