5 ms·

I have had the pleasure of visiting AbsInt and hearing talks on, amongst other things, CompCert. It really is a fascinating piece of software. I would highly re

I have had the pleasure of visiting AbsInt and hearing talks on, amongst other things, CompCert. It really is a fascinating piece of software. I would highly recommend looking at the 2016 paper [1] for a bit more detail on how it works. If you're interested you can find other publications as well. The core idea is that every phase of the compiler is proven not to change the behavior of the program. I.e. if you ran any intermediate representation you'd always get the same behavior. The main limitation is, in my opinion, that the C specification isn't available in any form that a proof assistant can consume. Therefore, they had to translate the specification into that form manually. It is possible that this step contains mistakes. On the upside, every C compiler has this problem. [1] https://hal.inria.fr/hal-01238879 https://hal.inria.fr/hal-01238879

moonchild 5y ago
> The main limitation is, in my opinion, that the C specification isn't available in any form that a proof assistant can consume. Therefore, they had to translate the specification into that form manually. It is possible that this step contains mistakes. On the upside, every C compiler has this problem. Most compiler bugs are not in their interpretation of the specification, but in various optimization passes. Compcert's formal verification ensures that all optimizations retain semantics; that alone makes it worth whatever they're charging.
- Cu3PO42 5y ago
  I wholeheartedly agree. I didn't mean to say that the translation of the specification was a big problem, merely that all others are even more insignificant.
  - MaxBarraclough 5y ago
    Also, this has been studied empirically, and CompCert holds up well: • https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf • https://compcert.org/motivations.html https://compcert.org/motivations.html I think things may have improved further since the 2011 paper, where they found bugs in parts of CompCert which were not, at the time at least, formally verified. The formally verified parts of CompCert withstood torture testing admirably.
    - pfdietz 5y ago
      PLDI does a "most influential paper" award each year, for the paper from the PLDI 10 years previous that had the most influence. The 2021 winner was that paper.
- pombalit 5y ago
  >Most compiler bugs are not in their interpretation of the specification, but in various optimization passes. I work on a large, open-source, industrial-grade compiler for a living and I disagree with this statement unless it is specifically referring to C compilers and not compilers for other languages.
  - tluyben2 5y ago
    Which compiler do you work on?
    - throwaway2037 5y ago
      "large, open-source, industrial-grade compiler". No kidding; I thought the same! How many can there really be?
      - tluyben2 5y ago
        Yeah and apparently a secret?
        pombalit 5y ago
        I indeed prefer to avoid doxing myself.
    - pombalit 5y ago
      I work on a GCC frontend, but not the C one.
  - pfdietz 5y ago
    Or are bugs due to interpretations of the specification just easier to find? The point of compiler fuzzing like Csmith was that optimization bugs are really hard to find by the kinds of testing that would find more typical conformance bugs. Before these test generators were written one might have thought that optimization bugs were rare, simply because they hadn't been triggered much.
- Diggsey 5y ago
  Eh, often there is not a clear distinction between the two. Whether an optimization is correct or not depends heavily on the interpretation of very subtle aspects of the specification. For correctness, it is most important that the programmer and the compiler agree on the interpretation of the specification. The good thing here is that there is an unambiguous interpretation which the compiler uses, and that anyone can read. The downside is that most C programmers probably can't understand this machine-readable language, and so will simply refer to the original human-readable specification. What would be quite neat is if they translated the machine-readale specification back into a set of clarifying notes against the original spec.
  - ncmncm 5y ago
    > "On the upside, every C compiler has this problem." Reminds me of the farmer who peeks out of the basement after a big storm, and reports back to his wife: "Good news and bad news. The bad news is, our barn blew down. The good news is, all the neighbors' barns blew down too!"

moonchild 5y ago

> The main limitation is, in my opinion, that the C specification isn't available in any form that a proof assistant can consume. Therefore, they had to translate the specification into that form manually. It is possible that this step contains mistakes. On the upside, every C compiler has this problem. Most compiler bugs are not in their interpretation of the specification, but in various optimization passes. Compcert's formal verification ensures that all optimizations retain semantics; that alone makes it worth whatever they're charging.

Cu3PO42 5y ago
I wholeheartedly agree. I didn't mean to say that the translation of the specification was a big problem, merely that all others are even more insignificant.
- MaxBarraclough 5y ago
  Also, this has been studied empirically, and CompCert holds up well: • https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf • https://compcert.org/motivations.html https://compcert.org/motivations.html I think things may have improved further since the 2011 paper, where they found bugs in parts of CompCert which were not, at the time at least, formally verified. The formally verified parts of CompCert withstood torture testing admirably.
  - pfdietz 5y ago
    PLDI does a "most influential paper" award each year, for the paper from the PLDI 10 years previous that had the most influence. The 2021 winner was that paper.
pombalit 5y ago
>Most compiler bugs are not in their interpretation of the specification, but in various optimization passes. I work on a large, open-source, industrial-grade compiler for a living and I disagree with this statement unless it is specifically referring to C compilers and not compilers for other languages.
- tluyben2 5y ago
  Which compiler do you work on?
  - throwaway2037 5y ago
    "large, open-source, industrial-grade compiler". No kidding; I thought the same! How many can there really be?
    - tluyben2 5y ago
      Yeah and apparently a secret?
      - pombalit 5y ago
        I indeed prefer to avoid doxing myself.
  - pombalit 5y ago
    I work on a GCC frontend, but not the C one.
- pfdietz 5y ago
  Or are bugs due to interpretations of the specification just easier to find? The point of compiler fuzzing like Csmith was that optimization bugs are really hard to find by the kinds of testing that would find more typical conformance bugs. Before these test generators were written one might have thought that optimization bugs were rare, simply because they hadn't been triggered much.
Diggsey 5y ago
Eh, often there is not a clear distinction between the two. Whether an optimization is correct or not depends heavily on the interpretation of very subtle aspects of the specification. For correctness, it is most important that the programmer and the compiler agree on the interpretation of the specification. The good thing here is that there is an unambiguous interpretation which the compiler uses, and that anyone can read. The downside is that most C programmers probably can't understand this machine-readable language, and so will simply refer to the original human-readable specification. What would be quite neat is if they translated the machine-readale specification back into a set of clarifying notes against the original spec.
- ncmncm 5y ago
  > "On the upside, every C compiler has this problem." Reminds me of the farmer who peeks out of the basement after a big storm, and reports back to his wife: "Good news and bad news. The bad news is, our barn blew down. The good news is, all the neighbors' barns blew down too!"