# Changeset 1830 for Deliverables

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

Rest of WP3 presentation.

File:
1 edited

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

 r1825 \documentclass{beamer} \documentclass[nopanel]{beamer} \usetheme{Frankfurt} } \section{Common} \begin{frame}[fragile] } \section{Clight} \frame{ \frametitle{Clight: syntax and semantics} % \end{itemize} % } \section{Cminor} \begin{frame}[fragile] \frametitle{Cminor syntax and semantics} \end{frame} \section{Clight to Cminor} \begin{frame} \frametitle{Clight to Cminor} \end{frame} \section{Initialisation} \begin{frame} \frametitle{Cminor: initialization} \end{frame} \section{RTLabs} \begin{frame}[fragile] \frametitle{RTLabs: syntax and semantics} \end{frame} \section{Cminor to RTLabs} \begin{frame} \frametitle{Cminor to RTLabs} \end{frame} % TODO: graph closed \frame{ \frametitle{Cminor to RTLabs: cost labels} } Two of the cost label properties are easy to deal with, the third requires more work: \begin{enumerate} \item cost label at head of function \item cost label after branching instructions \item cost labels at the head of each loop / \lstinline'goto' destination \end{enumerate} No simple notion of the head of a loop or \lstinline'goto' any more. Instead will prove in \alert{Cminor} that after following a finite number of instructions we reach either \begin{itemize} \item a cost label, or \item the end of the function \end{itemize} } \section{Structured traces} \frame{ \frametitle{RTLabs structured traces} Front-end only uses flat traces consisting of single steps. The back-end will need the function call structure and the labelling properties in order to show that the generated costs are correct. \begin{itemize} \item Traces are structured in sections from cost label to cost label, \item the entire execution of function calls nested as a single `step', \item A coinductive definition presents non-terminating traces, using the inductive definition for all terminating function calls \end{itemize} Have already established the existence of these traces \begin{itemize} \item termination decided classically \item syntactic labelling properties used to build these semantic structure \item tricky to establish guardedness of definitions \end{itemize} } \frametitle{Conclusion} Front-end in good shape: \begin{itemize} \item have executable semantics, \item have compilation stages. \end{itemize} \bigskip Refining some areas may be better in the long run. \bigskip Have a decent start on correctness-related activities. The syntax, semantics and translations of the prototype compiler have been implemented in Matita. We have already defined and established \begin{itemize} \item invariants regarding variables, typing and program structure \item a rich form of execution trace to pass to the back-end \end{itemize} We have plans for \begin{itemize} \item showing functional correctness of the front-end \item proving that the cost labelling is appropriate, and is preserved \item using the above in the whole compiler functional and cost correctness results. \end{itemize} }
Note: See TracChangeset for help on using the changeset viewer.