The Design and Implementation of a Verification Technique for GPU Kernels

No abstract is available for this paper.

• Publication year

  2015

• Venue

  ACM Transactions on Programming Languages and Systems

• Publication date

  2015-05-22

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1145/2743017
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• GPU concurrency Weak behaviours and programming assumptions

  2015cited by this paper
• Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels

  2014influential reference
• Syntax and semantics of a GPU kernel programming language

  2014cited by this paper
• The GPUVerify Method: a Tutorial Overview

  2014influential reference
• KernelInterceptor: automating GPU kernel verification by intercepting kernels and their parameters

  2014cited by this paper
• A sound and complete abstraction for reasoning about parallel prefix sums

  2014influential reference
• Engineering a Static Verification Tool for GPU Kernels

  2014influential reference
• Specification and verification of GPGPU programs

  2013cited by this paper
• Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

  2013influential reference
• Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding

  2013cited by this paper
• SLAM++: Simultaneous Localisation and Mapping at the Level of Objects

  2013cited by this paper
• Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels

  2013influential reference
• A Hoare Logic for SIMT Programs

  2013cited by this paper
• BarraCUDA - a fast short read sequence aligner using graphics processing units

  2012cited by this paper
• Parametric flows: Automated behavior equivalencing for symbolic analysis of races in CUDA programs

  2012cited by this paper
• Verifying GPU kernels by test amplification

  2012cited by this paper
• GKLEE: concolic verification and test generation for GPUs

  2012cited by this paper
• GPUVerify: a verifier for GPU kernels

  2012influential reference
• On the Correctness of the SIMT Execution Model of GPUs

  2012cited by this paper
• Automatic analysis of DMA races using model checking and k-induction

  2011cited by this paper
• Symbolic Testing of OpenCL Code

  2011cited by this paper
• OpenCL Programming Guide

  2011cited by this paper
• Thread contracts for safe parallelism

  2011cited by this paper
• Instantiation-Based Invariant Discovery

  2011cited by this paper
• Delay-bounded scheduling

  2011cited by this paper
• Checking Equivalence of SPMD Programs Using Non- Interference

  2010cited by this paper
• Scalable SMT-based verification of GPU kernel functions

  2010influential reference
• Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors

  2010cited by this paper
• A few billion lines of code later

  2010cited by this paper
• Formal SOS-Proofs for the Lambda-Calculus

  2009cited by this paper
• Complexity and Algorithms for Monomial and Clausal Predicate Abstraction

  2009cited by this paper
• Program verification using templates over predicate abstraction

  2009cited by this paper
• Going with the Flow: Parameterized Verification Using Message Flows

  2008cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Automated Dynamic Analysis of CUDA Programs

  2008cited by this paper
• KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs

  2008cited by this paper
• The Daikon system for dynamic detection of likely invariants

  2007cited by this paper
• Path invariants

  2007cited by this paper
• Lazy Abstraction with Interpolants

  2006cited by this paper
• Fast fluid dynamics simulation on the GPU

  2005cited by this paper
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs

  2005cited by this paper
• GIST: an interactive, GPU-based level set segmentation tool for 3D medical images

  2004cited by this paper
• A Simple Method for Parameterized Verification of Cache Coherence Protocols

  2004influential reference
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic

  2002cited by this paper
• Houdini, an Annotation Assistant for ESC/Java

  2001cited by this paper
• ESC/Java User's Manual

  2000influential reference
• Verification of Infinite State Systems by Compositional Model Checking

  1999cited by this paper
• Construction of Abstract State Graphs with PVS

  1997cited by this paper
• Points-to analysis in almost linear time

  1996cited by this paper
• Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints

  1977cited by this paper
• BIOINFORMATICS ORIGINAL PAPER

  year unknowncited by this paper
• Journal of Graph Algorithms and Applications Many-to-one Boundary Labeling

  year unknowncited by this paper

• A Modular Static Cost Analysis for GPU Warp-Level Parallelism

  2026cites this paper
• PhoenixOS: Concurrent OS-level GPU Checkpoint and Restore with Validated Speculation

  2024cites this paper
