9
$\begingroup$

I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve written a small toy example. Therewith I can prove that my optimizations are correct. For example that additions with zero can be eliminated, i.e. expressions like "x + 0".

Are there optimizations that are difficult to perform with a regular compiler, that would serve as a good example? Is it possible to prove certain properties of a program that allow optimizations that are not possible to perform with a regular compiler? (i.e. without the inference that is possible with a theorem prover)

I would be interested in ideas or examples and also references on the topic.

A related question: Compiler correctness proofs

edit: As Tsuyoshi nicely put it in the comments: I am looking for optimization techniques which are difficult to implement if a compiler is written in (say) C but easier to implement if a compiler is written in (say) Coq. As Agda compiles to C (via haskell) it is possible to do everything that is possible in Agda also in C. Probably the only benefit of theorem provers like Coq/Agda is that the compiler and the optimizations can be verified.

edit2: As suggested by Vijay D I write what I've read so far. I mainly focused on Xavier Leroy and the CompCert project at INRIA (there is a 80 pages paper that is a good read, I think). A second interest was in the work of Anton Setzer on interactive programs. I though that perhaps his work could be used to prove properties about IO programs and bisimulation of IO programs. Thanks for mentioning Sewell. I've heard his talk "Tales from the jungle" at ICFP and read perhaps 2-3 of his papers. But I haven't specifically looked at his work and that of his coauthors.
I did not yet find out where to start or look for papers on optimizing compilers; e.g., which optimizations would be interesting to look at in the setting of a verified compiler.

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ “Are there optimizations that are difficult to perform with a regular compiler”: Isn’t that impossible? If I remove a proof of correctness from a verified compiler, I would get a regular compiler. Therefore, anything that a verified compiler can do can be done also by a regular compiler. The point of a verified compiler is that it cannot perform an optimization which is incorrect. (My knowledge about compilers and program verification is minimal. Excuse me if I am missing the point.) $\endgroup$ – Tsuyoshi Ito Jan 29 '13 at 17:26
  • $\begingroup$ @Tsuyoshi thank you for your comment. I meant: Can I prove certain properties (that are guaranteed to hold) for a program (e.g., a subroutine is non-entrant and can never call itself) that allow to perform optimizations that are not usually possible. Some invariants might be hard to verify for a program and perhaps these optimizations are not performed by commonly used compilers. But perhaps I am completely wrong. $\endgroup$ – mrsteve Jan 29 '13 at 18:40
  • 1
    $\begingroup$ Are you talking about a compiler written in Coq/Agda or a compiler for Coq/Agda? I thought that your question was about a compiler written in Coq/Agda, but then I do not think that a compiler written in Coq/Agda can prove any more properties about target programs than a compiler written in C. $\endgroup$ – Tsuyoshi Ito Jan 29 '13 at 18:45
  • 2
    $\begingroup$ It would be good to add what you have read to the question. Are you familiar with work on verified compilation - that of Xavier Leroy, for example? Or that of Peter Sewell and collaborators? $\endgroup$ – Vijay D Jan 30 '13 at 4:33
  • 1
    $\begingroup$ There are no such optimizations, unless you further restrict your question. In the extreme case the C compiler can secretly implement a theorem prover in its bowels (and most actually do it in a limited way). I think it is unclear what you mean by "regular compiler". $\endgroup$ – Andrej Bauer Feb 1 '13 at 17:20
5
+100
$\begingroup$

this paper by Yves Bertot, Benjamin Gr´egoire, and Xavier Leroy builds an optimizing compiler for a C-like language based purely on the Coq specification. some of this technology is apparently utilized in the CompCert C compiler.

A structured approach to proving compiler optimizations based on dataflow analysis

it considers the correctness of two optimizations, constant propagation (CP) and common subexpression elimination (CSE), section 4. these optimizations are more advanced than those that are associated with the non Coq-based compiler(s) for the same language. see eg this benchmark chart compared to gcc. (the Coq-based compiler is presumably slower to compile although this is rarely mentioned!)

An original aspect of ConCert is that most of the compiler is written directly in the Coq specification language, in a purely functional style. The executable compiler is obtained by automatic extraction of Caml code from this specification.

however at the end of the paper they do note that there are some compiler optimizations in real compilers that cant be modelled in their framework.

improved optimization is not the only element of consideration here, another aspect is that compiler optimization logic can be subject to subtle defects esp due to its complex nature. over the years gcc has been found to have bugs in its numerous optimization logic routines. eg gcc bug?

|cite|improve this answer
$\endgroup$
3
$\begingroup$

Can I prove certain properties (that are guaranteed to hold) for a program (e.g., a subroutine is non-entrant and can never call itself) that allow to perform optimizations that are not usually possible.

It is equivalent to extending the typechecker to provide some properties of a program to the optimizer. I believe Tsuyoshi Ito is right and you may be little misguided about Coq. It is great tool for providing a bug-less compiler, but in the case you describe, it does not provide more power to the static analyses.

The only thing I can think about strengthening static analyses with Coq, is to equip your language with assertions containing some user-written proofs. -- If the compiler itself would be translated into a language including a feather for dynamic typechecking, and if the user-written proofs would be convertible to functions, then it would be possible to apply those functions as prerequired properties for some subtypings or optimizations. -- This indeed, would provide more power to the compiler.

However, as far I can see, it would be rather useful for strengthening subtyping. -- It is hard to make a programmer to know, what property in what place would be helpful for the optimizer.

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.