GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
Soham Chakraborty, S. Krishna, Andreas Pavlogiannis, Omkar Tuppe

TL;DR
GPUMC is a novel stateless model checker designed for GPU weak memory concurrency, capable of exploring all executions, detecting errors, and automatically repairing issues in GPU shared-memory programs.
Contribution
It introduces GPUMC, the first stateless model checker tailored for GPU weak memory models, enhancing error detection and repair in GPU concurrent programming.
Findings
GPUMC efficiently verifies large GPU programs where existing tools timeout.
GPUMC detects all known errors in tested benchmarks.
GPUMC automatically repairs certain errors.
Abstract
GPU computing is embracing weak memory concurrency for performance improvement. However, compared to CPUs, modern GPUs provide more fine-grained concurrency features such as scopes, have additional properties like divergence, and thereby follow different weak memory consistency models. These features and properties make concurrent programming on GPUs more complex and error-prone. To this end, we present GPUMC, a stateless model checker to check the correctness of GPU shared-memory concurrent programs under scoped-RC11 weak memory concurrency model. GPUMC explores all possible executions in GPU programs to reveal various errors - races, barrier divergence, and assertion violations. In addition, GPUMC also automatically repairs these errors in the appropriate cases. We evaluate GPUMC with benchmarks and real-life GPU programs. GPUMC is efficient both in time and memory in verifying…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsParallel Computing and Optimization Techniques · Network Packet Processing and Optimization · Graph Theory and Algorithms