• LLOR: Automated Repair of OpenMP Programs

  2024cites this paper
• Microsecond-scale Dynamic Validation of Idempotency for GPU Kernels

  2024cites this paper
• Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs

  2024cites this paper
• Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed

  2023cites this paper
• GPURepair: Automated Repair of GPU Kernels (Extended Version)

  2023cites this paper
• Memory access protocols: certified data-race freedom for GPU kernels

  2023influential citation
• Symbolic identification of shared memory based bank conflicts for GPUs

  2022cites this paper
• Provable GPU Data-Races in Static Race Detection

  2022cites this paper
• iGUARD: In-GPU Advanced Race Detection

  2021cites this paper
• Specifying and testing GPU workgroup progress models

  2021cites this paper
• Checking Data-Race Freedom of GPU Kernels, Compositionally

  2021influential citation
• Static detection of uncoalesced accesses in GPU programs

  2021cites this paper
• GPURepair: Automated Repair of GPU Kernels

  2020cites this paper
• Experiments-based parameter identification on the GPU for cooperative systems

  2020cites this paper
• Towards verified construction of correct and optimised GPU software

  2020cites this paper
• ScoRD: A Scoped Race Detector for GPUs

  2020cites this paper
• Efficient Precise Dynamic Data Race Detection for CPU and GPU

  2019cites this paper
• Analysis of GPGPU Programs for Data-race and Barrier Divergence

  2018cites this paper
• How Easy it is to Write Software for Heterogeneous Systems?

  2018cites this paper
• CURD: a dynamic CUDA race detector

  2018cites this paper
• GPU Schedulers: How Fair Is Fair Enough?

  2018cites this paper
• Automatic Synchronization for GPU Kernels

  2018influential citation
• Verification of Program Parallelization

  2018cites this paper
• Inter-workgroup barrier synchronisation on graphics processing units

  2018cites this paper
• Formal analysis techniques for reliable GPU programming: current solutions and call to action

  2017influential citation
• A Hoare Logic for GPU Kernels

  2017cites this paper
• Bounded exhaustive test-input generation on GPUs

  2017cites this paper
• Forward progress on GPU concurrency

  2017cites this paper
• Towards Self-Verification in Finite Difference Code Generation

  2017cites this paper
• GPUDrano: Detecting Uncoalesced Accesses in GPU Programs

  2017cites this paper
• SafeGPU: Contract- and library-based GPGPU for object-oriented languages

  2017cites this paper
• Termination analysis for GPU kernels

  2017cites this paper
• BARRACUDA: binary-level analysis of runtime RAces in CUDA programs

  2017cites this paper
• Exposing errors related to weak memory in GPU applications

  2016cites this paper
• Detecting bank conflict of GPU programs using symbolic execution

  2016cites this paper
• Scalable techniques for analysing and testing asynchronous software systems

  2016cites this paper
• A compiler for throughput optimization of graph algorithms on GPUs

  2016cites this paper
• Portable inter-workgroup barrier synchronisation for GPUs

  2016cites this paper
• Automated Verification of Functional Correctness of Race-Free GPU Programs

  2016influential citation
• Automatic Test Case Reduction for OpenCL

  2016influential citation
• The Hitchhiker's Guide to Cross-Platform OpenCL Application Development

  2016cites this paper
• Analysing the Program Analyser

  2016cites this paper
• Coherence-Free Multiview: Enabling Reference-Discerning Data Placement on GPU

  2016cites this paper
• Implementing and Evaluating Candidate-Based Invariant Generation

  2016cites this paper
• Remote-scope promotion: clarified, rectified, and verified

  2015cites this paper
• Overhauling SC atomics in C11 and OpenCL

  2015cites this paper
• Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers (T)

  2015cites this paper
• Contract-based general-purpose GPU programming

  2014cites this paper
• Syntax and semantics of a GPU kernel programming language

  2014cites this paper
• Hidden assumptions in static verification of data-race free GPU programs

  year unknowncites this paper
• Overhauling SC Atomics in C 11 and OpenCL Mark Batty

  year unknowncites this paper