Verification of program parallelization

Saeed Darabi

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    166 Downloads (Pure)

    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.
    Original languageEnglish
    Awarding Institution
    • University of Twente
    Supervisors/Advisors
    • Huisman, Marieke , Supervisor
    Award date2 Mar 2018
    Print ISBNs978-90-365-4484-9
    DOIs
    Publication statusPublished - 2 Mar 2018

    Fingerprint Dive into the research topics of 'Verification of program parallelization'. Together they form a unique fingerprint.

    Cite this