University of Twente Student Theses
GPU implementation of partial-order reduction
Neele, Thomas (2016) GPU implementation of partial-order reduction.
|
PDF
2MB |
| Abstract: | Model checking using GPUs has seen increased popularity over the last years. Because GPUs have only a limited amount of memory, only small to medium-sized systems can be verified. We improve memory efficiency for explicit-state GPU model checking by applying on-the-fly partial-order reduction. The correctness of the proposed algorithms is proved using a new 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 runtime overhead is acceptable. We also propose several optimisations for the tool GPUexplore. Benchmarks show that this results in a 7.8 times speed-up compared to the original implementation. For large models, our optimized version of GPUexplore can be more than two orders of magnitude faster than a sequential CPU implementation, reducing the runtime from more than an hour down to less than 37 seconds. |
| Item Type: | Essay (Master) |
| Clients: | Technische Universiteit Eindhoven, Eindhoven, The Netherlands |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/70500 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page