A Hoare Logic for GPU Kernels

DOI10.1145/3001834MaRDI QIDQ5278201zbMATH OpenOpenAlexWikidataFDO

Authors Kensuke Kojima, Atsushi Igarashi

Publication date 13 July 2017

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3001834

zbMATH Keywords

GPUHoare logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical problems of computer architecture (68M07) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
• Optimising purely functional GPU programs

Cites work

• A Hoare logic for SIMT programs
• An axiomatic proof technique for parallel programs
• Automated verification of functional correctness of race-free GPU programs
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
• On the correctness of the SIMT execution model of GPUs
• Verification of sequential and concurrent programs

Cited in

(6)

• Automated verification of functional correctness of race-free GPU programs
• On the correctness of the SIMT execution model of GPUs
• A Hoare logic for SIMT programs
• Interleaving and Lock-Step Semantics for Analysis and Verification of 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

• Coq
• CUDA
• OpenCL
• GPUVerify
• GKLEE
• KLEE-FP

This page was built for publication: A Hoare Logic for GPU Kernels

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