Discussion on:

147
Comments

Join the conversation!

Follow via:
RSS
Email Alert
1 Vote
+ -
Agreed given
Tony Hopkinson Updated - 31st May 2011
you have an umabigous requirement to start from, which is the holy grail of software development....
All this basically does is prove the code does what we said it would do, not what the client thinks it should do , now....

It's Given an unambiguous requirement then...
Which is why I'm saying whoopee f'ing do in an extremely sarcastic tone.
None of this stuff is new, it doesn't work in the real world.
You can't compare describing the base level features of an OS, with I'd like an MIS application for call usage, with some smileys on it please.
Being able to describe an ordered list mathemetically will not help you in any siginicant way with a combobox with some thingies in it. Especially seeing as the combo is a third party artifact you have absolutely no design oversight on.

Getting agreed requirements from clients that you and they understand is the real problem, using math to compare a requirement to code, simply means that code meets THAT description of the requirement, hooF***kingray.

Then we come in to writing bug free and secure (two very separate things) code, neither of which have any significant commercial values in almost all circumstances.
Our code is not buggy and insecure because competent people didn't understand the requirements, it's not because we couldn't relate it to the requirement, it's because it was commercially justifiable to do it poorly, and probabably with incompetents.

Welcome to the real world...

Sheesh.
0 Votes
+ -
Contributr
I'm no expert. But as it has been explained to me, they have gotten it to work for seL4. If you contest their findings, give me details. I will gladly pass your findings along.
of any use in the real world definitely.

In order to validate the code against the requirement both must be described in the same mathemtical notation, usually a mixture of predicate logic and propositional calculus, your client is more likey to understand badly written VB in Urdu...
So what you've really done is prove 'your' mathematical description of A requirement against your mathematical description of your code, whether you'll agree that it was or even is your requirement is as iffy as it ever was.
On top of that writing bug free secure code has very little commercial viability...
Even if this research doesn't flow into actual use, it may produce useful spinoffs such as metalanguage for describing what code is supposed to do, or even just something that can be useful as a universal commenting shorthand.

Small advances are advances too.
0 Votes
+ -
Contributr
If there isn't a first step, then a second, we stay put.
0 Votes
+ -
and say that if it the tool is that good, and its that important to secure our embedded systems (nuclear, automotive, etc) then it should be mandated - even unlawful, NOT to use it. Still, how do we know if the tool itself, this seL4 isn't bug-free? wink
variaties of case tool, all claiming to "be the best"...
Not new and just like this one don't address the real issue, specifying the requirement unambiguously so you can match it to an implementation.
This is 20 / 80 not 80/20...

Now if you can see a time coming when all requirements specified by laymmen are basically in some form of code that is not subject to more than one interpretation, I have this bridge....
1 Vote
+ -
No kidding?
seanferd 30th May 2011
I think the idea is to make these issues easier to deal with, so the business types have no gripe with the process.

You'll notice no one is trying to do the harder thing, which would be to get the business types and investors to understand that "it isn't all about you and your short-sighted self-interest".

The "real world" is always a funny thing, because no one ever addresses the real "real world" - not the real world of human constructs, but the real world of Nature, which people and corporations regularly ignore. Nature doesn't have much truck with human business sense. Just ask the folks who do things like, oh, think that because a levy has been raised on a river, that the land right behind it is a good place for development.

The above may be a bit off-topic, but the "real-world" of human socio-economic constructs isn't real outside of convention, and loosely based on fact, if at all. That's what I think of "welcome to the real world" statements, as if economics are the final arbiter of reality.

Not that your point isn't valid in the made-up real world of corporations, which are so unreal that they require constant lobbied legislation to maintain the reality that they want.
on professor's 350 page mathematical description. This solves the problem between designer and coder, t will never solve the problem between customer and software provider, not unless all these business types one, learn how their business actually works and two, becomes a gifted mathematician.
The problem with this method is it reduces the extent of the problem by taking people out of it. If we could actually do that we wouldn't have needed it in the first place....
0 Votes
+ -
... is that sometimes, it can produce theorems that are extremely simple to understand by common people (that already feel that the assertion is correct based on their experience).

