Designing Fast LTL Model Checking Algorithms for Many-core GPUs

BARNAT, Jiří, Petr BAUCH, Luboš BRIM a Milan ČEŠKA. Designing Fast LTL Model Checking Algorithms for Many-core GPUs. Journal of Parallel and Distributed Computing. Elsevier, 2012, roč. 72, č. 9, s. 1083-1097. ISSN 0743-7315. Dostupné z: https://dx.doi.org/10.1016/j.jpdc.2011.10.015.

Základní údaje

Originální název

Designing Fast LTL Model Checking Algorithms for Many-core GPUs

Autoři

BARNAT, Jiří (203 Česká republika, domácí), Petr BAUCH (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí) a Milan ČEŠKA (203 Česká republika, garant, domácí)

Vydání

Journal of Parallel and Distributed Computing, Elsevier, 2012, 0743-7315

---

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.859 v roce 2011

Kód RIV

RIV/00216224:14330/12:00057210

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.1016/j.jpdc.2011.10.015

UT WoS

000307156000005

Klíčová slova anglicky

Parallel model checking; Linear temporal logic; Massively parallel architectures; CUDA technology; Multiple CUDA devices

Štítky

best

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

V originále

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.

---

Návaznosti

GAP202/11/0312, projekt VaV	Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems) Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification
GA201/09/1389, projekt VaV	Název: Verifikace a analýza velmi velkých počítačových systémů Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
GD102/09/H042, projekt VaV	Název: Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů Investor: Grantová agentura ČR, Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
GP201/09/P497, projekt VaV	Název: Automatizovaná formální verifikace s využitím soudobého hardware Investor: Grantová agentura ČR, Automatizovaná formální verifikace s využitím soudobého hardware
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
MUNI/A/0057/2011, interní kód MU	Název: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKONF) Investor: Masarykova univerzita, Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/0914/2009, interní kód MU	Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV) Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty