Warning to newbies

[Nick Keighley]

Can't you just let Moore's Law handle "efficiency"?

interesting question.

Apparently the physics people always have a program "sitting on the
shelf" that can't be run on any existing computer. I guess they tweak
a constant to make a mesh denser or something everytime a new faster
computer comes out.

Have you read John Bently's "Programming Pearls". He has some
practical examples of efficiency. The time it takes to invert a large
matrix is dominated by improvements in algorithms rather than Moore's
law.

Recently a man computed <large number> digits of pi. He could use a
fairly ordinary PC to do this rather than a server farm because he had
a better algorithm.

Practical compression and encryption make all sorts of things
possible.

And you mention real time.

In my view, garbage collection is such a great thing that we shouldn't
be sad that it happens.

we might be sad if it happens at an inappropriate moment! I believe
modern garbage collectors are less "lumpy" than the old mark-and-sweep
ones. Perhaps another example of where efficiency matters!

However, I have NEVER programmed OSen or embedded systems for real
money, although I've written a number of compilers.

compilers aren't usually classified as real time.

I understand that
absolute performance goals may apply. I do object to treating
performance speed as an unalloyed good when the customer doesn't ask
for it.

quite right. On the other hand he may not *ask* for it and still
expect it. "You never told me it would take an hour to reload the
system!"

 

[Nick Keighley]

forgot an example! Games. The "physics" is always a compromise between
accuracy and runability and they have to aim the game at what they
*think* the typical hardware will be when they finish writing the
game!

[stuff on scalability]

Interesting comments. Thank you. OK, it sounds like software will be
in ten years something that only highly qualified postdocs will write
anew,

maybe clever libraries or frameworks will help?

and this directly contradicts what I said elsewhere: that
software is evolving in the direction of airline piloting.

If software becomes brain surgery then serious barriers to entry need
to be enforced by law.

Highly critical intellects will be needed to say "the emperor has no
clothes" since so much concurrent software seems to work as in your
ABA example. Ben Bacarisse is the only example here and I sense his
intellect is atrophying on the job.

The idea of a formal proof of software correctness, or Dijkstra's
idea, that we should develop the proof and code simultaneously, may
come into its own,

I've been waiting a long time for *that*

as may Dijsktra's memory; we badly need a solid
scientific biography of Dijkstra for the general reader, since so few
people outside the field know of his contributions.

<snip>

 

[Nick Keighley]

My civilian understanding is that the pilot of a jet fighter can in
most extreme situations bail out explosively and float gently to earth
in a parachute. His ass might hurt for a couple of days.

But they don't give parachutes to passengers of civilian jets.

they don't shoot a civilian aircraft.
Besides, it cost a lot of money to train a military pilot.

I conclude that the safety requirements for civilian aviation are
higher. Unfortunately, Langewiesche doesn't specify what programming
language was used for the A320's fly by wire software. I really,
really hope it's something like Ada or Eiffel and not C++.

I googled around but couldn't find anything.

Not everything went smoothly with the airbus software
http://catless.ncl.ac.uk/Risks/18.78.html#subj3.1

