On Mon, 17 Aug 2009, Roman Beslik wrote:
Hi. Are there any indications which properties of seL4 are verified?
{{{ Heiser said one of the primary research objectives was to come up with a kernel that would not only be verified but whose performance would be suitable for use in real-life systems.
?My briefing was that we must not *lose more than 10 per cent performance through the verification process*. Right from the start, this was not just an academic exercise but something that was for real-world use.? }}}
I just can't understand how a verification process can undermine performance.
simply by putting constraints on permitted code constructs and thus potentially prevent optimization in some cases - most C verification will require to use only a subset of C (something like C-light) putting constraints on switch statements, goto and the use of pointers.
hofrat