Re: Compiler Correctness

Hans-Peter Diettrich <DrDiettrich@compuserve.de>
14 Feb 2006 17:48:22 -0500

          From comp.compilers

Related articles
[9 earlier articles]
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Xavier.Leroy@inria.fr (Xavier Leroy) (2006-02-12)
Re: Compiler Correctness DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-02-14)
Re: Compiler Correctness marcov@stack.nl (Marco van de Voort) (2006-02-14)
Re: Compiler Correctness DrDiettrich@compuserve.de (Hans-Peter Diettrich) (2006-02-14)
Re: Compiler Correctness henry@spsystems.net (2006-02-17)
Re: Compiler Correctness henry@spsystems.net (2006-02-17)
Re: Compiler Correctness Sid.Touati@inria.fr (Sid Touati) (2006-02-17)
Re: Compiler Correctness gah@ugcs.caltech.edu (glen herrmannsfeldt) (2006-02-17)
Re: Compiler Correctness ingo.stuermer@gmx.de (=?iso-8859-1?Q?Ingo_St=FCrmer?=) (2006-04-27)
| List of all articles for this month |

From: Hans-Peter Diettrich <DrDiettrich@compuserve.de>
Newsgroups: comp.compilers
Date: 14 Feb 2006 17:48:22 -0500
Organization: Compilers Central
References: 06-02-053 06-02-061 06-02-078 06-02-093
Keywords: arithmetic, comment

The moderator nattered:


> [Where I come from, with a given floating point arithmetic model,
> there is only one correct result for each operation and one correct
> representation for each input value. The ambiguities arise when a
> compiler can use more than one possible sequence of operations to
> evaluate an expression. -John]


Most languages allow the compiler some freedom in the evaluation of
expressions, including CSE and reordering of instructions and arguments.
What does this mean, with regards to the correctness of compilers for
such languages?


Ambiguities also can arise from different models or precision, as
implemented in specific FPU hardware. Doesn't this imply that a correct
compiler must emulate all floating point operations, so that the output
does not depend on the host machine of the compiler? The same for all
the target machines of an cross compiler...


The operation of the Intel coprocessor (x87) is configurable, and this
configuration can be changed at runtime. In this case a "correct"
compiler has to assure that, after every call to external code, the FPU
configuration is restored to the expected state.


At least these points should be considered in a proof of the correctness
of any program, including compilers.


DoDi
[You're right, some languages permit multiple floating point models. -John]


Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.