Bounded Verification of Multi-threaded Programs via Lazy Sequentialization
Bounded Verification of Multi-threaded Programs via Lazy Sequentialization
复制标题
DOI：
10.1145/3478536
复制
发表时间：
2021-12
期刊：
影响因子：
--
通讯作者：
Omar Inverso;Ermenegildo Tomasco;B. Fischer;Salvatore La Torre;G. Parlato
中科院分区：
文献类型：
--
作者：
Omar Inverso;Ermenegildo Tomasco;B. Fischer;Salvatore La Torre;G. Parlato
有界验证技术，如有界模型检查（BMC）已经成功地用于许多实际的程序分析问题，但并发性仍然是一个挑战。在这里，我们描述了使用POSIX线程的顺序一致命令式程序的BMC的一种新方法。我们首先将多线程程序转换为一个不确定的顺序程序，该程序在给定的轮数范围内保持所有轮循调度的可达性。然后，我们重用现有的高性能BMC工具作为顺序验证问题的后端。我们的翻译经过精心设计，引入了非常小的内存开销和非常少的非确定性来源，因此它产生严格的SAT/SMT公式，因此在实践中非常有效：我们的Lazy-CSeq工具实现了C编程语言的这种翻译，在2014-2021年软件验证竞赛（SV-COMP）的并发类别中赢得了几枚金牌和银牌，并且能够在所有其他技术（包括测试）失败的程序中发现错误。在本文中，我们对我们的翻译进行了详细的描述并证明了它的正确性，使用CSeq框架勾画了它的实现，并对我们的方法进行了详细的评估和比较。
Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use POSIX threads. We first translate the multi-threaded program into a nondeterministic sequential program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. We then reuse existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so it produces tight SAT/SMT formulae, and is thus very effective in practice: Our Lazy-CSeq tool implementing this translation for the C programming language won several gold and silver medals in the concurrency category of the Software Verification Competitions (SV-COMP) 2014–2021 and was able to find errors in programs where all other techniques (including testing) failed. In this article, we give a detailed description of our translation and prove its correctness, sketch its implementation using the CSeq framework, and report on a detailed evaluation and comparison of our approach.