异构CUDA-C的形式语义：具有应用的模块化方法
摘要：使用现成的，可执行的 C 语言形式语义（Ellison 和 Rosu 的 K 框架语义）扩展 CUDA-C 的核心特性。CUDA-C 的混合 CPU/GPU 计算模型不仅对程序员提出挑战，也对形式方法的从业者提出了挑战。我们的形式语义有助于揭示和澄清这些问题。我们通过从语义生成工具来展示其有用性，该工具能够检测 CUDA-C 程序中的一些竞争条件和死锁。我们讨论了我们模型的局限性，并认为其可扩展性可以轻松实现更广泛的验证任务。
作者：Chris Hathhorn (University of Missouri), Michela Becchi (University of Missouri), William L. Harrison (University of Missouri), Adam Procter (University of Missouri)
论文ID：1211.6193
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-11-28