On 2 Mar 2015, at 20:49 , Grissiom <chaos.proton@gmail.com> wrote:

Hi all,

I've heard a formally verified optimizing C compiler: CompCert recently: http://www.absint.com/compcert/ HN: https://news.ycombinator.com/item?id=9130934 .

CompCert has been around for a while, about as long as seL4 in fact.

So what benefit will there be if some one use CompCert as the compiler for seL4?

None for seL4 itself: the kernel is significantly slower when compiled with CompCert. Furthermore, we have an independent proof that our ARM binary is a correct translation of the C source (http://www.ssrg.nicta.com.au/publications/nictaabstracts/Sewell_MK_13.abstract.pml), meaning we don’t have to trust the compiler.

For any user code, CompCert would get you peace of mind re compiler bugs, and it seems that for code that’s less challenging than seL4, the performance of CompCert’s output is quite good.

Gernot

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.