Towards a GPGPU-parallel SPIN model checker

Ezio Bartocci, Richard DeFrancisco, Scott A. Smolka

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

19 Scopus citations

Abstract

As General-Purpose Graphics Processing Units (GPGPUs) become more powerful, they are being used increasingly often in high-performance computing applications. State space exploration, as employed in model-checking and other verification techniques, is a large, complex problem that has successfully been ported to a variety of parallel architectures. Use of the GPU for this purpose, however, has only recently begun to be studied. We show how the 2012 multi-core CPU-parallel state-space exploration algorithm of the SPIN model checker can be re-engineered to take advantage of the unique parallel-processing capabilities of the GPGPU architecture, and demonstrate how to overcome the non-trivial design obstacles presented by this task. Our preliminary results demonstrate significant performance improvements over the traditional sequential model checker for state spaces of appreciable size (>∼10 million unique state.

Original languageEnglish (US)
Title of host publication2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings
PublisherAssociation for Computing Machinery, Inc
Pages87-96
Number of pages10
ISBN (Electronic)9781450324526
DOIs
StatePublished - Jul 21 2014
Externally publishedYes
Event21st International Symposium on Model Checking of Software, SPIN 2014 - San Jose, United States
Duration: Jul 21 2014Jul 23 2014

Publication series

Name2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings

Conference

Conference21st International Symposium on Model Checking of Software, SPIN 2014
CountryUnited States
CitySan Jose
Period7/21/147/23/14

Keywords

  • CUDA
  • GPGPU
  • Model checking
  • Multicore
  • SPIN
  • State space exploration

ASJC Scopus subject areas

  • Artificial Intelligence
  • Computer Science Applications
  • Software

Fingerprint Dive into the research topics of 'Towards a GPGPU-parallel SPIN model checker'. Together they form a unique fingerprint.

Cite this