"two of the remarked situations represent control anomalies of a sort
which may not occur with non-digital control systems. [...] The
flight-control computers responded to pilot inputs in a different mode
from that in which the aircraft was *in fact* configured. Crudely
speaking, the computers `thought' the aircraft was flying under
partial flaps, whereas in fact the flaps were full down. In the third
situation, contaminants in the pilot controls cause jerking of the
control surfaces without feedback to the pilots. "

 

[Nick Keighley]

So, you admit that the compiler can detect it. Good. Now the compiler
can fix it by generating an extra machine instruction to return a
zero.

I'd much rather have a diagnostic. Returning zero by accident is
almost bound to be wrong. If I'm doing a walkthrough and I find a path
through a function that omits the return I have to work out if he
meant to return zero or he just forgot. Much better if the compiler
issues a diagnostic.

Ada:
"A function body shall contain at least one return_statement [...]"

But as you yourself have shown us, a C program can be "standard" and
full of bugs.

you can write bugs in any language

The Standards don't mandate error reports in many
undefined situations: they simply say "gee, that's undefined, pal,
isn't that a shame", in essence.

This is an interesting read:-

http://www.amazon.co.uk/Safer-High-Integrity-Safety-Critical-McGraw-Hill-International/dp/0077076400

beware of brken link

and just curious, does that come up with my amazon page?

 

[Nick Keighley]

On Feb 4, 6:13 am, Phil Carmody <[email protected]>



Not really. The only way to shut down such an appliance is brutally,
by turning the power off.

that may be appropriate in some applications. When would you turn your
anti-lock brakes off or your heart pacemaker?

 

[Gus Gassmann]

forgot an example! Games. The "physics" is always a compromise between
accuracy and runability and they have to aim the game at what they
*think* the typical hardware will be when they finish writing the
game!

Not just "think", *expect*. Moore's law turned from being descriptive to
being prescriptive quite a while ago. Now that processor speeds seem to
have hit a limit, this means dual, quad, eight, sixteen etc.
configurations eighteen months apart. The gaming industry depends on it.

 

[spinoza1111]

spinoza1111wrote:

There already is significant legislation covering many software
applications including brain surgery.

I'm talking about legislation concerning who can write code.

Formal software proofs of the type that you mention rattled around
30+ years ago as a good idea had conceptual fatal flaws. Update your
reading, I suggest starting with papers on mechanical reliability that
were  being published about a 100 years ago.

What were those fatal flaws?

It was thought that the proof might have an error.

Which showed that the critic didn't understand how we need to reduce
probability of error to one over six sigma without ever eliminating
errors, by taking one extra step.

Furthermore, nobody understood Dijsktra's point: that the proof could
be developed alongside the program.

Also, I'd add that a properly constructed software walkthrough is a
venue for the presentation of software correctness proofs in ordinary
language. This never happened because of the toxic personal relations
fostered by American "free market" competition: consistently, people
with the purity of heart and verbal abilities to be able to construct
sentences of the form "my code works because" were made targets of
bullying with management's tacit approval, because management needs
office bullies to get people to Obey. As a result, structured
walkthroughs and other engineering reviews degenerated very rapidly
after the election of Ronald Reagan (and its message that verbal
abilities and purity of heart were for fools, and that being glamorous
and coated with Teflon were the way to go).

A direct result was the normalized deviance of the Challenger review
at NASA subcontractor Morton-Thiokol in early 1986, where engineers
with verbal abilities and purity of heart tried to tell NASA
management that the performance of allows in Space Shuttle O-rings was
unpredictable at low temperatures such as were obtaining in Florida in
that January. NASA, which was under pressure from the Reagan
administration to show that the USA could put a teacher in space,
bullied these engineers and ruined their careers by pressuring them to
"think like a manager and not an engineer", and in my experience at
Bell Northern Research, this happened in software as well.

As in these disgusting "newsgroups", little constructive work gets
done because nothing like a logical argument, much less a software
correctness proof, is ever presented. Therefore, the possibility of
presenting even an informal correctness proof is dismissed out of
hand, and instead the word of loudmouths is treated as Holy Writ.

For more information on NASA's Challenger disaster, and how
"skepticism" of the possibility of knowledge or partial proof killed
the crew of Challenger, cf Diane Vaughan, THE CHALLENGER LAUNCH
DECISION, U of C press 1999.

Nobody can "prove" that a real system won't fail. The Airbus A320's
"fly by wire" avionics system is software designed to make sure the
A320 doesn't go outside its performance limits: if the pilot pulls up
the "stick" (which is no longer a stick at all) the airplane won't
obey beyond the angle for which it is designed. Nonetheless an Airbus
crashed last June. Likewise the Toyota's accelerators (and now its
brakes, according to a story in today's International Herald Tribune)
are failing although they are software controlled for safety.

But this means...more software and correctness proofs too, not less.
You can't (according to my source which is Langewiesche) go back to
the cockpit of a 707 in the 1960s, with a flight engineer laboring
with a slide rule to recalculate course when the weather changes. The
level of traffic and the demand for air travel won't permit it.

Unlike Dijkstra, I think that English used well, and uninterrupted by
thugs, is a form of correctness proof, even a comment that says
clearly what a module does when read alongside the code.

 

[spinoza1111]

So, you admit that the compiler can detect it. Good. Now the compiler
can fix it by generating an extra machine instruction to return a
zero.

I'd much rather have a diagnostic. Returning zero by accident is
almost bound to be wrong. If I'm doing a walkthrough and I find a path
through a function that omits the return I have to work out if he
meant to return zero or he just forgot. Much better if the compiler
issues a diagnostic.

Ada:
"A function body shall contain at least one return_statement [...]"

<snip>

But as you yourself have shown us, a C program can be "standard" and
full of bugs.

you can write bugs in any language

The Standards don't mandate error reports in many
undefined situations: they simply say "gee, that's undefined, pal,
isn't that a shame", in essence.

This is an interesting read:-

http://www.amazon.co.uk/Safer-High-Integrity-Safety-Critical-McGraw-H...

This looks very interesting. Did you write this book? I might get it.

 

[Walter Banks]

What were those fatal flaws?

It was thought that the proof might have an error.

Sounds like a guess. Read/understand the reliability papers

w..

 

[osmium]

As a result, structured
walkthroughs and other engineering reviews degenerated very rapidly
after the election of Ronald Reagan (and its message that verbal
abilities and purity of heart were for fools, and that being glamorous
and coated with Teflon were the way to go).

Don't you sense even a tiny conflict between your claim a few days ago that
successful techs were hairy and fat and today's claim that glamorous is in?
My guess it that your notion of glamorous consists, at least partly, of
combing your hair on a daily basis.

You seem to think Reagan had no verbal abilities. You DO realize he got
elected, do you not?

 

[spinoza1111]

spinoza1111wrote:

Don't you sense even a tiny conflict between your claim a few days ago that
successful techs were hairy and fat and today's claim that glamorous is in?

No. The technical proletariat cultivated anti-glamor in futile passive
aggression.

My guess it that your notion of glamorous consists, at least partly, of
combing your hair on a daily basis.

You seem to think Reagan had no verbal abilities.  You DO realize he got
elected, do you not?

There may have been a secret deal between Reagan and Iran to hold off
the release of the hostages.

Also, never underestimate how fooled Americans can be by a half-
literate with a speech coach (Palin).

 

[blmblm]

The problem was one of computer science, but Kiki, filled with
resentment if not hate, kept whining that it was off topic because C
Sharp could handle the problem with ease.

Yes, C# can indeed handle the problem. However, it's not exactly all
that
"efficient" because it needs to do a full blown copy-on-write and use
garbage collection to ensure that everything works as expected. In other
words, I cannot operate on data-structures directly like I can using
assembly language. FWIW, this is exactly how Sun implemented
`AtomicStampedReference'.[...]

