Changeset 3297
 Timestamp:
 May 15, 2013, 10:51:15 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/Dissemination/backend/backend.tex
r3287 r3297 128 128 \hskip 42.5pt\overbrace{\hskip 42.5pt\s{LIN}}^{\text{linearisation}}}^{\texttt{joint}\text{ languages}}\longrightarrow 129 129 \hskip 42.5pt\underbrace{\hskip 42.5pt\s{ASM}}_{\text{linear map}}}^{\texttt{abstract\_status}\text{ (structured traces)}}$$ 130 \vskip 20pt 131 In the process a \structure{stack model} is produced: each function is assigned 132 its stack cost 130 133 \end{frame} 131 134 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% … … 133 136 %[] 134 137 \frametitle{Backend 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 149 the ASM output, \structure{with the same observables} (denoted by $\approx$) 150 \end{itemize} 136 151 $$ \begin{tikzpicture} 137 152 \node (s1) [is other, label=above:$s_1$] {}; … … 154 169 \end{tikzpicture} 155 170 $$ 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 186 the 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} 162 217 \end{frame} 163 218 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% … … 225 280 \begin{frame}% 226 281 %[] 227 \frametitle{ Extensional simulation}282 \frametitle{From extensional to intensional simulation} 228 283 \begin{itemize} 229 284 \item Usual \structure{extensional} simulation ($S$ for semantical relation): … … 288 343 \frametitle{Preserving calls} 289 344 \begin{itemize} 290 \item If we want to localise simulation result, we need need somethingto preserve345 \item If we want to localise simulation result, we need some global info to preserve 291 346 the \tikz{\node (a) [is call] {}; \node [right=of a, is other] (b) {}; \draw [densely dashed, thick] (a)  (b);} 292 347 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 294 349 \item For call states, we finally ask 295 350 $$ \begin{tikzpicture}[every join/.style={ar}, join all, thick] … … 322 377 \begin{itemize} 323 378 \item How do we put to use the $C$ relation? 324 \item Define relation$R$ as379 \item Define \structure{return relation} $R$ as 325 380 $$ \tikz[vcenter, start chain=going below, node distance=8mm] { 326 381 \node [on, is other, label=right:$s_1$] {}; \node [on, is other, label=right:$s_2$] {}; … … 499 554 \frametitle{Back to backend correctness} 500 555 \begin{theorem} 556 Provided the RTLabs traces respect stack bounds we have 501 557 $$ \begin{tikzpicture} 502 558 \node (s1) [is other, label=above:$s_1$] {}; … … 559 615 \item We use stack usage hypothesis (coming from frontend correctness) 560 616 to ensure error does not occur 561 \item States need not be remapped 617 \item States need not be remapped, 11 simulation 562 618 \end{itemize} 563 619 \item \structure{Unique bounded stack space} 564 620 \begin{itemize} 565 621 \item Remap states, absence of stack overflow errors ensures this can be done 566 correctly 622 correctly, 11 simulation 567 623 \end{itemize} 568 624 \end{enumerate} … … 707 763 function bodies have preambles 708 764 \item Status: the scaffolding underlying all graph passes 709 is done. The proof obligations regarding this particular pass are open765 is done. The (extensional) proof obligations regarding this particular pass are open 710 766 \end{itemize} 711 767 \end{frame} … … 720 776 function bodies have preambles 721 777 \item Status: the scaffolding underlying all graph passes 722 is done. The proof obligations regarding this particular pass are almost finished778 is done. The (extensional) proof obligations regarding this particular pass are almost finished 723 779 \end{itemize} 724 780 \end{frame} … … 731 787 \item From the intensional point of view, calls can have suffixes (GOTOs) 732 788 \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 734 791 \end{itemize} 735 792 … … 749 806 \section{Assembler correctness} 750 807 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 backend 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 backend: find 815 $S$ relation, define $C$ relation 788 816 \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) 790 818 \end{itemize} 791 819 \end{frame} … … 806 834 \item When returning from a call, we land at the correct point in the block 807 835 whose cost was already paid by a label 836 \item Status: done 808 837 \end{itemize} 809 838 \end{itemize} 810 839 811 840 \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 backend (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 812 857 813 858 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.