Citation
Stavros Tripakis, Christos Stergiou, Roberto Lublinerman. "Checking Non-Interference in SPMD Programs". 2nd USENIX Workshop on Hot Topics in Parallelism (HotPar 2010), 1-6, June, 2010.

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 the need for methods 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.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-11.html. (Related technical report)
• http://www.usenix.org/events/hotpar10/final_posters/Tripakis.pdf. (HotPar'10 paper publicly available from USENIX)
• http://www.usenix.org/event/hotpar10/tech/slides/tripakis.pdf

• HTML

  Stavros Tripakis, Christos Stergiou, Roberto Lublinerman.
  <a
  href="http://chess.eecs.berkeley.edu/pubs/663.html"
  >Checking Non-Interference in SPMD Programs</a>,
  2nd USENIX Workshop on Hot Topics in Parallelism (HotPar
  2010), 1-6, June, 2010.

• Plain text

  Stavros Tripakis, Christos Stergiou, Roberto Lublinerman.
  "Checking Non-Interference in SPMD Programs". 2nd
  USENIX Workshop on Hot Topics in Parallelism (HotPar 2010),
  1-6, June, 2010.

• BibTeX

  @inproceedings{TripakisStergiouLublinerman10_CheckingNonInterferenceInSPMDPrograms,
      author = {Stavros Tripakis and Christos Stergiou and Roberto
                Lublinerman},
      title = {Checking Non-Interference in SPMD Programs},
      booktitle = {2nd USENIX Workshop on Hot Topics in Parallelism
                (HotPar 2010)},
      pages = {1-6},
      month = {June},
      year = {2010},
      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 the need for methods 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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/663.html}
  }
  

Posted by Stavros Tripakis on 18 Mar 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.