May 02, 2017: Saeed Darabi: A Verification Technique for Deterministic Parallel Programs

May 02, 2017A Verification Technique for Deterministic Parallel Programs
Room: Hal B 2BSaeed Darabi

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.