Specifying and verifying program transformations with PTRANS

Mansky, William

Permalink

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

Description

Title

Specifying and verifying program transformations with PTRANS

Author(s)

Mansky, William

Issue Date

2014-05-30T16:41:23Z

Director of Research (if dissertation) or Advisor (if thesis)

Gunter, Elsa L.

Doctoral Committee Chair(s)

Gunter, Elsa L.

Committee Member(s)

• Roşu, Grigore
• Adve, Vikram S.
• Kalvala, Sara

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(s)

• compiler correctness
• control flow graphs
• temporal logic
• rewriting
• graph transformation
• interactive theorem proving
• operational semantics
• concurrency
• relaxed memory models
• Satisfiability Modulo Theories (SMT) solvers

Abstract

Software developers, compiler designers, and formal methods researchers all stand to benefit from improved tools for compiler design and verification. Program correctness for compiled languages depends fundamentally on compiler correctness, and compiler optimizations are usually not formally verified due to the effort involved. This is particularly true for optimizations on parallel programs, which are often more difficult to specify correctly and to verify than their sequential counterparts, especially in the presence of relaxed memory models. In this thesis, we outline a Verification Framework for Optimizations and Program Transformations, designed to facilitate stating and reasoning about compiler optimizations and transformations on parallel programs. Most verified compilation projects focus on a single intermediate language and a small number of input and output languages, later adding new targets as extensions; our framework, on the other hand, is designed with language-independence as a first principle, and we seek to generalize and reuse as much as possible across multiple target languages. Our framework makes use of the novel PTRANS transformation specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. The syntax of PTRANS allows cleaner, more proof-amenable specification of program optimizations. PTRANS has two sets of semantics: an abstract semantics for verification, and an executable semantics that allows specifications to act as prototypes for the optimizations themselves, so that candidate optimizations can be tested and refined before going on to formally verify them or include them in a compiler. We address the problems of parallelism head-on by developing a generic framework for memory models in VeriF-OPT, and present a method of importing external analyses such as alias analysis to overcome potential limitations of temporal logic. Finally, we demonstrate the use of the framework by prototyping, testing, and verifying the correctness of several variants of redundant store elimination in two markedly different intermediate languages.

Graduation Semester

2014-05

Permalink

http://hdl.handle.net/2142/49385

Copyright and License Information

Copyright 2014 by William Ernest Mansky

Owning Collections