But below the surface, the demonstration is extremely complex and can only be understood by mathematicians. In some cases some demonstrations were assumed to be correct, until a flow was found in the demonstration, and a new problem appeared that was as much complex to prove as the initial demonstration. When this occurs, there's a lot of mathematicians suddenly investigating the problem and a new genius will come to solve this last problem for at least a domain covering the initial demonstration, plus some other problems, creating an even more general theorem, whose formulation will even drop some preconditions, making the theorem even simpler to understand by non-specialists (for example two previously distinct theorems are now reduced to a single more general one).

The economical implication of these theorems is extremely huge, because it immediately suscitate creativity (by using it for many new cases of problems which were thought impossible to solve in a reasonnable time).

The problem of mathematics are a very long research project, without any warranty that the research will find something useful in a reasonnable time. This means that you cannot invest anything there with a reasonnable expectation on your return of investment in a warrantied time. The best that can be done is to donate to mathematicians regularly, and if you feel lucky, you will win. But it's like lottery : huge profits if you win, but warranty of losses in almost all cases.

Then you should not spend in mathmetics more than what you can give without any return. Mathematics research departments or labs everywhere are never winning money, they constantly look for money, independantly of their past successes.

Beside the few parts of the complex systems you want to assert as bug free, these parts together are not enough to build the useful systems we need and use every day. All the rest of the assembly is still "art". The art of programming, and essence to creativity... But no software vendor want to admit that their products are piece of arts, except if you read their licences : use at your own risks, no warranty implied (even in closed commercial softwares)... It's up to everyone to assume that there's a risk, and not depend too deeply on the software to keep you in business, even after a catastrophic software failure.
There's a difference beween knowing that the area of a triangle is 1/2 the base * height.
Then there's knowing why it is.
Then there's rigorous mathematical proof.

It's not genuis level math to use, though no doubt you have ti be on top of your game to prove it's rigor.
But we are talking about running out of greek symbols and resorting to ours upside and back to front etc, off putting for your run of the mill pointy head...
0 Votes
+ -
So...
AnsuGisalas 30th May 2011
a bug tax?
Choke the commercial justifiability...
Heard if it?

A bug tax, I can see one or three softwre providers lobbying their local poltical representatives to call an abrubt halt to that. Lawyers would love it.

As you can see here your honour next to this upside down A just before the opening brace (erm curly bracket your honour) cleary indcates that making error caption at position 343,162 of exhibit 42,356 blue wasn't in fact what my client wanted and is therefore a bug...
0 Votes
+ -
60s and 70s
phoenix_frozen 30th May 2011
It was also considered impossible to formally verify operating system code. The world changes around us, and this industry in particular is oddly cyclical.
system code. It was considered impractical to verify existing operating system code.
The only cycle here is the rewrite one, and that a commercial justification, not a technical one, always has been, always will be.
You take these new methods and apply them to version 2 DOS, that would impress me.
You need very fixed and unambiguous requirements for this to be practical, that's my issue with it.
making the judge see more bugs would mean paying a higher bug tax.
Just have a fuzzy mashup of the overall error-per-megabyte (EPM) ratio of the code, assign one 1% additional tax on profits on the product for each EPM percentage.
Mandatory out-of-house prerelease testing should cut down the cases of companies trying to counter charges.
And I'm dead serious, too silly
a beta version.... sad
Given one mans bug is another mans feature, how would you achieve a a description of say windows (or some linux distro) that would be the definitive requirement to measure 'bugs' against.
I doubt it exists now, I guarantee if any one anywhere did one, there would be a stonking great tax bill at the end of the proving exercise, and that's before you get to all the add on apps that come with the OS, don't even mention the crapware, resllers stuff in there with your off the shelf install, fresh install or upgrade, backwards compatibility, drivers, hardware differences, configurations.
0 Votes
+ -
of course, my vision also includes a Lord High Inquisitor with a license to torture CEOs at will, on a whim, or just for fun grin
0 Votes
+ -
Contributr
If not, I am in deep trouble
More often that not in fear, when the next panacea merchant sells something to management that's going to solve all their problems...
These guys are at least narrowing down it's applicability to a small subset of application development, basically embedded and firmware in practice, not what the guys in suits with the money perceive as software though is it.
They don't even think of an OS as software do they....
0 Votes
+ -
You are mostly right in stating that none of this is new. Most of the technical ingredients of the seL4 verification project have been around for quite a while, including the underlying proof method of forward simulation for showing that the kernel code refines the abstract kernel specification. This method is indeed closely related to what VDM calls reification. Does that mean it doesn't work in the real world? Not at all. This project is evidence to the contrary.

