The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Dear Coq-club,

There are some updates.

(1) Our proof of separate compilation for CompCert is simplified a lot and thus can be understood much easily.

      Now the whole development is less than 4K LOC.

(2) The github repository address is changed to:

      https://github.com/snu-sf/CompCert/tree/sepcomp

If you want to see more details, please visit our website:

http://sf.snu.ac.kr/compcertsep

Best regards,
Jeehoon Kang and Chung-Kil Hur,
Seoul National University

On Sun, Jan 11, 2015 at 4:27 AM, Chung-Kil Hur <gil.hur AT sf.snu.ac.kr> wrote:

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