Timo Kehrer and Alice Miller (Eds.):
Workshop on Graphs as Models 2017 (GAM ’17)
EPTCS 263, 2017, pp. 1–15, doi:10.4204/EPTCS.263.1
c
N.W. Cassee & A.J. Wijs
Analysing the Performance of GPU Hash Tables for State
Space Exploration
Nathan Cassee
Eindhoven University of Technology
Eindhoven, The Netherlands
N.W.Cassee@student.tue.nl
Anton Wijs
Eindhoven University of Technology
Eindhoven, The Netherlands
A.J.Wijs@tue.nl
Abstract: In the past few years, General Purpose Graphics Processors (GPUs) have been used to
significantly speed up numerous applications. One of the areas in which GPUs have recently led to a
significant speed-up is model checking. In model checking, state spaces, i.e., large directed graphs,
are explored to verify whether models satisfy desirable properties. GPUEXPLORE is a GPU-based
model checker that uses a hash table to efficiently keep track of already explored states. As a large
number of states is discovered and stored during such an exploration, the hash table should be able
to quickly handle many inserts and queries concurrently. In this paper, we experimentally compare
two different hash tables optimised for the GPU, one being the GPUEXPLORE hash table, and the
other using Cuckoo hashing. We compare the performance of both hash tables using random and
non-random data obtained from model checking experiments, to analyse the applicability of the two
hash tables for state space exploration. We conclude that Cuckoo hashing is three times faster than
GPUEXPLORE hashing for random data, and that Cuckoo hashing is five to nine times faster for
non-random data. This suggests great potential to further speed up GPUEXPLORE in the near future.
1 Introduction
General Purpose Graphics Processors (GPUs) have been used to significantly speed up computations in
numerous application domains. Contrary to CPUs, GPUs can handle many thousands of parallel threads,
allowing for a great increase in parallel processing of data. This increase has opened up new possibilities
to improve the performance of algorithms, as significant speedups can be achieved by using optimised
algorithms and lock-free data structures.
One of the domains to which GPU computing has been applied in the last few years is model check-
ing. Model checking involves taking a model of an (often concurrent) system and verifying whether
certain properties are satisfied by that model. The semantics of such models can be expressed in a state
space, which is a directed graph (often sparse), with labels either on the edges or the nodes. During model
checking, such a state space is constructed by interpreting the model. Starting from the initial state of the
model, exploration continues until either all reachable states have been explored, or a counter-example
to the property being verified has been encountered [4]. This operation can be very resource-demanding,
as state spaces tend to grow exponentially as the number of concurrent components in a model grows
linearly. This problem is commonly referred to as the state space explosion problem. For this reason,
the use of modern parallel architectures is very appealing, since it could make the analysis of large state
spaces more practically feasible.
In recent years, approaches have been developed to perform state space exploration either using a
combination of the CPU and the GPU, or specifically using the GPU [5, 7, 8, 21, 26, 27, 23, 28, 29].
Most approaches use an exploration strategy similar to Breadth-First Search (BFS).
剩余14页未读，继续阅读
资源评论
