Changeset 3287


Ignore:
Timestamp:
May 14, 2013, 3:58:12 PM (4 years ago)
Author:
tranquil
Message:

back-end slides

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/Dissemination/back-end/back-end.tex

    r3281 r3287  
    491491\item The issues with defining a good $S$ are no different than in extensional proofs
    492492\item $C$ is defined based on program counters only
     493\item The Matita proof is \structure{complete}
    493494\end{itemize}
    494495\end{frame}
     
    685686\end{columns}
    686687\end{frame}
    687 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    688 \begin{frame}%
    689 %[]
     688\section{Details on the passes}
     689%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     690\begin{frame}%
     691%[]
     692\frametitle{RTLabs $\to$ RTL}
     693\begin{itemize}
     694 \item Most of the effort must go to the \structure{extensional} part, as multi-byte operations
     695 are replaced by sequences of single byte operations
     696 \item Status: sketched
     697\end{itemize}
     698\end{frame}
     699%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     700\begin{frame}%
     701%[]
     702\frametitle{RTL $\to$ ERTL}
     703\begin{itemize}
     704 \item A \structure{graph} pass
     705 \item Implements the calling convention, with the first accesses to stack
     706 \item From the intensional point of view: calls have prefixes and suffixes, and
     707 function bodies have preambles
     708 \item Status: the scaffolding underlying all graph passes
     709 is done. The proof obligations regarding this particular pass are open
     710\end{itemize}
     711\end{frame}
     712%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     713\begin{frame}%
     714%[]
     715\frametitle{ERTL $\to$ LTL}
     716\begin{itemize}
     717\item A \structure{graph} pass
     718\item Register allocation, spilling, saving and restoring callee-saved hardware registers
     719\item From the intensional point of view, calls to pointer have prefixes, and
     720function bodies have preambles
     721\item  Status: the scaffolding underlying all graph passes
     722 is done. The proof obligations regarding this particular pass are almost finished
     723\end{itemize}
     724\end{frame}
     725%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     726\begin{frame}%
     727%[]
     728\frametitle{LTL $\to$ LIN}
     729\begin{itemize}
     730 \item A \structure{linearisation}
     731 \item From the intensional point of view, calls can have suffixes (GOTOs)
     732 \item Status: the generic linearisation scaffolding is complete.
     733 The proof obligations regarding this particular pass are open (but easy)
     734\end{itemize}
     735
     736\end{frame}
     737%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     738\begin{frame}%
     739%[]
     740\frametitle{LIN $\to$ ASM}
     741\begin{itemize}
     742\item A 1-to-1 simulation
     743\item Function names and code labels are collapsed in the same global namespace
     744\item Status: open
     745\end{itemize}
     746\end{frame}
     747%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     748
    690749\section{Assembler correctness}
    691750
     751\begin{frame}%
     752%[]
    692753\frametitle{Assembler correctness}
    693754Assembler outputs \structure{labelled} object code and the \structure{cost map}
Note: See TracChangeset for help on using the changeset viewer.