{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/109386"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/109386","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"A verification framework suitable for proving large language translations","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Li, Liyi"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Gunter, Elsa L","Rosu, Grigore","Padua, David","Adve, Vikram","Zdancewic, Steve"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2021,"date_issued":"2021-03-05T21:38:05Z","date_published":"2021-03-05T21:38:05Z","updated_at":"2026-07-22T22:24:50Z","subjects":["Compiler Verification","Language Semantics","K","Rewriting Logic","LLVM","Memory Model","Simulation Relation","Concurrency Model"],"languages":["en"],"rights":["Copyright 2020 Liyi Li"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/109386","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Gunter, Elsa L","Rosu, Grigore","Padua, David","Adve, Vikram","Zdancewic, Steve"]},{"key":"dc:creator","label":"Author","values":["Li, Liyi"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2021-03-05T21:38:05Z","2020-11-25","2020-12"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Compiler Verification","Language Semantics","K","Rewriting Logic","LLVM","Memory Model","Simulation Relation","Concurrency Model"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2020 Liyi Li"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/109386"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2021-03-04 without embargo terms","The student, Liyi Li, accepted the attached license on 2020-11-24 at 18:15.","The student, Liyi Li, submitted this Dissertation for approval on 2020-11-24 at 18:17.","This Dissertation was approved for publication on 2020-11-25 at 14:14.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15957 on 2021-03-04 at 15:35:04","Made available in DSpace on 2021-03-05T21:38:05Z (GMT). No. of bitstreams: 3 LI-DISSERTATION-2020.pdf: 2268749 bytes, checksum: d193de02c870e41afa2485b4ecb35972 (MD5) LICENSE.txt: 4204 bytes, checksum: 56228438826d3e9ba5d30e1924e879f2 (MD5) PROQUEST_LICENSE.txt: 4550 bytes, checksum: 42a2bd50efb7f6b80897d32a3d1e7ed3 (MD5) Previous issue date: 2020-11-25"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["A verification framework suitable for proving large language translations"]}]}],"canonical_facts":{"dc:contributor":["Gunter, Elsa L","Rosu, Grigore","Padua, David","Adve, Vikram","Zdancewic, Steve"],"dc:creator":["Li, Liyi"],"dc:date":["2021-03-05T21:38:05Z","2020-11-25","2020-12"],"dc:description":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2021-03-04 without embargo terms","The student, Liyi Li, accepted the attached license on 2020-11-24 at 18:15.","The student, Liyi Li, submitted this Dissertation for approval on 2020-11-24 at 18:17.","This Dissertation was approved for publication on 2020-11-25 at 14:14.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15957 on 2021-03-04 at 15:35:04","Made available in DSpace on 2021-03-05T21:38:05Z (GMT). No. of bitstreams: 3 LI-DISSERTATION-2020.pdf: 2268749 bytes, checksum: d193de02c870e41afa2485b4ecb35972 (MD5) LICENSE.txt: 4204 bytes, checksum: 56228438826d3e9ba5d30e1924e879f2 (MD5) PROQUEST_LICENSE.txt: 4550 bytes, checksum: 42a2bd50efb7f6b80897d32a3d1e7ed3 (MD5) Previous issue date: 2020-11-25"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/109386"],"dc:language":["en"],"dc:rights":["Copyright 2020 Liyi Li"],"dc:subject":["Compiler Verification","Language Semantics","K","Rewriting Logic","LLVM","Memory Model","Simulation Relation","Concurrency Model"],"dc:title":["A verification framework suitable for proving large language translations"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:50Z"}