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

Chris Hathhorn; Michela Becchi; William L.  Harrison; Adam Procter

doi:10.48550/arXiv.1211.6193

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

Chris Hathhorn
, Michela Becchi
, William L. Harrison
, Adam Procter

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosiu'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.

Original language	English
Title of host publication	Proceedings of the 2012 Systems Software Verification Conference
DOIs	https://doi.org/10.48550/arXiv.1211.6193
State	Published - 2012
Externally published	Yes

Access to Document

10.48550/arXiv.1211.6193

Cite this

@inproceedings{c85c002b26124772897e8916d629b170,

title = "Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications",

abstract = "We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosiu'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.",

author = "Chris Hathhorn and Michela Becchi and Harrison, \{William L.\} and Adam Procter",

year = "2012",

doi = "10.48550/arXiv.1211.6193",

language = "English",

booktitle = "Proceedings of the 2012 Systems Software Verification Conference",

}

TY - GEN

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

AU - Hathhorn, Chris

AU - Becchi, Michela

AU - Harrison, William L.

AU - Procter, Adam

PY - 2012

Y1 - 2012

N2 - We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosiu'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.

AB - We extend an off-the-shelf, executable formal semantics of C (Ellison and Rosiu'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.

U2 - 10.48550/arXiv.1211.6193

DO - 10.48550/arXiv.1211.6193

M3 - Conference contribution

BT - Proceedings of the 2012 Systems Software Verification Conference

ER -

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

Abstract

Access to Document

Fingerprint

Cite this