Reversing Parallel Programs with Blocks and Procedures

James Hoey
(University of Leicester)
Irek Ulidowski
(University of Leicester)
Shoji Yuen
(Nagoya University)

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.

In Jorge A. Pérez and Simone Tini: Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics (EXPRESS/SOS 2018), Beijing, China, September 3, 2018, Electronic Proceedings in Theoretical Computer Science 276, pp. 69–86.
Published: 24th August 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: