Checking Non-Interference in SPMD Programs

We study one of the basic multicore and GPU pro- gramming 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 synchro- nize via barriers. SPMD programs are written with the intention to be deterministic, although program- ming errors may result in this not being true. SPMD programs are also frequently modified toward optimal performance. These facts motivate the need for meth- ods to check determinism and program equivalence. A key property in achieving this is non-interference. We formulate non-interference as validity of logical formulas automatically derived from the program, we show that non-interference implies determinism, and we report on a prototype that can prove non- interference of NVIDIA CUDA programs.