Changeset 3212


Ignore:
Timestamp:
Apr 29, 2013, 5:24:44 PM (4 years ago)
Author:
campbell
Message:

Sort out some "to do"s, minimal conclusion.

Location:
Deliverables/D3.4/Report
Files:
2 edited

Legend:

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

    r3128 r3212  
    6666}
    6767
     68@article{Leroy-backend,
     69  author = {Xavier Leroy},
     70  title = {A formally verified compiler back-end},
     71  journal = {Journal of Automated Reasoning},
     72  volume = 43,
     73  number = 4,
     74  pages = {363--446},
     75  year = 2009,
     76  url = {http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf},
     77  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9155-4},
     78  hal = {http://hal.inria.fr/inria-00360768/},
     79  pubkind = {journal-int-mono}
     80}
     81
     82@article{Blazy-Leroy-Clight-09,
     83  author = {Sandrine Blazy and Xavier Leroy},
     84  title = {Mechanized semantics for the {Clight}
     85                         subset of the {C} language},
     86  year = 2009,
     87  journal = {Journal of Automated Reasoning},
     88  url = {http://gallium.inria.fr/~xleroy/publi/Clight.pdf},
     89  hal = {http://hal.inria.fr/inria-00352524/},
     90  urlpublisher = {http://dx.doi.org/10.1007/s10817-009-9148-3},
     91  volume = 43,
     92  number = 3,
     93  pages = {263-288}
     94}
  • Deliverables/D3.4/Report/report.tex

    r3211 r3212  
    140140\section{Introduction}
    141141
    142 \todo{add stack space for more precise statement.  Also do some
    143 translation validation on sound, precise labelling properties.}
    144 
    145142The \cerco{} compiler compiles C code, targeting microcontrollers
    146143implementing the Intel 8051 architecture.  It produces both the object
     
    154151into the verification of the whole compiler.
    155152
    156 \todo{maybe mention stack space here?  other additions?  refer to
    157   "layering"?}  A key part of this work was to separate the proofs
    158 about the compiled code's extensional behaviour (that is, the
    159 functional correctness of the compiler) from the intensional
    160 correctness that the costs given are correct.  Unfortunately, the
    161 ambitious goal of completely verifying the entire compiler was not
    162 feasible within the time available, but thanks to this separation of
     153A key part of this work was to layer the intensional correctness
     154results that show that the costs given are correct on top of the
     155proofs about the compiled code's extensional behaviour (that is, the
     156functional correctness of the compiler).  Unfortunately, the ambitious
     157goal of completely verifying the entire compiler was not feasible
     158within the time available, but thanks to this separation of
    163159extensional and intensional proofs we are able to axiomatize
    164160simulation results similar to those in other compiler verification
    165 projects and concentrate on the novel intensional proofs.  The proofs
    166 were also made more tractable by introducing compile-time checks for
     161projects and concentrate on the novel intensional proofs.  We were
     162also able to add stack space costs to obtain a stronger result.  The
     163proofs were made more tractable by introducing compile-time checks for
    167164the `sound and precise' cost labelling properties rather than proving
    168165that they are preserved throughout.
     
    177174statement more precise.  Following that, in Section~\ref{sec:fegoals} we
    178175describe the statements we need to prove about the intermediate \textsf{RTLabs}
    179 programs sufficient for the back-end proofs.  \todo{rest of document structure}
     176programs sufficient for the back-end proofs.
     177Section~\ref{sec:inputtolabelling} covers the passes which produce the
     178annotated source program and Section~\ref{sec:measurablelifting} the rest
     179of the transformations in the front-end.  Then the compile time checks
     180for good cost labelling are detailed in Section~\ref{sec:costchecks}
     181and the proofs that the structured traces required by the back-end
     182exist are discussed in Section~\ref{sec:structuredtrace}.
    180183
    181184\section{The compiler and main goals}
     
    242245transformation to \textsf{Cminor} and subsequently \textsf{RTLabs}
    243246bear considerable resemblance to some passes of the CompCert
    244 compiler\todo{cite}, although we use a simpler \textsf{Cminor} where
     247compiler~\cite{Blazy-Leroy-Clight-09,Leroy-backend}, although we use a simpler \textsf{Cminor} where
    245248all loops use \lstinline[language=C]'goto' statements, and the
    246249\textsf{RTLabs} language retains a target-independent flavour.  The
     
    272275code.  In the case of the annotated source code, it also inserts the actual
    273276costs alongside the cost labels, and optionally adds a global cost variable
    274 and instrumentation to support further reasoning.  \todo{Cross-ref case study
    275 deliverables}
     277and instrumentation to support further reasoning.
    276278
    277279\subsection{Revisions to the prototype compiler}
     
    496498
    497499\section{Input code to cost labelled program}
     500\label{sec:inputtolabelling}
    498501
    499502As explained on page~\pageref{page:switchintro}, the costs of complex
     
    596599
    597600\section{Finding corresponding measurable subtraces}
     601\label{sec:measurablelifting}
    598602
    599603There follow the three main passes of the front-end:
     
    867871the \textsf{RTLabs} intermediate code would reduce the proof burden
    868872considerably.  This is similar in spirit to the use of translation
    869 validation in certified compilation\todo{Cite some suitable work
    870   here}, which makes a similar trade-off between the potential for
    871 compile-time failure and the volume of proof required.
     873validation in certified compilation, which makes a similar trade-off
     874between the potential for compile-time failure and the volume of proof
     875required.
    872876
    873877The check cannot be pushed into a later stage of the compiler because
     
    917921
    918922\emph{Structured traces} enrich the execution trace of a program by
    919 nesting function calls in a mixed-step style\todo{Can I find a
    920   justification for mixed-step} and embedding the cost properties of
    921 the program.  It was originally designed to support the proof of
    922 correctness for the timing analysis of the object code in the
     923nesting function calls in a mixed-step style and embedding the cost
     924properties of the program.  It was originally designed to support the
     925proof of correctness for the timing analysis of the object code in the
    923926back-end, then generalised to provide a common structure to use from
    924927the end of the front-end to the object code.  See
    925 Figure~\ref{fig:strtrace} on page~\pageref{fig:strtrace}
    926 for an illustration of a structured trace.
     928Figure~\ref{fig:strtrace} on page~\pageref{fig:strtrace} for an
     929illustration of a structured trace.
    927930
    928931To make the definition generic we abstract over the semantics of the
     
    10231026\section{Conclusion}
    10241027
    1025 TODO
     1028In combination with the work on the CerCo back-end and by
     1029concentrating on the novel intensional parts of the proof, we have
     1030shown that it is possible to construct certifying compilers that
     1031correctly report execution time and stack space costs.
    10261032
    10271033TODO: appendix on code layout?
Note: See TracChangeset for help on using the changeset viewer.