Reversing Parallel Programs with Blocks and Procedures
James Hoey (University of Leicester), Irek Ulidowski (University of, Leicester), Shoji Yuen (Nagoya University)
TL;DR
This paper presents a method for reversing the execution of parallel programs with blocks, procedures, and interleaving, using annotated operational semantics to accurately restore initial states.
Contribution
It introduces a novel annotation scheme and operational semantics for reversing complex parallel programs with interleaving and local variables.
Findings
Annotation does not change original program behavior
Inversion correctly restores initial program state
Operational semantics effectively capture reversal information
Abstract
We show how to reverse a while language extended with blocks, local variables, procedures and the interleaving parallel composition. Annotation is defined along with a set of operational semantics capable of storing necessary reversal information, and identifiers are introduced to capture the interleaving order of an execution. Inversion is defined with a set of operational semantics that use saved information to undo an execution. We prove that annotation does not alter the behaviour of the original program, and that inversion correctly restores the initial program state.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.