Changeset 1854 for Deliverables


Ignore:
Timestamp:
Mar 15, 2012, 4:14:53 PM (8 years ago)
Author:
sacerdot
Message:

...

Location:
Deliverables/D1.2/Presentations
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP4-dominic.tex

    r1849 r1854  
    1212\title{CerCo Work Package 4}
    1313\date{CerCo project review meeting\\March 2012}
     14
     15\AtBeginSection[]
     16{
     17  \begin{frame}<beamer>
     18    \frametitle{Outline}
     19    \tableofcontents[currentsection]
     20  \end{frame}
     21}
    1422
    1523\lstdefinelanguage{matita-ocaml}
     
    2129
    2230\lstset{language=matita-ocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false,
    23         keywordstyle=\color{red}\bfseries,
     31        keywordstyle=\color{blue}\bfseries,
    2432        keywordstyle=[2]\color{blue},
    2533        keywordstyle=[3]\color{blue}\bfseries,
    2634        commentstyle=\color{green},
    2735        stringstyle=\color{blue},
    28         showspaces=false,showstringspaces=false}
     36        showspaces=false,showstringspaces=false,escapechar=\%}
    2937
    3038\begin{document}
     
    3543
    3644\begin{frame}
    37 \frametitle{Summary}
    38 Relevant tasks: T4.2 and T4.3 (from the CerCo Contract):
    39 \begin{quotation}
    40 \textbf{Task 4.2}
    41 Functional encoding in the Calculus of Inductive Construction (indicative effort: UNIBO: 8; UDP: 2; UEDIN: 0)
    42 \end{quotation}
    43 
    44 \begin{quotation}
    45 \textbf{Task 4.3}
    46 Formal semantics of intermediate languages (indicative effort: UNIBO: 4; UDP: 0; UEDIN: 0)
    47 \end{quotation}
     45\frametitle{Overview of progress}
     46Status at end of first period:
     47\begin{center}
     48{\large Executable semantics of MCS-51 in OCaml and Matita}
     49\end{center}
     50
     51~\\~\\Goals for the end of second period:
     52\begin{center}
     53{\large Executable semantics of back-end intermediate languages\\~\\
     54Encoding of compiler back-end in CIC}
     55\end{center}
    4856\end{frame}
    4957
     
    5664
    5765\begin{frame}
    58 \begin{center}
    59 Rationalisation of backend languages
    60 \end{center}
    61 \end{frame}
    62 
    63 \begin{frame}
    64 \frametitle{Backend intermediate languages I}
    65 \begin{itemize}
    66 \item
    67 OCaml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN
    68 \item
    69 RTLabs is the `frontier' between backend and frontend, last abstract language
    70 \item
    71 RTLabs, RTL, ERTL and LTL are graph based languages: functions represented as graphs of statements, with entry and exit points
    72 \item
    73 LIN is a linearised form of LTL, and is the exit point of the compiler's backend
    74 \item
    75 In contrast to frontend, backend is very different to CompCert's
    76 \end{itemize}
    77 \end{frame}
    78 
    79 \begin{frame}
    80 \frametitle{Backend intermediate languages II}
     66\frametitle{Backend intermediate languages}
    8167\vspace{-1em}
    8268\begin{small}
     
    179165\item
    180166Unify some proofs, making correctness proof easier
     167\item
     168Generic optimizations (e.g. constant propagation)
    181169\end{itemize}
    182170\end{frame}
     
    262250\end{frame}
    263251
    264 \section{Assembler correctness proof and structured traces}
    265 
    266 \begin{frame}
    267 \begin{center}
    268 Assembler correctness proof and structured traces
    269 \end{center}
    270 \end{frame}
     252\section{Optimizing assembler correctness proof}
    271253
    272254\begin{frame}
     
    369351\end{itemize}
    370352\end{frame}
     353
     354\section{Structured traces}
     355
    371356
    372357\begin{frame}[fragile]
     
    481466\begin{frame}
    482467\frametitle{Recursive structure of `good' execution}
    483 Structure captured by structured traces:
     468- All calls return to the correct place\\
     469- CALLS and JUMPS only to labels
    484470\begin{center}
    485471\includegraphics[scale=0.33]{recursive_structure.png}
    486472\end{center}
     473Static cost = k($l_1$) + \ldots + k($l_4$)\\
     474Dynamic cost = clock(Final$_1$) - clock(Start$_1$)\\
    487475\end{frame}
    488476
     
    522510
    523511\section{Changes to tools and prototypes, looking forward}
    524 
    525 \begin{frame}
    526 \begin{center}
    527 Changes to tools and prototypes, looking forward
    528 \end{center}
    529 \end{frame}
    530512
    531513\begin{frame}
Note: See TracChangeset for help on using the changeset viewer.