A Verification Technique for Deterministic Parallel Programs

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

Abstract

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.
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
Pages247-264
Number of pages18
ISBN (Electronic)978-3-319-57288-8
DOIs
StatePublished - 2017
Event9th NASA Formal Methods Symposium 2017 - NASA Ames Research Center, Moffett Field, United States
Duration: 16 May 201718 May 2017
Conference number: 9
https://ti.arc.nasa.gov/events/nfm-2017/

Publication series

NameLecture Notes in Computer Science
Volume10227

Conference

Conference9th NASA Formal Methods Symposium 2017
Abbreviated titleNFM 2017
CountryUnited States
CityMoffett Field
Period16/05/1718/05/17
Internet address

Fingerprint

Chemical analysis
Fusion reactions
Semantics

Cite this

Darabi, S., Blom, S. C. C., & Huisman, M. (2017). A Verification Technique for Deterministic Parallel Programs. In C. Barrett, M. Davies, & T. Kahsai (Eds.), NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings (pp. 247-264). (Lecture Notes in Computer Science; Vol. 10227). DOI: 10.1007/978-3-319-57288-8_17
Darabi, Saeed ; Blom, Stefan C. C. ; Huisman, Marieke. / A Verification Technique for Deterministic Parallel Programs. NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. editor / Clark Barrett ; Misty Davies ; Temesghen Kahsai. 2017. pp. 247-264 (Lecture Notes in Computer Science).
@inproceedings{2bf4f1e160054936bd3488c061b3c3ff,
title = "A Verification Technique for Deterministic Parallel Programs",
abstract = "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.",
author = "Saeed Darabi and Blom, {Stefan C. C.} and Marieke Huisman",
year = "2017",
doi = "10.1007/978-3-319-57288-8_17",
language = "English",
isbn = "978-3-319-57287-1",
series = "Lecture Notes in Computer Science",
pages = "247--264",
editor = "Clark Barrett and Misty Davies and Temesghen Kahsai",
booktitle = "NASA Formal Methods",

}

Darabi, S, Blom, SCC & Huisman, M 2017, A Verification Technique for Deterministic Parallel Programs. in C Barrett, M Davies & T Kahsai (eds), NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10227, pp. 247-264, 9th NASA Formal Methods Symposium 2017, Moffett Field, United States, 16/05/17. DOI: 10.1007/978-3-319-57288-8_17

A Verification Technique for Deterministic Parallel Programs. / Darabi, Saeed; Blom, Stefan C. C.; Huisman, Marieke.

NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. ed. / Clark Barrett; Misty Davies; Temesghen Kahsai. 2017. p. 247-264 (Lecture Notes in Computer Science; Vol. 10227).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - A Verification Technique for Deterministic Parallel Programs

AU - Darabi,Saeed

AU - Blom,Stefan C. C.

AU - Huisman,Marieke

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-57288-8_17

DO - 10.1007/978-3-319-57288-8_17

M3 - Conference contribution

SN - 978-3-319-57287-1

T3 - Lecture Notes in Computer Science

SP - 247

EP - 264

BT - NASA Formal Methods

ER -

Darabi S, Blom SCC, Huisman M. A Verification Technique for Deterministic Parallel Programs. In Barrett C, Davies M, Kahsai T, editors, NASA Formal Methods: 9th International Symposium, NFM 2017, Moffett Field, CA, USA, May 16-18, 2017, Proceedings. 2017. p. 247-264. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-57288-8_17