This is good news, but the class of software guys I've run into is decidedly out of date. The last one who took the business seriously was in Nijmegen around 1998, and she was more a coder than a system designer.
If things have moved on in the last twenty years, I'm not be particularly surprised - somewhat surprised because the people I dealt with were deeply not into theory - but entirely delighted.
This is excellent news.
-- Bill Sloman, Sydney
transparently cowboys, and the rest put their faith in simpler rules.
The fact that I haven't had much contact with software guys for about twent y years now is perfectly sane, and an entirely reasonable explanation for m y naivete. I learned about formal proof of correctness for software around
1980, and had enough contact with what was going on in the field to know th at it hadn't got anywhere in commercial software for the next twenty years.The fact that Clifford Heath thinks that it has now - finally - broken thro ugh is welcome news, but not have heard about it isn't any kind of evidence of insanity.
Jim-out-of-touch-with-reality-Thompson hasn't ever shown any sign of knowin g that proven-correct software might be written, but that's not insanity, i t's merely complacent ignorance. To be as ill-informed as Jim is when you a re as bright and well-connected as Jim is could be seen as a form of insani ty, but it is more likely his red-neck background insisting that he doesn't waste time on stuff that isn't obviously going to make him money.
It's still insane, but when everybody in your in-group adopts the same sill y idea nobody is going to put you away.
-- Bill Sloman, Sydney
In other words, where does "crappy" leave off and "has errors" begin?
-- Tim Wescott Control systems, embedded software and circuit design I'm looking for work! See my website if you're interested http://www.wescottdesign.com
I can't remember the details, but in my second job out of college (my first was using a Master's Degree and a screwdriver to assemble PCs) I ran into a conflict between a plain-jane voltage regulator that wanted to overshoot by a couple of volts on startup, and a mixed-signal chip (I think it was an ADC) that responded to this by going into classical CMOS lockup mode.
-- Tim Wescott Control systems, embedded software and circuit design I'm looking for work! See my website if you're interested http://www.wescottdesign.com
nd
damp.
1/4"ut
, but
It did have a crummy output stage - the lateral PNP was too close to the ou tput.
Widlar's LM101/201/301 parts were better, and hit the market first - in 196
7, a year before the uA741 - but the LM307 - the LM301 with the built-in co mpensation capacitor didn't arrive until 1968, only marginally (but as it t urned out) crucially later than the uA741.
It seems to have got written into a lot of university course material.
-- Bill Sloman, Sydney
When I last looked at formal proofs back in the 80s, there seemed to be several big stumbling blocks: - the formal proofs were at least as difficult as the actual design - the formal proofs always had to interact with informally specified systems; the conflict is obvious - were the requirements correctly
Do you have any indication as to how or whether those people approach those blocks?
The RSRE Viper/NewSpeak people were motivated by introducing micros into fire control systems. That stood a fighting (ho ho) chance because the complete domain was very limited.
The gain was sufficient to feed the next stage. I just heard that the audio quality might not have been good enough> It sounded fine to me, but hardly have a trained ear for music etc.
The domain of the seL4 operating system is also quite limited. All the specifications, code, proofs and proof tools are open source available online - have a read if you're interested.
The specification was developed in "literate Haskell". It covers all the obvious things like "one process can't read or write the memory of another", etc. They actually don't include memory allocation - instead a process may map parts of its memory space into a subprocess, and has a protocol for regaining control. The protocol ensures that the hand-over is well-controlled.
The point is that though the content of a process may be an "informal system", it cannot break the formal rules of its operating environment or violate O/S invariants. No single process can violate confidentiality, crash or hang the other processes.
Yes, the proofs are difficult. That's why they make extensive use of machine checking, to catch human errors. I'm most impressed (and mystified) by how they proved that the machine code correctly reflects the proven C source. Also impressive is that the proof rests on the *formal* specification of the ARM11 instruction set and architecture (though of course there is not a proof that any actual chip correctly implements the specification).
Clifford Heath.
A long time ago I had a chat with one of the Viper developers. If I remember correctly, only the processor itself was formally proved correct, not the i/o interfaces. Also, it was not possible to support interrupts in a formally proved system.
John
Very plausible.
I note that the XMOS processors (up to 16 processors/chip, IIRC, see digikey), where the the *dev* environment *guarantees* cycle-accurate timing, doesn't use interrupts. The basic idea is to dedicate a processor to an i/o or computation task, and inter-process comms are via channels.
If that sounds like CAR Hoare's CSP and the Transputer, it won't come as a surprise that David May is a key technical contributor. Some of the other personnel are equally impressive.
The XMOS also has single-cycle static ram (no caches, dram, etc.), no write-back buffers, no read-ahead buffers, no branch prediction logic, very strict pipelines in the cpu with no register renaming, super-scaler scheduling, etc. It is designed to give very predictable instruction timings. Even then, the predictability may be limited depending on the scheduling options - you have to give a hardware thread a fixed time-slot schedule to get cycle-accurate timing.
It is a really nice architecture, which I would like an excuse to use again. I used it during its early days, when the chips were limited by having far too small RAM, the tools and XC language were too restricted, and many of the examples were horrendously badly designed. But the principle was good, and I believe the practice is far better now than it was then.
ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.