A verification framework suitable for proving large language translations

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2021

Author dc:creator

• Li, Liyi

Contributors dc:contributor

• Gunter, Elsa L
• Rosu, Grigore
• Padua, David
• Adve, Vikram
• Zdancewic, Steve

• Compiler Verification
• Language Semantics
• K
• Rewriting Logic
• LLVM
• Memory Model
• Simulation Relation
• Concurrency Model

Statement dc:rights

• Copyright 2020 Liyi Li

Language dc:language

en

Handle dc:identifier

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

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/109386