Concurrent RSSA for CRIL: Flow Analysis for a Concurrent Reversible Programming Language

We present the CRSSA (Concurrent Reversible Static Single Assignment) form for a concurrent reversible intermediate language called CRIL, which the authors proposed. A CRIL program is a collection of basic blocks where each basic block consists of a single 3-address code with labels for forward and backward control flow. CRIL extends RIL by Mogensen, allowing the multiple calls of basic blocks to execute concurrently in forward and backward directions. The operational semantics of CRIL enjoy causal safety and causal liveness as the fundamental correctness for reversibility. RSSA proposed by Mogensen assigns a value to a pair of unique variables for both directions. In addition to \(\phi \) functions to present bidirectional splits and joins of sequential flow, we incorporate \(\pi \) functions for possible joins of concurrent flow via shared variables, where the \(\pi \) functions are proposed by Lee et al. to present the joins of the concurrent flow of parallel programs. We extend \(\pi \) functions for the backward execution to present bidirectional splits and joins of CRIL behavior. We give a translation from a CRIL program into a CRSSA form given a bidirectional data flow analysis. We apply the optimization technique using the CRSSA form, such as conditional constant propagation, dead code elimination, and copy propagation to CRIL programs. A CRSSA form is translated back to a CRIL program.