一句话：提出将 Go 参数化通道通信片段翻译为核心语言并编码为 Dafny 程序，自动验证无部分死锁并推断前置条件。
并发消息传递程序常面临部分死锁问题，可能导致长运行系统内存泄漏。现有针对 Go 的静态分析工具在真实企业代码中过于不精确，难以处理参数化进程通信，即通道通信操作数或通道容量在运行时才确定的情况。本文提出一种自动验证方法：将 Go 程序片段翻译为足以表达真实参数化通信模式的核心语言，再编码为带有后置条件的 Dafny 程序，以强制验证部分死锁自由性。当片段仅在并发参数满足特定条件时才无部分死锁，方法还能推断合适的前置条件。实验在一个真实代码库的 583 个现有技术无法处理的片段上进行，成功验证 145 个片段无部分死锁，并为另外 228 个片段推断出周边代码需满足的非平凡前置条件。
A challenge of writing concurrent message passing programs is ensuring the absence of partial deadlocks, which can cause severe memory leaks in long running systems. Several static analysis techniques have been proposed for automatically detecting partial deadlocks in Go programs. For a large enterprise code base, we found these tools too imprecise to reason about process communication that is parametric, i.e., where the number of channel communication operations or the channel capacities are determined at runtime. We present a novel approach to automatically verify the absence of partial deadlocks in Go program fragments with such parametric process communication. The key idea is to translate Go fragments to a core language that is sufficiently expressive to represent real-world parametric communication patterns and can be encoded into Dafny programs annotated with postconditions enforcing partial deadlock freedom. In situations where a fragment is partial deadlock free only when the concurrency parameters satisfy certain conditions, a suitable precondition can often be inferred. Experimental results on a real-world code base containing 583 program fragments that are beyond the reach of existing techniques have shown that the approach can verify the absence of partial deadlocks in 145 cases. For an additional 228 cases, a nontrivial precondition is inferred that the surrounding code must satisfy to ensure partial deadlock freedom.
@article{SaiocLM24,
title = {Automated Verification of Parametric Channel-Based Process Communication},
author = {Georgian-Vlad Saioc and Julien Lange and Anders Møller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689784}
}