The Coq mailing list

[Chung-Kil Hur <gil.hur AT sf.snu.ac.kr>]

Sorry, I have to fix one thing.

Actually what we did is not a strong induction.

We might be able to call it a strong coinduction.

We will introduce the idea in a future paper.

Best,

Gil

On Sun, Jan 11, 2015 at 2:38 AM, Xavier Leroy <Xavier.Leroy AT inria.fr> wrote:

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