3 ms·
> In CompCert's case though, the register allocation verifier itself is verified. I don't think so, I think moonchild's account of it is accurate. At least, it
by MaxBarraclough 6y ago
> In CompCert's case though, the register allocation verifier itself is verified.
I don't think so, I think moonchild's account of it is accurate. At least, it was accurate in 2012. From a 2012 blog post: [0]
> In CompCert, this algorithm is not proven correct. Instead, after generating the graph, the compiler calls an OCaml implementation of IRC and then checks that the coloring is valid. If the checker confirms that the coloring is valid, the compiler uses it and proceeds along. If it does not confirm that it's valid, compilation is aborted. This checker is proven correct, and because it is simpler, its proof of correctness is easier.
[0] http://gallium.inria.fr/blog/register-allocation/ http://gallium.inria.fr/blog/register-allocation/
- fuklief 6y agoBy "register allocation verifier", I meant the checker as mentioned in the post you quote.
- archi42 6y ago> This checker is proven correct, and because it is simpler, its proof of correctness is easier. Still correct ;) What I belief GP (fuklief) meant was: The SMT solver might still be incorrect. Like the register allocator itself in CompCert. But for CompCert, the result is checked by a formally verified checker. I do not know if that's true or not for the result of the SMT solver.
- creata 6y agoDon't SMT solvers output proof objects so that the results can be easily independently verified?
- syrak 6y agoEven if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.