Stating that bug free and/or secure code has no significant commercial value is disingenuous at least. Good luck selling, say, an anti-lock braking system to a car manufacturer, when it was done "poorly, and probably with incompetents."
It doesn't.
First and most important is colour. Purple indicates passion you know.
Then get somebody successful to put a sticker on it.
If you can show it's vaguely related to the current IT fad that's a major bonus, make that sticker a cloud with a purple lining.

Now what you do is you give your sales type an expense chit, and get him to waffle pasionately (while pouring the wine) about how good the product is, why it's the in thing, to some clueless pointy head who thinks the pedal is the brake, in a Flintstones sort of way.

Sale.....

What's disingenuous is any attempt to portray your narrow success as widely applicable...

I wish it was, but it isn't.
1 Vote
+ -
Just like a car...
Alpha_Dog Updated - 30th May 2011
Your dad was right. Just like we won't knowingly buy a lemon,we
shouldn't buy shoddy software. I am an old shadetree mechanic as well as a sysadmin. My favorite car was my '68 Mustang, not because of it speed, agility, comfort, or gas mileage, but rather it's simplicity. I could replace the head gasket with only 3 wrenches. I could do a brake job in an hour. When I hit the gas the computer didn't second guess me... it just worked. I feel software should be the same.

First, it should just work. After initial set up, the software should do what it was supposed to. Consider: a computer is among other things a machine we use to do enormous amounts of repetitive work. If it didn't work as expected even once murphy's law dictates that it will do so at the worst possible time. Given many of these functions are nested, the errors will cascade.

Second, when it breaks it should be simple to fix. Modern man uses modular architecture in software for a reason. There is no excuse for an executable to exceed a couple of meg. The enormous number of calls and includes yield a monolithic solution that any one developer can't track a bit through from beginning to end. This makes it hellish to solve the problem when you can't isolate the issue and use standard troubleshooting methods. If I wanted to use an executable like that I'll just code it start to finish in assembler, subverting the OS. It's not like the OS is going to see any clock cycles anyway with an executable that big.

Third, analysis must be done to ensure failure on the user's terms. The industry has used this analysis for years in aerospace and industrial work where a data processing failure could cause loss of life or property damage. Applied to general software engineering, we need to make sure that the failure modes either are self correcting or create a halt in a non-critical manner. Simply put, there is no excuse for a kernel panic or BSOD other than a hardware failure.

Fourth and finally, the mathematical modelling is important, especially in the early stages of software development, but nothing beats human inspection and testing. For this reason it is my belief that open source software is inherently more thoroughly tested than its closed source counterparts. With all the eyes on the code it must be both tested and inspected. Now, what is done with this testing data is what separates the men from the boys... or more appropriately a responsive company with a quality product and those who fail their users. This process will take care of the design part of security, with the other part being handled in the usability testing.

After these criteria are met, we can start talking about optimisation and aesthetics. It is better to have these as an afterthought than the previous 4 criteria. Once the code is optimised and GUI made pretty, usability testing begins. Have as many try to break the software as possible, both intentionally and accidentally. This is where open source has another benefit. Millions of people can download and use the software, submitting feature requests, bug reports, and security issues. Address these and slap a 1.0 badge on it.

