Messages in this thread | | | Date | Mon, 22 Jun 1998 01:53:24 -0400 (EDT) | From | Mathieu Bouchard <> | Subject | Re: 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
| |