# Changeset 3297 for Deliverables/Dissemination

Ignore:
Timestamp:
May 15, 2013, 10:51:15 PM (7 years ago)
Message:

final version

File:
1 edited

### Legend:

Unmodified
 r3287 \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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %[] \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$] {}; \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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}% %[] \frametitle{Extensional simulation} \frametitle{From extensional to intensional simulation} \begin{itemize} \item Usual \structure{extensional} simulation (S for semantical relation): \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] \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] {}; \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$] {}; \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} 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} 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} \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} \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} \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}