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. The authors 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.