Changeset 3226


Ignore:
Timestamp:
Apr 30, 2013, 12:54:18 PM (4 years ago)
Author:
campbell
Message:

More 3.4 revisions; mostly administrative.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3223 r3226  
    118118of the compiler can be layered on top of normal forward simulation results,
    119119if we split those results into local call-structure preserving simulations.
    120 
    121 This deliverable shows correctness results about the formalised
    122 compiler described in D3.2, using the source language semantics from
    123 D3.1 and intermediate language semantics from D3.3.  It builds on
    124 earlier work on the correctness of a toy compiler built to test the
    125 labelling approach in D2.1. Together with the companion deliverable
    126 about the correctness of the back-end, D4.4, we obtain results about
    127 the whole formalised compiler.
    128 
    129 % TODO: mention the deliverable about the extracted compiler et al?
     120This split allowed us to concentrate on the intensional proofs by
     121axiomatising some of the simulation results that are very similar to
     122existing compiler correctness results.
     123
     124This report is about the correctness results that are deliverable
     125D3.4, which are about the formalised compiler described in D3.2, using
     126the source language semantics from D3.1 and intermediate language
     127semantics from D3.3.  It builds on earlier work on the correctness of
     128a toy compiler built to test the labelling approach in D2.1. Together
     129with the companion deliverable about the correctness of the back-end,
     130D4.4, we obtain results about the whole formalised compiler.
    130131
    131132\newpage
     
    141142
    142143The \cerco{} compiler produces a version of the source code containing
    143 annotations describing the timing behaviour of the object code, as well
    144 as the object code itself. It compiles C code, targeting
     144annotations describing the timing behaviour of the object code, as
     145well as the object code itself. It compiles C code, targeting
    145146microcontrollers implementing the Intel 8051 architecture.  There are
    146147two versions: first, an initial prototype was implemented in
    147 \ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{} proof
    148 assistant~\cite{d3.2,d4.2} and extracted to \ocaml{} code to
     148\ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{}
     149proof assistant~\cite{d3.2,d4.2} and extracted to \ocaml{} code to
    149150produce an executable compiler.  In this document we present results
    150 formalised in \matita{} about the front-end of the latter version of
    151 the compiler, and how that fits into the verification of the whole
    152 compiler.
     151from Deliverable 3.4, the formalised proofs in \matita{} about the
     152front-end of the latter version of the compiler (culminating in the
     153\lstinline'front_end_correct' lemma), and describe how that fits
     154into the verification of the whole compiler.
    153155
    154156A key part of this work was to layer the intensional correctness
     
    414416observable witness is preserved, so the program must behave correctly.
    415417
     418These two results are combined in the the \lstinline'correct'
     419theorem in the file \lstinline'correctness.ma'.
     420
    416421\section{Goals for the front-end}
    417422\label{sec:fegoals}
     
    498503  preservation of observables.)
    499504\end{enumerate}
     505The \lstinline'front_end_correct' lemma in the
     506\lstinline'correctness.ma' file provides a record containing these.
    500507
    501508Following the outline in Figure~\ref{fig:compiler}, we will first deal
     
    580587details of the evaluation process for the source switch statement and
    581588its target counterpart can be found in the file
    582 \textbf{switchRemoval.ma}, along more details on the transformation
     589\lstinline'switchRemoval.ma', along more details on the transformation
    583590itself.
    584591
     
    11161123of existing results.
    11171124
    1118 
    1119 
    1120 TODO: appendix on code layout?
     1125\appendix
     1126
     1127\section{Files}
     1128
     1129The following table gives a high-level overview of the \matita{}
     1130source files in Deliverable 3.4:
     1131
     1132\bigskip
     1133
     1134\begin{tabular}{rp{.7\linewidth}}
     1135\lstinline'compiler.ma' & Top-level compiler definitions, in particular
     1136\lstinline'front_end', and the whole compiler definition
     1137\lstinline'compile'. \\
     1138\lstinline'correctness.ma' & Correctness results: \lstinline'front_end_correct'
     1139and \lstinline'correct', respectively. \\
     1140\lstinline'Clight/*' & \textsf{Clight}: proofs for switch
     1141removal, cost labelling, cast simplification and conversion to
     1142\textsf{Cminor}. \\
     1143\lstinline'Cminor/*' & \textsf{Cminor}: axioms of conversion to
     1144\textsf{RTLabs}. \\
     1145\lstinline'RTLabs/*' & \textsf{RTLabs}: definitions and proofs for
     1146compile-time cost labelling checks, construction of structured traces.
     1147\\
     1148\lstinline'common/Measurable.ma' & Definitions for measurable
     1149subtraces. \\
     1150\lstinline'common/FEMeasurable.ma' & Generic measurable subtrace
     1151lifting proof. \\
     1152\lstinline'common/*' & Other common definitions relevant to many parts
     1153of the compiler and proof. \\
     1154\lstinline'utilities/*' & General purpose definitions used throughout,
     1155including extensions to the standard \matita{} library.
     1156\end{tabular}
    11211157
    11221158\bibliographystyle{plain}
Note: See TracChangeset for help on using the changeset viewer.