Cost effective? Yes, but not in comparison to the closed source model. Fast? Not really, but perhaps that is the problem. In aerospace, we call it "go fever". This virulent disease is fatal, but usually not to those infected. Ground crews pay more attention to deadlines than safety in order to meet arbitrary launch dates set by politicians. Looks a lot like coders trying to meet production quotas and release schedules which are dictated by sales and marketing. Do it right and serve it then.

Good engineering and a modular approach works for cars, aerospace, hardware, and software... Too bad it's so rare.
1 Vote
+ -
Contributr
68 Mustangs, oh yah. I have a good friend, who owns a black 68 fastback with a serious 427. My neighbor just bought a new Mustang and was bragging. To my good fortune, my friend happened to be coming over. I don't have to tell you who went away whimpering.
Very few W-code (427-4bbl) mustangs were ever built. Some even believe that number to be zero. Mine was one (lime gold notchback) and your buddy in his black fastback probably account for about 10% of the current population!
0 Votes
+ -
Contributr
Was that the kid with the new Mustang said all he had to do was change the chip and it would be no contest. My friend told him, he would buy the chip and run for titles. The kid back peddled rather fast.
1 Vote
+ -
Change the chip...
AnsuGisalas Updated - 31st May 2011
That's just too funny. People thinking a mechanical machine can be upgraded with the help of digital hardware.
They don't seem to realize that what the chip actually does, is even out the performance, removing the potential for a good driver to get 100% out of the machine - in order to prevent poor drivers from going around using only 35% of it while spewing black smoke full of half-combusted fuel ... and transmission parts.
0 Votes
+ -
It is funny to see the look on their faces. Almost accusing their car of failing them. With all the handling issues and the ability to shell the tranny on demand, my old mustang made me a better driver than I would have become with a more sedate pony.
0 Votes
+ -
A '68 W-code fastback will eat a new mustang alive in 1/4 mile and top speed, with no glimmer of hope. On a track or road race the new mustang will win unless major work has been done to the 68's suspension.

Mine had major work done to the front and rear suspension, brakes, steering with modern rims and tires. It still couldn't quite hang because of the weight distribution. The big engine makes it nose heavy and impacts cornering terribly. I moved as much equipment as I could from the hood to the trunk and replaced all the front sheet metal with fiberglass. Even with all that, I never got the weight better than 70/30.

The result was a car that would pull .92G in a turn (not all that impressive), do 0-60 in 4.2 seconds, run 10's in the 1/4 mile and could top out at just over 200MPH (I have a pink slip to prove this). It would also drain a 20 gallon tank in just under 15 minutes running flat out.

Despite the issues, I miss that car. It was stolen and crashed during the joy ride with no survivors. One of these days when I am rich and famous I'll rebuild it, positioning the engine a little farther back this time.
That reminds me of a story that will actually bring this back to the computer realm...

Many years ago, my brother-in-law had just gotten a brand new laptop for work. (His work paid for it.) He was bragging up his laptop, saying it was the fastest laptop on the market. (Pentium 90, maxed RAM & Hard drive - prolly 32M RAM & 120M HD if memory serves... over $5000 worth of laptop at that time.) I told him mine was faster. He said "impossible" and challenged me to a race. I said sure; here's the parameters. We will open & power up our laptops at the same time, start the word processor, and type "Mary had a little lamb." First one done wins. He agreed.

I went out to my truck and grabbed my trusty Tandy 200 laptop (2.4MHz, 24K RAM, 72K ROM, no internal magnetic media) and when he saw it he said "You gotta be kidding me... that's ancient!" I said I wasn't worried, and asked if he was ready to start the race. He said sure (with a chuckle, thinking he was going to trounce me), and I said "Go." I opened my laptop, powered it up (which it did in under a second, booting from ROM) cursored over to "TEXT," typed my sentence, said "Done" and swung my laptop so he could see the screen. His machine had barely made it to the Win95 splash screen.

When his jaw dropped, I asked him if he was glad that we weren't racing for pink slips... wink

