Detecting Data Races on OpenCL Kernels with Symbolic Execution
Dino Distefano, Jeremy Dubreil
TL;DR
This paper introduces an automatic symbolic execution-based method using separation logic to detect data races in OpenCL kernels, aiming to improve reliability in parallel computing.
Contribution
It presents a novel symbolic execution approach tailored for OpenCL kernels, enabling automatic detection of non-benign data races.
Findings
Successfully detects data races in OpenCL kernels
Automates analysis process reducing manual effort
Improves reliability of parallel kernel execution
Abstract
We present an automatic analysis technique for checking data races on OpenCL kernels. Our method defines symbolic execution techniques based on separation logic with suitable abstractions to automatically detect non-benign racy behaviours on kernel
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
TopicsSoftware Testing and Debugging Techniques · Parallel Computing and Optimization Techniques · Logic, programming, and type systems