Re: Compiler Correctness

Sid Touati wrote:


> As example, suppose that the compiler executes on a 32 bits machine
> and generates a code for a 64 bits machine. If the compiler makes
> static constant propagation, it makes arithmetic computation on the
> 32 bit machine. This would not give you the same result if you
> generate the code on the 64 bits machines.


When two cross compilers, on arbitrary machines, produce the same
instructions for a third machine, they also must produce the same
constant argument values.


Provided that your 32 bit cross compiler code will (deterministically)
produce the same instructions, regardless of it's host machine, it also
must produce the same constant values, regardless of (the arithmetic of)
the host machine.


Otherwise a proof of the correctness of any program must take into
account the detailed behaviour of the host machine, and then is valid
only for that specific machine. IMO it's much simpler to write
machine-independent compiler code, instead of proofing the behaviour of
machine-dependent code, for every new host machine ;-)


>
> We can imagine more complex cases with floating point computations...


That's a different thing, because in floating point computations the
least significant bits can be lost at any time, whereas a loss of the
most significant bits in integral values definitely are overflow
errors. Just the mapping of literal floating point constants, from
source code into binary values, can be affected by the arithmetic of
the host machine, and all these representations may be correct, within
the inevitable and acceptable deviations for floating point operations
and values. The numerical stability of floating point algorithms, as
implemented in the source code of the compiler input, is not of
concern in a proof of the correctness of the compiler itself.


DoDi
[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]

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