Thomas Neele - GPU implementation of Partial-Order Reduction

author:Thomas Neele
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
Anton Wijs
dr. S.C.C. Blom
graduation date:14 July 2016 (mark: 10)

Research Topics


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.