Roberto Lublinerman and Stavros Tripakis

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-42

March 24, 2009

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-42.pdf

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.

---

BibTeX citation:

@techreport{Lublinerman:EECS-2009-42,
    Author= {Lublinerman, Roberto and Tripakis, Stavros},
    Title= {Checking Equivalence of SPMD Programs Using Non-Interference},
    Year= {2009},
    Month= {Mar},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-42.html},
    Number= {UCB/EECS-2009-42},
    Abstract= {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.},
}

EndNote citation:

%0 Report
%A Lublinerman, Roberto 
%A Tripakis, Stavros 
%T Checking Equivalence of SPMD Programs Using Non-Interference
%I EECS Department, University of California, Berkeley
%D 2009
%8 March 24
%@ UCB/EECS-2009-42
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-42.html
%F Lublinerman:EECS-2009-42