异构CUDA-C的形式语义：模块化方法及应用
编程语言
2012-11-28 v1
摘要
我们将一个现成的可执行C形式语义（Ellison和Rosu的K框架语义）扩展了CUDA-C的核心特性。CUDA-C的混合CPU/GPU计算模型不仅给程序员带来了挑战，也给形式化方法的实践者带来了挑战。我们的形式语义有助于揭示和澄清这些问题。我们通过从该语义生成一个能够检测CUDA-C程序中某些竞态条件和死锁的工具，展示了其有用性。我们讨论了模型的局限性，并论证了其可扩展性可以轻松实现更广泛的验证任务。
引用
@article{arxiv.1211.6193,
title = {Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications},
author = {Chris Hathhorn and Michela Becchi and William L. Harrison and Adam Procter},
journal= {arXiv preprint arXiv:1211.6193},
year = {2012}
}
备注
In Proceedings SSV 2012, arXiv:1211.5873