Language-parametric compiler validation with application to LLVM

Theodoros Kasampalis, Daejun Park, Zhengyao Lin, Vikram S. Adve, Grigore Rosu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We propose a new design for a Translation Validation (TV) system geared towards practical use with modern optimizing compilers, such as LLVM. Unlike existing TV systems, which are custom-tailored for a particular sequence of transformations and a specific, common language for input and output programs, our design clearly separates the transformation-specific components from the rest of the system, and generalizes the transformation-independent components. Specifically, we present Keq, the first program equivalence checker that is parametric to the input and output language semantics and has no dependence on the transformation between the input and output programs. The Keq algorithm is based on a rigorous formalization, namely cut-bisimulation, and is proven correct. We have prototyped a TV system for the Instruction Selection pass of LLVM, being able to automatically prove equivalence for translations from LLVM IR to the MachineIR used in compiling to x86-64. This transformation uses different input and output languages, and as such has not been previously addressed by the state of the art. An experimental evaluation shows that Keq successfully proves correct the translation of over 90% of 4732 supported functions in GCC from SPEC 2006.

Original languageEnglish (US)
Title of host publicationProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2021
PublisherAssociation for Computing Machinery
Pages1004-1019
Number of pages16
ISBN (Electronic)9781450383172
DOIs
StatePublished - Apr 19 2021
Event26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2021 - Virtual, Online, United States
Duration: Apr 19 2021Apr 23 2021

Publication series

NameInternational Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS

Conference

Conference26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2021
Country/TerritoryUnited States
CityVirtual, Online
Period4/19/214/23/21

Keywords

  • Compilers
  • Program Equivalence
  • Simulation
  • Translation Validation

ASJC Scopus subject areas

  • Software
  • Information Systems
  • Hardware and Architecture

Fingerprint

Dive into the research topics of 'Language-parametric compiler validation with application to LLVM'. Together they form a unique fingerprint.

Cite this