GPU Accelerated counterexample generation in LTL model checking
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 counterexamp...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2014
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/4988 https://ink.library.smu.edu.sg/context/sis_research/article/5991/viewcontent/gpu.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-5991 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-59912020-03-12T09:44:07Z GPU Accelerated counterexample generation in LTL model checking WU, Zhimin LIU, Yang LIANG, Yun SUN, Jun 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. 2014-05-11T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4988 info:doi/10.1007/978-3-319-11737-9_27 https://ink.library.smu.edu.sg/context/sis_research/article/5991/viewcontent/gpu.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Model Check Share Memory Task Schedule Strongly Connect Component Model Check Problem Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Model Check Share Memory Task Schedule Strongly Connect Component Model Check Problem Software Engineering |
spellingShingle |
Model Check Share Memory Task Schedule Strongly Connect Component Model Check Problem Software Engineering WU, Zhimin LIU, Yang LIANG, Yun SUN, Jun GPU Accelerated counterexample generation in LTL model checking |
description |
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. |
format |
text |
author |
WU, Zhimin LIU, Yang LIANG, Yun SUN, Jun |
author_facet |
WU, Zhimin LIU, Yang LIANG, Yun SUN, Jun |
author_sort |
WU, Zhimin |
title |
GPU Accelerated counterexample generation in LTL model checking |
title_short |
GPU Accelerated counterexample generation in LTL model checking |
title_full |
GPU Accelerated counterexample generation in LTL model checking |
title_fullStr |
GPU Accelerated counterexample generation in LTL model checking |
title_full_unstemmed |
GPU Accelerated counterexample generation in LTL model checking |
title_sort |
gpu accelerated counterexample generation in ltl model checking |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2014 |
url |
https://ink.library.smu.edu.sg/sis_research/4988 https://ink.library.smu.edu.sg/context/sis_research/article/5991/viewcontent/gpu.pdf |
_version_ |
1770575169100709888 |