一句话：提出基于有界模型检测的 Go 并发程序静态检查器，可处理大型代码库与静态未知参数，性能优于现有工具。
Go 语言提供 channel、waitgroup、mutex 等轻量线程协调原语，容易引入并发缺陷；而现有静态检查器要么漏报过多，要么无法处理大型程序。本文提出一种 Go 程序静态检查器，核心思想是将程序的并发行为抽取为模型，并对其进行有界模型检测。与已有工作不同，该方法能应对大型代码库、支持含静态未知参数的程序，并可扩展至更多并发原语。论文详细给出了从 Go 程序到模型的抽取算法、针对静态未知参数的自动检查算法，并进行了大规模实验评估，结果表明该方法优于当前最先进工具。
The Go programming language offers a wide range of primitives to coordinate lightweight threads, e.g., channels, waitgroups, and mutexes — all of which may cause concurrency bugs. Static checkers that guarantee the absence of bugs are essential to help programmers avoid these costly errors before their code is executed. However existing tools either miss too many bugs or cannot handle large programs. To address these limitations, we propose a static checker for Go programs which relies on performing bounded model checking of their concurrent behaviours. In contrast to previous works, our approach deals with large codebases, supports programs that have statically unknown parameters, and is extensible to additional concurrency primitives. Our work includes a detailed presentation of the extraction algorithm from Go programs to models, an algorithm to automatically check programs with statically unknown parameters, and a large scale evaluation of our approach. The latter shows that our approach outperforms the state-of-the-art.
DOI 原文 ·
@inproceedings{paperbot6493,
title = {Automated Verification of Go Programs via Bounded Model Checking},
author = {Nicolas Dilley and Julien Lange},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678571}
}