Swarm Model Checking on the {GPU}
Swarm Model Checking on the {GPU}
复制标题
{GPU} 上的群体模型检查
DOI：
10.1007/978-3-030-30923-7_6
复制
发表时间：
2020
影响因子：
1.5
通讯作者：
Smolka, S. A.
中科院分区：
文献类型：
--
作者：
DeFrancisco, R.;Cho, S.;Ferdman, M.;Smolka, S. A.
提出了一种新的、功能强大的显式状态模型检测框架--Grapple。Grapple基于群组验证(SV)，这是一种模型检查技术，其中并行运行一组或多个小型、内存和时间受限的验证测试(VT)，以执行状态空间探索。SV通过成员VT使用的搜索策略的多样化来实现高状态空间覆盖率。Grapple代表了一种针对GPU的群组实现。特别是，它运行一组内部并行的VT，这些VT的实现方式专门针对GPU体系结构及其计算核心提供的SIMD并行性。Grapple还有效地利用了GPU共享内存，消除了昂贵的块间通信开销。针对访问状态队列结构的大小、守卫语句的实现以及不确定的探测顺序等设计参数，我们对Grappple进行了全面的性能分析。测试在多种硬件配置下运行，包括在Amazon云上。我们的结果表明，与旋转群和先前的非群组GPU实现相比，Grapple具有更好的性能。虽然最近亮相的一款现场可编程门阵列要快一些，但部署到现场可编程门阵列的过程要比《S》复杂得多。
We present Grapple, a new and powerful framework for explicit-state model checking on GPUs. Grapple is based on swarm verification (SV), a model-checking technique wherein a collection or swarm of small, memory- and time-bounded verification tests (VTs) are run in parallel to perform state-space exploration. SV achieves high state-space coverage via diversification of the search strategies used by constituent VTs. Grapple represents a swarm implementation for the GPU. In particular, it runs a parallel swarm of internally parallel VTs, which are implemented in a manner that specifically targets the GPU architecture and the SIMD parallelism its computing cores offer. Grapple also makes effective use of the GPU shared memory, eliminating costly inter-block communication overhead. We conducted a comprehensive performance analysis of Grapple focused on various design parameters, including the size of the visited-state queue structure, implementation of guard statements, and nondeterministic exploration order. Tests are run with multiple hardware configurations, including on the Amazon cloud. Our results show that Grapple performs favorably compared to the SPIN swarm and a prior non-swarm GPU implementation. Although a recently debuted FPGA swarm is faster, the deployment process to the FPGA is much more complex than Grapple ’s.