A Verification Technique for Deterministic Parallel Programs

Saeed Darabi, Stefan C.C. Blom, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    8 Citations (Scopus)
    8 Downloads (Pure)


    A commonly used approach to develop parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to prove correctness of compiler directives combined with functional correctness of the program. We propose syntax and semantics for a simple core language, capturing the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorized and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show that it is sufficient to have contracts for the basic blocks to prove correctness of the compiler directives, and moreover that functional correctness of the sequential program implies correctness of the parallelized program. We formally prove correctness of our approach. In addition, we define a widely-used subset of OpenMP that can be encoded into our core language, thus effectively enabling the verification of OpenMP compiler directives, and we discuss automated tool support for this verification process.
    Original languageEnglish
    Title of host publicationNASA Formal Methods
    Subtitle of host publication9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings
    EditorsClark Barrett, Misty Davies, Temesghen Kahsai
    Number of pages18
    ISBN (Electronic)978-3-319-57288-8
    Publication statusPublished - 2017
    Event9th NASA Formal Methods Symposium 2017 - NASA Ames Research Center, Moffett Field, United States
    Duration: 16 May 201718 May 2017
    Conference number: 9

    Publication series

    NameLecture Notes in Computer Science


    Conference9th NASA Formal Methods Symposium 2017
    Abbreviated titleNFM 2017
    Country/TerritoryUnited States
    CityMoffett Field
    Internet address


    Dive into the research topics of 'A Verification Technique for Deterministic Parallel Programs'. Together they form a unique fingerprint.

    Cite this