一句话：提出基于动态分数权限的翻译验证技术，证明异步数据流图与源命令式程序在所有输入和调度下行为等价。
粗粒度可重构阵列（CGRA）能效优于传统 von Neumann 架构，但用 C 等语言编程时，数据流编译器需把串行命令式程序转换为由并行数据流算子组成的图。由于数据流图异步且允许乱序执行，可能产生源程序没有的行为，正确性难以保证。本文提出 FlowCert，一种针对数据流编译器的翻译验证技术，借助动态分数权限刻画算子的资源所有权与异步执行，验证生成的数据流程序在所有输入和执行调度下与原命令式程序行为一致。作者将该方法用于面向 RipTide CGRA 的最新数据流编译器，发现 8 个编译器缺陷，包括一个测试难以发现的数据竞争；修复后，工具成功验证 RipTide 基准套件中所有程序的编译正确性。
Coarse-grained reconfigurable arrays (CGRAs) 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. Weaddress 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 CGRAarchitecture. Our tool uncovers 8 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.
@article{LinGP24,
title = {FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions},
author = {Zhengyao Lin and Joshua Gancher and Bryan Parno},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689729}
}