GPUexplore 2.0: unleashing GPU explicit-state model checking

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

12 Citations (Scopus)
6 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationFM 2016: Formal Methods - 21st International Symposium, Proceedings
PublisherSpringer
Pages694-701
Number of pages8
ISBN (Print)978-3-319-48988-9
DOIs
Publication statusPublished - 2016
Event21st International Symposium on Formal Methods, FM 2016 - Limassol, Cyprus
Duration: 9 Nov 201611 Nov 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9995
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Symposium on Formal Methods, FM 2016
CountryCyprus
CityLimassol
Period9/11/1611/11/16

Fingerprint

Dive into the research topics of 'GPUexplore 2.0: unleashing GPU explicit-state model checking'. Together they form a unique fingerprint.

Cite this