Skip to content

Instantly share code, notes, and snippets.

@jeehoonkang

jeehoonkang/README.md

Last active November 7, 2015 20:09
Show Gist options
  • Save jeehoonkang/0f2da2d6e2a70e38de46 to your computer and use it in GitHub Desktop.
Save jeehoonkang/0f2da2d6e2a70e38de46 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
README.md

Lightweight Verification of Separate Compilation

Jeehoon Kang*, Yoonseung Kim*, Chung-Kil Hur*, Derek Dreyer**, Viktor Vafeiadis**

* Seoul National University & ** MPI-SWS

This is the artifact for the POPL 2016 paper: "Lightweight Verification of Separate Compilation".

Downloads

Paper Abstract

Major compiler verification efforts, such as the CompCert project, have traditionally simplified the verification problem by restricting attention to the correctness of whole-program compilation, leaving open the question of how to verify the correctness of separate compilation. Recently, a number of sophisticated techniques have been proposed for proving more flexible, compositional notions of compiler correctness, but these approaches tend to be quite heavyweight compared to the simple "closed simulations" used in verifying whole-program compilation. Applying such techniques to a compiler like CompCert, as Stewart et.al. have done, involves major changes and extensions to its original verification.

In this paper, we show that if we aim somewhat lower --- to prove correctness of separate compilation, but only for a single compiler --- we can drastically simplify the proof effort. Toward this end, we develop several lightweight techniques that recast the compositional verification problem in terms of whole-program compilation, thereby enabling us to largely reuse the closed-simulation proofs from existing compiler verifications. We demonstrate the effectiveness of these techniques by applying them to CompCert 2.4, converting its verification of whole-program compilation into a verification of separate compilation in less than two person-months. This conversion only required a small number of changes to the original proofs, and uncovered two compiler bugs along the way. The result is SepCompCert, the first verification of separate compilation for the full CompCert compiler.

During the proof, we found two bugs in CompCert 2.4. Bug #1 is due to an analysis that is invalidated in the presence of linking and Bug #2 is due to an invalid axiom assumed. We reported these bugs and they are now fixed in CompCert 2.5.

Virtual Machine

  • ID / Password: artifact / artifact, root / artifact

  • All contents are in /home/artifact/Desktop/SepCompCert-2.4.

Contents

  • CompCert2.4/: CompCert 2.4 with the following four patches applied:

  • levelA/: Level A compositional verification of CompCert (§2.2, §4.1, and §5).

    • The main theorem is driver/Linkerproof.v's linker_correct: if the C programs in ctree are linked into cprog, and the C programs in ctree are separately compiled into the ASM programs in asmtree, then there exists an ASM program asmprog such that asmtree is linked into asmprog and asmprog simulates cprog.

    • The main theorem is equivalent to the claim in the paper.

      • In the paper, we claim that (§2.2):

        For Level A, we aim to show that if we separately
compile n different C modules (s1.c, ... , sn.c) using
the same exact verified compiler C, producing n assembly
modules (t1.asm, ... , tn.asm), then the assembly-level
linking of the ti’s will refine the C-level linking of
the si’s."

        Note that we did not specify the order of the linkings among multiple modules.

      • In the development, we define only the linking of two modules, and used a tree data structure to specify the order of the linkings. For example, the following tree represents (m1 ◦ m2) ◦ m3:

            ◦
   / \
  ◦  m3
 / \
m1 m2

        Basically, the main theorem in the development proves the level A correctness, regardless of the order of the linkings.

  • levelB/: Level B compositional verification of CompCert (§2.3, §4.2).

    • The main theorem is driver/Linkerproof.v's linker_correct_optd: similar to the level A correctness main theorem, but the C programs in ctree are separately compiled with possibly different optimization flags into the ASM programs in asmtree.

    • The main theorem is equivalent to the claim in the paper, similarly to the level A correctness.

  • count_locs.py, results.table.tex: Changes to lines of code when porting CompCert to SepCompCert LevelA and LevelB (§6, Fig. 10)

    • count_locs.py is a script that counts differences between CompCert2.4/ and level?/. The table in the paper (results.table.tex) is automatically generated from this script.

    • We classify the changed lines into three categories: removed lines from the original CompCert 2.4 (Rm), added lines in our development which are derived from the original CompCert 2.4 (AddD), and added lines which are newly introduced in our development (AddN).

    • We classify the changed lines by the Unix diff tool. To further classify the added lines into two categories (AddD & AddN), we used the following criteria:

      • Added lines in the existing files are regarded as derived (AddD), except for those lines that begin with "(* new *)". Those lines are regarded as new (AddN).

      • Added lines in the newly created files are regarded as new (AddN), except for those lines that begin with "(* derived *)". Those lines are regarded as derived (AddD).

        The only file that contains "(* derived *)" is levelB/backend/RTLExtra.v. The contents are derived from the proofs of RTL optimizations, such as CSEproof.v or Inliningproof.v.

Build

  • We succeeded in compiling CompCert2.4/, levelA/, and levelB/ directories with Coq 8.4pl5 for all Linux targets. You can reproduce it in the virtual machine with the following commands:

    • ./configure arm-linux; make depend; make
    • ./configure ia32-linux; make depend; make
    • ./configure ppc-linux; make depend; make

    In the virtual machine, you can run build.sh to build all architecture (arm, ia32, ppc) & directory (CompCert2.4/, levelA/, levelB/) combinations.

    We also succeeded in compiling our development in MAC OS X with:

    • ./configure ia32-macosx; make depend; make

  • We recommend reviewers to use graphical diff tools, such as meld, for browsing our development. Meld is installed in the virtual machine.

Minor Technical Notes

  • There are some files with a .vp extension, which are turned by CompCert's preprocessor into generated .v files. We have not touched these files, but in any case count the lines of code in the original .vp files, not the generated .v files.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment