Messages in this thread | | | From | (David Monniaux) | Date | Tue, 8 Jun 1999 21:21:58 +0200 (MET DST) | Subject | Re: is Linux obsolete? |
| |
AmigaDOS, or at least its early incarnations that ran on A500, A1000's, didn't implement memory protection. This of course reduces overhead considerably when it comes to layer separations. No expensive copies; no context switching...
I have not yet heard of any efficient way to handle memory protection between layers. If somebody is aware of something neat in this area, please let me know.
As for kernel safety through type safety: indeed type safety as in traditional languages can catch lots of errors - my experience is that developing in Caml (http://caml.inria.fr) is much more pleasant than in C, especially when it comes to bugs. However, usually stronger invariants than mere elementary type safety are required; a ML-like type system can't encompass notions like "a and b are lists and the sum of their lengths is the product of c and d". You can do that using more elaborate type systems (see Coq, http://coq.inria.fr); this amounts to providing a proof of safety with the code (see the works on proof-carrying code, for instance George Necula's). This is still highly experimental, since the programming hassles and the experience required for such safe programming exceed what is bearable by the general industry (the situation is different for critical embedded systems).
This is beginning to be quite out-of-topic for the Linux-kernel list, since it's more of a general discussion on OS and language designs...
-- David
- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.tux.org/lkml/
| |