J 2012

Designing Fast LTL Model Checking Algorithms for Many-core GPUs

BARNAT, Jiří, Petr BAUCH, Luboš BRIM and Milan ČEŠKA

Basic information

Original name

Designing Fast LTL Model Checking Algorithms for Many-core GPUs

Authors

BARNAT, Jiří (203 Czech Republic, belonging to the institution), Petr BAUCH (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and Milan ČEŠKA (203 Czech Republic, guarantor, belonging to the institution)

Edition

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

Other information

Language

English

Type of outcome

Článek v odborném periodiku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

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

References:

Impact factor

Impact factor: 0.859 in 2011

RIV identification code

RIV/00216224:14330/12:00057210

Organization unit

Faculty of Informatics

DOI

UT WoS

000307156000005

Keywords in English

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

Tags

Tags

International impact, Reviewed
Změněno: 12/12/2012 11:09, Mgr. Petr Bauch, Ph.D.

Abstract

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.

Links

GAP202/11/0312, research and development project
Name: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)
Investor: Czech Science Foundation
GA201/09/1389, research and development project
Name: Verifikace a analýza velmi velkých počítačových systémů
Investor: Czech Science Foundation, Verification and Analysis of Large-Scale Computer Systems
GD102/09/H042, research and development project
Name: 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: Czech Science Foundation
GP201/09/P497, research and development project
Name: Automatizovaná formální verifikace s využitím soudobého hardware
Investor: Czech Science Foundation, Automated formal verification using modern hardware
MSM0021622419, plan (intention)
Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
MUNI/A/0057/2011, interní kód MU
Name: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKONF)
Investor: Masaryk University, Category A
MUNI/A/0914/2009, interní kód MU
Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)
Investor: Masaryk University, Category A