Changeset 3109 for Deliverables/D5.2/report.tex

Timestamp:

Apr 9, 2013, 5:28:39 PM (8 years ago)

Author:

sacerdot

Message:

New version.

File:

• Deliverables/D5.2/report.tex (modified) (7 diffs)

Deliverables/D5.2/report.tex

@@ -161 +161 @@
 \end{verbatim}
 
-\begin{figure}[b]
+\begin{figure}[t]
 \begin{verbatim}
 char a[] = {3, 2, 7, -4};
@@ -180 +180 @@
 \end{figure}
 
-\begin{figure}
+\begin{figure}[!p]
 \begin{verbatim}
-int __cost = 0;
-
-int __stack_size = 0, __stack_size_max = 0;
+int __cost = 33;
+
+int __stack_size = 5, __stack_size_max = 5;
 
 void __cost_incr(int incr) {
@@ -616 +616 @@
    types~\cite{christinexx}. The calculi implemented by Coq and Matita, however,
    are more expressive than CoC, and several type constructions have no
-   counterparts in System $F\_omega$. Moreover, core OCaml does not even
-   implement $F\_omega$, but only the Hindley-Milner fragment of it.
+   counterparts in System $F_\omega$. Moreover, core OCaml does not even
+   implement $F_\omega$, but only the Hindley-Milner fragment of it.
    Therefore, in all situations listed below, code extraction is not able to
    type the extracted code using informative types, but it uses the
@@ -642 +642 @@
    \item Case analysis and recursion over inhabitants of primitive inductive
     types can be used in types (strong elimination), which is not allowed in
-    $F\_omega$. In the CerCo compiler we largely exploit type formers declared
+    $F_\omega$. In the CerCo compiler we largely exploit type formers declared
     in this way, for example to provide the same level of type safety achieved
     in the untrusted compiler via polymorphic variants~\cite{guarriguesxx}.
@@ -659 +659 @@
     (pseudo)-registers for back-end languages --- some terms working on the
     type --- e.g. functions to set/get values from (pseudo)-registers --- and
-    properties over them. In System $F\_omega$ terms and types abstractions
+    properties over them. In System $F_\omega$ terms and types abstractions
     are kept syntactically separate and there is no way to pack them in
     records.
@@ -683 +683 @@
  \item We already have a prototype that extracts code from Matita to GHC plus
   several extensions that allow GHC to use a very large subset of System
-  $F\_omega$. However, the prototype is not fully functional yet because we
+  $F_\omega$. However, the prototype is not fully functional yet because we
   still need to solve at the theoretical level a problem of interaction
-  between $F\_omega$ types and strong elimination. Roughly speaking, the
+  between $F_\omega$ types and strong elimination. Roughly speaking, the
   two branches of a strong elimination always admit a most general unifier in
   Hindley-Milner plus the super-type \texttt{Obj.magic}, but the same property
-  is lost for $F\_omega$. As a consequence, we loose modularity in code
+  is lost for $F_\omega$. As a consequence, we loose modularity in code
   extraction and we need to figure out static analysis techniques to reduce
   the impact of the loss of modularity.
@@ -712 +712 @@
 \end{itemize}
 
-\subsection{Connection with other deliverables}
+\section{The Cost-Annotating Plug-In}
+
+The functionalities of the Cost Annotating Plug-In have already been described
+in Deliverables~D5.1 and D5.3.
+The plug-in interfaces with the CerCo compiler via
+the command line. Therefore there was no need to update the plug-in code for
+integration in the Trusted CerCo Prototype. Actually, it is even possible
+to install at the same time the untrusted and the trusted compilers. The
+\texttt{-cost-acc} flag of the plug-in can be used to select the executable
+to be used for compilation.
+
+The code of the plug-in has been modified w.r.t. D5.1 in order to take care
+also of the cost model for stack-size consumption. From the user point of view,
+time and space cost annotations and invariants are handled in a similar way.
+Nevertheless, we expect automated theorem provers to face more difficulties
+in dealing with stack usage because elapsed time is additive, whereas what
+is interesting for space usage is the maximum amount of stack used, which is
+not additive. On the other hand, programs produced by our compiler require
+more stack only at function calls. Therefore the proof obligations generated
+to bound the maximum stack size for non recursive programs are trivial.
+Most C programs, and in particular those used in time critical systems, avoid
+recursive functions.
+
+\section{Connection with other deliverables}
 \label{subsect.connection.other.deliverables}
 
-This deliverable is based on all the work previously done in CerCo.
-The software delivered links together most of the software already developed in
-previous deliverables.
-
-The executable formal semantics of C and machine code (Deliverables D3.1 and
-D4.1) 
-
-TO BE COMPLETED
+This deliverable represents the final milestone of the CerCo project.
+The software delivered links together most of the software already developed
+in previous deliverables, and it benefits from the studies performed in
+other deliverables. In particular:
+
+\begin{itemize}
+ \item The compiler links the code extracted from the executable formal
+  semantics of C (D3.1), machine code (D4.1), front-end intermediate languages
+  (D3.3) and back-end intermediate languages (D4.3). The \texttt{-is} flag
+  of the compiler invokes the semantics of every intermediate
+  representation of the program to be compiled. The executability of the
+  C and machine code languages has been important to debug the the two
+  semantics, that are part of the trusted code base of the compiler.
+  The executability of the intermediate languages has been important during
+  development for early detection of bugs both in the semantics and in the
+  compiler passes. They are also useful to users to profile programs in early
+  compilation stages to detect where the code spends more time.
+  Those semantics, however, are not part of the trusted code base.
+ \item The compiler links the code extracted from the CIC encoding of the
+  Front-end (D3.2) and Back-end (D4.2). The two encodings have been partially
+  proved correct in D3.4 (Front End Correctness Proof) and D4.4 (Back End
+  Correctness Proof). The formal proofs to be delivered in those deliverables
+  have not been completed. The most urgent future work after the end of the
+  project will consist in completing those proofs. 
+ \item Debian Packages have been provided in D6.6 for the Cost-Annotating
+  Plug-In, the Untrusted CerCo Compiler and the Trusted CerCo Compiler.
+  The first and third installed together form a full installation of the
+  Trusted CerCo Prototype. In order to allow interested people to test the
+  prototype more easily, we also provided in D6.6 a Live CD based on
+  Debian with the CerCo Packages pre-installed.
+\end{itemize}
+
 \end{document}
-
-XXXXXXXXX
-
-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}).
-We provide an executable semantics in both O'Caml and the internal language of the Matita proof assistant.
-
-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.
-Further, additional deliverables listed under Work Package 4 will later make use of the work reported in this document.
-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.
-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.
-The emulator(s) discussed in this report are the formalized semantics of our target processor made manifest.