We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings. Delay-bounded deterministic scheduling, introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique to lift the delay bound for the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol.
翻译:我们考虑了在任意的线性交织下分析非同步并行程序的安全特性这一广泛的问题。在先前的工作中引入了迟到的确定性时间安排,这是一种高效的监听技术,可以抑制与全时间列表非确定性相关的巨大成本。在本文件中,我们首先提出一种技术,可以解除有限面变量程序所涉的延迟,从而提高在任意线性交织下验证程序安全性的能力的错误检测效率。第二,我们展示了我们的技术如何结合上游抽象抽象的抽象抽象性,既可以反驳和核实无限制变量域程序的安全特性,甚至对于未受限制的线性计数。我们以前的工作已经确定,对于非三面共通式常规而言,上游抽象抽象程序会产生非常复杂的程序语义。然而,我们的技术从来不是静态地构建一个抽象的参数程序;我们的技术仅仅要求某些抽象国家在某些行动中关闭,从而消除了对存在核查算法对抽象程序的依赖性。我们展示了我们技术在先前工作中的许多例子上的效率,并展示了它与早先的简单化协议方法相比较。