Yes, my old Tandy 200 still works (26 years young now) and I still use it. I've had to fix it once (the 5-year NiCad NVRAM Battery only lasted 15 years) and I've upgraded the RAM to 72K.

Laterz!
"Merch"
0 Votes
+ -
Contributr
Great story and brings fond memories flooding back.

I just heard this week, that Radio Shack announced it is finally waking up and returning to its roots. Planning to take care of DIY types. About time,I say.
0 Votes
+ -
Awesome!!!
Alpha_Dog 6th Jun 2011
That was great. I had an old 100 that I still miss. Man, in those days we made magic with things that today don't even qualify as a calculator!
0 Votes
+ -
We are going to build a new car for the business to race at Bonneville. We are conservatively expecting a street legal 240mph vehicle that we will occasionally use for client visits... just for the fun of it.
0 Votes
+ -
I will serve...
SkyNET32 2nd Jun 2011
No wine (software), before its time. (to management that means: **** off until its ready. grin )
0 Votes
+ -
After all, computer operations isn't exactly - ahem - exact, is it?
So I wonder about how one can predict an operation execution that results of a processing error?

Interesting stuff, as always, Michael.
...is why not? Why are computer operations not exact? Do we have the right to expect a machine we build to work as it was designed and programmed?

If this is too much to ask, I am in the wrong business. I have built machines that exceed six-sigma uptime (regardless of how you figure it) on a routine basis. I expect it. Machines which do not meet this are repaired or replaced. This includes my router, servers, desktops, and yes, even my car.

I comes down to ownership. If I own the machine and the software on it, I can and will require this. If I don't own it and it doesn't meet my requirements, I send it back.

