Title
GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking.
Abstract
In earlier work, we were the first to investigate the potential of using graphics processing units (GPUs) to speed up explicit-state model checking. Back then, the conclusion was clearly that this potential exists, having measured speed-ups of around 10 times, compared to state-of- the-art single-core model checking. In this paper, we present a new version of our GPU model checker, GPUexplore. Since publication of our earlier work, we have identified and implemented several approaches to improve the performance of the model checker considerably. These include enhanced lock-less hashing of the states and improved thread synchronizations. We discuss experimental results that show the impact of both the progress in hardware in the last few years and our proposed optimisations. The new version of GPUexplore running on state-of-the- art hardware can be more than 100 times faster than a sequential implementation for large models and is on average eight times faster than the previous version of the tool running on the same hardware.
Year
DOI
Venue
2016
10.1007/978-3-319-48989-6_42
Lecture Notes in Computer Science
Field
DocType
Volume
Graphics,Model checking,Shared memory,Computer science,Parallel computing,Thread (computing),Theoretical computer science,State model,Hash function,Speedup,Hash table
Conference
9995
ISSN
Citations 
PageRank 
0302-9743
1
0.36
References 
Authors
16
3
Name
Order
Citations
PageRank
Anton Wijs120322.84
Thomas Neele221.72
Dragan Bosnacki327626.95