lua-users home
lua-l archive

[Date Prev][Date Next][Thread Prev][Thread Next] [Date Index] [Thread Index]


[Sorry for not threading... I read via the Digest...]

G'day,

There is only one way to understand of the abstract machines which
is a contract between you and the system, brokered by the programming
language, OS libraries etc.

If some operation is defined to be "undefined", and a client performs
that operation, then there is only one way to understand the entire
remainder of the OS environment/program/process/acquired resources/
whatever:

      ABSOLUTELY ALL BETS ARE OFF.

      THERE IS NO GUARANTEE THAT ANY, ABSOLUTELY ANY, FURTHER
      OPERATION OF THE SYSTEM WILL BEHAVE AS EXPECTED.

Even if, for some reason, the underlying implementation happens
to act in some way that the undefined operation "seems" to be okay...
this is still a time-bomb ticking for the remainder of the life of
the system, with the potential to go off at any time.

By breaking the "contract" between you and the language+environment,
such contract being specified explicitly via the Reference Manual,
you cannot rely on the contract at all from the breakage point
onwards, for any purpose whatever.

Another common trap is to read too much into the contract.  This
tends to happen when you want performance guarantees from the
system, but such guarantees are not spelt out in the contract.

--

I recall a presentation by Gerard Holzmann, of JPL Laboratory for
Reliable Software, on how they wrote about 3.8 million lines of
code, primarily in C, and successfully landed and then operated
the Curiosity Rover on the surface of the planet.  Note how they
first enabled ALL warnings, then turned ALL warnings into errors,
then tightened the screws even further to demand "pedantic"
conformation of the code to the chosen C Standard.  They also
ran several other static and dynamic checks (Valgrind, Code Sonar
and others) every night to check the quality of the codebase.

Some diagnostics were triaged to be ignored, as being "the tool
has not traced the situation sufficiently well, and we know that
its diagnostic is spurious", but in almost all cases, the team
started from a default of "If the tool's nervous about the code,
then rewrite the code to eliminate the diagnostic"; in a few
cases, the author disagreed with the diagnostic, and then a
review (author + 1-2 others?) had a meeting to discuss the
validity and the handling of the defect reported by the automated
tool -- if decided to be a false positive, then the triage
database was updated for the specific tool, to suppress the
spurious diagnostic:

        Mars Code - Gerard Holzmann, JPL Laboratory for Reliable Software

        https://www.youtube.com/watch?v=16dQLBgOwbE

--

So, the only correct response is:

        Any and all valid programs must never, never depend
        on undefined behaviour at any point whatsoever.

--

cheers,

sur-behoffski (Brenton Hoff)
programmer, Grouse Software