Re: Compiler Correctness

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]

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