> Translation validation can be used even with a compiler that sometimes generates incorrect code, as long as this incorrect does not manifest itself for a given program. Depending on the input program the translation validation can fail (because the generated code is wrong or the translation validation technique is too weak to show correctness). However, if translation validation succeeds, then the compiled program is guaranteed to be correct for all inputs.
I don't remember where I read this, but I think there are some examples in practice where instead of proving the correctness of some optimizations of existing C compilers (which is a codebase that keeps evolving), there have been situations where the correctness was ensured using program equivalence checking. So you'd "freeze" the reference compiler and the equivalence checker (which would be qualified), and pair that with an upstream compiler with sophisticated optimizations. So long as the equivalence checker keeps passing, you're golden.
> I don't remember where I read this, but I think there are some examples in practice where instead of proving the correctness of some optimizations of existing C compilers (which is a codebase that keeps evolving), there have been situations where the correctness was ensured using program equivalence checking.
This is what CompCert does (or at least did when I last looked inside CompCert) for register allocation; the graph colouring algorithm is unverified, but a verified validator is used to check the colouring is correct.
Whilst this is relatively straightforward for something like graph colouring, it is substantially more difficult for comparing the outputs of two different compilers, which I think is what you are suggesting here?
There was some work to do a translation validation for the entire RTL -> LTL pass of CompCert, but I'm not sure how much progress was made or if this is currently used.
I guess to me I see that as isomorphic; you're still qualifying the output, even if there's an intermediate step involved. The path towards qualifying the output of the sophisticated compiler may be more indirect, but you're still doing it.
> Translation validation can be used even with a compiler that sometimes generates incorrect code, as long as this incorrect does not manifest itself for a given program. Depending on the input program the translation validation can fail (because the generated code is wrong or the translation validation technique is too weak to show correctness). However, if translation validation succeeds, then the compiled program is guaranteed to be correct for all inputs.
I don't remember where I read this, but I think there are some examples in practice where instead of proving the correctness of some optimizations of existing C compilers (which is a codebase that keeps evolving), there have been situations where the correctness was ensured using program equivalence checking. So you'd "freeze" the reference compiler and the equivalence checker (which would be qualified), and pair that with an upstream compiler with sophisticated optimizations. So long as the equivalence checker keeps passing, you're golden.