llvm dev - Jul 2006 - [LLVMdev] Correctness of Optimization Phases

>> I may sound stupid but can someone tell me that after applying
>> optimization sequences randomly whether we can surely say that the
>> final output is correct?
>
> Answering this question is equivalent to solving the Halting Problem.
Prooving correctness of a compiler is really an NP problem. This goes for 
any compiler backend. All you can do is have enough test cases.

Aaron

> Prooving correctness of a compiler is really an NP problem. This goes for
> any compiler backend. All you can do is have enough test cases.
No. To be in NP it would be necessary for a Non-deterministic
Polynomial algorithm to exist. There is no such algorithm. The problem
is undecidable.

It doesn't means that it is impossible to prove the correctness of a
compiler. It means that no algorithm can do it.
>From a practical point of view, I think that the original question was:
Are the different optimizations "expected" to work in any order or do
they have some inter dependencies?
(I don't know the answer)
> Aaron
Rafael

On Tue, 18 Jul 2006, [UTF-8] Rafael Esp?ndola wrote:
>> From a practical point of view, I think that the original question was:
>
> Are the different optimizations "expected" to work in any order
or do
> they have some inter dependencies?
> (I don't know the answer)
There are some interdependencies, which they self enforce.

To put it another way any list of optimizations specified to 'opt' is 
expected to produce good code and not crash, if you stick to supported 
optimizations (e.g. those run by gccas or gccld).

-Chris

-- 
http://nondot.org/sabre/
http://llvm.org/

>> Prooving correctness of a compiler is really an NP problem. This goes
for
>> any compiler backend. All you can do is have enough test cases.
> No. To be in NP it would be necessary for a Non-deterministic
> Polynomial algorithm to exist. There is no such algorithm. The problem
> is undecidable.
Thanks for putting me right.
> It doesn't means that it is impossible to prove the correctness of a
> compiler. It means that no algorithm can do it.
Formal proof using Z would probably be the best means of attack.
>>From a practical point of view, I think that the original question was:
>
> Are the different optimizations "expected" to work in any order
or do
> they have some inter dependencies?
> (I don't know the answer)
Yes.

Testing non optimized test programs against optimized either using JIT or a 
set platform might be a way forward.

Another means of attack might be an approach simular to generative fuzzing.

Aaron