Swarm Model Checking on the GPU

Richard DeFrancisco, Shenghsun Cho, Michael Ferdman, Scott A. Smolka

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

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 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.

Original languageEnglish (US)
Title of host publicationModel Checking Software - 26th International Symposium, SPIN 2019, Proceedings
EditorsFabrizio Biondi, Thomas Given-Wilson, Axel Legay
PublisherSpringer
Pages94-113
Number of pages20
ISBN (Print)9783030309220
DOIs
StatePublished - 2019
Externally publishedYes
Event26th International Symposium on Model Checking Software, SPIN 2019 - Beijing, China
Duration: Jul 15 2019Jul 16 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11636 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Symposium on Model Checking Software, SPIN 2019
CountryChina
CityBeijing
Period7/15/197/16/19

Keywords

  • GPU
  • Grapple
  • Model checking
  • Swarm verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Swarm Model Checking on the GPU'. Together they form a unique fingerprint.

Cite this