Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs
Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs
复制标题
用于无界并发程序安全验证的惰性序列化
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
G. Parlato
中科院分区：
文献类型：
--
作者：
Truc L. Nguyen;B. Fischer;S. L. Torre;G. Parlato
懒惰序列化已经成为并发程序分析的最有前途的方法之一，但到目前为止，唯一有效的实现只适用于有界程序。这将该方法限制在查找错误的目的上。在本文中，我们描述和评估一个新的懒惰的序列化翻译，不解开循环，从而允许分析无界的计算，即使有无限数量的上下文切换。结合适当的顺序后端验证工具，它也可以用于并发程序的安全性验证，而不仅仅是错误查找。我们翻译的主要技术新奇是模拟线程恢复的方式，不使用gotos，因此不需要每个语句最多执行一次。我们已经在UL-CSeq工具中为使用pthreads API的C99程序实现了这种转换。我们评估UL-CSeq在几个基准测试，使用不同的顺序验证后端的顺序化程序，并表明它是更有效的比以前的方法在证明安全基准的正确性，仍然保持竞争力与国家的最先进的方法在不安全的基准中发现错误。
Lazy sequentialization has emerged as one of the most promising approaches for concurrent program analysis but the only efficient implementation given so far works just for bounded programs. This restricts the approach to bug-finding purposes. In this paper, we describe and evaluate a new lazy sequentialization translation that does not unwind loops and thus allows to analyze unbounded computations, even with an unbounded number of context switches. In connection with an appropriate sequential backend verification tool it can thus also be used for the safety verification of concurrent programs, rather than just for bug-finding. The main technical novelty of our translation is the simulation of the thread resumption in a way that does not use gotos and thus does not require that each statement is executed at most once. We have implemented this translation in the UL-CSeq tool for C99 programs that use the pthreads API. We evaluate UL-CSeq on several benchmarks, using different sequential verification backends on the sequentialized program, and show that it is more effective than previous approaches in proving the correctness of the safe benchmarks, and still remains competitive with state-of-the-art approaches for finding bugs in the unsafe benchmarks.