On the scalability of the GPUexplore explicit-state model checker
| Autor: | Cassee, Nathan W., Neele, T.S., Wijs, A.J., Kehrer, Timo, Miller, Alice |
|---|---|
| Přispěvatelé: | Mathematics and Computer Science, Software Engineering and Technology |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
State model
Model checking FOS: Computer and information sciences Speedup Computer science Computation lcsh:Mathematics 05 social sciences 050801 communication & media studies 020207 software engineering 02 engineering and technology Parallel computing lcsh:QA1-939 Hash table lcsh:QA75.5-76.95 0508 media and communications Computer Science - Distributed Parallel and Cluster Computing Scalability Computer Science - Data Structures and Algorithms 0202 electrical engineering electronic engineering information engineering Data Structures and Algorithms (cs.DS) Software system Distributed Parallel and Cluster Computing (cs.DC) lcsh:Electronic computers. Computer science Graphics |
| Zdroj: | Proceedings Third Workshop on Graphs as Models (GaM 2017), 23 April 2017, Uppsala, Sweden, 38-52 STARTPAGE=38;ENDPAGE=52;TITLE=Proceedings Third Workshop on Graphs as Models (GaM 2017), 23 April 2017, Uppsala, Sweden Electronic Proceedings in Theoretical Computer Science, Vol 263, Iss Proc. GaM 2017, Pp 38-52 (2017) GaM@ETAPS |
| Popis: | The use of graphics processors (GPUs) is a promising approach to speed up model checking to such an extent that it becomes feasible to instantly verify software systems during development. GPUexplore is an explicit-state model checker that runs all its computations on the GPU. Over the years it has been extended with various techniques, and the possibilities to further improve its performance have been continuously investigated. In this paper, we discuss how the hash table of the tool works, which is at the heart of its functionality. We propose an alteration of the hash table that in isolated experiments seems promising, and analyse its effect when integrated in the tool. Furthermore, we investigate the current scalability of GPUexplore, by experimenting both with input models of varying sizes and running the tool on one of the latest GPUs of NVIDIA. In Proceedings GaM 2017, arXiv:1712.08345 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|