Changeset 3109


Ignore:
Timestamp:
Apr 9, 2013, 5:28:39 PM (4 years ago)
Author:
sacerdot
Message:

New version.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D5.2/report.tex

    r3108 r3109  
    161161\end{verbatim}
    162162
    163 \begin{figure}[b]
     163\begin{figure}[t]
    164164\begin{verbatim}
    165165char a[] = {3, 2, 7, -4};
     
    180180\end{figure}
    181181
    182 \begin{figure}
     182\begin{figure}[!p]
    183183\begin{verbatim}
    184 int __cost = 0;
    185 
    186 int __stack_size = 0, __stack_size_max = 0;
     184int __cost = 33;
     185
     186int __stack_size = 5, __stack_size_max = 5;
    187187
    188188void __cost_incr(int incr) {
     
    616616   types~\cite{christinexx}. The calculi implemented by Coq and Matita, however,
    617617   are more expressive than CoC, and several type constructions have no
    618    counterparts in System $F\_omega$. Moreover, core OCaml does not even
    619    implement $F\_omega$, but only the Hindley-Milner fragment of it.
     618   counterparts in System $F_\omega$. Moreover, core OCaml does not even
     619   implement $F_\omega$, but only the Hindley-Milner fragment of it.
    620620   Therefore, in all situations listed below, code extraction is not able to
    621621   type the extracted code using informative types, but it uses the
     
    642642   \item Case analysis and recursion over inhabitants of primitive inductive
    643643    types can be used in types (strong elimination), which is not allowed in
    644     $F\_omega$. In the CerCo compiler we largely exploit type formers declared
     644    $F_\omega$. In the CerCo compiler we largely exploit type formers declared
    645645    in this way, for example to provide the same level of type safety achieved
    646646    in the untrusted compiler via polymorphic variants~\cite{guarriguesxx}.
     
    659659    (pseudo)-registers for back-end languages --- some terms working on the
    660660    type --- e.g. functions to set/get values from (pseudo)-registers --- and
    661     properties over them. In System $F\_omega$ terms and types abstractions
     661    properties over them. In System $F_\omega$ terms and types abstractions
    662662    are kept syntactically separate and there is no way to pack them in
    663663    records.
     
    683683 \item We already have a prototype that extracts code from Matita to GHC plus
    684684  several extensions that allow GHC to use a very large subset of System
    685   $F\_omega$. However, the prototype is not fully functional yet because we
     685  $F_\omega$. However, the prototype is not fully functional yet because we
    686686  still need to solve at the theoretical level a problem of interaction
    687   between $F\_omega$ types and strong elimination. Roughly speaking, the
     687  between $F_\omega$ types and strong elimination. Roughly speaking, the
    688688  two branches of a strong elimination always admit a most general unifier in
    689689  Hindley-Milner plus the super-type \texttt{Obj.magic}, but the same property
    690   is lost for $F\_omega$. As a consequence, we loose modularity in code
     690  is lost for $F_\omega$. As a consequence, we loose modularity in code
    691691  extraction and we need to figure out static analysis techniques to reduce
    692692  the impact of the loss of modularity.
     
    712712\end{itemize}
    713713
    714 \subsection{Connection with other deliverables}
     714\section{The Cost-Annotating Plug-In}
     715
     716The functionalities of the Cost Annotating Plug-In have already been described
     717in Deliverables~D5.1 and D5.3.
     718The plug-in interfaces with the CerCo compiler via
     719the command line. Therefore there was no need to update the plug-in code for
     720integration in the Trusted CerCo Prototype. Actually, it is even possible
     721to install at the same time the untrusted and the trusted compilers. The
     722\texttt{-cost-acc} flag of the plug-in can be used to select the executable
     723to be used for compilation.
     724
     725The code of the plug-in has been modified w.r.t. D5.1 in order to take care
     726also of the cost model for stack-size consumption. From the user point of view,
     727time and space cost annotations and invariants are handled in a similar way.
     728Nevertheless, we expect automated theorem provers to face more difficulties
     729in dealing with stack usage because elapsed time is additive, whereas what
     730is interesting for space usage is the maximum amount of stack used, which is
     731not additive. On the other hand, programs produced by our compiler require
     732more stack only at function calls. Therefore the proof obligations generated
     733to bound the maximum stack size for non recursive programs are trivial.
     734Most C programs, and in particular those used in time critical systems, avoid
     735recursive functions.
     736
     737\section{Connection with other deliverables}
    715738\label{subsect.connection.other.deliverables}
    716739
    717 This deliverable is based on all the work previously done in CerCo.
    718 The software delivered links together most of the software already developed in
    719 previous deliverables.
    720 
    721 The executable formal semantics of C and machine code (Deliverables D3.1 and
    722 D4.1)
    723 
    724 TO BE COMPLETED
     740This deliverable represents the final milestone of the CerCo project.
     741The software delivered links together most of the software already developed
     742in previous deliverables, and it benefits from the studies performed in
     743other deliverables. In particular:
     744
     745\begin{itemize}
     746 \item The compiler links the code extracted from the executable formal
     747  semantics of C (D3.1), machine code (D4.1), front-end intermediate languages
     748  (D3.3) and back-end intermediate languages (D4.3). The \texttt{-is} flag
     749  of the compiler invokes the semantics of every intermediate
     750  representation of the program to be compiled. The executability of the
     751  C and machine code languages has been important to debug the the two
     752  semantics, that are part of the trusted code base of the compiler.
     753  The executability of the intermediate languages has been important during
     754  development for early detection of bugs both in the semantics and in the
     755  compiler passes. They are also useful to users to profile programs in early
     756  compilation stages to detect where the code spends more time.
     757  Those semantics, however, are not part of the trusted code base.
     758 \item The compiler links the code extracted from the CIC encoding of the
     759  Front-end (D3.2) and Back-end (D4.2). The two encodings have been partially
     760  proved correct in D3.4 (Front End Correctness Proof) and D4.4 (Back End
     761  Correctness Proof). The formal proofs to be delivered in those deliverables
     762  have not been completed. The most urgent future work after the end of the
     763  project will consist in completing those proofs.
     764 \item Debian Packages have been provided in D6.6 for the Cost-Annotating
     765  Plug-In, the Untrusted CerCo Compiler and the Trusted CerCo Compiler.
     766  The first and third installed together form a full installation of the
     767  Trusted CerCo Prototype. In order to allow interested people to test the
     768  prototype more easily, we also provided in D6.6 a Live CD based on
     769  Debian with the CerCo Packages pre-installed.
     770\end{itemize}
     771
    725772\end{document}
    726 
    727 XXXXXXXXX
    728 
    729 Deliverable D4.1 is an executable formal semantics of the machine code of our target processor (a brief overview of the processor architecture is provided in Section~\ref{sect.brief.overview.target.processor}).
    730 We provide an executable semantics in both O'Caml and the internal language of the Matita proof assistant.
    731 
    732 The C compiler delivered by Work Package 3 will eventually produce machine code executable by our emulator, and we expect that the emulator will be useful as a debugging aid for the compiler writers.
    733 Further, additional deliverables listed under Work Package 4 will later make use of the work reported in this document.
    734 Deliverables D4.2 and D4.3 entail the implementation of a formalised version of the intermediate language of the compiler, along with an executable formal semantics of these languages.
    735 In particular, Deliverable D4.3 requires a formalisation of the semantics of the intermediate languages of the compiler, and Deliverable D4.4 requires a formal proof of the correspondence between the semantics of these formalized languages, and the formal semantics of the target processor.
    736 The emulator(s) discussed in this report are the formalized semantics of our target processor made manifest.
Note: See TracChangeset for help on using the changeset viewer.