Other formats:
BibTeX
LaTeX
RIS
@inproceedings{905389,
author = {Barnat, Jiří and Bauch, Petr and Brim, Luboš and Češka, Milan},
address = {Neuveden},
booktitle = {Proceedings of 16th International Conference on Parallel and Distributed Systems (ICPADS 2010)},
keywords = {Model Checking; Linear Temporal Logic; Multiple CUDA devices},
language = {eng},
location = {Neuveden},
isbn = {978-0-7695-4307-9},
pages = {259-266},
publisher = {IEEE Computer Society},
title = {Employing Multiple CUDA Devices to Accelerate LTL Model Checking},
year = {2010}
}
TY - JOUR
ID - 905389
AU - Barnat, Jiří - Bauch, Petr - Brim, Luboš - Češka, Milan
PY - 2010
TI - Employing Multiple CUDA Devices to Accelerate LTL Model Checking
PB - IEEE Computer Society
CY - Neuveden
SN - 9780769543079
KW - Model Checking
KW - Linear Temporal Logic
KW - Multiple CUDA devices
N2 - Recently, the CUDA technology has been used to accelerate many computation demanding tasks. For example, in~\cite{BBCL09} we have shown how CUDA technology can be employed to accelerate the process of Linear Temporal Logic (LTL) Model Checking. While the raw computing power of a CUDA enabled device is tremendous, the applicability of the technology is quite often limited to small or middle-sized instances of the problems being solved. This is because the memory that a single device is equipped with, is simply not large enough to cope with large or realistic instances of the problem, which is also the case of our CUDA-aware LTL Model Checking solution. In this paper we suggest how to overcome this limitations by employing multiple (two in our case) CUDA devices for acceleration of our fine-grained communication-intensive parallel algorithm for LTL Model Checking.
ER -
BARNAT, Jiří, Petr BAUCH, Luboš BRIM and Milan ČEŠKA. Employing Multiple CUDA Devices to Accelerate LTL Model Checking. In \textit{Proceedings of 16th International Conference on Parallel and Distributed Systems (ICPADS 2010)}. Neuveden: IEEE Computer Society, 2010, p.~259-266. ISBN~978-0-7695-4307-9.
|
