On a related note - I think formally verified R4 is great idea but you've
got to be
aware that as long as it's running on top of unverified Linux kernel we
can only
assure that some properties hold under the assumption that kernel actually
does the
right thing. Not sure how practically viable it is outside of general
academic curiosity.
True enough. The SeL4 verification apparently took on the order of a few
manyears, and we don't have that. I do think, however, there's likely to be
value in incomplete efforts. I personally know that I've had bugs in my code
that I've spent a couple of days trying to iron out, only to find that when
I stop and write out hoare triples for each of the statements in the code I
find the issue in about ten minutes.
We can start with a highly abstract model and gradually introduce more
details while establishing that each more detailed model doesn't invalidate
proofs made on more general ones. Having a proven yet highly abstract model
to informally compare the actual source to would make debugging quite a bit
easier, I think, and we could gradually build on it to reduce the semantic
"distance" between the model and the kernel code.
--
DH
--
To unsubscribe from this list: send the line "unsubscribe reiserfs-devel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
