Changeset 3109 for Deliverables/D5.2/report.tex
- Timestamp:
- Apr 9, 2013, 5:28:39 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D5.2/report.tex
r3108 r3109 161 161 \end{verbatim} 162 162 163 \begin{figure}[ b]163 \begin{figure}[t] 164 164 \begin{verbatim} 165 165 char a[] = {3, 2, 7, -4}; … … 180 180 \end{figure} 181 181 182 \begin{figure} 182 \begin{figure}[!p] 183 183 \begin{verbatim} 184 int __cost = 0;185 186 int __stack_size = 0, __stack_size_max = 0;184 int __cost = 33; 185 186 int __stack_size = 5, __stack_size_max = 5; 187 187 188 188 void __cost_incr(int incr) { … … 616 616 types~\cite{christinexx}. The calculi implemented by Coq and Matita, however, 617 617 are more expressive than CoC, and several type constructions have no 618 counterparts in System $F \_omega$. Moreover, core OCaml does not even619 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. 620 620 Therefore, in all situations listed below, code extraction is not able to 621 621 type the extracted code using informative types, but it uses the … … 642 642 \item Case analysis and recursion over inhabitants of primitive inductive 643 643 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 declared644 $F_\omega$. In the CerCo compiler we largely exploit type formers declared 645 645 in this way, for example to provide the same level of type safety achieved 646 646 in the untrusted compiler via polymorphic variants~\cite{guarriguesxx}. … … 659 659 (pseudo)-registers for back-end languages --- some terms working on the 660 660 type --- e.g. functions to set/get values from (pseudo)-registers --- and 661 properties over them. In System $F \_omega$ terms and types abstractions661 properties over them. In System $F_\omega$ terms and types abstractions 662 662 are kept syntactically separate and there is no way to pack them in 663 663 records. … … 683 683 \item We already have a prototype that extracts code from Matita to GHC plus 684 684 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 we685 $F_\omega$. However, the prototype is not fully functional yet because we 686 686 still need to solve at the theoretical level a problem of interaction 687 between $F \_omega$ types and strong elimination. Roughly speaking, the687 between $F_\omega$ types and strong elimination. Roughly speaking, the 688 688 two branches of a strong elimination always admit a most general unifier in 689 689 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 code690 is lost for $F_\omega$. As a consequence, we loose modularity in code 691 691 extraction and we need to figure out static analysis techniques to reduce 692 692 the impact of the loss of modularity. … … 712 712 \end{itemize} 713 713 714 \subsection{Connection with other deliverables} 714 \section{The Cost-Annotating Plug-In} 715 716 The functionalities of the Cost Annotating Plug-In have already been described 717 in Deliverables~D5.1 and D5.3. 718 The plug-in interfaces with the CerCo compiler via 719 the command line. Therefore there was no need to update the plug-in code for 720 integration in the Trusted CerCo Prototype. Actually, it is even possible 721 to 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 723 to be used for compilation. 724 725 The code of the plug-in has been modified w.r.t. D5.1 in order to take care 726 also of the cost model for stack-size consumption. From the user point of view, 727 time and space cost annotations and invariants are handled in a similar way. 728 Nevertheless, we expect automated theorem provers to face more difficulties 729 in dealing with stack usage because elapsed time is additive, whereas what 730 is interesting for space usage is the maximum amount of stack used, which is 731 not additive. On the other hand, programs produced by our compiler require 732 more stack only at function calls. Therefore the proof obligations generated 733 to bound the maximum stack size for non recursive programs are trivial. 734 Most C programs, and in particular those used in time critical systems, avoid 735 recursive functions. 736 737 \section{Connection with other deliverables} 715 738 \label{subsect.connection.other.deliverables} 716 739 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 740 This deliverable represents the final milestone of the CerCo project. 741 The software delivered links together most of the software already developed 742 in previous deliverables, and it benefits from the studies performed in 743 other 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 725 772 \end{document} 726 727 XXXXXXXXX728 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.