Re: Formal description of system call interface

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