| BARNAT, Jiří, Petr BAUCH, Luboš BRIM and Milan ČEŠKA. Designing Fast LTL Model Checking Algorithms for Many-core GPUs. Journal of Parallel and Distributed Computing. Elsevier, 2012, vol. 72, No 9, p. 1083-1097. ISSN 0743-7315. Available from: https://dx.doi.org/10.1016/j.jpdc.2011.10.015. |
Other formats:
BibTeX
LaTeX
RIS
@article{958069,
author = {Barnat, Jiří and Bauch, Petr and Brim, Luboš and Češka, Milan},
article_number = {9},
doi = {http://dx.doi.org/10.1016/j.jpdc.2011.10.015},
keywords = {Parallel model checking; Linear temporal logic; Massively parallel architectures; CUDA technology; Multiple CUDA devices},
language = {eng},
issn = {0743-7315},
journal = {Journal of Parallel and Distributed Computing},
title = {Designing Fast LTL Model Checking Algorithms for Many-core GPUs},
url = {http://www.sciencedirect.com/science/article/pii/S0743731511002140},
volume = {72},
year = {2012}
}
TY - JOUR
ID - 958069
AU - Barnat, Jiří - Bauch, Petr - Brim, Luboš - Češka, Milan
PY - 2012
TI - Designing Fast LTL Model Checking Algorithms for Many-core GPUs
JF - Journal of Parallel and Distributed Computing
VL - 72
IS - 9
SP - 1083-1097
EP - 1083-1097
PB - Elsevier
SN - 07437315
KW - Parallel model checking
KW - Linear temporal logic
KW - Massively parallel architectures
KW - CUDA technology
KW - Multiple CUDA devices
UR - http://www.sciencedirect.com/science/article/pii/S0743731511002140
N2 - Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this paper we show how the algorithms for LTL model checking can be redesigned in order to accelerate LTL model checking on many-core GPU platforms. Our detailed experimental evaluation demonstrates that using the NVIDIA CUDA technology results in a significant speedup of the verification process. Together with state space generation based on shared hash-table and DFS exploration, our CUDA accelerated model checker is the fastest among state-of-the-art shared memory model checking tools. The effective utilisation of CUDA technology, however, is quite often reduced by the costly preparation of suitable data structures and limited to small or middle-sized instances due to space limitations, which is also the case of our CUDA-aware LTL Model Checking solutions. Hence, we further suggest how to overcome these limitations by multi-core construction of the compact data structures and by employing multiple CUDA devices for acceleration of fine-grained communication-intensive parallel algorithms for LTL Model Checking.
ER -
BARNAT, Jiří, Petr BAUCH, Luboš BRIM and Milan ČEŠKA. Designing Fast LTL Model Checking Algorithms for Many-core GPUs. \textit{Journal of Parallel and Distributed Computing}. Elsevier, 2012, vol.~72, No~9, p.~1083-1097. ISSN~0743-7315. Available from: https://dx.doi.org/10.1016/j.jpdc.2011.10.015.
|
