Citation
Roberto Lublinerman, Stavros Tripakis. "Checking Equivalence of SPMD Programs Using Non-Interference". Technical report, EECS Department, University of California, Berkeley, UCB/EECS-2009-42, March, 2009.

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.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-42.html

• HTML

  Roberto Lublinerman, Stavros Tripakis. <a
  href="http://chess.eecs.berkeley.edu/pubs/540.html"
  ><i>Checking Equivalence of SPMD Programs Using
  Non-Interference</i></a>, Technical report, 
  EECS Department, University of California, Berkeley,
  UCB/EECS-2009-42, March, 2009.

• Plain text

  Roberto Lublinerman, Stavros Tripakis. "Checking
  Equivalence of SPMD Programs Using Non-Interference".
  Technical report,  EECS Department, University of
  California, Berkeley, UCB/EECS-2009-42, March, 2009.

• BibTeX

  @techreport{LublinermanTripakis09_CheckingEquivalenceOfSPMDProgramsUsingNonInterference,
      author = {Roberto Lublinerman and Stavros Tripakis},
      title = {Checking Equivalence of SPMD Programs Using
                Non-Interference},
      institution = {EECS Department, University of California, Berkeley},
      number = {UCB/EECS-2009-42},
      month = {March},
      year = {2009},
      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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/540.html}
  }
  

Posted by Stavros Tripakis on 24 Mar 2009.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.