CRIL: A Concurrent Reversible Intermediate Language

TL;DR

CRIL is a reversible intermediate language designed for concurrent programming, enabling translation between high-level and low-level languages while preserving causality and enabling reversibility in concurrent executions.

Contribution

This paper introduces CRIL, a novel reversible intermediate language that supports concurrency, multi-threading, and synchronization primitives, extending previous reversible languages to handle concurrent behaviors.

Findings

CRIL's operational semantics satisfy reversibility properties including causal safety and liveness.

CRIL's dependency annotations enable precise control flow and memory updates in reversible concurrent execution.

An airline ticketing example demonstrates CRIL's ability to preserve causality in imperative concurrent programs.

Abstract

We present a reversible intermediate language with concurrency for translating a high-level concurrent programming language to another lower-level concurrent programming language, keeping reversibility. Intermediate languages are commonly used in compiling a source program to an object code program closer to the machine code, where an intermediate language enables behavioral analysis and optimization to be decomposed in steps. We propose CRIL (Concurrent Reversible Intermediate Language) as an extension of RIL used by Mogensen for a functional reversible language, incorporating a multi-thread process invocation and the synchronization primitives based on the P-V operations. We show that the operational semantics of CRIL enjoy the properties of reversibility, including the causal safety and causal liveness proposed by Lanese et al., checking the axiomatic properties. The operational semantics is defined by composing the bidirectional control flow with the dependency information on updating the memory, called annotation DAG. We show a simple example of `airline ticketing' to illustrate how CRIL preserves the causality for reversibility in imperative programs with concurrency.