一句话:提出 GenCoG,用 DSL 描述算子类型约束并通过混合执行求解,增量生成有效且高表达力的计算图以测试 TVM。
现有 Muffin、NNSmith 等深度学习编译器测试方法生成的计算图要么类型不合法,要么表达力不足,难以覆盖 TVM 的核心功能。GenCoG 由两部分组成:GenCoGL,一种用于描述算子类型约束的领域特定语言;以及基于混合执行(concolic)求解类型约束并增量生成高表达力计算图的方法。作者在多个 TVM 版本上评估:GenCoG 生成的计算图全部通过类型检查,顶点和边多样性分别达到现有方法的 1.65~6.93 倍和 1.06~7.08 倍,并在 TVM v0.8/v0.9 中发现 16 个缺陷,其中 14 个确认、12 个修复。
TVM is a popular deep learning (DL) compiler. It is designed for compiling DL models, which are naturally computation graphs, and as well promoting the efficiency of DL computation. State-of-the-art methods, such as Muffin and NNSmith, allow developers to generate computation graphs for testing DL compilers. However, these techniques are inefficient — their generated computation graphs are either type-invalid or inexpressive, and hence not able to test the core functionalities of a DL compiler. To tackle this problem, we propose GenCoG, a DSL-based approach to generating computation graphs for TVM testing. GenCoG is composed of (1) GenCoGL, a domain-specific language for specifying type constraints of operators, and (2) an approach that concolically solves type constraints and incrementally generates computation graphs of high expressivity. We implement and evaluate GenCoG on TVM releases. Our results show that GenCoG is effective in generating valid and expressive computation graphs — all of the GenCoG-generated graphs pass type checking, a critical graph validation stage; letting the graphs’ expressivity be measured by their vertex and edge diversities, GenCoG outperforms state-of-the-arts by achieving 1.65~6.93× in vertex diversity and 1.06~7.08× in edge diversity, respectively. Furthermore, GenCoG has detected 16 bugs in TVM v0.8 and v0.9, with 14 confirmed and 12 fixed.
@inproceedings{WangNMCWB023,
title = {GenCoG: A DSL-Based Approach to Generating Computation Graphs for TVM Testing},
author = {Zihan Wang and Pengbo Nie and Xinyuan Miao and Yuting Chen and Chengcheng Wan and Lei Bu and Jianjun Zhao},
booktitle = {ISSTA},
year = {2023},
doi = {10.1145/3597926.3598105}
}