Changeset 3297 for Deliverables/Dissemination

Timestamp:

May 15, 2013, 10:51:15 PM (8 years ago)

Author:

tranquil

Message:

final version

File:

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

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

@@ -128 +128 @@
 \hskip -42.5pt\overbrace{\hskip 42.5pt\s{LIN}}^{\text{linearisation}}}^{\texttt{joint}\text{ languages}}\longrightarrow
 \hskip -42.5pt\underbrace{\hskip 42.5pt\s{ASM}}_{\text{linear map}}}^{\texttt{abstract\_status}\text{ (structured traces)}}$$
+\vskip 20pt
+In the process a \structure{stack model} is produced: each function is assigned
+its stack cost
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -133 +136 @@
 %[]
 \frametitle{Back-end correctness}
-\begin{theorem}
+\structure{Hypotheses}
+\begin{itemize}
+ \item A \structure{RTLabs program} compiling to an \structure{ASM program} and
+ a \structure{stack model}
+ \item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
+ the RTLabs program, 
+ \structure{respecting the stack bounds } imposed by the stack model
+\end{itemize}
+\structure{Result}
+\begin{itemize}
+\item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
+the ASM output, \structure{with the same observables} (denoted by $\approx$)
+\end{itemize}
   $$ \begin{tikzpicture}
      \node (s1) [is other, label=above:$s_1$] {};
@@ -154 +169 @@
     \end{tikzpicture}
 $$
-\begin{itemize}
- \item $\approx$ denotes having the same \structure{observables} (labels, calls, returns)
- \item The RTLabs traces respect stack bounds
-\end{itemize}
-\end{theorem}
-
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}%
+[label=assembler]
+\frametitle{Assembler correctness}
+\structure{Hypotheses}
+\begin{itemize}
+ \item An \structure{ASM program} successfully assembling to
+ \structure{labelled object code} with attached \structure{cost map}
+ \item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
+    the ASM program
+\end{itemize}
+\structure{Result}
+\begin{itemize}
+ \item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
+the ASM output, \structure{with the same observables}
+\end{itemize}
+  $$
+  \begin{gathered}
+ \begin{tikzpicture}
+     \node (s1) [is other, label=above:$s_1$] {};
+     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
+     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
+     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
+     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
+     \begin{scope}[blue]
+     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
+     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
+     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
+     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
+     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
+     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
+     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
+     \end{scope}
+     \node (l1) [left=of s1] {ASM:};
+     \node (l2) [left=of s2] {LOC:};
+     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
+    \end{tikzpicture}
+  \end{gathered}
+$$
+\vskip -5pt
+\begin{itemize}
+ \item The machine cost \structure{equals} the cost according to
+ the cost map: $\sum_{\alpha\in m_2\to t_2}\costmap(\alpha) =
+\clock(t_2) - \clock(m_2)$
+\end{itemize}
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -225 +280 @@
 \begin{frame}%
 %[]
-\frametitle{Extensional simulation}
+\frametitle{From extensional to intensional simulation}
 \begin{itemize}
  \item Usual \structure{extensional} simulation ($S$ for semantical relation):
@@ -288 +343 @@
 \frametitle{Preserving calls}
 \begin{itemize}
- \item If we want to localise simulation result, we need need something to preserve
+ \item If we want to localise simulation result, we need some global info to preserve
      the \tikz{\node (a) [is call] {}; \node [right=of a, is other] (b) {}; \draw [densely dashed, thick] (a) -- (b);}
      relation
- \item We use a \structure{call relation} $C$ (based on program counters)
+ \item We use a \structure{call relation} $C$, relating call locations in the code
  \item For call states, we finally ask
  $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
@@ -322 +377 @@
 \begin{itemize}
  \item How do we put to use the $C$ relation?
- \item Define relation $R$ as
+ \item Define \structure{return relation} $R$ as
  $$ \tikz[vcenter, start chain=going below, node distance=8mm] {
      \node [on, is other, label=right:$s_1$] {}; \node [on, is other, label=right:$s_2$] {};
@@ -499 +554 @@
 \frametitle{Back to back-end correctness}
 \begin{theorem}
+Provided the RTLabs traces respect stack bounds we have
   $$ \begin{tikzpicture}
      \node (s1) [is other, label=above:$s_1$] {};
@@ -559 +615 @@
   \item We use stack usage hypothesis (coming from front-end correctness)
   to ensure error does not occur
-  \item States need not be remapped
+  \item States need not be remapped, 1-1 simulation
  \end{itemize}
  \item \structure{Unique bounded stack space}
  \begin{itemize}
   \item Remap states, absence of stack overflow errors ensures this can be done
-  correctly
+  correctly, 1-1 simulation
  \end{itemize}
 \end{enumerate}
@@ -707 +763 @@
  function bodies have preambles
  \item Status: the scaffolding underlying all graph passes
- is done. The proof obligations regarding this particular pass are open
+ is done. The (extensional) proof obligations regarding this particular pass are open
 \end{itemize}
 \end{frame}
@@ -720 +776 @@
 function bodies have preambles
 \item  Status: the scaffolding underlying all graph passes
- is done. The proof obligations regarding this particular pass are almost finished
+ is done. The (extensional) proof obligations regarding this particular pass are almost finished
 \end{itemize}
 \end{frame}
@@ -731 +787 @@
  \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)
+ The lacking proof obligations regard only the easy (extensional) fact that the common
+ LTL/LIN semantics is oblivious to program counter remapping
 \end{itemize}
 
@@ -749 +806 @@
 \section{Assembler correctness}
 
-\begin{frame}%
-%[]
-\frametitle{Assembler correctness}
-Assembler outputs \structure{labelled} object code and the \structure{cost map}
-\begin{theorem}
-  $$ \begin{tikzpicture}
-     \node (s1) [is other, label=above:$s_1$] {};
-     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
-     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
-     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
-     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
-     \begin{scope}[blue]
-     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
-     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
-     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
-     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
-     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
-     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
-     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
-     \end{scope}
-     \node (l1) [left=of s1] {ASM:};
-     \node (l2) [left=of s2] {LOC:};
-     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
-    \end{tikzpicture}
-$$
-and
-$$
-\sum_{\mathclap{l\in\text{ASM structured trace}}}\costmap(l) =
-\clock(t_2) - \clock(m_2)$$
-\end{theorem}
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}%
-%[]
-\frametitle{Preserving the traces}
-\begin{itemize}
- \item The preservation of structured traces part is as in the back-end
+\againframe{assembler}
+
+\begin{frame}%
+%[]
+\frametitle{ASM $\to$ labelled object code}
+\begin{itemize}
+ \item The preservation of structured traces part is as in the back-end: find
+ $S$ relation, define $C$ relation
  \item A novelty in the extensional part is our proof of the correctness
- of a branch displacement algorithm
+ of a branch displacement algorithm (done)
 \end{itemize}
 \end{frame}
@@ -806 +834 @@
  \item When returning from a call, we land at the correct point in the block
      whose cost was already paid by a label
+ \item Status: done
  \end{itemize}
 \end{itemize}
 
 \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}%
+%[]
+\frametitle{Conclusion}
+\begin{itemize}
+ \item The executable compiler is complete
+ \item Much effort has gone in providing generic scaffolding:
+ structured traces preservation, graph translations and linearisation, all complete
+ \item The scaffolding will scale to any change in the back-end (different architecture,
+ possible different linearisation passes)
+ \item Correctness of the cost static analysis
+ \item \structure{Intensional} parts complete, up to \structure{extensional} holes in the proofs
+\end{itemize}
+
+\end{frame}
+
 
 \end{document}