lkml.org 
[lkml]   [1998]   [Jun]   [22]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
From
SubjectRe: RT cache management
Date
"A month of sundays ago Mathieu Bouchard wrote:"
>
> > Transparency: If cryptographic reliability only comes from peer review, I
> > suggest that safety has the same characteristics.
> > Robustness: Crash proof
>
> Is there a big suite of tests for Linux?

No. Some informal ones are being collected. But no. In particular there
are no regression tests, which would seem to me to be of most immediate
utility. And no, nobody bothers to test the new kernels _before_
putting them out. They are development releases. Putting them out
constitutes the test!

> Are preconditions and postconditions enablable where they make sense?

No. When I do go through code I attempt to add these. In my opinion the
_networking code_ especially would benefit from this. It isa maze of
counters. There are assumptions everywhere that are known only to the
authors.

> Could we do mathematical proofs of algorithms used in Linux, especially
> the really critical ones?

There aren't any (critical ones). All of them "fail" in some way or
other, and it doesn't matter. That's a result of the development
style.

> Is there such a thing as a code analyzer that would prove that a
> C-function "foo" does the job "bar" that is asked?

C? Well, that's the hard part. C pointers. I believe there is such a
tool somewhere in the states but I haven't interested myself in it.
Basically, one shouldn't write in C if you want to verify your code.
And anyway, we can pass hidden data through the mobo itself, so why
bother ...

> Could a program scan the source and make a proof that for every valid
> input to the function "foo" the postcondition "bar" will be satisfied?

In general, no. But obviously I can sometimes do that. For example,
I can easily prove for a function that doesn't make calls to another
and which doesn't touch an input pointer, and which satisfies other
requirements, that on output the contents of the pointer will be
unchanged (in a single threaded environment).

> including assume() macros in the kernel could perform a empirical
> verification of the validity. There would be a kernel compile-option to
> enable them (they would normally compile to null statements, for speed).

I think assert() statements woould be very useful. I urge developers to
put them in. #define assert(x) .

> But many rare exceptions would be missed -- and that's what a code
> analyzer would be for.
>
> If the code analyzer thing doesn't exist, it's maybe too complex to exist.
> If we'd rewrite the whole kernel in ML or Haskell, it would be easier to
> prove its validity :-) hopefully the kernel isn't written in C++... but

But you couldn't. Just extracting the functionality of the kernel codes
is very difficult for me.

> anytime, side effects don't help the problem.

That's not the real problem. Pointer arithmetic is probably the
bugbear, that and the mobo and assumptions on the environment which
aren't actually known explicitly to anybody.

> An intermediate idea is to test pre/post conditions of functions outside
> of their context. but if there are several side-effects, or situations
> that are difficult to reconstruct outside of a living kernel, this might
> be a nightmare, and just plain old torture-tests might do the job better.
>
> comments?

As above.

> matju
>


Peter ptb@it.uc3m.es

-
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.rutgers.edu

\
 
 \ /
  Last update: 2005-03-22 13:43    [W:1.103 / U:0.532 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site