Changeset 1830


Ignore:
Timestamp:
Mar 13, 2012, 3:53:51 PM (8 years ago)
Author:
campbell
Message:

Rest of WP3 presentation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP3.tex

    r1825 r1830  
    1 \documentclass{beamer}
     1\documentclass[nopanel]{beamer}
    22
    33\usetheme{Frankfurt}
     
    122122}
    123123
     124\section{Common}
    124125
    125126\begin{frame}[fragile]
     
    176177}
    177178
    178 
     179\section{Clight}
    179180\frame{
    180181\frametitle{Clight: syntax and semantics}
     
    263264% \end{itemize}
    264265% }
    265 
     266\section{Cminor}
    266267\begin{frame}[fragile]
    267268\frametitle{Cminor syntax and semantics}
     
    391392\end{frame}
    392393
     394
     395\section{Clight to Cminor}
     396
    393397\begin{frame}
    394398\frametitle{Clight to Cminor}
     
    427431\end{frame}
    428432
     433\section{Initialisation}
    429434\begin{frame}
    430435\frametitle{Cminor: initialization}
     
    445450\end{frame}
    446451
     452\section{RTLabs}
    447453\begin{frame}[fragile]
    448454\frametitle{RTLabs: syntax and semantics}
     
    495501\end{frame}
    496502
    497 
     503\section{Cminor to RTLabs}
    498504\begin{frame}
    499505\frametitle{Cminor to RTLabs}
     
    574580\end{frame}
    575581
    576 % TODO: graph closed
    577 
    578582\frame{
    579583\frametitle{Cminor to RTLabs: cost labels}
    580584
    581 }
    582 
     585Two of the cost label properties are easy to deal with, the third requires more
     586work:
     587\begin{enumerate}
     588\item cost label at head of function
     589\item cost label after branching instructions
     590\item cost labels at the head of each loop / \lstinline'goto' destination
     591\end{enumerate}
     592
     593No simple notion of the head of a loop or \lstinline'goto' any more.
     594
     595Instead will prove in \alert{Cminor} that after following a finite
     596number of instructions we reach either
     597\begin{itemize}
     598\item a cost label, or
     599\item the end of the function
     600\end{itemize}
     601
     602}
     603
     604\section{Structured traces}
    583605\frame{
    584606\frametitle{RTLabs structured traces}
    585607
     608Front-end only uses flat traces consisting of single steps.
     609
     610The back-end will need the function call structure and the labelling
     611properties in order to show that the generated costs are correct.
     612
     613\begin{itemize}
     614\item Traces are structured in sections from cost label to cost label,
     615\item the entire execution of function calls nested as a single `step',
     616\item A coinductive definition presents non-terminating traces, using the
     617  inductive definition for all terminating function calls
     618\end{itemize}
     619
     620Have already established the existence of these traces
     621\begin{itemize}
     622\item termination decided classically
     623\item syntactic labelling properties used to build these semantic structure
     624\item tricky to establish guardedness of definitions
     625\end{itemize}
    586626}
    587627
     
    612652\frametitle{Conclusion}
    613653
    614 Front-end in good shape:
    615 \begin{itemize}
    616 \item have executable semantics,
    617 \item have compilation stages.
    618 \end{itemize}
    619 
    620 \bigskip
    621 Refining some areas may be better in the long run.
    622 
    623 \bigskip
    624 Have a decent start on correctness-related activities.
     654The syntax, semantics and translations of the prototype compiler have
     655been implemented in Matita.
     656
     657We have already defined and established
     658\begin{itemize}
     659\item invariants regarding variables, typing and program structure
     660\item a rich form of execution trace to pass to the back-end
     661\end{itemize}
     662
     663We have plans for
     664\begin{itemize}
     665\item showing functional correctness of the front-end
     666\item proving that the cost labelling is appropriate, and is preserved
     667\item using the above in the whole compiler functional and cost correctness results.
     668\end{itemize}
     669
    625670}
    626671
Note: See TracChangeset for help on using the changeset viewer.