University of Twente Student Theses


GPU implementation of partial-order reduction

Neele, Thomas (2016) GPU implementation of partial-order reduction.

[img] PDF
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)
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:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page