DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2020.7

K-LLVM: A Relatively Complete Semantics of LLVM IR

Authors: Liyi Li and Elsa L. Gunter

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract

LLVM [Lattner and Adve, 2004] is designed for the compile-time, link-time and run-time optimization of programs written in various programming languages. The language supported by LLVM targeted by modern compilers is LLVM IR [llvm.org, 2018]. In this paper we define K-LLVM, a reference semantics for LLVM IR. To the best of our knowledge, K-LLVM is the most complete formal LLVM IR semantics to date, including all LLVM IR instructions, intrinsic functions in the LLVM documentation and Standard-C library functions that are necessary to execute many LLVM IR programs. Additionally, K-LLVM formulates an abstract machine that executes all LLVM IR instructions. The machine allows to describe our formal semantics in terms of simulating a conceptual virtual machine that runs LLVM IR programs, including non-deterministic programs. Even though the K-LLVM memory model in this paper is assumed to be a sequentially consistent memory model and does not include all LLVM concurrency memory behaviors, the design of K-LLVM’s data layout allows the K-LLVM abstract machine to execute some LLVM IR programs that previous semantics did not cover, such as the full range of LLVM IR behaviors for the interaction among LLVM IR casting, pointer arithmetic, memory operations and some memory flags (e.g. readonly) of function headers. Additionally, the memory model is modularized in a manner that supports investigating other memory models. To validate K-LLVM, we have implemented it in 𝕂 [Roşu, 2016], which generated an interpreter for LLVM IR. Using this, we ran tests including 1,385 unit test programs and around 3,000 concrete LLVM IR programs, and K-LLVM passed all of them.

Cite as

Liyi Li and Elsa L. Gunter. K-LLVM: A Relatively Complete Semantics of LLVM IR. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 7:1-7:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ECOOP.2020.7,
  author =	{Li, Liyi and Gunter, Elsa L.},
  title =	{{K-LLVM: A Relatively Complete Semantics of LLVM IR}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{7:1--7:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.7},
  URN =		{urn:nbn:de:0030-drops-131649},
  doi =		{10.4230/LIPIcs.ECOOP.2020.7},
  annote =	{Keywords: LLVM, formal semantics, K framework, memory model, abstract machine}
}

Document

DOI: 10.4230/OASIcs.WPTE.2014.15

Verifying Optimizations for Concurrent Programs

Authors: William Mansky and Elsa L. Gunter

Published in: OASIcs, Volume 40, First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (2014)

Abstract

While program correctness for compiled languages depends fundamentally on compiler correctness, compiler optimizations are not usually formally verified due to the effort involved, particularly in the presence of concurrency. In this paper, we present a framework for stating and reasoning about compiler optimizations and transformations on programs in the presence of relaxed memory models. The core of the framework is the PTRANS specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. We demonstrate our technique by verifying the correctness of a redundant store elimination optimization in a simple LLVM-like intermediate language, relying on a theorem that allows us to lift single-thread simulation relations to simulations on multithreaded programs.

Cite as

William Mansky and Elsa L. Gunter. Verifying Optimizations for Concurrent Programs. In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 15-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{mansky_et_al:OASIcs.WPTE.2014.15,
  author =	{Mansky, William and Gunter, Elsa L.},
  title =	{{Verifying Optimizations for Concurrent Programs}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{15--26},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Schmidt-Schau{\ss}, Manfred and Sakai, Masahiko and Sabel, David and Chiba, Yuki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2014.15},
  URN =		{urn:nbn:de:0030-drops-45869},
  doi =		{10.4230/OASIcs.WPTE.2014.15},
  annote =	{Keywords: optimizing compilers, interactive theorem proving, program transformations, temporal logic, relaxed memory models}
}

Search Results

Documents authored by Gunter, Elsa L.

K-LLVM: A Relatively Complete Semantics of LLVM IR

Abstract

Cite as

Verifying Optimizations for Concurrent Programs

Abstract

Cite as

Thanks for your feedback!

Could not send message