University of Illinois Urbana-Champaign

The PTRANS Specification Language

Mansky, William

Content Files
ptrans.pdf

Permalink

https://hdl.handle.net/2142/47101

Description

Title
The PTRANS Specification Language
Author(s)
Mansky, William
Contributor(s)
Gunter, Elsa L.
Issue Date
2014-02-01
Keyword(s)
  • compiler optimization
  • parallel programming
  • program transformations
  • temporal logic
Date of Ingest
2014-02-01T18:28:25Z
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.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/47101
Sponsor(s)/Grant Number(s)
NSF Grant CCF 13-18191

Owning Collections

Research and Tech Reports - Computer Science PRIMARY