Can't you just let Moore's Law handle "efficiency"?

That's a fair point Edward,

Ah, but is it? As I understand it, Moore's Law is an observation
not about performance or efficiency but about the number of
transistors on a chip. For many years chip designers *have* been
able to translate more transistors into faster processor speed, but
again as I understand it such improvements have rather stalled in
the past few years, with the focus shifting to using the additional
transistors to provide multiple processing elements per chip, in
the hope of getting better overall processing through parallelism
rather than through increases in single-processor speed.

Which may be more or less the point you were making in the rest of
your post.

however I am highly interested in exploring
techniques that allow software to have excellent scalability, throughput and
performance characteristics on multi-processor systems. If the algorithm
does not scale well, then it's basically dead in the water wrt upcoming
many-core systems.


IMHO, it's not really enough anymore to simply think in terms of `faster
clock rate's = faster software'. Instead, you need to think about how your
software can possibly scale up and adapt to a new system that might have 5
to 10 times the number of processors that you are normally accustomed to
working with.

Quite.

[ snip ]

http://www.gotw.ca/publications/concurrency-ddj.htm

On a quick skim, the author of the above seems to be confirming my
impressions described above.

[ snip ]

 

[Nick Keighley]

spinoza1111 wrote:

Formal software proofs of the type that you mention rattled around
30+ years ago as a good idea had conceptual fatal flaws.

Could you give a short summary. Or is it not amenable to that?

