Checking data-race freedom of GPU kernels, compositionally

DOI10.1007/978-3-030-81685-8_19zbMath1493.68025OpenAlexW3186710384MaRDI QIDQ832190

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

Publication date: 25 March 2022

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

zbMATH Keywords

static analysisGPUbehavioural typesdata-race

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

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

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