A Verification Technique for Deterministic Parallel Programs (extended version)

Saeed Darabi, Stefan Blom, Marieke Huisman

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.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages19
StatePublished - 25 Feb 2017

Publication series

NameCTIT technical report
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-17-01
ISSN (Print)1381-3625

Fingerprint

Chemical analysis
Fusion reactions
Semantics

Keywords

  • IR-103779
  • EC Grant Agreement nr.: FP7/287767
  • EC Grant Agreement nr.: FP7/258405
  • EWI-27789

Cite this

Darabi, S., Blom, S., & Huisman, M. (2017). A Verification Technique for Deterministic Parallel Programs (extended version). (CTIT technical report; No. TR-CTIT-17-01). Enschede: Centre for Telematics and Information Technology (CTIT).

Darabi, Saeed; Blom, Stefan; Huisman, Marieke / A Verification Technique for Deterministic Parallel Programs (extended version).

Enschede : Centre for Telematics and Information Technology (CTIT), 2017. 19 p. (CTIT technical report; No. TR-CTIT-17-01).

Research output: Other research outputReport

@book{83014b71746744caaac9951ef4ae1ea5,
title = "A Verification Technique for Deterministic Parallel Programs (extended version)",
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.",
keywords = "IR-103779, EC Grant Agreement nr.: FP7/287767, EC Grant Agreement nr.: FP7/258405, EWI-27789",
author = "Saeed Darabi and Stefan Blom and Marieke Huisman",
year = "2017",
month = "2",
series = "CTIT technical report",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-17-01",
address = "Netherlands",

}

Darabi, S, Blom, S & Huisman, M 2017, A Verification Technique for Deterministic Parallel Programs (extended version). CTIT technical report, no. TR-CTIT-17-01, Centre for Telematics and Information Technology (CTIT), Enschede.

A Verification Technique for Deterministic Parallel Programs (extended version). / Darabi, Saeed; Blom, Stefan; Huisman, Marieke.

Enschede : Centre for Telematics and Information Technology (CTIT), 2017. 19 p. (CTIT technical report; No. TR-CTIT-17-01).

Research output: Other research outputReport

TY - BOOK

T1 - A Verification Technique for Deterministic Parallel Programs (extended version)

AU - Darabi,Saeed

AU - Blom,Stefan

AU - Huisman,Marieke

PY - 2017/2/25

Y1 - 2017/2/25

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.

KW - IR-103779

KW - EC Grant Agreement nr.: FP7/287767

KW - EC Grant Agreement nr.: FP7/258405

KW - EWI-27789

M3 - Report

T3 - CTIT technical report

BT - A Verification Technique for Deterministic Parallel Programs (extended version)

PB - Centre for Telematics and Information Technology (CTIT)

ER -

Darabi S, Blom S, Huisman M. A Verification Technique for Deterministic Parallel Programs (extended version). Enschede: Centre for Telematics and Information Technology (CTIT), 2017. 19 p. (CTIT technical report; TR-CTIT-17-01).