Checking data-race freedom of GPU kernels, compositionally

DOI10.1007/978-3-030-81685-8_19MaRDI QIDQ832190zbMATH OpenOpenAlexFDO

Authors Tiago Cogumbreiro, Julien Lange, Dennis Liew Zhen Rong, Hannah Zicarelli

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-81685-8_19

zbMATH Keywords

behavioural typesdata-raceGPUstatic analysis

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Automated verification of functional correctness of race-free GPU programs
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
• A Hoare Logic for GPU Kernels
• Dataflow analysis for datarace-free programs
• scientific article; zbMATH DE number 6712238

Cites work

• A Certified Data Race Analysis for a Java-like Language
• A Hoare Logic for GPU Kernels
• A Hoare logic for SIMT programs
• Automated verification of functional correctness of race-free GPU programs
• CONCUR 2004 - Concurrency Theory
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

Cited in

(7)

• Automated verification of functional correctness of race-free GPU programs
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• Strengthening induction-based race checking with lightweight static analysis
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
• Static detection of uncoalesced accesses in GPU programs
• Preface of the special issue on the conference on computer-aided verification 2020 and 2021
• Memory access protocols: certified data-race freedom for GPU kernels

Describes a project that uses

Uses Software

• GMRace
• GPUVerify
• GRace
• GKLEE
• CUDA
• BARRACUDA
• Boogie
• CURD
• LLVM
• KLEE-FP

This page was built for publication: Checking data-race freedom of GPU kernels, compositionally

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