Zhengyao Lin, Yi Cai, Milijana Surbatovich
Dataflow architectures have gained renewed interest due to their balance between energy efficiency and performance. In (spatial) dataflow architectures, a program is represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through asynchronous channels, which greatly improves data locality and parallelism. However, compiling to dataflow architectures remains an error-prone process, due to the difficulty of maintaining determinacy while enabling pipelining . Determinacy means that the result of a dataflow program is deterministic and independent of the schedule of operator execution, and pipelining is an important optimization in spatial dataflow that enables parallelism across loop iterations. In this work, we present Wavelet, the first effort to formally verify a compiler for asynchronous dataflow. We use a mix of techniques to achieve this goal. Our frontend uses a novel capability type system with fences to synchronize conflicting memory accesses and enable pipelining . We then verify a Lean formalization of two core compiler passes that translate elaborated programs from the type checker to dataflow graphs, proving important properties of forward simulation and determinacy . Notably, our formalization semantically propagates the soundness guarantees of the frontend type system, ensuring modularity between simulation and determinacy proofs. In our evaluation, we show that dataflow graphs compiled by Wavelet have comparable quality to those produced by unverified dataflow compilers from RipTide and LLVM CIRCT.