Verification of program parallelization

Saeed Darabi

Research output: ThesisPhD Thesis - Research UT, graduation UT

Abstract

This thesis presents a set of verification techniques based on permission-based separation logic to reason about the data race freedom and functional correctness of program parallelizations. Our reasoning techniques address different forms of high-level and low-level parallelization. For high-level parallel programs, we first define the Parallel Programming Language (PPL), a simple core language that captures the main features of deterministic parallel programming; then we discuss how PPL programs and consequently, real-world deterministic parallel programs (e.g. OpenMP programs) are verified. For low-level parallel programs, we specifically focus on reasoning about GPGPU kernels. At the end we discuss how the presented verification techniques are chained together to reason about the semantic equivalence of high-level parallel programs where they are automatically transformed to low-level parallel programs by a parallelizing compiler. Thus, effectively enabling a holistic verification solution for such parallelization frameworks.
LanguageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Huisman, Marieke , Supervisor
Award date2 Mar 2018
Print ISBNs978-90-365-4484-9
DOIs
StatePublished - 2 Mar 2018

Fingerprint

Parallel programming
Computer programming languages
Semantics

Cite this

Darabi, Saeed . / Verification of program parallelization. 2018. 167 p.
@phdthesis{e36589ceaad34ad595fd9fbd0626542b,
title = "Verification of program parallelization",
abstract = "This thesis presents a set of verification techniques based on permission-based separation logic to reason about the data race freedom and functional correctness of program parallelizations. Our reasoning techniques address different forms of high-level and low-level parallelization. For high-level parallel programs, we first define the Parallel Programming Language (PPL), a simple core language that captures the main features of deterministic parallel programming; then we discuss how PPL programs and consequently, real-world deterministic parallel programs (e.g. OpenMP programs) are verified. For low-level parallel programs, we specifically focus on reasoning about GPGPU kernels. At the end we discuss how the presented verification techniques are chained together to reason about the semantic equivalence of high-level parallel programs where they are automatically transformed to low-level parallel programs by a parallelizing compiler. Thus, effectively enabling a holistic verification solution for such parallelization frameworks.",
author = "Saeed Darabi",
note = "IPA Dissertation Series No. 2018-02 IDS PhD. Thesis Series No. 18-458",
year = "2018",
month = "3",
day = "2",
doi = "10.3990/1.9789036544849",
language = "English",
isbn = "978-90-365-4484-9",
school = "University of Twente",

}

Darabi, S 2018, 'Verification of program parallelization', University of Twente. DOI: 10.3990/1.9789036544849

Verification of program parallelization. / Darabi, Saeed .

2018. 167 p.

Research output: ThesisPhD Thesis - Research UT, graduation UT

TY - THES

T1 - Verification of program parallelization

AU - Darabi,Saeed

N1 - IPA Dissertation Series No. 2018-02 IDS PhD. Thesis Series No. 18-458

PY - 2018/3/2

Y1 - 2018/3/2

N2 - This thesis presents a set of verification techniques based on permission-based separation logic to reason about the data race freedom and functional correctness of program parallelizations. Our reasoning techniques address different forms of high-level and low-level parallelization. For high-level parallel programs, we first define the Parallel Programming Language (PPL), a simple core language that captures the main features of deterministic parallel programming; then we discuss how PPL programs and consequently, real-world deterministic parallel programs (e.g. OpenMP programs) are verified. For low-level parallel programs, we specifically focus on reasoning about GPGPU kernels. At the end we discuss how the presented verification techniques are chained together to reason about the semantic equivalence of high-level parallel programs where they are automatically transformed to low-level parallel programs by a parallelizing compiler. Thus, effectively enabling a holistic verification solution for such parallelization frameworks.

AB - This thesis presents a set of verification techniques based on permission-based separation logic to reason about the data race freedom and functional correctness of program parallelizations. Our reasoning techniques address different forms of high-level and low-level parallelization. For high-level parallel programs, we first define the Parallel Programming Language (PPL), a simple core language that captures the main features of deterministic parallel programming; then we discuss how PPL programs and consequently, real-world deterministic parallel programs (e.g. OpenMP programs) are verified. For low-level parallel programs, we specifically focus on reasoning about GPGPU kernels. At the end we discuss how the presented verification techniques are chained together to reason about the semantic equivalence of high-level parallel programs where they are automatically transformed to low-level parallel programs by a parallelizing compiler. Thus, effectively enabling a holistic verification solution for such parallelization frameworks.

U2 - 10.3990/1.9789036544849

DO - 10.3990/1.9789036544849

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-365-4484-9

ER -

Darabi S. Verification of program parallelization. 2018. 167 p. Available from, DOI: 10.3990/1.9789036544849