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
> Is there a big suite of tests for Linux?

The userbase for 2.1.x kernels is a lot of it

> Are preconditions and postconditions enablable where they make sense?

No, and for many things it would be hard. There is probably an interesting
project in there somewhere

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

Almost all the core small algorithms in Linux are 'obviously correct'
which means they normally work right 8). Proving bigger stuff is hard
nobody Ive seen has yet really managed to mathemtically describe such
complex interactions, and before that you'd need to prove the compiler
and the CPU and its microcode

Building an optional compiled in set of constraints for entry/exit is
doable, I think the rest becomes rapidly infeasible

Alan


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