It is definitely not as complete or mature as Linux or BSD yet, but it clearly demonstrates that implementing a reliable, self-healing, multiserver UNIX clone in user space based on a small, easy-to-understand microkernel is doable. Don't confuse lack of maturity (we've only been at it for a bit over a year with three people) with issues relating to microkernels.
Interesting, that statement. "Self-healing".... he pushes drivers out to userland and restarts them when they bugger up.
I remember years ago (newbie), writing a daemon that kept crashing - massive memory leaks somewhere. Not feeling particularly energetic, I hit upon the idea of sticking it in/etc/inittab so that the system would restart it.
Anybody here want to guess just how many people shit on me for doing that? "If you have to rely on inittab to restart your programme, FIX IT! IT'S BROKEN! YOU'RE USING A CRUTCH!" etc etc etc.
Maybe it's just me, but unless T is talking about examining the offending carcass, rewriteing the code (self-modifying code? *gasp*) and then resurrecting the thing, isn't he talking about basically the same thing?
you forgot one of the other things about 24-7 environments..... even a 3% performance penalty doesn't stack up very well if that means you have to spend a couple of hundred thou to upgrade your servers to handle the load, when they'd be good to go for another 2 years if they *didn't* have that extra 3% sucked out of them for the sace of a bit design purity.
Not true. The Mythbusters proved quite convincingly that if you want to shoot somebody who is at least 18 inches under water, you're not going to be able to do it with ANY high-powered modern weapon - the speed of the projectile is so great that it shatters on contact with the water.
The only way to get a kill is to use something with a much lower muzzle velocity, and higher round mass....... like a musket.
You'd be surprised how much you might need that precision. I have a small network here at home..... my source files are based on my server, and I work with them (mounted via nfs) under unix on one machine, and under windows (mounted via smb) on another.
RCS/CVS/make et all can get SERIOUSLY screwed up if the timestamps are off by even a second.
In the 80's, many of the folks in the current Bush Administration were defending right-wing, paramilitary death squads in Latin America.
And who were they defending them from? The people who were supporting left-wing, paramilitary death squads in Latin America.
I hate these dem/rep pissing matches you see so often on here. Republicans are nor more good, evil, closeminded, bigoted, rich, poor, smart or stupid than Democrats.... and the only think I can see, given the frequency that those "accusations" are thrown about here, is that the only people who take part in these discussions are the worst of both sides.
Anybody come up with an American political equivalent of Godwin? I want to invoke somebody's ass
You're absolutly right.... but there's only one, tiny, little problem with it.
Traffic analysis is normally differential - that is, you establish a "normal" pattern, for "normal" behaviour. Any changes in that pattern then tells you that something unusual is happening - different changes signifying different things, etc.
You have somebody (a reporter) who's job it is to talk to government officials and politicos of all stripes in the NORMAL course of doing his job. So just how, pray tell, is knowing that said reporter talked to official XXX going to give you any clues as to who might be leaking what?
Unless the reporter/leak are stupid enough to talk to each other at 3AM when both are normally in bed (a break in the pattern), there's not going to be anything to be found. Certainly not by traffic analysis, anyway.
That is one of the things that DOES make him a "typical" user. Most users outside *don't* want to play with the computer - they want to do stuff. And if they can't "do stuff" easily, without having to think, they just won't bother.
THAT is why Windows is so successfull. It doesn't matter how crappy the O/S is on technical grounds, or how buggy it and the other software is.
Put the CD in, click on a few buttons, and you can "do stuff".
Neither Linux, nor any other O/S, has any chance in hell of being a general windows replacement unless they become just as well packaged.
Remember, folks - Microsoft has not, and never will be, a technology company. Bill Gates has not, and never will be, a geek - he's just an incredibly accomplished marketeer with funny looking glasses.
What microsoft does well is market and package. And that really DOES count.
What does that mean? What do you find so offensive about proportinal representation?
Proprotional representations guarentees that you will have a minority situation and require coalitions. What that means is that regardless of how close you are to a majority - say, 49% - you're still going to have to deal with the fring, specialinterest parties to get yourself over the hump to that magic 51% so you can pass legeslation.
The occasional minority government helps keep the parties honest.... but having a system that will give you (in practice) a minority every time, it's a recipie for disaster.
In order to get there you will need to defeat dozens of incumbents. Considering that their re-election rate is higher then the house of lords in England I'd say you are dreaming.
No, you don't - all you need is one. Case in point: In one Newfoundland provincial election back in the mid-70's. Tories - 49 seats. Liberals - 49 seats. New Labrador Party - 3. The government lasted only about 6/8 months, if I recall correctly, before we had another election.... but in that 6 or 8 months, the ONLY legislation that was passed dealt with Labrador's concerns. (Labrador is that part of Newfoundland which is on the mainland of North America, on Canada's east coast).
If you want to work for change work to get rid of winner take all. Work to institute a better way of voting
Personally, I think the first-past-the-post system that you currently have *is* the best system...... unless you only have two parties. That's what leads you to an "us vs them" situation that you have now. If you had at least one other party, both the Republicans and the Democrats would be doing things to try to woo voters away from that party, as well, which would tend to lead to more moderate positions for ALL parties, instead of giving you a choice between one extreme or another.
Yes to #1 - absolutly no to #2. And I also never said anything about proportional representation, which as far as I'm concerned is just an institutional method for letting the tail wag the dog.
All you need to have a minority house, or senate, is to have a 3rd (or 4th) party hold the balance of power - that is, no one party be able to have 50% of the body without support of at least one other party.
It has it's drawbacks - Italy, for example, which is an extreme case but in Canada, minority parliaments have been some of the most positive and productive in history.
Would this be a good time to point out that just before the Soviet Union coopted the Cominterm, Marx himself that that communism was IMPOSSIBLE in Russia, because communism presupposed a surplus of supply for all things, because of the industrial state, before the conditions would exist to allow the state to "wither away"? The Soviet Union - and to a lesser extent, it's still true of Russia today - was still more of a feudal than an industrial society.
People here constantly preface their posts with IANAL...... I wish the hell people would also start using IANAPS
THANK you - that was one of the few informative posts in this entire thread. Somebody mod parent up.
Here in Canada, in a case like this, the judge has the power to require the state to disclose the information to HIM, so he can rule on the validity of the secret status of whatever the hell it is.
It's implied in your post that that's not the case in the states - is that true?
It would not work. We don't have a parliment like the rest of the world. We have a winner take all system so there is no reason to form coalition governments.
WOW...... that's one hellova statement.
There is a big difference between having more than 2 parties and being the biggest, baddest Italy on the block.
It would be nice to occasionally hear one of you folk say something occasionally that indicated that at least *some* political systems in the world might have features in their favour inspite of the fact that they wern't the american system.
And maybe - just *maybe* - the occasional minority/coalition governemt might keep your two parties honest enough that you wouldn't HAVE crap like this happening.
Maybe I'm just being silly, but I always assumed that a lot of the NSA budget in the past was consumed by having to deal with things like the cold war.
I'm sorry, folks - but this is what you get when you try to apply technology inapproriatly.
KISS - remember that? KEEP IT SIMPLE, STUPID
What you're doing with ANy form of electronic voting machine in unnecessarily complicating the entire process. Why the hell don't you just give out paper ballots, mark them, and count them - they way they do everywhere else in the world?
I grew up in a mining town in Labrador.... United Steelworkers of America.
They have some really, really, REALLY big trucks up there - the suckers will all 240 tonns of dirt in a single load.
My first memory of unions? One of those truckdrivers being fired for drinking on the job (caught with the flask to his lips in the cab)..... and the resulting wildcat strike untill he was hired back beause he was the prez's buddy.
THREE TIMES
And as far as the mean, evil PHBs sending the jobs to Indea to save 5 bucks.... how many jobs will they shift - and how QUICKLY..... if wages go up overnight, regardless of merit, by 30% because of the coercive power of a union?
Thanks - I'll pass. Unions are the last refuge of the incompotent and lazy.
Yes, it was - but the shutdown system had nothing to do with a microkernel. As a matter of fact, it essentially didn't *have* an operating system at all. (Don't go there, folks - I know that that's not strictly true). And you don't want me to tell you how it was structured, either - it was the must #@($*&#@ up piece of code I have ever seen in my life. Absolutly unmaintainable.... but it was proven to be correct.
Let me restate the point I was trying to make with my original post.
Tannenbaum says micro good, mono bad. This is based on the design elegance and simplicity of the microkernel architecture. If that was the ONLY criteria for judging the worth of an operating system, I would agree with him. But it's not.
This is where the shutdown system came in, by way of example.
Parnas's notation enabled us to prove that the system was mathamatically correct, but still didn't tell us if the system would do the job, because it ignoreed the time domain - the constraints the shutdown system had to work under.
My point was that Tannenbaum is doing the same thing - he's ignoring OTHER criteria that are important for an operating system - mainly, performance, and the ability to handle the workload.
The difference between the two systems is that Parnas' notation didn't *claim* to prove suitability for the task - just that the programme was mathamatically correct. Parnas didn't ignore the timing constraints the shutdown system had to operate under - he simply didn't address that particular constraint, and left it for other methods. Tannenbaum, on the other hand, is trying to pretend that those other constraints just simply don't exist.
Yes, it has been in interesting thread, and I've enjoyed it... but my intention was to use it to illustrate a point, not to be a topic in and of itself.
Regarding being able to prove that Linux was correct - I don't think it would be that difficult. Don't get me wrong - it would take a VERY long time, and would make even the most ardent techie's head explode from the effort. But the notation Dr Parnas developed that we used was designed to "roll up".... once you had proved the correctness of one particular routine, you didn't refer to the resulting 6 or 10 or 15 lines of proof again - you simply plugged in the top most line - the one that proved the correctness of that particular routine - into the calling routine.. lower-level proofs just dropped off the bottom, so to speak.
This was also what - 20 years ago? I'm sure that notations, and idea like that, have come a long way since then.
In programming terms, his notation wasn't much more than a very high-level psudo-code that you used to construct a description of an existing system.
So conceptually, proving that Linux was correct (or not) would be about the same degress of difficulty & effort as reading the kernel code, and transcribing (not re-writing) to Pascal, or C++, or some other language. I know, I know - please don't start a flamefest over that statement. I'm trying to illustrate the size of the effort, and simply show that it WOULD be doable, even if it isn't particularly practical.
So if there is a way for a driver to lock up the PCI bus by setting the wrong register then the microkernel should be the setting the registers. The way the drivers are written is totally diferent in the microkernel archicture. All the interrupts are processed by the microkernel, not immediatly by the drivers.
I'm sorry, but that's just unworkable in practice - and a good example of one of the things Linus was trying to say.
If it's a microkernel, by definition it should't concern itself with - nor does it have any way of knowing of - what the driver is or is not capable of doing.And as soon as you start worrying about *some* state, you have to worry about *all* state - just so you can maintain consistancy.
And as soon as you have the kernel doing things like setting registers (and knowing what those settings mean, which it has to if it wants to protect from harm)..... guess what? You've got a monolithic kernel - because now you just took 90% of the code from the device driver and moved it back INTO the kernel.
What does a the driver for a network card do? It's sets the registers to initialise the card - it sets the registers to tell it to transfer data in - it sets the registers to tell it to transfer data out - it reads other registers to see what current state is.... etc, etc, etc
As a matter of fact, no - because the time domain wasn't an issue. But I did use Parnas' notation on it, just to prove it's correctness..... it didn't matter how long it took to run.
An addendum of sorts - here is a link that will give you some more information regarding Dr Parnas. I just did a quick search for him on google - I haven't really thought about that project in *years*. And it was interested to see that the project I've been refering to is very near the top of his bio:-)
http://www.cas.mcmaster.ca/sqrl/parnas.homepg.html
So, given the line estimates brought up here now, with a microkernel you have about 10k lines of code that can possibly bring down the kernel, and ~6M lines of code that can't. But with a monolithic kernel you have 6M lines that potentially any of them could bring down the kernel.
And why, pray tell, would you give a shit how pristine your kernel state was if the driver for your XXX Inc network card set the wrong register and seized the PCI bus?
Kernel state is one thing, but it's not the ONLY thing. But a kernel isn't a normal application programme like a word processor, or a web browser. Even if Linus did factor linux down to a microkernel, it still wouldn't be any more (or less) reliable that the most unreliable device driver in the system.
The point I'm trying to make is that if the spec is wrong (or if you don't even have a spec) then your likelihood of producing a reliable and secure -- but complex -- system is practically nil. At least with a "provably correct" system, you know that if your spec is right, then your results will be right. If your system isn't provably correct, then your system will probably be still broken if your spec is wrong, but even if it's right, your implementation still might be broken.
Case in point - again, from the same IV&V.
The boys at Hydro had no idea wtf they were doing. They wern't incompotent by a long shot - they were very good, very bright, and very conscientious. But their background was basically analog design (all electrical engineers), and they wern't overly familiar with software - and it showed.
When I was going over the spec and their timing measurements (the requirements were stated in the form of "maximum time from A to B shall be XXX milliseconds max" etc) on my initial perusal, I came across the statement that one particular sensor was required to react "in a reasonable period of time".
I nearly shit my pants. We're talking about a reactor shutdown system here.... there was a lot of debate within the company I was working for as to how I would document my reaction to that statement and it's appearance in the spec. We finally settled on "I am unaware of any quantitative definition of 'reasonable'"
Slashdot Mirror
It is definitely not as complete or mature as Linux or BSD yet, but it clearly demonstrates that implementing a reliable, self-healing, multiserver UNIX clone in user space based on a small, easy-to-understand microkernel is doable. Don't confuse lack of maturity (we've only been at it for a bit over a year with three people) with issues relating to microkernels.
.... he pushes drivers out to userland and restarts them when they bugger up.
/etc/inittab so that the system would restart it.
Interesting, that statement. "Self-healing"
I remember years ago (newbie), writing a daemon that kept crashing - massive memory leaks somewhere. Not feeling particularly energetic, I hit upon the idea of sticking it in
Anybody here want to guess just how many people shit on me for doing that? "If you have to rely on inittab to restart your programme, FIX IT! IT'S BROKEN! YOU'RE USING A CRUTCH!" etc etc etc.
Maybe it's just me, but unless T is talking about examining the offending carcass, rewriteing the code (self-modifying code? *gasp*) and then resurrecting the thing, isn't he talking about basically the same thing?
you forgot one of the other things about 24-7 environments ..... even a 3% performance penalty doesn't stack up very well if that means you have to spend a couple of hundred thou to upgrade your servers to handle the load, when they'd be good to go for another 2 years if they *didn't* have that extra 3% sucked out of them for the sace of a bit design purity.
Not true. The Mythbusters proved quite convincingly that if you want to shoot somebody who is at least 18 inches under water, you're not going to be able to do it with ANY high-powered modern weapon - the speed of the projectile is so great that it shatters on contact with the water.
....... like a musket.
The only way to get a kill is to use something with a much lower muzzle velocity, and higher round mass
You'd be surprised how much you might need that precision. I have a small network here at home ..... my source files are based on my server, and I work with them (mounted via nfs) under unix on one machine, and under windows (mounted via smb) on another.
RCS/CVS/make et all can get SERIOUSLY screwed up if the timestamps are off by even a second.
In the 80's, many of the folks in the current Bush Administration were defending right-wing, paramilitary death squads in Latin America.
.... and the only think I can see, given the frequency that those "accusations" are thrown about here, is that the only people who take part in these discussions are the worst of both sides.
And who were they defending them from? The people who were supporting left-wing, paramilitary death squads in Latin America.
I hate these dem/rep pissing matches you see so often on here. Republicans are nor more good, evil, closeminded, bigoted, rich, poor, smart or stupid than Democrats
Anybody come up with an American political equivalent of Godwin? I want to invoke somebody's ass
You're absolutly right .... but there's only one, tiny, little problem with it.
Traffic analysis is normally differential - that is, you establish a "normal" pattern, for "normal" behaviour. Any changes in that pattern then tells you that something unusual is happening - different changes signifying different things, etc.
You have somebody (a reporter) who's job it is to talk to government officials and politicos of all stripes in the NORMAL course of doing his job. So just how, pray tell, is knowing that said reporter talked to official XXX going to give you any clues as to who might be leaking what?
Unless the reporter/leak are stupid enough to talk to each other at 3AM when both are normally in bed (a break in the pattern), there's not going to be anything to be found. Certainly not by traffic analysis, anyway.
Anybody remember the Pueblo?
That is one of the things that DOES make him a "typical" user. Most users outside *don't* want to play with the computer - they want to do stuff. And if they can't "do stuff" easily, without having to think, they just won't bother.
THAT is why Windows is so successfull. It doesn't matter how crappy the O/S is on technical grounds, or how buggy it and the other software is.
Put the CD in, click on a few buttons, and you can "do stuff".
Neither Linux, nor any other O/S, has any chance in hell of being a general windows replacement unless they become just as well packaged.
Remember, folks - Microsoft has not, and never will be, a technology company. Bill Gates has not, and never will be, a geek - he's just an incredibly accomplished marketeer with funny looking glasses.
What microsoft does well is market and package. And that really DOES count.
What does that mean? What do you find so offensive about proportinal representation?
.... but having a system that will give you (in practice) a minority every time, it's a recipie for disaster.
.... but in that 6 or 8 months, the ONLY legislation that was passed dealt with Labrador's concerns. (Labrador is that part of Newfoundland which is on the mainland of North America, on Canada's east coast).
...... unless you only have two parties. That's what leads you to an "us vs them" situation that you have now. If you had at least one other party, both the Republicans and the Democrats would be doing things to try to woo voters away from that party, as well, which would tend to lead to more moderate positions for ALL parties, instead of giving you a choice between one extreme or another.
Proprotional representations guarentees that you will have a minority situation and require coalitions. What that means is that regardless of how close you are to a majority - say, 49% - you're still going to have to deal with the fring, specialinterest parties to get yourself over the hump to that magic 51% so you can pass legeslation.
The occasional minority government helps keep the parties honest
In order to get there you will need to defeat dozens of incumbents. Considering that their re-election rate is higher then the house of lords in England I'd say you are dreaming.
No, you don't - all you need is one. Case in point: In one Newfoundland provincial election back in the mid-70's. Tories - 49 seats. Liberals - 49 seats. New Labrador Party - 3. The government lasted only about 6/8 months, if I recall correctly, before we had another election
If you want to work for change work to get rid of winner take all. Work to institute a better way of voting
Personally, I think the first-past-the-post system that you currently have *is* the best system
Yes to #1 - absolutly no to #2. And I also never said anything about proportional representation, which as far as I'm concerned is just an institutional method for letting the tail wag the dog.
All you need to have a minority house, or senate, is to have a 3rd (or 4th) party hold the balance of power - that is, no one party be able to have 50% of the body without support of at least one other party.
It has it's drawbacks - Italy, for example, which is an extreme case but in Canada, minority parliaments have been some of the most positive and productive in history.
Would this be a good time to point out that just before the Soviet Union coopted the Cominterm, Marx himself that that communism was IMPOSSIBLE in Russia, because communism presupposed a surplus of supply for all things, because of the industrial state, before the conditions would exist to allow the state to "wither away"? The Soviet Union - and to a lesser extent, it's still true of Russia today - was still more of a feudal than an industrial society.
...... I wish the hell people would also start using IANAPS
People here constantly preface their posts with IANAL
THANK you - that was one of the few informative posts in this entire thread. Somebody mod parent up.
Here in Canada, in a case like this, the judge has the power to require the state to disclose the information to HIM, so he can rule on the validity of the secret status of whatever the hell it is.
It's implied in your post that that's not the case in the states - is that true?
It would not work. We don't have a parliment like the rest of the world. We have a winner take all system so there is no reason to form coalition governments.
...... that's one hellova statement.
WOW
There is a big difference between having more than 2 parties and being the biggest, baddest Italy on the block.
It would be nice to occasionally hear one of you folk say something occasionally that indicated that at least *some* political systems in the world might have features in their favour inspite of the fact that they wern't the american system.
And maybe - just *maybe* - the occasional minority/coalition governemt might keep your two parties honest enough that you wouldn't HAVE crap like this happening.
Maybe I'm just being silly, but I always assumed that a lot of the NSA budget in the past was consumed by having to deal with things like the cold war.
Does this all of a sudden mean that oil companies being full of shit is a *good* thing?
I'm sorry, folks - but this is what you get when you try to apply technology inapproriatly.
KISS - remember that? KEEP IT SIMPLE, STUPID
What you're doing with ANy form of electronic voting machine in unnecessarily complicating the entire process. Why the hell don't you just give out paper ballots, mark them, and count them - they way they do everywhere else in the world?
This is just a self-inflicted injoury
I grew up in a mining town in Labrador .... United Steelworkers of America.
..... and the resulting wildcat strike untill he was hired back beause he was the prez's buddy.
.... how many jobs will they shift - and how QUICKLY ..... if wages go up overnight, regardless of merit, by 30% because of the coercive power of a union?
They have some really, really, REALLY big trucks up there - the suckers will all 240 tonns of dirt in a single load.
My first memory of unions? One of those truckdrivers being fired for drinking on the job (caught with the flask to his lips in the cab)
THREE TIMES
And as far as the mean, evil PHBs sending the jobs to Indea to save 5 bucks
Thanks - I'll pass. Unions are the last refuge of the incompotent and lazy.
Yes, it was - but the shutdown system had nothing to do with a microkernel. As a matter of fact, it essentially didn't *have* an operating system at all. (Don't go there, folks - I know that that's not strictly true). And you don't want me to tell you how it was structured, either - it was the must #@($*&#@ up piece of code I have ever seen in my life. Absolutly unmaintainable .... but it was proven to be correct.
... but my intention was to use it to illustrate a point, not to be a topic in and of itself.
.... once you had proved the correctness of one particular routine, you didn't refer to the resulting 6 or 10 or 15 lines of proof again - you simply plugged in the top most line - the one that proved the correctness of that particular routine - into the calling routine .. lower-level proofs just dropped off the bottom, so to speak.
Let me restate the point I was trying to make with my original post.
Tannenbaum says micro good, mono bad. This is based on the design elegance and simplicity of the microkernel architecture. If that was the ONLY criteria for judging the worth of an operating system, I would agree with him. But it's not.
This is where the shutdown system came in, by way of example.
Parnas's notation enabled us to prove that the system was mathamatically correct, but still didn't tell us if the system would do the job, because it ignoreed the time domain - the constraints the shutdown system had to work under.
My point was that Tannenbaum is doing the same thing - he's ignoring OTHER criteria that are important for an operating system - mainly, performance, and the ability to handle the workload.
The difference between the two systems is that Parnas' notation didn't *claim* to prove suitability for the task - just that the programme was mathamatically correct. Parnas didn't ignore the timing constraints the shutdown system had to operate under - he simply didn't address that particular constraint, and left it for other methods. Tannenbaum, on the other hand, is trying to pretend that those other constraints just simply don't exist.
Yes, it has been in interesting thread, and I've enjoyed it
Regarding being able to prove that Linux was correct - I don't think it would be that difficult. Don't get me wrong - it would take a VERY long time, and would make even the most ardent techie's head explode from the effort. But the notation Dr Parnas developed that we used was designed to "roll up"
This was also what - 20 years ago? I'm sure that notations, and idea like that, have come a long way since then.
In programming terms, his notation wasn't much more than a very high-level psudo-code that you used to construct a description of an existing system.
So conceptually, proving that Linux was correct (or not) would be about the same degress of difficulty & effort as reading the kernel code, and transcribing (not re-writing) to Pascal, or C++, or some other language. I know, I know - please don't start a flamefest over that statement. I'm trying to illustrate the size of the effort, and simply show that it WOULD be doable, even if it isn't particularly practical.
So if there is a way for a driver to lock up the PCI bus by setting the wrong register then the microkernel should be the setting the registers. The way the drivers are written is totally diferent in the microkernel archicture. All the interrupts are processed by the microkernel, not immediatly by the drivers.
..... guess what? You've got a monolithic kernel - because now you just took 90% of the code from the device driver and moved it back INTO the kernel.
.... etc, etc, etc
I'm sorry, but that's just unworkable in practice - and a good example of one of the things Linus was trying to say.
If it's a microkernel, by definition it should't concern itself with - nor does it have any way of knowing of - what the driver is or is not capable of doing.And as soon as you start worrying about *some* state, you have to worry about *all* state - just so you can maintain consistancy.
And as soon as you have the kernel doing things like setting registers (and knowing what those settings mean, which it has to if it wants to protect from harm)
What does a the driver for a network card do? It's sets the registers to initialise the card - it sets the registers to tell it to transfer data in - it sets the registers to tell it to transfer data out - it reads other registers to see what current state is
Where, in anything that I've posted, have I said or even implied that proving something is correct *isn't* a good thing?
Please, read before you respond.
As a matter of fact, no - because the time domain wasn't an issue. But I did use Parnas' notation on it, just to prove it's correctness ..... it didn't matter how long it took to run.
An addendum of sorts - here is a link that will give you some more information regarding Dr Parnas. I just did a quick search for him on google - I haven't really thought about that project in *years*. And it was interested to see that the project I've been refering to is very near the top of his bio :-)
http://www.cas.mcmaster.ca/sqrl/parnas.homepg.html
The same way you prove 1+1=2
.... so don't go there :-)
Yes, I know it could be 10 depending on the number base
So, given the line estimates brought up here now, with a microkernel you have about 10k lines of code that can possibly bring down the kernel, and ~6M lines of code that can't. But with a monolithic kernel you have 6M lines that potentially any of them could bring down the kernel.
And why, pray tell, would you give a shit how pristine your kernel state was if the driver for your XXX Inc network card set the wrong register and seized the PCI bus?
Kernel state is one thing, but it's not the ONLY thing. But a kernel isn't a normal application programme like a word processor, or a web browser. Even if Linus did factor linux down to a microkernel, it still wouldn't be any more (or less) reliable that the most unreliable device driver in the system.
The point I'm trying to make is that if the spec is wrong (or if you don't even have a spec) then your likelihood of producing a reliable and secure -- but complex -- system is practically nil. At least with a "provably correct" system, you know that if your spec is right, then your results will be right. If your system isn't provably correct, then your system will probably be still broken if your spec is wrong, but even if it's right, your implementation still might be broken.
.... there was a lot of debate within the company I was working for as to how I would document my reaction to that statement and it's appearance in the spec. We finally settled on "I am unaware of any quantitative definition of 'reasonable'"
Case in point - again, from the same IV&V.
The boys at Hydro had no idea wtf they were doing. They wern't incompotent by a long shot - they were very good, very bright, and very conscientious. But their background was basically analog design (all electrical engineers), and they wern't overly familiar with software - and it showed.
When I was going over the spec and their timing measurements (the requirements were stated in the form of "maximum time from A to B shall be XXX milliseconds max" etc) on my initial perusal, I came across the statement that one particular sensor was required to react "in a reasonable period of time".
I nearly shit my pants. We're talking about a reactor shutdown system here