Changeset 3297


Ignore:
Timestamp:
May 15, 2013, 10:51:15 PM (4 years ago)
Author:
tranquil
Message:

final version

File:
1 edited

Legend:

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

    r3287 r3297  
    128128\hskip -42.5pt\overbrace{\hskip 42.5pt\s{LIN}}^{\text{linearisation}}}^{\texttt{joint}\text{ languages}}\longrightarrow
    129129\hskip -42.5pt\underbrace{\hskip 42.5pt\s{ASM}}_{\text{linear map}}}^{\texttt{abstract\_status}\text{ (structured traces)}}$$
     130\vskip 20pt
     131In the process a \structure{stack model} is produced: each function is assigned
     132its stack cost
    130133\end{frame}
    131134%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    133136%[]
    134137\frametitle{Back-end correctness}
    135 \begin{theorem}
     138\structure{Hypotheses}
     139\begin{itemize}
     140 \item A \structure{RTLabs program} compiling to an \structure{ASM program} and
     141 a \structure{stack model}
     142 \item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
     143 the RTLabs program,
     144 \structure{respecting the stack bounds } imposed by the stack model
     145\end{itemize}
     146\structure{Result}
     147\begin{itemize}
     148\item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
     149the ASM output, \structure{with the same observables} (denoted by $\approx$)
     150\end{itemize}
    136151  $$ \begin{tikzpicture}
    137152     \node (s1) [is other, label=above:$s_1$] {};
     
    154169    \end{tikzpicture}
    155170$$
    156 \begin{itemize}
    157  \item $\approx$ denotes having the same \structure{observables} (labels, calls, returns)
    158  \item The RTLabs traces respect stack bounds
    159 \end{itemize}
    160 \end{theorem}
    161 
     171\end{frame}
     172%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     173\begin{frame}%
     174[label=assembler]
     175\frametitle{Assembler correctness}
     176\structure{Hypotheses}
     177\begin{itemize}
     178 \item An \structure{ASM program} successfully assembling to
     179 \structure{labelled object code} with attached \structure{cost map}
     180 \item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
     181    the ASM program
     182\end{itemize}
     183\structure{Result}
     184\begin{itemize}
     185 \item A prefix \structure{unstructured trace} followed by a \structure{structured one} of
     186the ASM output, \structure{with the same observables}
     187\end{itemize}
     188  $$
     189  \begin{gathered}
     190 \begin{tikzpicture}
     191     \node (s1) [is other, label=above:$s_1$] {};
     192     \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
     193     \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
     194     \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
     195     \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
     196     \begin{scope}[blue]
     197     \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
     198     \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
     199     \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
     200     \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
     201     \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
     202     \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
     203     \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
     204     \end{scope}
     205     \node (l1) [left=of s1] {ASM:};
     206     \node (l2) [left=of s2] {LOC:};
     207     \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
     208    \end{tikzpicture}
     209  \end{gathered}
     210$$
     211\vskip -5pt
     212\begin{itemize}
     213 \item The machine cost \structure{equals} the cost according to
     214 the cost map: $\sum_{\alpha\in m_2\to t_2}\costmap(\alpha) =
     215\clock(t_2) - \clock(m_2)$
     216\end{itemize}
    162217\end{frame}
    163218%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    225280\begin{frame}%
    226281%[]
    227 \frametitle{Extensional simulation}
     282\frametitle{From extensional to intensional simulation}
    228283\begin{itemize}
    229284 \item Usual \structure{extensional} simulation ($S$ for semantical relation):
     
    288343\frametitle{Preserving calls}
    289344\begin{itemize}
    290  \item If we want to localise simulation result, we need need something to preserve
     345 \item If we want to localise simulation result, we need some global info to preserve
    291346     the \tikz{\node (a) [is call] {}; \node [right=of a, is other] (b) {}; \draw [densely dashed, thick] (a) -- (b);}
    292347     relation
    293  \item We use a \structure{call relation} $C$ (based on program counters)
     348 \item We use a \structure{call relation} $C$, relating call locations in the code
    294349 \item For call states, we finally ask
    295350 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick]
     
    322377\begin{itemize}
    323378 \item How do we put to use the $C$ relation?
    324  \item Define relation $R$ as
     379 \item Define \structure{return relation} $R$ as
    325380 $$ \tikz[vcenter, start chain=going below, node distance=8mm] {
    326381     \node [on, is other, label=right:$s_1$] {}; \node [on, is other, label=right:$s_2$] {};
     
    499554\frametitle{Back to back-end correctness}
    500555\begin{theorem}
     556Provided the RTLabs traces respect stack bounds we have
    501557  $$ \begin{tikzpicture}
    502558     \node (s1) [is other, label=above:$s_1$] {};
     
    559615  \item We use stack usage hypothesis (coming from front-end correctness)
    560616  to ensure error does not occur
    561   \item States need not be remapped
     617  \item States need not be remapped, 1-1 simulation
    562618 \end{itemize}
    563619 \item \structure{Unique bounded stack space}
    564620 \begin{itemize}
    565621  \item Remap states, absence of stack overflow errors ensures this can be done
    566   correctly
     622  correctly, 1-1 simulation
    567623 \end{itemize}
    568624\end{enumerate}
     
    707763 function bodies have preambles
    708764 \item Status: the scaffolding underlying all graph passes
    709  is done. The proof obligations regarding this particular pass are open
     765 is done. The (extensional) proof obligations regarding this particular pass are open
    710766\end{itemize}
    711767\end{frame}
     
    720776function bodies have preambles
    721777\item  Status: the scaffolding underlying all graph passes
    722  is done. The proof obligations regarding this particular pass are almost finished
     778 is done. The (extensional) proof obligations regarding this particular pass are almost finished
    723779\end{itemize}
    724780\end{frame}
     
    731787 \item From the intensional point of view, calls can have suffixes (GOTOs)
    732788 \item Status: the generic linearisation scaffolding is complete.
    733  The proof obligations regarding this particular pass are open (but easy)
     789 The lacking proof obligations regard only the easy (extensional) fact that the common
     790 LTL/LIN semantics is oblivious to program counter remapping
    734791\end{itemize}
    735792
     
    749806\section{Assembler correctness}
    750807
    751 \begin{frame}%
    752 %[]
    753 \frametitle{Assembler correctness}
    754 Assembler outputs \structure{labelled} object code and the \structure{cost map}
    755 \begin{theorem}
    756   $$ \begin{tikzpicture}
    757      \node (s1) [is other, label=above:$s_1$] {};
    758      \node (m1) [is other, label=above:$m_1$, right=4cm of s1] {};
    759      \node (t1) [is other, label=above:$t_1$, right=4cm of m1] {};
    760      \draw [-stealth] (s1) -- node [above] {unstructured trace} (m1);
    761      \draw [-stealth] (m1) -- node [above] {structured trace} (t1);
    762      \begin{scope}[blue]
    763      \node (s2) [is other, label=below:$s_2$, below=1cm of s1] {};
    764      \node (m2) [is other, label=below:$m_2$, right=4cm of s2] {};
    765      \node (t2) [is other, label=below:$t_2$, right=4cm of m2] {};
    766      \draw [-stealth] (s2) -- node [below] {unstructured trace} (m2);
    767      \draw [-stealth] (m2) -- node [below] {structured trace} (t2);
    768      \path ($(s1)!.5!(m1)$) -- node [sloped] {\LARGE$\approx$} ($(s2)!.5!(m2)$);
    769      \path ($(m1)!.5!(t1)$) -- node [sloped] {\LARGE$\approx$} ($(m2)!.5!(t2)$);
    770      \end{scope}
    771      \node (l1) [left=of s1] {ASM:};
    772      \node (l2) [left=of s2] {LOC:};
    773      \node [rotate=-90, blue] at ($(l1)!.5!(l2)$) {$\Rightarrow$};
    774     \end{tikzpicture}
    775 $$
    776 and
    777 $$
    778 \sum_{\mathclap{l\in\text{ASM structured trace}}}\costmap(l) =
    779 \clock(t_2) - \clock(m_2)$$
    780 \end{theorem}
    781 \end{frame}
    782 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    783 \begin{frame}%
    784 %[]
    785 \frametitle{Preserving the traces}
    786 \begin{itemize}
    787  \item The preservation of structured traces part is as in the back-end
     808\againframe{assembler}
     809
     810\begin{frame}%
     811%[]
     812\frametitle{ASM $\to$ labelled object code}
     813\begin{itemize}
     814 \item The preservation of structured traces part is as in the back-end: find
     815 $S$ relation, define $C$ relation
    788816 \item A novelty in the extensional part is our proof of the correctness
    789  of a branch displacement algorithm
     817 of a branch displacement algorithm (done)
    790818\end{itemize}
    791819\end{frame}
     
    806834 \item When returning from a call, we land at the correct point in the block
    807835     whose cost was already paid by a label
     836 \item Status: done
    808837 \end{itemize}
    809838\end{itemize}
    810839
    811840\end{frame}
     841%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     842\begin{frame}%
     843%[]
     844\frametitle{Conclusion}
     845\begin{itemize}
     846 \item The executable compiler is complete
     847 \item Much effort has gone in providing generic scaffolding:
     848 structured traces preservation, graph translations and linearisation, all complete
     849 \item The scaffolding will scale to any change in the back-end (different architecture,
     850 possible different linearisation passes)
     851 \item Correctness of the cost static analysis
     852 \item \structure{Intensional} parts complete, up to \structure{extensional} holes in the proofs
     853\end{itemize}
     854
     855\end{frame}
     856
    812857
    813858\end{document}
Note: See TracChangeset for help on using the changeset viewer.