Swarm model checking on the GPU
- PDF / 2,686,221 Bytes
- 17 Pages / 595.276 x 790.866 pts Page_size
- 28 Downloads / 239 Views
STTT Special Issue: SPIN 2019
Swarm model checking on the GPU Richard DeFrancisco1 · Shenghsun Cho1 · Michael Ferdman1 · Scott A. Smolka1
© Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract 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. Keywords GPU · Model checking · Swarm verification · Grapple
1 Introduction Modern computing exists in a space that is increasingly parallel, distributed, and heterogeneous. High-performance co-processors such as GPUs (Graphics Processing Units) are utilized in many super-computing applications due to their high computational throughput, energy efficiency, and low cost [20]. GPGPU (General-Purpose Computing on a GPU) is achieved through the use of GPU programming languages such as the Open Computing Language (OpenCL) [33] and the Compute Unified Device Architecture (CUDA) [1]. In 2014, we adapted the multicore SPIN model checking (MC) algorithm of [22] to the GPU [7]. While our approach achieved speedups up to 7.26× over traditional SPIN, and 1.26× over multicore SPIN, it was severely limited by the memory footprint of the GPU, and by an explicit limit on the state-vector size set by the hash function [34].
B 1
Richard DeFrancisco [email protected]
The introduction of Swarm Verification (SV) in [25] represented an entirely new approach to parallel MC. In SV, a large number of MC instances are executed in parallel, each with a restricted memory footprint and a different search path. Each instance is called a verification test (VT), because it does not seek to cover the full state space as a model checker would. Through the use of diversification techniques, VTs are largely independent of one other in terms of the portions of the model’s state space they cover. By executing a
Data Loading...
