Parallel bug-finding in concurrent programs via reduced interleaving instances
Parallel bug-finding in concurrent programs via reduced interleaving instances
复制标题
DOI：
10.1109/ase.2017.8115686
复制
发表时间：
2017-10
期刊：
影响因子：
--
通讯作者：
Truc L. Nguyen;P. Schrammel;B. Fischer;S. L. Torre;G. Parlato
中科院分区：
文献类型：
--
作者：
Truc L. Nguyen;P. Schrammel;B. Fischer;S. L. Torre;G. Parlato
并发性对程序验证提出了重大挑战，但当可以并行分析子问题时，它也可以提供扩展的机会。我们在这里利用这个机会，并使用可参数化的代码到代码转换来生成一组更简单的程序实例，每个实例捕获一组减少的原始程序的交错。然后可以并行地独立检查这些实例。我们的方法不依赖于最终分析所选择的工具，与弱内存模型兼容，并放大现有工具的有效性，使它们更快地发现错误并使用更少的资源。我们使用 Lazy-CSeq 作为现成的最终验证器，以证明我们的方法能够在少量核心的情况下在几分钟内找到最难的已知并发基准中的错误，而其他动态和静态工具则无法在数小时内找到这一点。
Concurrency poses a major challenge for program verification, but it can also offer an opportunity to scale when subproblems can be analysed in parallel. We exploit this opportunity here and use a parametrizable code-to-code translation to generate a set of simpler program instances, each capturing a reduced set of the original program's interleavings. These instances can then be checked independently in parallel. Our approach does not depend on the tool that is chosen for the final analysis, is compatible with weak memory models, and amplifies the effectiveness of existing tools, making them find bugs faster and with fewer resources. We use Lazy-CSeq as an off-the-shelf final verifier to demonstrate that our approach is able, already with a small number of cores, to find bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.