Files in this item



application/pdfptrans.pdf (276kB)
(no description provided)PDF


Title:The PTRANS Specification Language
Author(s):Mansky, William
Contributor(s):Gunter, Elsa L.
Subject(s):compiler optimization
parallel programming
program transformations
temporal logic
Abstract:The VeriF-OPT project seeks to provide a framework for stating and reasoning about compiler optimizations and transformations on parallel programs in the presence of relaxed memory models. The core of the framework is a domain-specific language for specifying compiler optimizations: PTRANS, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. This document describes the syntax of PTRANS and its two semantics: the abstract semantics used to verify specifications, and the executable semantics used to prototype specifications.
Issue Date:2014-02-01
Genre:Technical Report
Publication Status:unpublished
Peer Reviewed:not peer reviewed
Sponsor:NSF Grant CCF 13-18191
Date Available in IDEALS:2014-02-01

This item appears in the following Collection(s)

Item Statistics