Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

5-2014

Abstract

Strongly Connected Component (SCC) based searching is one of the most popular LTL model checking algorithms. When the SCCs are huge, the counterexample generation process can be time-consuming, especially when dealing with fairness assumptions. In this work, we propose a GPU accelerated counterexample generation algorithm, which improves the performance by parallelizing the Breadth First Search (BFS) used in the counterexample generation. BFS work is irregular, which means it is hard to allocate resources and may suffer from imbalanced load. We make use of the features of latest CUDA Compute Architecture-NVIDIA Kepler GK110 to achieve the dynamic parallelism and memory hierarchy so as to handle the irregular searching pattern in BFS. We build dynamic queue management, task scheduler and path recording such that the counterexample generation process can be completely finished by GPU without involving CPU. We have implemented the proposed approach in PAT model checker. Our experiments show that our approach is effective and scalable.

Keywords

Model Check, Share Memory, Task Schedule, Strongly Connect, Component, Model Check Problem

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, November 3–5

First Page

413

Last Page

429

ISBN

9783319117362

Identifier

10.1007/978-3-319-11737-9_27

Publisher

Springer Link

City or Country

Luxembourg

Additional URL

https://doi.org/10.1007/978-3-319-11737-9_27

Download

Share

COinS