The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 10/01/15 16:26, Chung-Kil Hur wrote:
> We are happy to announce that we completed the correctness proof of
> separate compilation of CompCert 2.4.

That's certainly interesting, to put it mildly!

> Our proof is essentially based on a strong induction.

Can you suggest a paper that introduces the basics of the approach?

> During the proof, we found two bugs in CompCert 2.4. One is due to an
> invalid axiom assumed and the other is due to an analysis that is
> invalidated in the presence of linking. We think this shows why we
> should verify separate compilation though linking seems so simple.

Indeed, it's been known for a while that the addition of concurrency
(threads) invalidates many classic optimizations, but I wasn't
expecting that separate compilation and linking could invalidate
simple optimizations like CompCert's.

> These bugs are reported to Xavier Leroy and the second bug is fixed in
> the CompCert repository. We are currently waiting for the first bug to
> be fixed.

It's coming, just be patient :-)

- Xavier Leroy