my understanding (very slight and very dated) was that proving an
existing pogram correct was insuperably difficult. But constructing a
correct program from a formal requirement was a reasonable thing to
do. Though if your requirement notation was rich enough to describe
your problem you could argue you'd already written a program...

Aren't things like VDM and Z still floating around?

John Bentley's "Programming Pearls" (two mentions in a day) constructs
a quick sort program using formal arguments.

Even if formal proofs don't work they are handy to have the concepts
at the back of your mind. When will this loop terminate? What
invarient is this data structure supposed to maintain? OO could be
thought of as maintaining invariants.

Update your
reading, I suggest starting with papers on mechanical reliability that
were  being published about a 100 years ago.

do you have a suggested starting point?

 

[Nick Keighley]

spinoza1111wrote:

Formal software proofs of the type that you mention rattled around
30+ years ago as a good idea had conceptual fatal flaws. Update your
reading, I suggest starting with papers on mechanical reliability that
were  being published about a 100 years ago.

What were those fatal flaws?

It was thought that the proof might have an error.
[...]

Furthermore, nobody understood Dijsktra's point: that the proof could
be developed alongside the program.

except for you of course!

Also, I'd add that a properly constructed software walkthrough is a
venue for the presentation of software correctness proofs in ordinary
language.

I'm not so sure about ordinary language. Mathematicians invented their
notations for a reason.

Nobody can "prove" that a real system won't fail. The Airbus A320's
"fly by wire" avionics system is software designed to make sure the
A320 doesn't go outside its performance limits:

airbus don't prove their programs formally correct. Or they didn't
used to. Several UK comp.sci people got quite hot under the collar
about it.

if the pilot pulls up
the "stick" (which is no longer a stick at all)

I've seen more impressive joy sticks on the average games machine.

Unlike Dijkstra, I think that English used well, and uninterrupted by
thugs, is a form of correctness proof, even a comment that says
clearly what a module does when read alongside the code.

I try to put those sorts of comment in. And there's assert() the ghost
of formal methods.

 

[Nick Keighley]

On Feb 4, 6:33 pm, Nick Keighley <[email protected]>


This looks very interesting. Did you write this book? I might get it.

I'm almost flattered...
No, I have no connection with the book or its author except that I've
read it.

 

[Michael Foukarakis]

Could you give a short summary. Or is it not amenable to that?

my understanding (very slight and very dated) was that proving an
existing pogram correct was insuperably difficult. But constructing a
correct program from a formal requirement was a reasonable thing to
do. Though if your requirement notation was rich enough to describe
your problem you could argue you'd already written a program...

From what I remember, proving a given program correct was equivalent
to solving the halting problem. Nevertheless, a team of researchers
some time ago (under Gernot Heiser, iirc) claimed to have proven a
7,5k LOC kernel formally correct in about 250 LOC per man-year. Linux
& Windows probably have more than 50 MLOC, which would take something
like 200.000 years to verify, assuming no increased complexity from,
well, the increased complexity..

 

[Walter Banks]

Could you give a short summary. Or is it not amenable to that?

The basic science behind proof of software correctness is that
if software correct then it will never fail. A good idea.

System reliability is determining when system will fail to produce
the expected result. At the end of the industrial revolution and at the
beginning of the 20th century a whole body of math was developed
to describe system reliability. This calculus can be applied to any
system and is used to determine life and failure expectancy of
components in a system. Much of this math depends on the
organization of component parts. (Redundancy helps a lot)

Spinoza father's quote covers life expectancy of software
but not its failure modes in this calculus.

Software correctness immediately produced a flurry of
implementation approaches. The fatal flaw was that when the
approaches were examined as a system the software proofs
were less reliable than the reliably of the software they were
testing resulting in inconclusive results.

Regards,

walter..

 

[Walter Banks]

From what I remember, proving a given program correct was equivalent
to solving the halting problem. Nevertheless, a team of researchers
some time ago (under Gernot Heiser, iirc) claimed to have proven a
7,5k LOC kernel formally correct in about 250 LOC per man-year. Linux
& Windows probably have more than 50 MLOC, which would take something
like 200.000 years to verify, assuming no increased complexity from,
well, the increased complexity..

A conservative estimate, it isn't a linear problem,

Regards,

w..

 

[spinoza1111]

