Thomas Neele - GPU implementation of Partial-Order Reduction
|title:||GPU implementation of Partial-Order Reduction|
|keywords:||LTSmin, GPUexplore GPU, POR|
|topics:||Algorithms and Data Structures|
|committee:||prof.dr. J.C. van de Pol|
dr. S.C.C. Blom
|graduation date:||14 July 2016 (mark: 10)|
Model checking using GPUs has seen increased popularity over the last years. Be- cause 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 pro- posed 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.