Checking Equivalence of SPMD Programs Using Non-Interference

Motivated by the recent interest in multicore architectures, and in particular GPUs, we study one of their basic programming models, namely SPMD (Single-Program Multiple-Data) programs. We define a formal model of SPMD programs based on spawning and interleaving a variable number of threads manipulating global and local arrays, and synchronizing via barriers. SPMD programs are written with the intention to be deterministic, although programming errors may result in this not being true. These programs are also frequently modified, to achieve optimal performance. This motivates us to develop methods to check determinism and equivalence. A key property in achieving this is a non- interference property, that we formulate as validity of logical formulas derived from the program, that imply determinism. We also derive program post-conditions and show how they can be used to check equivalence of non-interfering programs.