Files in this item

FilesDescriptionFormat

application/pdf

application/pdfLI-DISSERTATION-2020.pdf (2MB)
(no description provided)PDF

Description

Title:A verification framework suitable for proving large language translations
Author(s):Li, Liyi
Director of Research:Gunter, Elsa L
Doctoral Committee Chair(s):Gunter, Elsa L
Doctoral Committee Member(s):Rosu, Grigore; Padua, David; Adve, Vikram; Zdancewic, Steve
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Degree:Ph.D.
Genre:Dissertation
Subject(s):Compiler Verification
Language Semantics
K
Rewriting Logic
LLVM
Memory Model
Simulation Relation
Concurrency Model
Abstract:Previously, researchers established some frameworks, such as Morpheus, to specify a compiler translation in a small language and prove the semantic preservation property of the translation in the language under the assumption of sequential consistency. Based on the Morpheus specification language, we extend the verification framework to prove the compiler translation semantic preservation property in a large real-world programming language with a real-world weak concurrency model. The framework combines four different pieces. First, we specify a complete semantics of the K framework and a translation from K to Isabelle as our basis for defining language specifications and proving properties about the specifications. Second, we define a complete operational semantics of LLVM in K, named K-LLVM, including the specifications of all instructions and intrinsic functions in LLVM, as well as the concurrency model of LLVM. Third, to verify the correctness of the K-LLVM operational model, we create an axiomatic model, named Hybrid Axiomatic Timed Relaxed Concurrency Model (HATRMM). The creation of HATRMM is to bridge the traditional C++ candidate execution models and the K-LLVM operational concurrency model. Finally, to enhance our framework to prove the semantic preservation property in a relaxed memory model, we define a new simulation framework, named Per Location Simulation (PLS). PLS is suitable for proving semantic preservation property in a relaxed memory model.
Issue Date:2020-11-25
Type:Thesis
URI:http://hdl.handle.net/2142/109386
Rights Information:Copyright 2020 Liyi Li
Date Available in IDEALS:2021-03-05
Date Deposited:2020-12


This item appears in the following Collection(s)

Item Statistics