lkml.org 
[lkml]   [1998]   [Jun]   [22]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: RT cache management
> 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?
Are preconditions and postconditions enablable where they make sense?

Could we do mathematical proofs of algorithms used in Linux, especially
the really critical ones?
Is there such a thing as a code analyzer that would prove that a
C-function "foo" does the job "bar" that is asked?
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?

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).
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
anytime, side effects don't help the problem.

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?

matju


-
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:0.070 / U:0.628 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site