Coarse-grained reconfigurable arrays (CGRAs), or dataflow architectures in general, have gained attention in recent years due to their promising power efficiency compared to traditional von Neumann architectures. To program these architectures using ordinary languages such as C, a dataflow compiler must transform the original sequential, imperative program into an equivalent dataflow graph, composed of dataflow operators running in parallel. This transformation is challenging since the asynchronous nature of dataflow graphs allows out-of-order execution of operators, leading to behaviors not present in the original imperative programs. We address this challenge by developing a translation validation technique for dataflow compilers to ensure that the dataflow program has the same behavior as the original imperative program on all possible inputs and schedules of execution. We apply this method to a state-of-the-art dataflow compiler targeting the RipTide CGRA architecture. Our tool uncovers 7 compiler bugs where the compiler outputs incorrect dataflow graphs, including a data race that is otherwise hard to discover via testing. After repairing these bugs, our tool verifies the correct compilation of all programs in the RipTide benchmark suite.

翻译：粗粒度可重构阵列（CGRA），或广义上的数据流架构，因其相较于传统冯·诺依曼架构具有显著能效优势，近年来备受关注。为使用C这类常规语言对这些架构编程，数据流编译器必须将原始的顺序命令式程序转换为等价的数据流图，该图由并行运行的数据流算子构成。这一转换极具挑战性，因为数据流图的异步特性允许算子乱序执行，从而产生原始命令式程序中不存在的执行行为。我们通过为数据流编译器开发翻译验证技术来应对这一挑战，确保数据流程序在所有可能的输入和执行调度下，与原始命令式程序行为一致。我们将该方法应用于面向RipTide CGRA架构的先进数据流编译器。我们的工具发现了7处编译器错误（编译器输出错误的数据流图），其中包括一种难以通过常规测试发现的竞态条件。在修复这些错误后，我们的工具成功验证了RipTide基准测试套件中所有程序的正确编译。