I do not need help making errors; I make plenty myself. I need my tools and machines to be ready when I am and to help me make my work better.
0 Votes
+ -
That's a fact of optimizing against diminishing returns.
Making a computer processor that makes no erroneous operations is likely going to be prohibitively expensive and/or slow.
The right way to handle it (if the instruction set to be handled isn't hardened against errors) is to have triplexed processing, taking advantage of the unlikelyhood of the the same random error happening in two out of three processors simultaneously. Of course, that's expensive too.
One way around it is to use a vast array of inexpensive processors; like someone once did with a busload of those faulty original pentium chips; put enough of them together in an array and you get the error margin down lower than that of any normal not-very-fault-prone CPU of the next higher generation, and with a power advantage too.
Fault tolerance is critical in an environment where a stray proton can set bit errors.
Just like buying ECC memory may make sense your OS can provide processor fault tolerance at an expense of overhead. If you design OS's for spacecraft you would probably require redundant fault tolerance at every level.
I'm sure the team of programmers for the NEAR Shoemaker spacecraft wished that they had formally verified the OS after it lost its mind mid flight.
http://klabs.org/richcontent/Reports/Failure_Reports/NEAR_Rendezvous_Burn.pdf
Thirteen months late and a lot of programming hours later the cost may have been justified
0 Votes
+ -
Contributr
I was thinking about those types of projects when I heard NASA has given up hope on the Spirit rover. That team sure can be proud.
Landing the craft on the asteroid, without all the extra fuel in the plan, with a craft never designed for a landing.

Reprogramming to replace the sun location sensor with other inputs.

Makes me want to go off to the space coast or Huston.
0 Votes
+ -
Nailed it.
Alpha_Dog 31st May 2011
Space is unforgiving. Between the ionizing radiation and temperature variance computers have it rough. ECC memory and parity schemes are a good start, but more can be done. A voting system and having non-identical parallel architecture works a treat... but at an extreme cost. You think hammers and toilet seats are expensive in space, you should price a man rated DPS system!
0 Votes
+ -
Contributr
Question, Ansu
Michael Kassner Updated - 31st May 2011
Is it fair to say that you refer to firmware? Or can hardware create errors?
0 Votes
+ -
Hardware too.
AnsuGisalas Updated - 31st May 2011
At least that's what I've understood.
As BBoyd points out, there's always radiation, even down here in the atmosphere. Cosmic and/or manmade.
Noise in the power feed perhaps.
Electromagnetic pollution from nearby wiring or equipment, certainly.

But I've also come to understand that errors occur by themselves too... electrons quantum-mechanically jumping across the boundaries in the processors perhaps. There are no certainties with subatomic particles, only stochastic tendencies approaching certainty (never getting there).

But I am sure there are CPU architecture specialists out there who can give an actual answer to this, rather than my patently inexpert musings grin
0 Votes
+ -
Hardware too
Alpha_Dog 1st Jun 2011
Besides normal amount of hardware errors, equipment that is outside of our protective atmosphere is subjected to a cornucopia of nasty stuff, all of which can induce a charge ranging in intensity from insignificant to enough to blow chips off the board. There is a bias toward the low level events, with the probability curve looking like a slope.

While charged particles are a constant issue, it was a big surprise to find out that non-ionizing radiation striking ferrous materials produces an incredible amount of ionizing radiation which is lethal to computer and bio-critter alike. The trouble is that it it comes from a system board fastener, the resulting radiation source is very close to the area where it can do the most harm.
0 Votes
+ -
True
Alpha_Dog 31st May 2011
but would I knowingly implement one of those old Pentiums with the math error, thinking it's all right? Ummm... NO!

When these came out I had 2 CAD workstations with them. Considering some of the industrial control and aerospace projects we were running at the time we could not afford this kind of error. We donated them to a local community college and bought replacements.

Likewise in software and hardware as a system. I expect errors, but not in any measurable quantity.

The reason I quoted 6-sigma in the original thread (the statistical term not management book philosophy) is because the metric actually means something. I want my failures to be less than 6 times the standard deviation in a normal distribution curve which is where 100% confidence level begins in statistics.

Put into real world numbers, I expect to have 99.99966% uptime, where uptime is defined as being free of unscheduled downtime and does not count routine booting or shutting down times. Putting this into perspective, this is a little over 10 seconds of allowable downtime per year, and we did it with our router appliances.
I didn't mean to say that people should use the flawed pentium, nor that they should accept such flaws, but to say that by lashing the flawed CPUs together some lab somewhere was able to make a very precise and very powerful machine.
It was a proof of concept which most likely is part of the basis for todays cloud adventures.

But my point was that all CPUs have a certain ratio of erroneous operations (as far as I have come to understand), probably far less than the 6-sigma requirement, but existing nonetheless. If you take into account that CPUs have numbers of operations numbering in the millions, this means that errors do occur, every hour, maybe every second.
In any CPU.
0 Votes
+ -
Contributr
Errors?
Michael Kassner 1st Jun 2011
I asked this earlier. Are you referring to hardware errors or firmware? I realize silicon is as much cooking as science and there are bad bits. But, I am confused as to what errors you are looking at.
0 Votes
+ -
Errors.
Alpha_Dog 1st Jun 2011
The infamous Pentium error was due to bad data in a look up table. Whether this is firmware, hardware, or software kind of depends on you point of view. I will submit that it wasn't software since it was hard-coded on the chip.

My reason for bringing this up is that hardware issues are just another type of error we can see in a computer. We do not tolerate these, but we accept software that ships with several thousand bugs, some of them crippling. I see this as a double standard.

We need to apply the same criteria to software issues that we do for hardware. The reason is that as computers become more integral in our lives, it is more and more likely that these digital helpers will take some part in a life or death decision of ours. I am far from flawless, but my tools make me more than I am.
Keyboard Shortcuts:
Prev
Next
Toggle
Join the conversation
Formatting +
BB Codes - Note: HTML is not supported in forums
  • [b] Bold [/b]
  • [i] Italic [/i]
  • [u] Underline [/u]
  • [s] Strikethrough [/s]
  • [q] "Quote" [/q]
  • [ol][*] 1. Ordered List [/ol]
  • [ul][*] · Unordered List [/ul]
  • [pre] Preformat [/pre]
  • [quote] "Blockquote" [/quote]

Join the TechRepublic Community and join the conversation! Signing-up is free and quick, Do it now, we want to hear your opinion.