Ignore:
Timestamp:
Jan 23, 2013, 12:26:41 PM (8 years ago)
Author:
campbell
Message:

Many improvements to proof/structured traces talk.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex

    r2583 r2585  
    4747\begin{itemize}
    4848\item formalise the CerCo compiler in Matita,
    49 \item prove usual \alert{extensional} result: \alert{functional correctness}
    50 \item also prove \alert{intensional} properties,
    51   \begin{itemize} \item i.e.~cost bound correctness \end{itemize}
    52 \end{itemize}
    53 
     49\item prove usual \red{extensional} result: \blue{functional correctness}
     50\item also prove \red{intensional} properties: \blue{cost bound correctness}
     51\end{itemize}
     52
     53\bigskip
     54\alert{Extract} compiler code from development for practical execution.
     55
     56\bigskip
     57Informed by earlier formal experiment with a toy compiler.
    5458}
    5559
     
    7276\end{enumerate}
    7377
     78\bigskip
     79\pause
     80Functional correctness for similar compilers already studied in
     81Leroy et al.'s \blue{CompCert}.
     82
     83Concentrate on cost correctness.
    7484}
    7585
     
    8292
    8393\begin{itemize}
    84 \item Unverified CompCert parser
    85 \item Transform away troublesome constructs
    86   \begin{itemize}
    87   \item e.g.~\texttt{switch}
    88   \item fallthrough requires slightly more sophisticated labelling
    89   \item but not fundamentally different
     94\item Reuse unverified CompCert parser
     95%\item Transform away troublesome constructs
     96%  \begin{itemize}
     97%  \item e.g.~\texttt{switch}
     98%  \item fallthrough requires slightly more sophisticated labelling
     99%  \item but not fundamentally different
     100%  \end{itemize}
     101\item Intermediate language for most passes
     102\item Executable semantics for each
     103\item Outputs
     104  \begin{itemize}
     105  \item 8051 machine code
     106  \item Clight code annotated with \alert{cost labels}
     107  \item \alert{Cost map} of cost labels to 8051 clock cycles
    90108  \end{itemize}
    91109\end{itemize}
     
    146164\end{tabular}
    147165
    148 %Experiments with toy compiler splits into
     166From experiments with toy compiler:
    149167\begin{enumerate}
    150168\item Functional correctness, \emph{including trace of labels}
    151 \item Source labelling function is sound and precise
    152 \item Preservation of soundness and precision of labelling
     169%\item Source labelling function is sound and precise
     170%\item Preservation of soundness and precision of labelling
     171\item Target labelling function is sound and precise
    153172% TODO: detail about soundness and precision?
    154173\item Target cost analysis produces a map of labels to times
     
    183202\end{center}
    184203
     204\pause
     205
    185206\begin{center}
    186207\begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c}
     
    203224&
    204225
    205 \begin{uncoverenv}<1-2>
     226\begin{uncoverenv}<2-3>
    206227\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    207228                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     
    225246&
    226247
    227 \begin{uncoverenv}<2-3>
     248\begin{uncoverenv}<3-4>
    228249\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    229250                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
     
    233254_cost2
    234255call g
    235 
     256...
    236257return g
    237258
     
    249270
    250271\begin{overprint}
    251 \onslide<1-2>
     272\onslide<2>
    252273\begin{itemize}
    253274\item Use labels and end of function as measurement points
    254 \item<2> Actual position of unobservable computation is unimportant
    255 \item<2> All costs are considered local to the function
     275\item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of whole function
    256276\end{itemize}
    257277
    258278\onslide<3>
     279\begin{itemize}
     280\item Use labels and end of function as measurement points
     281\item Actual position of unobservable computation is unimportant
     282\item All costs are considered local to the function
     283\end{itemize}
     284
     285\onslide<4>
    259286\begin{itemize}
    260287\item Use labels and end of function as measurement points
     
    292319  emit _cost2
    293320  ...
    294   %\only<2>{\blue{reduce return address}}%
     321  %\only<2->{\blue{reduce return address}}%
    295322  return
    296323\end{lstlisting}
     
    299326\end{center}
    300327
    301 Total cost should be costmap(\lstinline'_cost1') + costmap(\lstinline'_cost2').
    302 
    303 \begin{itemize}
    304 \item<2> Changing return address reexecutes code from \lstinline'f'
    305 \item<2> Cost no longer equals sum of cost labels
    306 \end{itemize}
    307 
    308 \onslide<2>
     328Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).
     329
     330\begin{itemize}
     331\item<2-> Changing return address reexecutes code from \lstinline'f'
     332\item<2-> Cost no longer equals sum of cost labels
     333\end{itemize}
     334
     335\onslide<2->
    309336Need to enforce correct call/return structure.
     337
     338\onslide<3>
     339\emph{Not easy to observe at ASM.}
    310340
    311341\end{frame}
     
    355385
    356386\onslide<4>
    357 Reason for choice: first language with explicit \alert{addresses}.
     387Reason for choice: first language with explicit \alert{addresses}, implicit
     388\alert{call handling}.
    358389
    359390\end{frame}
     
    439470\bigskip
    440471\begin{itemize}
    441 \item preserving trace structure provides correctness in more challenging
     472\item Preserving trace structure provides correctness in more challenging
    442473  setting
    443 \item full formal proof still in progress
     474\item Formal proof still in progress
    444475  \begin{itemize}
    445476  \item key definitions, structured trace lifting, some simulations done
    446   \end{itemize}
    447 \item expect results to generalise to more general labelling schemes
     477  \item increasing confidence in approach
     478  \end{itemize}
     479\item Expect results to generalise to more general labelling schemes
    448480  \begin{itemize}
    449481  \item hence more sophisticated targets
Note: See TracChangeset for help on using the changeset viewer.