Changeset 3269


Ignore:
Timestamp:
May 14, 2013, 5:47:32 AM (4 years ago)
Author:
stark
Message:

Some revised slides in front end, not complete

File:
1 edited

Legend:

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

    r3267 r3269  
    2626\begin{document}
    2727
    28 \title{Front-end Correctness Proofs}
    29 \author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark}
     28\title{WP3: Verified Compiler --- Front End\\[1\jot]
     29D3.4: Front-End Correctness Proofs}
     30\author{Brian~Campbell, Ilias~Garnier, James~McKinna, \underline{Ian~Stark}}
    3031\institute{LFCS, University of Edinburgh\\[1ex]
    3132\includegraphics[width=.3\linewidth]{cerco_logo.png}\\
     
    3536\maketitle
    3637
    37 \frame{
    38 \frametitle{Introduction}
    39 
    40 D3.4 consists of the front-end correctness proofs:
    41 
    42 \begin{description}
    43 \item[Primary focus:] novel \red{intensional} properties: \blue{cost
    44     bound correctness}
    45 \end{description}
    46 \vskip-2ex
    47 \begin{itemize}
    48 \item Now have \blue{stack} costs as well as \blue{time}\\
    49 --- yields stronger overall correctness result
    50 \item Informed by earlier formal experiment with a toy compiler.
    51 \end{itemize}
    52 
    53 \medskip
    54 \begin{description}
    55 \item[Secondary focus:] usual \red{extensional} result: \blue{functional correctness}
    56 \end{description}
    57 \vskip-2ex
    58 \begin{itemize}
    59 \item Similar functional correctness already studied in
    60 \blue{CompCert}
    61 \item Axiomatize similar results
    62 \item \red{Intensional} proofs form a layer on top
    63 \end{itemize}
    64 }
     38
     39\begin{frame}{CerCo Outcomes}
     40
     41  The final results of the CerCo project include the following:
     42
     43  \medskip %
     44  \begin{itemize}
     45  \item A compiler from C to executable 8051 binaries, formalised in Matita as
     46    \blue{\lstinline|compiler.ma|} \dots
     47  \item \dots which adds labels and cost information to C source code
     48  \item \dots with exact values for time and space used by the binary.
     49
     50    \medskip %
     51  \item A machine-checked proof of this in Matita
     52    \blue{\lstinline|correctness.ma|}:
     53
     54    \smallskip %
     55    \begin{itemize}
     56    \item Addressing \red{intensional} properties --- clock cycles, stack bytes
     57
     58      \smallskip %
     59    \item As well as \red{extensional} properties --- functional correctness.
     60    \end{itemize}
     61  \item An executable cost-annotating compiler \blue{\lstinline|cerco|}
     62    extracted from the formalisation.
     63  \end{itemize}
     64
     65  \medskip %
     66  This talk treats the front-end compiler and proof, describing the technical
     67  challenges and contributions from the work in Period~3.
     68 
     69\end{frame}
     70
     71\begin{frame}{Compiler}
     72
     73  The CerCo compiler, given C source code, will generate:
     74  \begin{itemize}
     75  \item Labelled Clight source code;
     76  \item Labelled 8051 object code;
     77  \item Cost maps: for each label a count of time (clock cycles) and space
     78    (stack bytes) usage.
     79  \end{itemize}
     80
     81  \medskip %
     82  The compiler operates in multiple passes, with each intermediate language
     83  having an executable semantics in Matita: %
     84  \vspace*{-\medskipamount}
     85  \begin{center}
     86    \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
     87  \end{center}
     88  \vspace*{-\medskipamount}
     89
     90\end{frame}
     91
     92\begin{frame}{Correctness}
     93 
     94  Suppose we have C source with labelled Clight, labelled 8051 binary, and
     95  cost maps all generated from the CerCo compiler.
     96
     97  \medskip %
     98  Then the Matita theorem for correctness is that:
     99  \begin{itemize}
     100  \item Executing the original and labelled Clight source gives the same
     101    behaviour;
     102  \item Executing the 8051 binary gives the same observables: labels and
     103    call/return;
     104  \item Applying the cost maps to the trace of C labels correctly
     105    describes the time and space usage of the 8051 execution.
     106  \end{itemize}
     107
     108  In fact we give an exact result on all \red{measurable subtraces}: from any
     109  label to the end of its enclosing function.
     110
     111  \medskip %
     112  The machine-checked proof is the concatenation of correctness results for
     113  the front end, the back end, and the assembler.
     114
     115\end{frame}
     116
     117\begin{frame}{Front-End Progress}
     118 
     119  \vspace*{-\bigskipamount}
     120  \begin{center}
     121    \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
     122  \end{center}
     123  \vspace*{-\medskipamount}
     124
     125  At the start of Period~3 the front end included in Matita:
     126  \begin{itemize}
     127  \item Executable semantics for source and intermediate languages;
     128  \item Labelling and compilation of source through these;
     129  \item Innovation of \red{structured traces}, originally to support timing
     130    computation in the assembler.
     131  \end{itemize}
     132
     133  At the completion of Period~3, the front end included proofs of correctness
     134  for all these, extension to stack usage, and considerable refinement of the
     135  existing formal development.
     136 
     137\end{frame}
     138
     139\begin{frame}{Front-End Contribution}
     140
     141  Notable features and original elements of the front-end include:
     142  \begin{itemize}
     143  \item Proof layering:
     144    \begin{itemize}
     145    \item A \blue{functional correctness proof};
     146    \item A \blue{cost proof}, separate but depending on functional
     147      correctness.
     148    \end{itemize}
     149  \item \blue{Internal checks} as a proof shortcut, like translation
     150    validation.
     151  \item \blue{Structured traces} for holding detailed data on resource
     152    behaviour, not just for assembler cost calculation.
     153  \item Introduction of \blue{measurable subtraces} as a unit of cost
     154    proof.
     155  \end{itemize}
     156  These features are significant in particular because:
     157  \begin{itemize}
     158  \item Compilation is not 1-1 transliteration: code is rearranged and
     159    modified, but label sequencing is preserved;
     160  \item The source language has implicit control flow constraints not present
     161    in the target (call/return, branches, loops).
     162  \end{itemize}
     163
     164\end{frame}
     165
     166\begin{frame}{Axiomatization}
     167
     168  The translation in \blue{\lstinline|compile.ma|} is complete --- essential
     169  for extracting a compiler.
     170
     171  \medskip %
     172  The simulation results in \blue{\lstinline|correctness.ma|} are fully
     173  specified, and with substantially complete proofs.  Some parts, however,
     174  have been axiomatized and their correctness assumed.
     175
     176  \medskip %
     177  In the front-end there are two sources of this axiomatisation:
     178  \begin{itemize}
     179  \item \red{Functional correctness.}  Other projects, notably
     180    \blue{CompCert}, provide assurances that such proofs can be completed; so
     181    certain parts of this proof have been assumed.
     182  \item Simulation steps with \red{many cases}, sometimes similar; here we
     183    have identified representative and more challenging cases for detailed
     184    proof.
     185  \end{itemize}
     186 
     187\end{frame}
     188
     189\begin{frame}[fragile]
     190\frametitle{Structure of the Proof}
     191
     192\begin{center}
     193\includegraphics[width=0.7\linewidth]{compiler.pdf}
     194\end{center}
     195
     196The transition from front-end to back-end marks the change:
     197\begin{itemize}
     198\item From a language with explicit call/return structure and high-level
     199  control flow;
     200\item To a language with explicit addresses and control-flow graph.
     201\end{itemize}
     202
     203Correspondingly, the proof hands over
     204\begin{itemize}
     205\item From measurable subtraces with labelling that must be checked
     206  \blue{sound} and \blue{precise};
     207\item To \blue{structured traces} which embed these invariants.
     208\end{itemize}
     209
     210\end{frame}
     211
     212
     213% \frame{
     214% \frametitle{Introduction}
     215
     216% D3.4 is the front-end correctness proofs:
     217
     218% \begin{description}
     219% \item[Primary focus:] novel \red{intensional} properties: \blue{cost
     220%     bound correctness}
     221% \item[Secondary:] usual \red{extensional} result: \blue{functional correctness}
     222% \end{description}
     223
     224% Functional correctness for similar compilers already studied in
     225% Leroy et al.'s \blue{CompCert}.
     226% \begin{itemize}
     227% \item Axiomatize similar results
     228% \end{itemize}
     229
     230% \medskip
     231% Now have \blue{stack} costs as well as \blue{time}
     232% \begin{itemize}
     233% \item yields stronger overall correctness result
     234% \end{itemize}
     235
     236% \medskip
     237% \alert{Extract} compiler code from development for practical execution.
     238
     239% \medskip
     240% Informed by earlier formal experiment with a toy compiler.
     241% }
    65242
    66243% TODO: could reuse some of this to make stronger intro?
     
    93270% }
    94271
    95 \frame{
    96 \frametitle{Outline}
    97 \tableofcontents
    98 }
    99 
    100 \section{CerCo Compiler}
    101 
    102 \frame{
    103 \frametitle{CerCo compiler}
    104 
    105 \begin{center}
    106 \includegraphics[width=0.6\linewidth]{compiler-plain.pdf}
    107 \end{center}
    108 
    109 \begin{itemize}
    110 \item Reuse unverified CompCert \alert{parser}
    111 %\item Transform away troublesome constructs
    112 %  \begin{itemize}
    113 %  \item e.g.~\texttt{switch}
    114 %  \item fallthrough requires slightly more sophisticated labelling
    115 %  \item but not fundamentally different
    116 %  \end{itemize}
    117 \item Intermediate language for most passes
    118 \item \alert{Executable semantics} for each
    119 \item \alert{Extract} OCaml compiler code from development
    120 \item Outputs
    121   \begin{itemize}
    122   \item \alert{8051 machine code}
    123   \item Clight code instrumented with costs in 8051 \alert{clock cycles} and
    124     \alert{bytes of stack space}
    125   \end{itemize}
    126 \end{itemize}
    127 Instrumentation updates global cost variable; suitable for further analysis and
    128 verification.
    129 }
    130 
    131 \section{Overall correctness}
    132 
    133 \begin{frame}[fragile]
    134 \frametitle{Correctness of labelling approach}
    135 
    136 \begin{tabular}{ccc}
    137 
    138 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    139                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    140 char f(char x) {
    141   char y;
    142   _cost3:
    143   if (x>10) {
    144     _cost1:
    145     y = g(x);
    146   } else {
    147     _cost2:
    148     y = 5;
    149   }
    150   return y+1;
    151 }
    152 \end{lstlisting}
    153 
    154 &
    155 
    156 \begin{minipage}{9em}
    157 \begin{center}
    158 $\Rightarrow$\\[4ex]
    159 \blue{soundness}\\[2ex]
    160 \red{precision}
    161 \end{center}
    162 \end{minipage}
    163 
    164 &
    165 
    166 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    167                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    168   "f"
    169     emit _cost3
    170     *** Prologue ***
    171     move A, R06
    172     clear CARRY
    173     ...
    174     branch A <> 0, f10
    175     emit _cost2
    176     imm R00, 5
    177     ...
    178     f10:
    179     emit _cost1
    180     call "g"
    181     ...
    182 \end{lstlisting}
    183 
    184 
    185 \end{tabular}
    186 
    187 From experiments with toy compiler [D2.1, FMICS'12]:
    188 \begin{enumerate}
    189 \item Functional correctness, \emph{including trace of labels}
    190 %\item Source labelling function is sound and precise
    191 %\item Preservation of soundness and precision of labelling
    192 \item Target labelling function is sound and precise
    193 % TODO: detail about soundness and precision?
    194 \item Target cost analysis produces a map of labels to times
    195   \begin{itemize}
    196   \item Accurate for sound and precise labellings
    197   \end{itemize}
    198 %\item Correctness of instrumentation
    199 \end{enumerate}
    200 
    201 \end{frame}
    202 
    203 %\frame{
    204 %\frametitle{}
    205 %
    206 %Due to resource constraints
    207 %\begin{itemize}
    208 %\item Instrumentation is done in language semantics
    209 %\item Soundness and precision of labelling is checked during compilation
    210 %  \begin{itemize}
    211 %  \item c.f.~translation validation
    212 %  \end{itemize}
    213 %\item Focusing effort on novel parts --- cost proofs over functional correctness
    214 %\end{itemize}
    215 %
    216 %}
    217 
    218 \begin{frame}[fragile]
    219 \frametitle{Overall correctness statement}
    220 
    221 \[ \text{max predicted stack usage} \leq \text{limit} \]
    222 implies
    223 \begin{itemize}
    224 \item successful execution, with
    225 \end{itemize}
    226 \begin{center}
    227 \fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
    228 \end{center}
    229 \end{frame}
    230 
    231 
    232 \begin{frame}[fragile]
    233 \frametitle{Overall correctness statement}
    234 
    235 \begin{center}
    236 \fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
    237 \end{center}
    238 
    239 %\pause
    240 
    241 \begin{center}
    242 \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c}
    243 
    244 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    245                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    246 int f(int x) {
    247   _cost1:
    248   int y = 0;
    249   while (x) {
    250     _cost2:
    251     y = g(y);
    252     x = x - 1;
    253   }
    254   _cost3:
    255   return y;
    256 }
    257 \end{lstlisting}
    258 
    259 &
    260 
    261 \begin{uncoverenv}<1-2>
    262 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    263                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    264 call f
    265 _cost1
    266 init y
    267 _cost2
    268 call g
    269 ...
    270 return g
    271 assign y
    272 decrement x
    273 test x
    274 _cost2
    275 ...
    276 _cost3
    277 return f
    278 \end{lstlisting}
    279 \end{uncoverenv}
    280 
    281 &
    282 
    283 \begin{uncoverenv}<2-4>
    284 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    285                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    286 call f
    287 _cost1
    288 
    289 _cost2
    290 call g
    291 ...
    292 return g
    293 
    294 
    295 
    296 _cost2
    297 ...
    298 _cost3
    299 return f
    300 \end{lstlisting}
    301 \end{uncoverenv}
    302 
    303 \end{tabular}
    304 \end{center}
    305 
    306 \begin{overprint}
    307  \onslide<1-2>
    308  \begin{itemize}
    309  \item Which parts can we measure execution costs of?
    310  \item Actual position of unobservable computation is unimportant
    311  \item Want to get \alert{exact} execution time
    312  \end{itemize}
    313 
    314  \onslide<3>
    315  \begin{itemize}
    316  \item Use labels and end of function as measurement points
    317  \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
    318  \item All costs are considered local to the function
    319  \end{itemize}
    320 
    321  \onslide<4>
    322  \begin{itemize}
    323  \item Use labels and end of function as measurement points
    324  \item[$\star$] Call suitable subtraces \alert{measurable}
    325  \item[$\star$] Core part is a proof that the trace \alert{terminates} at return
    326  \end{itemize}
    327 
    328 % \onslide<1>
     272% \frame{
     273% \frametitle{Outline}
     274% \tableofcontents
     275% }
     276
     277% \section{CerCo Compiler}
     278
     279% \frame{
     280% \frametitle{CerCo compiler}
     281
     282% \begin{center}
     283% \includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
     284% \end{center}
     285
     286% \begin{itemize}
     287% \item Reuse unverified CompCert parser
     288% %\item Transform away troublesome constructs
     289% %  \begin{itemize}
     290% %  \item e.g.~\texttt{switch}
     291% %  \item fallthrough requires slightly more sophisticated labelling
     292% %  \item but not fundamentally different
     293% %  \end{itemize}
     294% \item Intermediate language for most passes
     295% \item Executable semantics for each
     296% \item Outputs
     297%   \begin{itemize}
     298%   \item 8051 machine code
     299%   \item Clight code instrumented with costs in 8051 clock cycles and
     300%     bytes of stack space
     301%   \end{itemize}
     302% \end{itemize}
     303% Instrumentation updates global cost variable; suitable for further analysis and
     304% verification.
     305% }
     306
     307% \section{Overall correctness}
     308
     309% \begin{frame}[fragile]
     310% \frametitle{Correctness of labelling approach}
     311
     312% \begin{tabular}{ccc}
     313
     314% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
     315%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     316% char f(char x) {
     317%   char y;
     318%   _cost3:
     319%   if (x>10) {
     320%     _cost1:
     321%     y = g(x);
     322%   } else {
     323%     _cost2:
     324%     y = 5;
     325%   }
     326%   return y+1;
     327% }
     328% \end{lstlisting}
     329
     330% &
     331
     332% \begin{minipage}{9em}
     333% \begin{center}
     334% $\Rightarrow$\\[4ex]
     335% \blue{soundness}\\[2ex]
     336% \red{precision}
     337% \end{center}
     338% \end{minipage}
     339
     340% &
     341
     342% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
     343%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     344%   "f"
     345%     emit _cost3
     346%     *** Prologue ***
     347%     move A, R06
     348%     clear CARRY
     349%     ...
     350%     branch A <> 0, f10
     351%     emit _cost2
     352%     imm R00, 5
     353%     ...
     354%     f10:
     355%     emit _cost1
     356%     call "g"
     357%     ...
     358% \end{lstlisting}
     359
     360
     361% \end{tabular}
     362
     363% From experiments with toy compiler [D2.1, FMICS'12]:
     364% \begin{enumerate}
     365% \item Functional correctness, \emph{including trace of labels}
     366% %\item Source labelling function is sound and precise
     367% %\item Preservation of soundness and precision of labelling
     368% \item Target labelling function is sound and precise
     369% % TODO: detail about soundness and precision?
     370% \item Target cost analysis produces a map of labels to times
     371%   \begin{itemize}
     372%   \item Accurate for sound and precise labellings
     373%   \end{itemize}
     374% %\item Correctness of instrumentation
     375% \end{enumerate}
     376
     377% \end{frame}
     378
     379% %\frame{
     380% %\frametitle{}
     381% %
     382% %Due to resource constraints
     383% %\begin{itemize}
     384% %\item Instrumentation is done in language semantics
     385% %\item Soundness and precision of labelling is checked during compilation
     386% %  \begin{itemize}
     387% %  \item c.f.~translation validation
     388% %  \end{itemize}
     389% %\item Focusing effort on novel parts --- cost proofs over functional correctness
     390% %\end{itemize}
     391% %
     392% %}
     393
     394% \begin{frame}[fragile]
     395% \frametitle{Overall correctness statement}
     396
     397% \begin{center}
     398% \fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
     399% \end{center}
     400
     401% \pause
     402
     403% \begin{center}
     404% \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c}
     405
     406% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
     407%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     408% int f(int x) {
     409%   _cost1:
     410%   int y = 0;
     411%   while (x) {
     412%     _cost2:
     413%     y = g(y);
     414%     x = x - 1;
     415%   }
     416%   _cost3:
     417%   return y;
     418% }
     419% \end{lstlisting}
     420
     421% &
     422
     423% \begin{uncoverenv}<2-3>
     424% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
     425%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     426% call f
     427% _cost1
     428% init y
     429% _cost2
     430% call g
     431% ...
     432% return g
     433% assign y
     434% decrement x
     435% test x
     436% _cost2
     437% ...
     438% _cost3
     439% return f
     440% \end{lstlisting}
     441% \end{uncoverenv}
     442
     443% &
     444
     445% \begin{uncoverenv}<3-5>
     446% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
     447%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     448% call f
     449% _cost1
     450
     451% _cost2
     452% call g
     453% ...
     454% return g
     455
     456
     457
     458% _cost2
     459% ...
     460% _cost3
     461% return f
     462% \end{lstlisting}
     463% \end{uncoverenv}
     464
     465% \end{tabular}
     466% \end{center}
     467
     468% \begin{overprint}
     469% \onslide<2>
    329470% \begin{itemize}
    330471% \item Use labels and end of function as measurement points
     
    332473% \end{itemize}
    333474
    334 % \onslide<2-3>
     475% \onslide<3-4>
    335476% \begin{itemize}
    336477% \item Use labels and end of function as measurement points
     
    339480% \end{itemize}
    340481
    341 % \onslide<4>
     482% \onslide<5>
    342483% \begin{itemize}
    343484% \item Use labels and end of function as measurement points
     
    345486% \item[$\star$] Core part is a proof of \alert{termination}
    346487% \end{itemize}
    347 \end{overprint}
    348 
    349 \end{frame}
    350 
    351 \begin{frame}[fragile]
    352 \frametitle{Correct cost analysis depends on call structure}
    353 
    354 Two straight-line functions:
    355 
    356 \begin{center}
    357 \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}}
    358 
    359 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    360                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    361 "f"
    362   emit _cost1
    363   ...
    364   call "g"
    365   ...
    366   return
    367 \end{lstlisting}
    368 
    369 &
    370 
    371 \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    372                    emph={[2]_cost3},emphstyle={[2]\color{blue}},
    373                    escapechar=\%]
    374 "g"
    375   emit _cost2
    376   ...
    377   %\only<2->{\blue{increase return address}}%
    378   return
    379 \end{lstlisting}
    380 
    381 \end{tabular}
    382 \end{center}
    383 
    384 Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).
    385 
    386 \begin{itemize}
    387 \item<2-> Changing return address skips code from \lstinline'f'
    388 \item<2-> Cost no longer equals sum of cost labels
    389 \end{itemize}
    390 
    391 \onslide<2->
    392 \alert{Need to observe correct call/return structure.}
    393 
    394 \onslide<3>
    395 \emph{Not easy at ASM --- observe earlier in compiler \& maintain.}
    396 
    397 \end{frame}
    398 
    399 \section{Front-end correctness}
    400 
    401 \frame{
    402 \frametitle{Front-end correctness}
    403 
    404 Recalling the toy compiler, need
    405 \begin{enumerate}
    406 \item Functional correctness
    407 \item Cost labelling sound and precise
    408 \item\label{it:return} To demonstrate return addresses are correct
    409 \end{enumerate}
    410 % TODO: stack space?  from obs, from fnl correctness
    411 
    412 \bigskip
    413 For~\ref{it:return} we generalise notion of \emph{structured traces}
    414 originally introduced for the correctness of timing analysis.
    415 }
     488% \end{overprint}
     489
     490% \end{frame}
     491
     492% \begin{frame}[fragile]
     493% \frametitle{Correct cost analysis depends on call structure}
     494
     495% Two straight-line functions:
     496
     497% \begin{center}
     498% \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}}
     499
     500% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
     501%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     502% "f"
     503%   emit _cost1
     504%   ...
     505%   call "g"
     506%   ...
     507%   return
     508% \end{lstlisting}
     509
     510% &
     511
     512% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
     513%                    emph={[2]_cost3},emphstyle={[2]\color{blue}},
     514%                    escapechar=\%]
     515% "g"
     516%   emit _cost2
     517%   ...
     518%   %\only<2->{\blue{increase return address}}%
     519%   return
     520% \end{lstlisting}
     521
     522% \end{tabular}
     523% \end{center}
     524
     525% Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).
     526
     527% \begin{itemize}
     528% \item<2-> Changing return address skips code from \lstinline'f'
     529% \item<2-> Cost no longer equals sum of cost labels
     530% \end{itemize}
     531
     532% \onslide<2->
     533% \alert{Need to observe correct call/return structure.}
     534
     535% \onslide<3>
     536% \emph{Not easy at ASM --- observe earlier in compiler \& maintain.}
     537
     538% \end{frame}
     539
     540% \section{Front-end correctness}
     541
     542% \frame{
     543% \frametitle{Front-end correctness}
     544
     545% Recalling the toy compiler, need
     546% \begin{enumerate}
     547% \item Functional correctness
     548% \item Cost labelling sound and precise
     549% \item\label{it:return} To demonstrate return addresses are correct
     550% \end{enumerate}
     551% % TODO: stack space?  from obs, from fnl correctness
     552
     553% \bigskip
     554% For~\ref{it:return} we generalise notion of \emph{structured traces}
     555% originally introduced for the correctness of timing analysis.
     556% }
    416557
    417558\begin{frame}[fragile]
    418559\frametitle{Structured traces}
    419560
    420 \alert{Embed} the call/return structure into execution traces.
     561Embed call structure and label invariants into execution traces.
    421562
    422563\begin{center}
     
    425566
    426567\begin{itemize}
    427 \item Traces of \alert{called functions} are nested
    428 \item Invariants on positions of cost labels enforced
    429 \item Steps are \alert{grouped} according to cost label
    430 \item Forbid \alert{repeating} addresses in grouped steps for
    431   \blue{sound} labelling
    432 \end{itemize}
    433 
    434 % moved later
    435 %\onslide<2>
    436 %Construct by folding up \alert{measurable} subtrace, using soundness
    437 %and preciseness of labelling.
    438 
    439 \end{frame}
    440 
    441 \frame{
    442 \frametitle{Front-end correctness statement}
    443 
    444 Given a \red{measurable} subtrace of a \textbf{Clight} execution, including
    445 the \textbf{prefix} of that trace from initial state,
    446 
    447 \medskip
    448 we have in \textbf{RTLabs}
    449 \begin{itemize}
    450 \item a new \textbf{prefix}
    451 \item a \blue{structured trace} corresponding to \red{measurable}
    452   subtrace
    453 \item the no \blue{repeating} addresses property
    454 \item proof that the same \textbf{stack limit} is observed
    455 \end{itemize}
    456 which the back-end requires, and
    457 \begin{itemize}
    458 \item the observables for the \textbf{prefix} and \blue{structured
    459     trace} are the same as their \textbf{Clight} counterparts
    460 \end{itemize}
    461 which links the behaviour and costs to the original program.
    462 }
    463 
    464 \begin{frame}[fragile]
    465 \frametitle{Structure in the compiler proof}
    466 
    467 \begin{center}
    468 \includegraphics[width=0.8\linewidth]{compiler.pdf}
    469 \end{center}
    470 
    471 %\onslide<1>
    472 %\green{Assembler} provides part of local cost analysis (CPP'12).
    473 
    474 %\onslide<2-4>
    475 Switch at RTLabs:
    476 \begin{itemize}
    477 \item from \red{measurable} subtrace of \alert{sound} and \alert{precise}
    478 labelling
    479 \item to \blue{structured trace} where they are embedded
    480 \end{itemize}
    481 
    482 %\onslide<3>
    483 %Changes \blue{syntactic} properties of labelling into \blue{semantic}
    484 %properties.
    485 
    486 %\onslide<4>
    487 Reason for choice: first language with explicit \alert{addresses}, implicit
    488 \alert{call handling}.
    489 
    490 \end{frame}
    491 
    492 \section{Correctness proofs}
    493 \subsection{Generic lifting result}
     568\item Enforces \blue{invariants} on positions of cost labels.
     569\item \blue{Groups} execution steps according to preceding cost label.
     570\item Forbids \blue{repeating} addresses in grouped steps.
     571\end{itemize}
     572
     573Constructed by folding up measurable subtraces, using the fact that labelling
     574is sound and precise.
     575
     576\end{frame}
     577
     578\begin{frame}{Step-by-Step: Getting to Labelled Source}
     579
     580\blue{C $\to$ Clight}
     581
     582\smallskip %
     583To translate from C to Clight we reuse the CompCert parser.
     584
     585\bigskip %
     586\blue{Switch Removal}
     587
     588\smallskip %
     589Control flow for \red{\lstinline'switch'} is too subtle for simple labelling;
     590we replace with an \red{\lstinline'if .. then .. else'} tree.  Proof requires
     591tracking memory extension for an extra test variable.
     592
     593\bigskip %
     594\blue{Cost Labels}
     595
     596\smallskip %
     597Labels added at function start, branch targets, \dots
     598
     599\smallskip %
     600Simulation of execution is exact, just skipping over labels.
     601
     602\end{frame}
     603
     604\begin{frame}{Front-End Correctness}
     605
     606  Suppose we have a \blue{measurable} subtrace of Clight execution, including
     607  the \blue{prefix} of that trace from initial state.
     608
     609  \medskip %
     610  Then for handover to the back-end we have in RTLabs:
     611  \begin{itemize}
     612  \item A corresponding \red{prefix};
     613  \item A \red{structured trace} corresponding to the measurable subtrace;
     614  \item The required invariants, including \red{no repeating addresses};
     615  \item A proof that the same \red{stack limit} is observed.
     616  \end{itemize}
     617
     618  \medskip %
     619  In addition, to link this with the source program:
     620  \begin{itemize}
     621  \item The observables for the RLabs \blue{prefix} and \blue{structured
     622      trace} are the same as for their counterparts in Clight.
     623  \end{itemize}
     624
     625\end{frame}
     626
     627
     628% \section{Correctness proofs}
     629% \subsection{Generic lifting result}
    494630
    495631\begin{frame}[fragile]
     
    572708%\end{frame}
    573709
    574 \subsection{Simulations for compiler passes}
     710% \subsection{Simulations for compiler passes}
    575711
    576712%\frame{
     
    579715
    580716% TODO: perhaps much earlier for the pre-measurable bits?
    581 \frame{
    582 \frametitle{Simulation between input and annotated code}
    583 
    584 Two stages provide the annotated version of input:
    585 
    586 \bigskip
    587 Switch removal
    588 \begin{itemize}
    589 \item \lstinline[language=C]'switch' statement control flow too subtle
    590   for simple labelling
    591 \item Replaces with \lstinline[language=C]'if ... then ... else' tree
    592 \item Tricky part of proof: memory extension for extra variable
    593 \item Partial proof: enough to validate approach;\\
    594       \quad --- this stage not relevant to intensional properties
    595 \end{itemize}
    596 
    597 \bigskip
    598 Cost labelling
    599 \begin{itemize}
    600 \item For simulation don't care \emph{which} labels are added
    601 \item Just have to skip over extra cost label expressions and
    602   statements
    603 \item Complete simulation proof, simple
    604 \end{itemize}
    605 
    606 % TODO: consider whether to mention full simulation
    607 % termination-preserving proof?
    608 }
    609717
    610718\frame{
     
    639747\item But do have invariants:
    640748  \begin{itemize}
    641   \item[$\bullet$] Statements well-typed with respect to pseudo-register
     749  \item Statement well-typed with respect to pseudo-register
    642750    environment
    643   \item[$\bullet$] CFG complete
    644   \item[$\bullet$] Entry and exit nodes present, unique
     751  \item CFG complete
     752  \item Entry and exit nodes complete, unique
    645753  \end{itemize}
    646754\item Translation function is \emph{total} as a result
     
    650758% TODO: sloganize: proved more about unusual bits
    651759
    652 \section{Checking cost labelling properties}
     760% \section{Checking cost labelling properties}
    653761
    654762\frame{
     
    721829}
    722830
    723 \section{Construction of structured traces}
     831% \section{Construction of structured traces}
    724832
    725833\frame{
     
    739847}
    740848
    741 \section{Whole compiler}
     849% \section{Whole compiler}
    742850
    743851\begin{frame}[fragile]
     
    749857
    750858\begin{itemize}
    751 \item Instantiate measurable subtracing lifting with simulations
    752 \item Show existence of \textbf{RTLabs} structured trace
    753 \item Apply back-end to show \textbf{RTLabs} costs correct
    754 \item Use equivalence of observables to show \textbf{Clight} costs correct
    755 % \item `Clock' difference in Clight is sum of cost labels
    756 % \item Observables, including trace of labels, is preserved to ASM
    757 % \item Labelling at bottom level is sound and precise
    758 % \item Sum of labels at ASM is equal to difference in real clock
     859\item `Clock' difference in Clight is sum of cost labels
     860\item Observables, including trace of labels, is preserved to ASM
     861\item Labelling at bottom level is sound and precise
     862\item Sum of labels at ASM is equal to difference in real clock
    759863\end{itemize}
    760864
Note: See TracChangeset for help on using the changeset viewer.