一句话：将 Lazy-CSeq 扩展为基于 swarm 的多线程 C 程序缺陷查找工具，通过分块限制上下文切换以降低内存与时间开销。
本文提出工具 VeriSmart 2.0，面向使用 POSIX 线程的 C 程序进行缺陷查找。现有基于顺序化的有界模型检验工具 Lazy-CSeq 在多线程交错下易出现状态空间爆炸，导致内存与时间开销过高。作者将 swarm 式验证方法引入 Lazy-CSeq：把验证问题分解为大量相互独立的简单任务以利用多核并行，并通过“tile”（各线程内部的连续代码段）约束交错，使上下文切换只能发生在所选 tile 边界内。该做法对程序行为进行欠近似，同时以 tile 的数量与大小作为参数灵活调节每个任务的复杂度。评估表明，该方法显著改善了峰值内存消耗与墙钟分析时间；摘要未给出具体基准集与量化数据。
Swarm-based verification methods split a verification problem into a large number of independent simpler tasks and so exploit the availability of large numbers of cores to speed up verification. Lazy-CSeq is a BMC-based bug-finding tool for C programs using POSIX threads that is based on sequentialization. Here we present the tool VeriSmart 2.0, which extends Lazy-CSeq with a swarm-based bug-finding method. The key idea of this approach is to constrain the interleaving such that context switches can only happen within selected tiles (more specifically, contiguous code segments within the individual threads). This under-approximates the program's behaviours, with the number and size of tiles as additional parameters, which allows us to vary the complexity of the tasks. Overall, this significantly improves peak memory consumption and (wall-clock) analysis time.
DOI 原文 ·
@inproceedings{paperbot5241,
title = {VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq},
author = {Bernd Fischer and Salvatore La Torre and Gennaro Parlato},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00124}
}