Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking

Anton J. Wijs, Dragan Bosnacki
Eindhoven University of Technology, The Netherlands
Model Checking Software, Lecture Notes in Computer Science, Volume 7385/2012, 98-116, 2012


   title={Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking},

   author={Wijs, A. and Bo{v{s}}na{v{c}}ki, D.},

   journal={Model Checking Software},





Download Download (PDF)   View View   Source Source   Source codes Source codes




We present several methods to improve the run times of probabilistic model checking on general-purpose graphics processing units (GPUs). The methods enhance sparse matrix-vector multiplications, which are in the core of the probabilistic model checking algorithms. The improvement is based on the analysis of the transition matrix structures corresponding to state spaces of a selection of examples from the literature. Our first method defines an enumeration of the matrix elements (states of the Markov chains), based on breadth-first search which can lead to a more regular representation of the matrices. We introduce two additional methods that adjust the execution paths and memory access patterns of the individual processors of the GPU. They exploit the specific features of the transition matrices arising from probabilistic/stochastic models as well as the logical and physical architectures of the device. We implement the matrix reindexing and the efficient memory access methods in GPU-PRISM, an extension of the probabilistic model checker PRISM. The experiments with the prototype implementation show that each of the methods can bring a significant run time improvement – more than four times compared to the previous version of GPU-PRISM. Moreover, in some cases, the methods are orthogonal and can be used in combination to achieve even greater speed ups.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2017 hgpu.org

All rights belong to the respective authors

Contact us: