随流而行：异步数据流的形式化验证编译框架
Let it Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
浏览论文内容
中文总结 AI 辅助
该研究提出首个异步数据流编译器的形式化验证框架Wavelet，通过带围栏的能力类型系统等技术，验证编译器核心 passes 并证明相关属性，编译的数据流图规模与未经验证编译器相当。
中文摘要 AI 辅助
数据流架构因在能效与性能间取得平衡而重新受到关注。在（空间）数据流架构中，程序被表示为一组完全分布式且动态调度的数据流算子，这些算子通过异步通道通信，这极大提升了数据局部性与并行性。然而，编译至数据流架构仍是一个易出错的过程，需在维持确定性的同时实现流水线化。确定性指数据流程序的结果是确定的，且与算子执行调度无关；流水线化是空间数据流中实现循环迭代间并行性的重要优化。本研究中，我们提出Wavelet，这是首个针对异步数据流编译器的形式化验证工作。我们采用多种技术组合实现该目标：前端使用新颖的带围栏的能力类型系统，用于同步冲突内存访问并启用流水线化；随后，我们验证了编译器两个核心 passes 的 Lean 形式化，该 passes 将类型检查后的精细化程序转换为数据流图，并证明了前向模拟与确定性的重要属性。值得注意的是，我们的形式化在语义上传播了前端类型系统的正确性保证，确保了模拟与确定性证明间的模块化。在评估中，我们展示了由Wavelet编译生成的数据流图，其规模与用于RipTide空间数据流架构的未经验证优化编译器生成的数据流图规模相当。
英文摘要
Dataflow architectures have gained renewed interest due to their balance between power 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, in order to maintain 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 passes of our compiler that translates 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 evaluation, we show that dataflow graphs compiled by Wavelet have comparable sizes to those produced by an unverified optimizing compiler for the RipTide spatial dataflow architecture.
