Ignore:
Timestamp:
Oct 10, 2011, 6:18:10 PM (9 years ago)
Author:
campbell
Message:

Minor corrections and a paragraph of context in the abstract to deliverables 3.2 and 3.3.

File:
1 edited

Legend:

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

    r1317 r1346  
    9999\vspace*{7cm}
    100100\paragraph{Abstract}
    101 We describe the translation of the front end of the \cerco{} compiler from the
     101We describe the translation of the front-end of the \cerco{} compiler from the
    102102\ocaml{} prototype to the Calculus of Inductive Constructions (CIC) in the
    103103\matita{} proof assistant.  This transforms programs in the C-like
     
    110110will assist in future work proving correctness properties.
    111111
     112This work was Task~3.2 of the \cerco{} project, translating the prototype
     113described in Deliverable~2.2~\cite{d2.2} into CIC using the intermediate languages
     114formalized in Deliverables~3.1~\cite{d3.1} and~3.3.  It will feed into the front-end
     115correctness proofs in Task~3.4 and is a counterpart to the back-end
     116formalization in Task~4.2.
     117
    112118\newpage
    113119
     
    115121
    116122% TODO: clear up any -ize vs -ise
    117 % TODO: clear up any "front end" vs "front-end"
    118 % TODO: clear up any mentions of languages that aren't textsf'd.
    119 % TODO: fix unicode in listings
    120 % TODO: make it clear that our correctness is intended to go beyond compcert's
    121 % TODO: capitalise deliverable/task?
     123% CHECK: clear up any "front end" vs "front-end"
     124% CHECK: clear up any mentions of languages that aren't textsf'd.
     125% CHECK: fix unicode in listings
     126% CHEKC: capitalise deliverable/task when referring to a particular one
    122127
    123128\section{Introduction}
     
    154159\> $\downarrow$ \> transform to RTL graph\\
    155160\textsf{RTLabs}\\
    156 \> $\downarrow$ \> start of target specific backend\\
     161\> $\downarrow$ \> start of target specific back-end\\
    157162\>\quad \vdots
    158163\end{tabbing}
     
    170175
    171176\item[\textsf{RTLabs}] --- a language in the form of a control flow graph
    172 which retains the values and front end operations from \textsf{Cminor}
     177which retains the values and front-end operations from \textsf{Cminor}
    173178\end{description}
    174179More details on the formalisation of the syntax and semantics of these
    175 languages can be found in the accompanying deliverable 3.4.
     180languages can be found in the accompanying Deliverable 3.4.
    176181Development of the formalized front-end was conducted in concert with the
    177182development of these intermediate languages to facilitate testing.
     
    205210\end{itemize}
    206211
    207 This document describes the formalized front end after these changes.
     212This document describes the formalized front-end after these changes.
    208213
    209214\section{\textsf{Clight} phases}
     
    243248This has been implemented in \matita.  We have also performed a few proofs that
    244249the arithmetic behind these changes is correct to gain confidence in the
    245 technique.  During task 3.4 we will extend these proofs to cover more
     250technique.  During Task 3.4 we will extend these proofs to cover more
    246251operations and show that the semantics of the expressions are equivalent, not
    247252just the underlying arithmetic.
     
    252257simple recursive definition, and was straightforward to port to \matita.  The
    253258generation of cost labels was handled by our generic identifiers code,
    254 described in the accompanying deliverable 3.3 on intermediate languages.
     259described in the accompanying Deliverable 3.3 on intermediate languages.
    255260
    256261\subsection{Runtime functions}
     
    275280\textsf{Clight} abstract syntax trees directly.
    276281
    277 \subsection{Conversion to Cminor}
     282\subsection{Conversion to \textsf{Cminor}}
    278283
    279284The conversion to \textsf{Cminor} performs two essential tasks.  First, it
     
    346351formed early in the compilation process.
    347352
    348 This work overlaps with deliverable 3.3 (where more details of the additions
     353This work overlaps with Deliverable 3.3 (where more details of the additions
    349354to the syntax and semantics of the intermediate languages can be found) and
    350 task 3.4 on the correctness of the compiler.  Thus this work is experimental
    351 in nature, and will evolve during task 3.4.
     355Task 3.4 on the correctness of the compiler.  Thus this work is experimental
     356in nature, and will evolve during Task 3.4.
    352357
    353358The use of the invariants follows a common pattern.  Each language embeds
     
    428433
    429434To provide some early testing and bug fixing of this code we constructed it in
    430 concert with the executable semantics described in deliverable 3.3, and
     435concert with the executable semantics described in Deliverable 3.3, and
    431436\matita{} term pretty printers in the prototype compiler.  Using these, we
    432437were able to test the phases individually and together by running programs
     
    439444proof assistant, and shown that invariants can be added to the intermediate
    440445languages to help show properties of it.  This work provides a solid basis for
    441 the compiler correctness proofs in task 3.4.
     446the compiler correctness proofs in Task 3.4.
    442447
    443448\bibliographystyle{plain}
Note: See TracChangeset for help on using the changeset viewer.