Changeset 1346


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

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

Location:
Deliverables
Files:
2 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}
  • Deliverables/D3.3/Report/report.tex

    r1317 r1346  
    6868\bf
    6969Report n. D3.3\\
    70 Executable Formal Semantics of front end intermediate languages\\
     70Executable Formal Semantics of front-end intermediate languages\\
    7171\end{LARGE}
    7272\end{center}
     
    9999\vspace*{7cm}
    100100\paragraph{Abstract}
    101 We report on the formalization of the front end intermediate languages for the
     101We report on the formalization of the front-end intermediate languages for the
    102102\cerco{} project's compiler using executable semantics in the \matita{} proof
    103103assistant.  This includes common definitions for fresh identifier handling,
    104 $n$-bit arithmetic and operations and testing of the smeantics.  We also
     104$n$-bit arithmetic and operations and testing of the semantics.  We also
    105105consider embedding invariants into the semantics for showing correctness
    106106properties.
    107107
     108This work was Task~3.3 of the \cerco{} project and the languages that were
     109formalized were first described in Deliverable~2.1~\cite{d2.1}.  They are used
     110by the formalized front-end in Task~3.2 to provide the syntax for the
     111transformations, and to test them by animating programs in the executable
     112semantics.  It will also be a crucial part of the specifications for the
     113correctness results in Task~3.4.
     114
    108115\newpage
    109116
    110117\tableofcontents
    111118
    112 % TODO: clear up any -ize vs -ise
    113 % TODO: clear up any "front end" vs "front-end"
    114 % TODO: clear up any mentions of languages that aren't textsf'd.
    115 % TODO: fix unicode in listings
     119% CHECK: clear up any -ize vs -ise
     120% CHECK: clear up any "front end" vs "front-end"
     121% CHECK: clear up any mentions of languages that aren't textsf'd.
     122% CHECK: fix unicode in listings
    116123
    117124\section{Introduction}
    118125
    119 This work formalizes the front end intermediate languages from the \cerco{}
     126This work formalizes the front-end intermediate languages from the \cerco{}
    120127prototype compiler, described in previous deliverables~\cite{d2.1,d2.2}.  The
    121 front end of the compiler is summarized in Figure~\ref{fig:summary} including
     128front-end of the compiler is summarized in Figure~\ref{fig:summary} including
    122129the intermediate languages and the compiler passes described in the
    123 accompanying deliverable 3.2.  We have also refined parts of the formal
     130accompanying Deliverable 3.2.  We have also refined parts of the formal
    124131development that are used for several of the languages in the compiler.
    125132
    126 The input language to the formalized front end is the \textsf{Clight}
     133The input language to the formalized front-end is the \textsf{Clight}
    127134language.  The executable semantics for this language were presented in a
    128135previous deliverable~\cite{d3.1}.  Here we will report on some
     
    134141done in the Calculus of Inductive Constructions (CIC), as implemented in the
    135142\matita{} proof assistant.  These definitions will be essential for the
    136 correctness proofs of the compiler in task 3.4.
     143correctness proofs of the compiler in Task 3.4.
    137144
    138145Finally, we will report on work to add several invariants to the
    139 languages.  This activity overlaps with task 3.4 on the correctness of the
    140 compiler front end.  However, the use of dependent types mean that this work
     146languages.  This activity overlaps with Task 3.4 on the correctness of the
     147compiler front-end.  However, the use of dependent types mean that this work
    141148is tied closely to the definition of the languages and the transformations of
    142 the front end in task 3.2.  By considering it now we can experiment with and
     149the front-end in Task 3.2.  By considering it now we can experiment with and
    143150judge its impact on the formal semantics, and how feasible retrofitting such
    144151invariants is.
     
    158165 simplification\\
    159166\textsf{Cminor}\\
    160 \> $\downarrow$ \> generate global variable initialisation code\\
     167\> $\downarrow$ \> generate global variable initialization code\\
    161168\> $\downarrow$ \> transform to RTL graph\\
    162169\textsf{RTLabs}\\
    163 \> $\downarrow$ \> start of target specific backend\\
     170\> $\downarrow$ \> start of target specific back-end\\
    164171\>\quad \vdots
    165172\end{tabbing}
    166173\end{minipage}
    167174\end{center}
    168 \caption{Front end languages and transformations}
     175\caption{Front-end languages and transformations}
    169176\label{fig:summary}
    170177\end{figure}
     
    189196a monad for encapsulating failure and I/O (using resumptions).  The executable
    190197memory model was ported from CompCert as part of the work on \textsf{Clight}
    191 and was reused for the front end languages\footnote{However, it is likely that
     198and was reused for the front-end languages\footnote{However, it is likely that
    192199we will revise the memory model to make it better suited for describing the
    193200back-end of our compiler.}.  The failure and I/O monad was introduced in the
     
    234241
    235242The bit vectors in~\cite{d4.1} also came equipped with some basic arithmetic
    236 for the target semantics.  The front end required these operations to be
     243for the target semantics.  The front-end required these operations to be
    237244generalized and extended.  In particular, we required operations such as zero
    238245and sign extension and translation between bit vectors and full integers.  It
     
    242249front-end semantics.
    243250
    244 \subsection{Front end operations}
    245 
    246 The two front end intermediate languages, \textsf{Cminor} and \textsf{RTLabs},
     251\subsection{Front-end operations}
     252
     253The two front-end intermediate languages, \textsf{Cminor} and \textsf{RTLabs},
    247254share the same set of operations on values.  They differ from
    248255\textsf{Clight}'s operations by incorporating casts and by having a separate
     
    274281is similar to the prototype, except that the types attached to expressions are
    275282restricted so that some corner cases are ruled out in the \textsf{Cminor} to
    276 \textsf{RTLabs} stage (see the accompanying deliverable 3.2 for details):
     283\textsf{RTLabs} stage (see the accompanying Deliverable 3.2 for details):
    277284\begin{lstlisting}
    278285    inductive expr : typ $\rightarrow$ Type[0] ≝
     
    289296In principle we could extend this to statically ensure that only well-typed
    290297\textsf{Cminor} expressions are considered, and we will consider this as part
    291 of the work on correctness in task 3.4.
     298of the work on correctness in Task 3.4.
    292299
    293300We also provide a variant of the syntax where the only initialization data is
     
    311318prototype compiler.  Some of the syntax is shown below, including the type of
    312319the control flow graphs.  The same common elements are used as for \textsf{Cminor},
    313 including the front end operations mentioned above.
     320including the front-end operations mentioned above.
    314321
    315322\begin{lstlisting}[language=matita]
     
    339346
    340347To provide some assurance that the semantics were properly implemented, and to
    341 support the testing described in the accompanying deliverable 3.2, we have
     348support the testing described in the accompanying Deliverable 3.2, we have
    342349adapted the pretty printers in the prototype compiler to produce \matita{}
    343350terms for the syntax of each language described above.
    344351
    345352A few common definitions were added for animating the small step semantics
    346 definitions for any of the front end languages in \matita.  We then used a
     353definitions for any of the front-end languages in \matita.  We then used a
    347354small selection of test cases to ensure basic functionality.  However, this is
    348355still a time consuming process, so more testing will carried out once the
     
    362369involves manipulating the syntax and semantics of the intermediate languages
    363370(the present work), the encoding of the front-end compiler phases in \matita{}
    364 (task 3.2) and the correctness of the front-end (task 3.4).  Thus this work is
     371(Task 3.2) and the correctness of the front-end (Task 3.4).  Thus this work is
    365372rather experimental; it is being carried out on branches in our source code
    366 repository and the final form will be decided and merged in during task 3.4.
     373repository and the final form will be decided and merged in during Task 3.4.
    367374
    368375So far we have tried adding two forms of invariant --- one using dependent
     
    474481
    475482The \textsf{Clight} semantics can be amended to use these invariants, although
    476 the main benefit is for the compiler stages (see the accompanying deliverable
     483the main benefit is for the compiler stages (see the accompanying Deliverable
    4774843.2 for details).  The semantics require the invariants to be added to the
    478485state and continuations.  It was convenient to split the continuations between
     
    491498presence of proof terms and more dependent pattern matching in the semantics
    492499will have on the complexity of future correctness proofs.  We plan to examine
    493 this issue during task 3.4.
     500this issue during Task 3.4.
    494501
    495502We use a similar method to specify the invariant that the \textsf{RTLabs}
     
    503510We have developed executable semantics for each of the front-end languages of
    504511the \cerco{} compiler.  These will form the basis of the correctness
    505 statements for each stage of the compiler in task 3.4.  We have also shown
     512statements for each stage of the compiler in Task 3.4.  We have also shown
    506513that useful invariants can be added as dependent types, and intend to use
    507514these in subsequent work.
Note: See TracChangeset for help on using the changeset viewer.