Re: pitfalls of verifying floating-point computations

[David Monniaux <David.Monniaux@xxxxxx>]

> With all respect to the authors of that paper (who are very good),
> they are completely deluded in this respect.  Even if we ignore all
> of the double rounding, association and similar issues, there is a
> fundamental, mathematically unavoidable problem that any program
> that involves true asynchronicity (including BOTH serial real-time
> programs with unserialised event streams and parallel code) will
> NECESSARILY produce non-reproducible floating-point results.
>
> And most large, important programs involve one or the other!
Hi
I'm the author of the paper that you're discussing. :-)

I spent the last 6 or so years building static analysis tools, mostly
for the aerospace industry (we've been involved in the Airbus A340 and
A380 programs, most notably for their fly-by-wire controls). A large
share of the work dealt with a the massive number of floating-point
computations (filters etc.) involved. See http://www.astree.ens.fr

Depending on the industry, and the locale, some of the critical systems
are written with synchronous programming languages, a simplified view of
which is a program that takes streams of inputs, with one vector of
inputs per clock tick, and produces streams of outputs. There are no
unserializerd event streams and no parallel code. These kind of
synchronous systems are prized for their predictibility, because a given
sequence of inputs should always produce the same sequence of outputs.

In addition, even in systems with parallel code, unserialized inputs
etc., there are generally library portions (e.g. numerical algorithms)
that can be analyzed independently of i/o and parallelism.

The existence of systems (compiler + ABI + libraries + processors) where
the results of computations depend on vagaries such as register
allocation or optimizations hinders such simple things as unit testing
with debugging code that can be turned on and off. It also breaks formal
methods that expect that variables do not change for no visible reason.

The thing is, most people in the industry are not aware of these kinds
of issues. It is one thing to discuss "well known" problems between
specialists, but what good is it if people in the general industry
believe things work in a way that they do not?

So, I do not think I am deluded in suggesting that computations should
be reproducible independently of whether or not somebody inserted a
printf() in the code. :-)

Regards
DM