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/AsyncEndpoint.lhs
)
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 <[email protected]
<mailto:[email protected]>> wrote:
Are they generated automatically from Haskell code?
On Tue, Jan 27, 2015 at 3:31 PM, Gerwin Klein
<[email protected] <mailto:[email protected]>> 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
<[email protected]
<mailto:[email protected]>> wrote:
>
>
> What is the significance of the various "Haskell error:"
comments found throughout the kernel code?
>
> _______________________________________________
> Devel mailing list
> [email protected] <mailto:[email protected]>
> 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
[email protected] <mailto:[email protected]>
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
