Files in this item

FilesDescriptionFormat

application/pdf

application/pdfWilliam_Mansky.pdf (1MB)
(no description provided)PDF

application/octet-stream

application/octet-streamtrans_syntax.thy (5kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamtrans_sim.thy (41kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamtrans_semantics.thy (11kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamtrans_preds.thy (20kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamtrans_flowgraph.thy (36kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamstep_rel.thy (22kB)
(no description provided)Unknown

application/octet-stream

application/octet-streammemory_model.thy (23kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamLLVM_sim.thy (12kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamLLVM_RSE_TSO.thy (26kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamLLVM_RSE_SC.thy (17kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamLLVM_RSE_PSO.thy (22kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamLLVM_RSE_pre.thy (4kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamLLVM_preds.thy (114kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamLLVM.thy (43kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamBIL_opt.thy (17kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamBIL_graph.thy (108kB)
(no description provided)Unknown

application/octet-stream

application/octet-streamBIL.thy (14kB)
(no description provided)Unknown

Description

Title:Specifying and verifying program transformations with PTRANS
Author(s):Mansky, William
Director of Research:Gunter, Elsa L.
Doctoral Committee Chair(s):Gunter, Elsa L.
Doctoral Committee Member(s):Roşu, Grigore; Adve, Vikram S.; Kalvala, Sara
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(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.
Issue Date:2014-05-30
URI:http://hdl.handle.net/2142/49385
Rights Information:Copyright 2014 by William Ernest Mansky
Date Available in IDEALS:2014-05-30
Date Deposited:2014-05


This item appears in the following Collection(s)

Item Statistics