Changeset 1438

Ignore:
Timestamp:
Oct 21, 2011, 5:36:38 PM (8 years ago)
Message:

changed claudio's english, added bib file

Location:
Deliverables/D4.2-4.3/reports
Files:
 r1437 \item The compiler is buggy, or an invariant in the compiler is invalidated. \item Some non complete heuristics in the compiler fails. \item The compiled code exhausts some bounded resource, tipically the processor's code memory. \item An incomplete heuristic in the compiler fails. \item The compiled code exhausts some bounded resource, for instance the processor's code memory. \end{enumerate} Standard compilers can fail for all the above reasons. Certified compilers are only required to rule out the second class of failures, but they can still fail for all other reasons. In particular, a compiler that systematically refuses to compile any well formed program is a sound compiler. On the contrary, we would like our certified compiler to fail only in the fourth case. We plan to achieve this aim using the following strategy. First of all, the compiler is abstracted over all non complete heuristics, seen as total functions. To obtain an executable code, the compiler is eventually composed with implementations of the strategies, and the composition takes care of the possibility that the heuristics can fail to find a solution. Secondly, we will reject all malformed programs using dependent types: only well-formed programs should typecheck and the compiler can be applied only to well-typed programs. Finally, exhaustion of bounded resources can be checked only at the very end of the compilation. Therefore, all intermediate compilation steps are now total functions that cannot diverge, nor fail: these properties are directly guaranteed by the type system of Matita. At the moment, the plan has not been fulfilled, and we are improving the code according to the plan by progressively strenghthening the code by means of dependent types. We now detail the different ways in which dependent types have been exploited so far. Standard compilers can fail for all the above reasons. Certified compilers are only required to rule out the second class of failures, but they can still fail for all the remaining reasons. In particular, a compiler that systematically refuses to compile any well formed program is a sound compiler. On the contrary, we would like our certified compiler to fail only in the fourth case. We plan to achieve this with the following strategy. First, the compiler is abstracted over all incomplete heuristics, seen as total functions. To obtain executable code, the compiler is eventually composed with implementations of the abstracted strategies, with the composition taking care of any potential failure of the heuristics in finding a solution. Second, we reject all malformed programs using dependent types: only well-formed programs should typecheck and the compiler can be applied only to well-typed programs. Finally, exhaustion of bounded resources can be checked only at the very end of compilation. Therefore, all intermediate compilation steps are now total functions that cannot diverge, nor fail: these properties are directly guaranteed by the type system of Matita. Presently, the plan is not yet fulfilled. However, we are improving the implemented code according to our plan. We are doing this by progressively strenghthening the code through the use of dependent types. We detail the different ways in which dependent types have been used so far. First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions. In contrast, we wish to make as much use of dependent types as possible, both to experiment with different ways of encoding compilers in a proof assistant, but also as a way of stress testing' Matita's support for dependent types. Moreover, at the moment we make practically no use of inductive predicates to specify compiler invariants and to describe the semantics of intermediate languages. On the contrary, all predicates are computable functions. Therefore, the proof style that we will adopt will be necessarily significantly different from, say, CompCert's one. At the moment, in Matita Russell-''-style reasoning (in the sense of~\cite{sozeauXXX}) seems to be the best solution to work on computable functions. This style is heavily based on the idea that all computable functions should be specified using dependent types to describe their pre and post-conditions. As a consequence, it is natural to add dependent types almost everywhere in the code. Moreover, at the moment we make practically no use of inductive predicates to specify compiler invariants and to describe the semantics of intermediate languages. On the contrary, all predicates are computable functions. Therefore, the proof style that we will adopt will be necessarily significantly different from, say, CompCert's one. At the moment, in Matita Russell-'-style reasoning (in the sense of~\cite{sozeau:subset:2006}) seems to be the best solution for working with computable functions. This style is heavily based on the idea that all computable functions should be specified using dependent types to describe their pre- and post-conditions. As a consequence, it is natural to add dependent types almost everywhere in the Matita compiler's codebase. %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-% \end{center} \bibliographystyle{alpha} \bibliography{report} \end{document}