Correct Compilation for Asynchronous Dataflow Architectures

Dataflow execution is a computational model in which operations execute as soon as their input data becomes available, rather than according to some centralized control(e.g., a program counter), greatly improving data locality and parallelism. To realize this execution model, programs can be represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through asynchronous channels, i.e., a dataflow graph (DFG), where this graph can be mapped directly onto reconfigurable compute fabrics like CGRAs. Such Dataflow Architectures are rapidly gaining increased interest due to their balance between energy efficiency and performance, in both edge-computing and HPC spaces.
Unfortunately, dataflow architectures are difficult to program both correctly and effectively, as existing programming languages lack good abstractions for dataflow features. Compiling languages originally meant for sequential execution into highly-parallel dataflow graphs easily introduces concurrency bugs or sacrifices potential parallelism. In this talk, I present my group's work on creating a practical, high-assurance dataflow programming framework. First, I introduce the basics of dataflow execution and challenges of correct compilation. Then, I present Wavelet, our formally verified dataflow compiler, discussing the co-design between the front-end language and the graph-level abstractions that aids the verification process. I conclude by describing our future directions in extendingWavelet for more complex dataflow models and architectures.