Publication details

<< back
 

Employing Multiple CUDA Devices to Accelerate LTL Model Checking

Basic information
Original title:Employing Multiple CUDA Devices to Accelerate LTL Model Checking
Authors:Jiří Barnat, Petr Bauch, Luboš Brim, Milan Češka
Further information
Citation:BARNAT, Jiří - BAUCH, Petr - BRIM, Luboš - ČEŠKA, Milan. Employing Multiple CUDA Devices to Accelerate LTL Model Checking. In Proceedings of 16th International Conference on Parallel and Distributed Systems (ICPADS 2010). Neuveden : IEEE Computer Society, 2010. ISBN 978-0-7695-4307-9, pp. 259-266. 2010, Shanghai, China.
Original language:English
Field:Informatika
Type:Article in Proceedings
Keywords:Model Checking; Linear Temporal Logic; Multiple CUDA devices

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.

Related projects:

 
 
top