Abstract Static Elaboration of Recursion for Concurrent Software

Unlike sequential software, concurrent software needs a structuring mechanism capable of specifying constructs such as pipelines, scatter-gather, and other networks. Concurrent software languages usually provide mechanisms for dynamically creating such structures, but this makes them difficult to analyze statically. In particular, it would be very convenient to be able to put bounds on the resources (memory, processes) required by a particular system. We present a static elaboration technique that can remove bounded recursion from concurrent programs, useful for tools that cannot handle recursion such as those for formal verification and hardware synthesis. We work with SHIM, a concurrent language that provides concurrent, recursive function calls that can be used to elegantly construct concurrent structures such as pipelines and the FFT. Our technique first slices the program from every recursive call to determine which variables control the recursion, then perform a simulation of the program with respect to those variables, performing constant propagation to produce simplified code without recursion. Experimental results suggest our slicing procedure is effective at selecting just those variables that participate in the recursion and that our simulation technique for generating non-recursive code can quickly produce small non-recursive programs, making this technique practical