Re: Formal description of system call interface

[Cyril Hrubis <chrubis-AlSwsSmVLrQ@public.gmane.org>]

Hi!
> Description of "returns fd or this set of errors" looks simple and useful.
> Any test system or fuzzer will be able to verify that kernel actually returns
> claimed return values. Also Carlos expressed interested in errno values
> in the context of glibc.
> I would do it from day one.
> 
> Re more complex side effects. I always feared that a description suitable
> for automatic verification (i.e. zero false positives, otherwise it is useless)
> may be too difficult to achieve.

I'm afraid it may be as well. I would expect that we will end up with
something quite complex with a large set of exceptions from the rules.

> Cyril, Tavis, can you come up with some set of predicates that can be
> checked automatically yet still useful?
> We can start small, e.g. "must not alter virtual address space".

I will try to thing about this a bit.

-- 
Cyril Hrubis
chrubis-AlSwsSmVLrQ@public.gmane.org