Improving GPU sparse matrix-vector multiplication for probabilistic model checking

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

16 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationModel Checking Software (19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings)
EditorsA. Donaldson, D. Parker
Place of PublicationBerlin
ISBN (Print)978-3-642-31758-3
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Improving GPU sparse matrix-vector multiplication for probabilistic model checking'. Together they form a unique fingerprint.

Cite this