The basic science behind proof of software correctness is that
if software correct then it will never fail. A good idea.

System reliability is determining when system will fail to produce
the expected result. At the end of the industrial revolution and at the
beginning of the 20th century a whole body of math was developed
to describe system reliability. This calculus can be applied to any
system and is used to determine life and failure expectancy of
components in a system. Much of this math depends on the
organization of  component parts. (Redundancy helps a lot)

Spinoza  father's quote covers life expectancy of software
but not its failure modes in this calculus.

Software correctness immediately produced a flurry of
implementation approaches. The fatal flaw was that when the
approaches were examined as a system the software proofs
were less reliable than the reliably of the software they were
testing resulting in inconclusive results.

You don't want to automate or support with software the proofs. You
want something that multiplies the probability of failure by n >=
1e-10, that reduces it in other words by at least an order of
magnitude, and the probability of errors in the proof software works
against this.

This is why you need to do formal or informal software correctness
proofs in a humanistic structured walkthrough from which assholes have
been excluded, using a whiteboard and not even using
videoconferencing; the use of video conferencing in the Morton Thiokol
review of Challenger O-rings caused key messages, including "think
like a manager and not an engineer" to be made offline, where the
managers allowed themselves to speak deviantly offline (cf Vaughan
1999
http://www.amazon.com/Challenger-La...=sr_1_1?ie=UTF8&s=books&qid=1265297165&sr=8-1).

 

[spinoza1111]

From what I remember, proving a given program correct was equivalent

That is not correct. The Halting Problem is a proof that a Turing
Machine cannot be constructed that will be able to detect whether any
other TM will halt. Whereas programs can be proven correct (for much
the same reason we proved the negative truth of the Halting Problem).

It's amazing that in "break room [or Hooters] bullshit sessions",
programmers have in my experience regularly confused "writing a proof
that a program is correct" with "writing a program that can determine
algorithmically whether another program is correct". The latter is an
instance of the Halting problem. The former is applied mathematics.

Indeed, there is (probably?) no such thing as a correct program that
cannot be proven correct, especially if we're mathematical
intuitionists or pragmatists. If the "halting problem" on the Toyota
is traced to software then program correctness proving may get new
life.

[I really miss the late Dik Winter, familiar to many readers here.
He'd jump me using a Dutch rule: if you speak of things that come from
Holland, such as Intuitionism, you'd better be Dutch. Otherwise you
probably don't understand them. A variant in fine of what
Shakespeare's Captain MacMorris says in Henry V: what is my nation?]

For all sorts of correctness proofs of programs see the Edsger W
Dijkstra archive: http://www.cs.utexas.edu/users/EWD.

"Beware of 'the real world'. A speaker's appeal to it is always an
invitation not to challenge his tacit assumptions. When a speaker
refers to the real world, a useful counterploy is pointing out that he
only refers to HIS perception of it. We find it nowadays hyphenated in
'real-world problems'; please remember that those are typically the
ones we are left with when we have refused to apply their effective
solutions."

Edsger W Dijkstra, 1982

to solving the halting problem. Nevertheless, a team of researchers
some time ago (under Gernot Heiser, iirc) claimed to have proven a
7,5k LOC kernel formally correct in about 250 LOC per man-year. Linux
& Windows probably have more than 50 MLOC, which would take something
like 200.000 years to verify, assuming no increased complexity from,
well, the increased complexity..

This reasoning is absurd. Dijkstra had a lot of laughs at its expense:

"We have shown her representatives what measures we had taken, such as
our ISAPS (Interactive Semi-Automatic Proof System) and even the more
impressive TDF (Theory Development Facility). The first one enables an
average mathematician to increase his proof productivity from 30 to 60
lines a month, the second one allows a mathematician with a minimum of
skills to produce up to a 100 times as much text as he has keyed in."

The silliness is imposing bureaucracy, bullshit and bullying on
software development. If you force the programmers to check a working
if at first minimal system at 5:00 PM every day, along with an
informal correctness proof in the form of minutes of a 4:00 PM
structured walkthrough, you'd have your OS in about the same amount of
time...simply by not dividing the work of proving from that of coding,
an alienation which is based on a silly respect for specialization and
a contempt for humanity.