Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

DOI10.1007/978-3-642-37036-6_16MaRDI QIDQ5326291zbMATH OpenOpenAlexFDO

Authors Peter Collingbourne, Alastair Donaldson, Jeroen Ketema, Shaz Qadeer

Publication date 5 August 2013

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-37036-6_16

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Recommendations

• Checking data-race freedom of GPU kernels, compositionally
• Automated verification of functional correctness of race-free GPU programs
• A Hoare Logic for GPU Kernels
• Static detection of uncoalesced accesses in GPU programs

Cited in

(9)

• Automated verification of functional correctness of race-free GPU programs
• An optimal \(k\)-exclusion real-time locking protocol motivated by multi-GPU systems
• GPUVerify
• On the correctness of the SIMT execution model of GPUs
• A Hoare logic for SIMT programs
• Hardware Support for Concurrent Detection of Multiple Concurrency Bugs on Fused CPU-GPU Architectures
• A Hoare Logic for GPU Kernels
• Memory access protocols: certified data-race freedom for GPU kernels
• Checking data-race freedom of GPU kernels, compositionally

Describes a project that uses

Uses Software

• Boogie
• GKLEE
• CUDA
• OpenCL

This page was built for publication: Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326291)