TY - GEN
T1 - Swarm Model Checking on the GPU
AU - DeFrancisco, Richard
AU - Cho, Shenghsun
AU - Ferdman, Michael
AU - Smolka, Scott A.
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2019.
PY - 2019
Y1 - 2019
N2 - 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 the various design parameters, including the size of the 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.
AB - 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 the various design parameters, including the size of the 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.
KW - GPU
KW - Grapple
KW - Model checking
KW - Swarm verification
UR - http://www.scopus.com/inward/record.url?scp=85075580217&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85075580217&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-30923-7_6
DO - 10.1007/978-3-030-30923-7_6
M3 - Conference contribution
AN - SCOPUS:85075580217
SN - 9783030309220
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 94
EP - 113
BT - Model Checking Software - 26th International Symposium, SPIN 2019, Proceedings
A2 - Biondi, Fabrizio
A2 - Given-Wilson, Thomas
A2 - Legay, Axel
PB - Springer
T2 - 26th International Symposium on Model Checking Software, SPIN 2019
Y2 - 15 July 2019 through 16 July 2019
ER -