Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications

TL;DR

This paper develops a formal, modular semantics for CUDA-C based on an existing C semantics, enabling better understanding and verification of GPU-accelerated programs, including race conditions and deadlocks.

Contribution

It extends an existing formal semantics to include CUDA-C features, providing a foundation for verifying heterogeneous GPU-accelerated programs.

Findings

Generated a tool that detects race conditions in CUDA-C programs

Identified limitations and extensibility of the semantics for broader verification

Demonstrated the semantics' usefulness in clarifying CUDA-C's hybrid computation model

Abstract

We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosu's K Framework semantics) with the core features of CUDA-C. The hybrid CPU/GPU computation model of CUDA-C presents challenges not just for programmers, but also for practitioners of formal methods. Our formal semantics helps expose and clarify these issues. We demonstrate the usefulness of our semantics by generating a tool from it capable of detecting some race conditions and deadlocks in CUDA-C programs. We discuss limitations of our model and argue that its extensibility can easily enable a wider range of verification tasks.