Checking Equivalence of SPMD Programs Using Non- Interference
Checking Equivalence of SPMD Programs Using Non- Interference
复制标题
使用无干扰检查 SPMD 程序的等价性
DOI：
10.21236/ada538815
复制
发表时间：
2010
影响因子：
0.8
通讯作者：
Roberto Lublinerman
中科院分区：
文献类型：
--
作者：
S. Tripakis;C. Stergiou;Roberto Lublinerman
摘要：我们研究了基本的多项和GPU编程模型之一，即SPMD（单程序多数据）程序。我们基于操纵全球和本地阵列的相互交织线的形式模型SPMD程序，并通过壁垒进行同步。 SPMD程序的编写意图是确定性的，尽管编程错误可能会导致这不是真的。 SPMD程序也经常用于最佳性能。这些事实激发了我们开发检查确定性和等价性的方法。实现这一目标的关键属性是从程序自动得出的逻辑公式的有效性，这意味着确定性。自动派生的后条件可用于检查非屈服程序的等效性。我们报告了可以证明NVIDIA CUDA程序不干预的原型。
Abstract : We study one of the basic multicore and GPU programming models, namely, SPMD (Single-Program Multiple-Data) programs. We define a formal model of SPMD programs based on interleaving threads that manipulate global and local arrays, and synchronize via barriers. SPMD programs are written with the intention to be deterministic, although programming errors may result in this not being true. SPMD programs are also frequently modified toward optimal performance. These facts motivate us to develop methods to check determinism and equivalence. A key property in achieving this is noninterference formulated as validity of logical formulas automatically derived from the program, that imply determinism. Automatically derived post-conditions can be used to check equivalence of noninterfering programs. We report on a prototype that can prove non-interference of NVIDIA CUDA programs.