*banner
 

Checking Non-Interference in SPMD Programs
Stavros Tripakis, Christos Stergiou, Roberto Lublinerman

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess