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

changed claudio's english, added bib file

Location:
Deliverables/D4.2-4.3/reports
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1437 r1438  
    336336\item
    337337The compiler is buggy, or an invariant in the compiler is invalidated.
    338 \item Some non complete heuristics in the compiler fails.
    339 \item The compiled code exhausts some bounded resource, tipically the
    340 processor's code memory.
     338\item
     339An incomplete heuristic in the compiler fails.
     340\item
     341The compiled code exhausts some bounded resource, for instance the processor's code memory.
    341342\end{enumerate}
    342 Standard compilers can fail for all the above reasons. Certified compilers
    343 are only required to rule out the second class of failures, but they can
    344 still fail for all other reasons. In particular, a compiler that systematically
    345 refuses to compile any well formed program is a sound compiler. On the contrary,
    346 we would like our certified compiler to fail only in the fourth case. We
    347 plan to achieve this aim using the following strategy. First of all,
    348 the compiler is abstracted over all non complete heuristics, seen as total
    349 functions. To obtain an executable code, the compiler is eventually composed
    350 with implementations of the strategies, and the composition takes care of the
    351 possibility that the heuristics can fail to find a solution. Secondly,
    352 we will reject all malformed programs using dependent types:
    353 only well-formed programs should typecheck and the compiler can be applied only
    354 to well-typed programs. Finally, exhaustion of bounded resources can be checked
    355 only at the very end of the compilation. Therefore, all intermediate compilation
    356 steps are now total functions that cannot diverge, nor fail: these properties
    357 are directly guaranteed by the type system of Matita.
    358 
    359 At the moment, the plan has not been fulfilled, and we are improving the code
    360 according to the plan by progressively strenghthening the code by means of
    361 dependent types. We now detail the different ways in which dependent types
    362 have been exploited so far.
     343Standard compilers can fail for all the above reasons.
     344Certified compilers are only required to rule out the second class of failures, but they can still fail for all the remaining reasons.
     345In particular, a compiler that systematically refuses to compile any well formed program is a sound compiler.
     346On the contrary, we would like our certified compiler to fail only in the fourth case.
     347We plan to achieve this with the following strategy.
     348
     349First, the compiler is abstracted over all incomplete heuristics, seen as total functions.
     350To 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.
     351
     352Second, 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.
     353
     354Finally, exhaustion of bounded resources can be checked only at the very end of compilation.
     355Therefore, all intermediate compilation steps are now total functions that cannot diverge, nor fail: these properties are directly guaranteed by the type system of Matita.
     356
     357Presently, the plan is not yet fulfilled.
     358However, we are improving the implemented code according to our plan.
     359We are doing this by progressively strenghthening the code through the use of dependent types.
     360We detail the different ways in which dependent types have been used so far.
    363361
    364362First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions.
     
    401399In 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.
    402400
    403 Moreover, at the moment we make practically no use of inductive predicates
    404 to specify compiler invariants and to describe the semantics of intermediate
    405 languages. On the contrary, all predicates are computable functions. Therefore,
    406 the proof style that we will adopt will be necessarily significantly different
    407 from, say, CompCert's one. At the moment, in Matita ``Russell-''-style reasoning
    408 (in the sense of~\cite{sozeauXXX}) seems to be the best solution to work on
    409 computable functions. This style is heavily based on the idea that all
    410 computable functions should be specified using dependent types to describe
    411 their pre and post-conditions. As a consequence, it is natural to add
    412 dependent types almost everywhere in the code.
     401Moreover, at the moment we make practically no use of inductive predicates to specify compiler invariants and to describe the semantics of intermediate languages.
     402On the contrary, all predicates are computable functions.
     403Therefore, the proof style that we will adopt will be necessarily significantly different from, say, CompCert's one.
     404At 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.
     405This style is heavily based on the idea that all computable functions should be specified using dependent types to describe their pre- and post-conditions.
     406As a consequence, it is natural to add dependent types almost everywhere in the Matita compiler's codebase.
    413407
    414408%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
     
    694688\end{center}
    695689
     690\bibliographystyle{alpha}
     691\bibliography{report}
     692
    696693\end{document}
Note: See TracChangeset for help on using the changeset viewer.