×

Accelerating SpMV multiplication in probabilistic model checkers using GPUs. (English) Zbl 07500639

Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2021. 18th international colloquium, virtual event, Nur-Sultan, Kazakhstan, September 8–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12819, 86-104 (2021).
Summary: Probabilistic model checking is a prominent formal verification technique for analyzing stochastic systems. Probabilistic model checkers hinge upon the sparse matrix-vector (SpMV) multiplications to compute reachability probabilities, i.e., the probability of reaching a target state from a given initial state. Being compute- and memory-intensive task, SpMV is a bottleneck in using probabilistic model checking for analyzing scalable real-world case studies. This paper presents a methodology to accelerate SpMV multiplication in probabilistic model checkers using graphic processing units (GPUs). Since GPUs efficiently execute basic linear algebraic operations such as multiplication, one achieves improvements in computation times. These improvements, however, are not significant in the presence of memory transfer overheads. We apply traditional optimization techniques and hide the memory transfers from the host computer to the GPU inside the state-space-exploration stage. This hiding significantly reduces the latency caused by memory transfers during execution. We implemented the proposed acceleration approach with CUDA-based cuSPARSE API and asynchronous multiple copy algorithms in the probabilistic model checker Storm, with a focus on its SpMV multiplier. In our experiments, we observed 16 times speed up on average over the state-of-the-art.
For the entire collection see [Zbl 1483.68007].

MSC:

68Qxx Theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ajanovic, J.: PCI express 3.0 overview. In: Proceedings of Hot Chip: A Symposium on High Performance Chips, vol. 69, p. 143 (2009)
[2] Baier, C., Principles of Model Checking (2008), Cambridge: MIT press, Cambridge · Zbl 1179.68076
[3] Barnat, J., Parallel model checking algorithms for linear-time temporal logic, Handbook of Parallel Constraint Reasoning, 457-507 (2018), Cham: Springer, Cham · doi:10.1007/978-3-319-63516-3_12
[4] Barnat, J.; Brim, L.; Stříbrná, J.; Dwyer, M., Distributed LTL model-checking in SPIN, Model Checking Software, 200-216 (2001), Heidelberg: Springer, Heidelberg · Zbl 0985.68519 · doi:10.1007/3-540-45139-0_13
[5] Bell, N.; Garland, M., Efficient Sparse Matrix-Vector Multiplication on CUDA (2008), Citeseer: Tech. rep, Citeseer
[6] Bell, N., Garland, M.: Cusp: Generic parallel algorithms for sparse matrix and graph computations. Version 0.3. 0 35 (2012)
[7] Berger, P.: GPU-aided model checking of Markov decision processes (2014)
[8] Bošnački, D., Edelkamp, S., Sulewski, D., Wijs, A.: GPU-PRISM: An extension of prism for general purpose graphics processing units. In: 2010 Ninth International Workshop on Parallel and Distributed Methods in Verification, and Second International Workshop on High Performance Computational Systems Biology, pp. 17-19. IEEE (2010)
[9] Bošnački, D.; Edelkamp, S.; Sulewski, D.; Wijs, A., Parallel probabilistic model checking on general purpose graphics processors, Int. J. Softw. Tools Technol. Transfer, 13, 1, 21-35 (2011) · doi:10.1007/s10009-010-0176-4
[10] Bylina, B.; Bylina, J.; Karwacki, M., Computational aspects of GPU-accelerated sparse matrix-vector multiplication for solving Markov models, Theor. Appl. Inform., 23, 127-145 (2011) · doi:10.2478/v10179-011-0009-5
[11] Clarke, EM; Grumberg, O.; Long, DE, Model checking and abstraction, ACM Trans. Program. Lang. Syst. (TOPLAS), 16, 5, 1512-1542 (1994) · doi:10.1145/186025.186051
[12] Cormie-Bowins, E.: A comparison of sequential and GPU implementations of iterative methods to compute reachability probabilities. arXiv preprint arXiv:1210.6412 (2012) · Zbl 1458.68116
[13] Corporation, N.: The API reference guide for cuSPARSE (2021). https://docs.nvidia.com/cuda/cusparse/index.html
[14] Corporation, N.: Cuda c++ best practices guide (2021). https://docs.nvidia.com/cuda/cuda-c-best-practices-guide/index.html
[15] Corporation, N.: Nvidia nsight compute (2021). https://developer.nvidia.com/nsight-compute
[16] Corporation, N.: Nvidia visual profiler (2021). https://developer.nvidia.com/nvidia-visual-profiler
[17] Dehnert, C.; Junges, S.; Katoen, J-P; Volk, M.; Majumdar, R.; Kunčak, V., A storm is coming: a modern probabilistic model checker, Computer Aided Verification, 592-600 (2017), Cham: Springer, Cham · doi:10.1007/978-3-319-63390-9_31
[18] Fabarisov, T., Yusupova, N., Ding, K., Morozov, A., Janschek, K.: The efficiency comparison of the prism and storm probabilistic model checkers for error propagation analysis tasks. Industry 4.0 3(5), 229-231 (2018)
[19] Fang, J., Varbanescu, A.L., Sips, H.: A comprehensive performance comparison of CUDA and OpenCL. In: 2011 International Conference on Parallel Processing, pp. 216-225. IEEE (2011)
[20] Gonzales, D.: PCI express 4.0 electrical previews. In: PCI-SIG Developers Conference (2015)
[21] Greathouse, J.L., Daga, M.: Efficient sparse matrix-vector multiplication on GPUs using the CSR storage format. In: SC’14: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 769-780. IEEE (2014)
[22] Harris, M.: Optimizing cuda. SC07: High Performance Computing With CUDA 60 (2007)
[23] Hasan, O., Tahar, S.: Formal verification methods. In: Encyclopedia of Information Science and Technology, 3rd Edition, pp. 7162-7170. IGI Global (2015)
[24] Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. arXiv preprint arXiv:2002.07080 (2020)
[25] Hérault, T.; Lassaigne, R.; Magniette, F.; Peyronnet, S.; Steffen, B.; Levi, G., Approximate probabilistic model checking, Verification, Model Checking, and Abstract Interpretation, 73-84 (2004), Heidelberg: Springer, Heidelberg · Zbl 1202.68249 · doi:10.1007/978-3-540-24622-0_8
[26] Katoen, J.: The probabilistic model checking landscape. In: LICS, pp. 31-45. ACM (2016) · Zbl 1401.68201
[27] Khan, H.: Storm-cuda (2021). https://github.com/khan-hannan/StoRM-CUDA
[28] Khan, S.; Katoen, J-P; Volk, M.; Bouissou, M.; Dutle, A.; Moscato, MM; Titolo, L.; Muñoz, CA; Perez, I., Scalable reliability analysis by lazy verification, NASA Formal Methods, 180-197 (2021), Cham: Springer, Cham · doi:10.1007/978-3-030-76384-8_12
[29] Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: 9th International Conference on Quantitative Evaluation of SysTems, pp. 203-204. IEEE CS press (2012)
[30] Kwiatkowska, M.; Norman, G.; Parker, D., Probabilistic verification of Herman’s self-stabilisation algorithm, Formal Aspects Comput., 24, 4, 661-670 (2012) · Zbl 1259.68130 · doi:10.1007/s00165-012-0227-6
[31] Markidis, S., Der Chien, S.W., Laure, E., Peng, I.B., Vetter, J.S.: Nvidia tensor core programmability, performance and precision. In: 2018 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW), pp. 522-531. IEEE (2018)
[32] Munshi, A., Gaster, B., Mattson, T.G., Ginsburg, D.: OpenCL programming guide. Pearson Education (2011)
[33] Nambiar, PP; Saveetha, V.; Sophia, S.; Sowbarnika, VA, GPU acceleration using CUDA framework, Int. J. Innovative Res. Comput. Commun. Eng., 2, 3, 200-205 (2014)
[34] Naumov, M., Chien, L., Vandermersch, P., Kapasi, U.: Cusparse library. In: GPU Technology Conference (2010)
[35] Norman, G.; Parker, D.; Kwiatkowska, M.; Shukla, S., Evaluating the reliability of NAND multiplexing with PRISM, IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 24, 10, 1629-1637 (2005) · doi:10.1109/TCAD.2005.852033
[36] Sanders, J., Kandrot, E.: CUDA by example: an introduction to general-purpose GPU programming. Addison-Wesley Professional (2010)
[37] Stern, Ulrich, Dill, David L..: Parallelizing the mur \(\phi\) verifier. In: Grumberg, Orna (ed.) CAV 1997. LNCS, vol. 1254, pp. 256-267. Springer, Heidelberg (1997). doi:10.1007/3-540-63166-6_26
[38] Valmari, A.; Reisig, W.; Rozenberg, G., The state explosion problem, Lectures on Petri Nets I: Basic Models, 429-528 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-65306-6_21
[39] Wijs, A.; Neele, T.; Bošnački, D.; Fitzgerald, J.; Heitmeyer, C.; Gnesi, S.; Philippou, A., GPUexplore 2.0: unleashing gpu explicit-state model checking, FM 2016: Formal Methods, 694-701 (2016), Cham: Springer, Cham · doi:10.1007/978-3-319-48989-6_42
[40] Wijs, AJ; Bošnački, D.; Donaldson, A.; Parker, D., Improving GPU sparse matrix-vector multiplication for probabilistic model checking, Model Checking Software, 98-116 (2012), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-31759-0_9
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.