Changeset 3287

Timestamp:

May 14, 2013, 3:58:12 PM (4 years ago)

Author:

tranquil

Message:

back-end slides

File:

• Deliverables/Dissemination/back-end/back-end.tex (modified) (2 diffs)

Deliverables/Dissemination/back-end/back-end.tex

@@ -491 +491 @@
 \item The issues with defining a good $S$ are no different than in extensional proofs
 \item $C$ is defined based on program counters only
+\item The Matita proof is \structure{complete}
 \end{itemize}
 \end{frame}
@@ -685 +686 @@
 \end{columns}
 \end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}%
-%[]
+\section{Details on the passes}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}%
+%[]
+\frametitle{RTLabs $\to$ RTL}
+\begin{itemize}
+ \item Most of the effort must go to the \structure{extensional} part, as multi-byte operations
+ are replaced by sequences of single byte operations
+ \item Status: sketched
+\end{itemize}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}%
+%[]
+\frametitle{RTL $\to$ ERTL}
+\begin{itemize}
+ \item A \structure{graph} pass
+ \item Implements the calling convention, with the first accesses to stack
+ \item From the intensional point of view: calls have prefixes and suffixes, and
+ function bodies have preambles
+ \item Status: the scaffolding underlying all graph passes
+ is done. The proof obligations regarding this particular pass are open
+\end{itemize}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}%
+%[]
+\frametitle{ERTL $\to$ LTL}
+\begin{itemize}
+\item A \structure{graph} pass
+\item Register allocation, spilling, saving and restoring callee-saved hardware registers
+\item From the intensional point of view, calls to pointer have prefixes, and
+function bodies have preambles
+\item  Status: the scaffolding underlying all graph passes
+ is done. The proof obligations regarding this particular pass are almost finished
+\end{itemize}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}%
+%[]
+\frametitle{LTL $\to$ LIN}
+\begin{itemize}
+ \item A \structure{linearisation}
+ \item From the intensional point of view, calls can have suffixes (GOTOs)
+ \item Status: the generic linearisation scaffolding is complete.
+ The proof obligations regarding this particular pass are open (but easy)
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}%
+%[]
+\frametitle{LIN $\to$ ASM}
+\begin{itemize}
+\item A 1-to-1 simulation
+\item Function names and code labels are collapsed in the same global namespace
+\item Status: open
+\end{itemize}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 \section{Assembler correctness}
 
+\begin{frame}%
+%[]
 \frametitle{Assembler correctness}
 Assembler outputs \structure{labelled} object code and the \structure{cost map}