A verification framework suitable for proving large language translations

Li, Liyi

Permalink

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

Description

Title

A verification framework suitable for proving large language translations

Author(s)

Li, Liyi

Issue Date

2020-11-25

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

Gunter, Elsa L

Doctoral Committee Chair(s)

Gunter, Elsa L

Committee Member(s)

• Rosu, Grigore
• Padua, David
• Adve, Vikram
• Zdancewic, Steve

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 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.

Graduation Semester

2020-12

Type of Resource

Thesis

Permalink

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

Copyright and License Information

Copyright 2020 Liyi Li

Owning Collections