Partial-order reduction for GPU model checking
| Autor: | Neele, T., Wijs, A., Bosnacki, D., van de Pol, Jan Cornelis, Artho, C, Legay, A., Peled, D. |
|---|---|
| Přispěvatelé: | Software Engineering and Technology |
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Model checking
Correctness Computer science CR-D.2.4 Parallel algorithm 020207 software engineering 02 engineering and technology Parallel computing FMT-MC: MODEL CHECKING Hash table EWI-27826 Reduction (complexity) Partial order reduction Shared memory 0202 electrical engineering electronic engineering information engineering Overhead (computing) 020201 artificial intelligence & image processing |
| Zdroj: | Automated Technology for Verification and Analysis-14th International Symposium, ATVA 2016, Proceedings, 357-374 STARTPAGE=357;ENDPAGE=374;TITLE=Automated Technology for Verification and Analysis-14th International Symposium, ATVA 2016, Proceedings Automated Technology for Verification and Analysis ISBN: 9783319465197 ATVA Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, 357-374 STARTPAGE=357;ENDPAGE=374;TITLE=Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 |
| Popis: | Model checking using GPUs has seen increased popularity over the last years. Because GPUs have a limited amount of memory, only small to medium-sized systems can be verified. For on-the-fly explicitstate model checking, we improve memory efficiency by applying partialorder reduction. We propose novel parallel algorithms for three practical approaches to partial-order reduction. Correctness of the algorithms is proved using a new, weaker version of the cycle proviso. Benchmarks show that our implementation achieves a reduction similar to or better than the state-of-the-art techniques for CPUs, while the amount of runtime overhead is acceptable. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|