The PTRANS Specification Language

Mansky, William

Permalink

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

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