Changeset 3109 for Deliverables

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

New version.

File:
1 edited

Legend:

Unmodified
 r3108 \end{verbatim} \begin{figure}[b] \begin{figure}[t] \begin{verbatim} char a[] = {3, 2, 7, -4}; \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) { 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 \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}. (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. \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. \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.