GPU Accelerated On-the-Fly Reachability Checking

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


Model checking suffers from the infamous state space explosion problem. In this paper, we propose an approach, named GPURC, to utilize the Graphics Processing Units (GPUs) to speed up the reachability verification. The key idea is to achieve a dynamic load balancing so that the many cores in GPUs are fully utilized during the state space exploration. To this end, we firstly construct a compact data encoding of the input transition systems to reduce the memory cost and fit the calculation in GPUs. To support a large number of concurrent components, we propose a multi-integer encoding with conflict-release accessing approach. We then develop a BFS-based state space generation algorithm in GPUs, which makes full use of the GPU memory hierarchy and the latest dynamic parallelism feature in CUDA to achieve a high parallelism. GPURC also supports a parallel collaborative event synchronization approach and integrates a GPU hashing method to reduce the cost of data accessing. The experiments show that GPURC can give significant performance speedup (average 50X and up to 100X) compared with the traditional sequential algorithms.
Original languageEnglish
Title of host publication20th International Conference on Engineering of Complex Computer Systems, ICECCS 2015, Gold Coast, Australia, December 9-12, 2015
Publication statusPublished - 2015
Event20th International Conference on Engineering of Complex Computer Systems (ICECCS) - Queensland , Gold Coast, Australia
Duration: 9 Dec 201512 Dec 2015
Conference number: 20


Conference20th International Conference on Engineering of Complex Computer Systems (ICECCS)
CityGold Coast


Dive into the research topics of 'GPU Accelerated On-the-Fly Reachability Checking'. Together they form a unique fingerprint.

Cite this