Designing Fast LTL Model Checking Algorithms for Many-core GPUs
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057210" target="_blank" >RIV/00216224:14330/12:00057210 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1016/j.jpdc.2011.10.015" target="_blank" >http://dx.doi.org/10.1016/j.jpdc.2011.10.015</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.jpdc.2011.10.015" target="_blank" >10.1016/j.jpdc.2011.10.015</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Designing Fast LTL Model Checking Algorithms for Many-core GPUs
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Designing Fast LTL Model Checking Algorithms for Many-core GPUs
Popis výsledku anglicky
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.
Klasifikace
Druh
J<sub>x</sub> - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2012
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
Journal of Parallel and Distributed Computing
ISSN
0743-7315
e-ISSN
—
Svazek periodika
72
Číslo periodika v rámci svazku
9
Stát vydavatele periodika
CZ - Česká republika
Počet stran výsledku
15
Strana od-do
1083-1097
Kód UT WoS článku
000307156000005
EID výsledku v databázi Scopus
—