TY - GEN
T1 - Towards a GPGPU-parallel SPIN model checker
AU - Bartocci, Ezio
AU - DeFrancisco, Richard
AU - Smolka, Scott A.
N1 - Publisher Copyright:
Copyright 2014 ACM.
PY - 2014/7/21
Y1 - 2014/7/21
N2 - 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.
AB - 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.
KW - CUDA
KW - GPGPU
KW - Model checking
KW - Multicore
KW - SPIN
KW - State space exploration
UR - http://www.scopus.com/inward/record.url?scp=84926637775&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84926637775&partnerID=8YFLogxK
U2 - 10.1145/2632362.2632379
DO - 10.1145/2632362.2632379
M3 - Conference contribution
AN - SCOPUS:84926637775
T3 - 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings
SP - 87
EP - 96
BT - 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014 - Proceedings
PB - Association for Computing Machinery
T2 - 21st International Symposium on Model Checking of Software, SPIN 2014
Y2 - 21 July 2014 through 23 July 2014
ER -