Publication Type

Conference Paper

Version

publishedVersion

Publication Date

12-2015

Abstract

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.

Discipline

Computer and Systems Architecture | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

20th International Conference on Engineering of Complex Computer Systems, Gold Coast, Australia, 2015 December 9-12

Identifier

10.1109/ICECCS.2015.21

City or Country

Gold Coast, Australia

Additional URL

https://doi.org/10.1109/ICECCS.2015.21

Download

Share

COinS