Are they generated automatically from Haskell code?

On Tue, Jan 27, 2015 at 3:31 PM, Gerwin Klein Gerwin.Klein@nicta.com.au wrote:

Hi David,

these comments are supposed to document that the assertion or condition corresponds to a 'fail' statement on the design level that we will have to prove does not occur.

Cheers, Gerwin

...

On 28.01.2015, at 00:38, David Greve david.greve@rockwellcollins.com

wrote:

...

What is the significance of the various "Haskell error:" comments

found throughout the kernel code?

...

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

---

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.

Let me expand on a couple of these points. There's a bit of history.

The C version of the kernel was originally written by rapidly transcribing the Haskell prototype into C. A number of comments persist in the C source which explain the relationship to the Haskell source, or which refer to the documentation available in the Haskell prototype.

For instance, sendAsyncIPC in C ( https://github.com/seL4/seL4/blob/master/src/object/asyncendpoint.c ) was written by transcribing sendAsyncIPC from Haskell ( https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Object/AsyncEndpoi... )

The line-to-line conversion is pretty obvious.

The comment about "WaitingAEP AEP must have non-empty queue" references the matching fail line in the Haskell sources. This is significant because we had, by that stage, proven that the Haskell specification executed without any of the errors/failures occuring, so these failures were actually a golden reference for what should and should not happen.

Someting to clarify: Gerwin claims that the assertions will be proven. He means the *Haskell* assertions. We don't prove anything about the C assertions, which are stripped out by the C preprocessor in the verification target. We did discover once, after verification, that one of the C assertions was wrongly transcribed from its Haskell counterpart, so the debug build of the kernel could panic in a situation where nothing was actually wrong.

On a related note, you asked earlier whether the halt () semantics are baked into the proofs. The C-parser doesn't assign any special meaning to halt () as opposed to any other hidden function. However the C-parser outputs are currently plumbed through a conversion in a theory called Substitute ( https://github.com/seL4/l4v/blob/master/spec/cspec/Substitute.thy ) which happens to wrap calls to the halt procedure in "DontReach" assertions. So we do directly prove that the halt/fail calls that remain in the kernel after preprocessing aren't reached. Gerwin doesn't know about this, because I added this conversion recently and it didn't change any of the proofs.

The substituted definitions are proven to be an anti-refinement of the C-parser's definitions in the theory CToCRefine ( https://github.com/seL4/l4v/blob/master/lib/clib/CToCRefine.thy ) which seems to have ended up in an odd place.

Well, that's probably more details than you ever wanted to know.

Cheers, Thomas.

On 28/01/15 08:45, Gerwin Klein wrote:

No, they’re manually written, so the comments themselves may be wrong or out of date. The assertions will still be proved, though.

Cheers, Gerwin

...

On 28.01.2015, at 08:37, David Greve <david.greve@rockwellcollins.com mailto:david.greve@rockwellcollins.com> wrote:

Are they generated automatically from Haskell code?

On Tue, Jan 27, 2015 at 3:31 PM, Gerwin Klein <Gerwin.Klein@nicta.com.au mailto:Gerwin.Klein@nicta.com.au> wrote:

Hi David,

these comments are supposed to document that the assertion or
condition corresponds to a ‘fail’ statement on the design level
that we will have to prove does not occur.

Cheers,
Gerwin

> On 28.01.2015, at 00:38, David Greve
<david.greve@rockwellcollins.com
<mailto:david.greve@rockwellcollins.com>> wrote:
>
>
>   What is the significance of the various "Haskell error:"
comments found throughout the kernel code?
>
> _______________________________________________
> Devel mailing list
> Devel@sel4.systems <mailto:Devel@sel4.systems>
> https://sel4.systems/lists/listinfo/devel


________________________________

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.

---

Devel mailing list Devel@sel4.systems mailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Glad to clear that up.

Thanks to Tom for raising that point: C "assert" is indeed stripped in the preprocessing phase for the production kernel, but "halt" isn't. It's the design-level (Haskell) assertions we prove don't fail.

Cheers, Gerwin

On 28.01.2015, at 2:29 pm, David Greve david.greve@rockwellcollins.com wrote:

On Tue, Jan 27, 2015 at 5:43 PM, Thomas Sewell thomas.sewell@nicta.com.au wrote:

...

There's a bit of history.

There always is ..

...

We did discover once, after verification, that one of the C assertions was wrongly transcribed from its Haskell counterpart, so the debug build of the kernel could panic in a situation where nothing was actually wrong.

That is an interesting story.

...

Well, that's probably more details than you ever wanted to know.

Actually, this is precisely why I asked.

Thanks, Dave

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

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.