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.

翻译：我们提出一种具有并发性的可逆中间语言，用于将高级并发编程语言翻译为另一较低级并发编程语言，同时保持可逆性。中间语言通常用于将源程序编译为更接近机器码的目标代码程序，其中中间语言使得行为分析与优化能够分步进行。我们提出的CRIL（并发可逆中间语言）是Mogensen在函数式可逆语言中所用RIL的扩展，引入了多线程进程调用及基于P-V操作的同步原语。研究表明，CRIL的操作语义具有可逆性性质，包括Lanese等人提出的因果安全性与因果活性，并通过公理化性质验证。该操作语义通过结合双向控制流与内存更新的依赖信息（称为注解DAG）来定义。我们通过一个简单的“航空订票”示例，说明CRIL如何在包含并发的命令式程序中维护可逆性的因果关系。