Ignore:
Timestamp:
May 13, 2013, 11:26:11 AM (7 years ago)
Author:
campbell
Message:

Improve a few awkward parts of front-end slides.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/Dissemination/front-end/front-end.tex

    r3266 r3267  
    3838\frametitle{Introduction}
    3939
    40 D3.4 is the front-end correctness proofs:
     40D3.4 consists of the front-end correctness proofs:
    4141
    4242\begin{description}
    4343\item[Primary focus:] novel \red{intensional} properties: \blue{cost
    4444    bound correctness}
    45 \item[Secondary:] usual \red{extensional} result: \blue{functional correctness}
    4645\end{description}
    47 
    48 Functional correctness for similar compilers already studied in
    49 Leroy et al.'s \blue{CompCert}.
    50 \begin{itemize}
     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}
    5161\item Axiomatize similar results
    52 \end{itemize}
    53 
    54 \medskip
    55 Now have \blue{stack} costs as well as \blue{time}
    56 \begin{itemize}
    57 \item yields stronger overall correctness result
    58 \end{itemize}
    59 
    60 \medskip
    61 \alert{Extract} compiler code from development for practical execution.
    62 
    63 \medskip
    64 Informed by earlier formal experiment with a toy compiler.
     62\item \red{Intensional} proofs form a layer on top
     63\end{itemize}
    6564}
    6665
    … …  
    105104
    106105\begin{center}
    107 \includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
    108 \end{center}
    109 
    110 \begin{itemize}
    111 \item Reuse unverified CompCert parser
     106\includegraphics[width=0.6\linewidth]{compiler-plain.pdf}
     107\end{center}
     108
     109\begin{itemize}
     110\item Reuse unverified CompCert \alert{parser}
    112111%\item Transform away troublesome constructs
    113112%  \begin{itemize}
    … …  
    117116%  \end{itemize}
    118117\item Intermediate language for most passes
    119 \item Executable semantics for each
     118\item \alert{Executable semantics} for each
     119\item \alert{Extract} OCaml compiler code from development
    120120\item Outputs
    121121  \begin{itemize}
    122   \item 8051 machine code
    123   \item Clight code instrumented with costs in 8051 clock cycles and
    124     bytes of stack space
     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}
    125125  \end{itemize}
    126126\end{itemize}
    … …  
    219219\frametitle{Overall correctness statement}
    220220
     221\[ \text{max predicted stack usage} \leq \text{limit} \]
     222implies
     223\begin{itemize}
     224\item successful execution, with
     225\end{itemize}
    221226\begin{center}
    222227\fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
    223228\end{center}
    224 
    225 \pause
     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
    226240
    227241\begin{center}
    … …  
    245259&
    246260
    247 \begin{uncoverenv}<2-3>
     261\begin{uncoverenv}<1-2>
    248262\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    249263                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    … …  
    267281&
    268282
    269 \begin{uncoverenv}<3-5>
     283\begin{uncoverenv}<2-4>
    270284\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
    271285                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
    … …  
    291305
    292306\begin{overprint}
    293 \onslide<2>
    294 \begin{itemize}
    295 \item Use labels and end of function as measurement points
    296 \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
    297 \end{itemize}
    298 
    299 \onslide<3-4>
    300 \begin{itemize}
    301 \item Use labels and end of function as measurement points
    302 \item All costs are considered local to the function
    303 \item Actual position of unobservable computation is unimportant
    304 \end{itemize}
    305 
    306 \onslide<5>
    307 \begin{itemize}
    308 \item Use labels and end of function as measurement points
    309 \item[$\star$] Call suitable subtraces \alert{measurable}
    310 \item[$\star$] Core part is a proof of \alert{termination}
    311 \end{itemize}
     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>
     329% \begin{itemize}
     330% \item Use labels and end of function as measurement points
     331% \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
     332% \end{itemize}
     333
     334% \onslide<2-3>
     335% \begin{itemize}
     336% \item Use labels and end of function as measurement points
     337% \item All costs are considered local to the function
     338% \item Actual position of unobservable computation is unimportant
     339% \end{itemize}
     340
     341% \onslide<4>
     342% \begin{itemize}
     343% \item Use labels and end of function as measurement points
     344% \item[$\star$] Call suitable subtraces \alert{measurable}
     345% \item[$\star$] Core part is a proof of \alert{termination}
     346% \end{itemize}
    312347\end{overprint}
    313348
    … …  
    407442\frametitle{Front-end correctness statement}
    408443
    409 Given a \blue{measurable} subtrace of a \textbf{Clight} execution, including
     444Given a \red{measurable} subtrace of a \textbf{Clight} execution, including
    410445the \textbf{prefix} of that trace from initial state,
    411446
    … …  
    414449\begin{itemize}
    415450\item a new \textbf{prefix}
    416 \item a \red{structured trace} corresponding to \blue{measurable}
     451\item a \blue{structured trace} corresponding to \red{measurable}
    417452  subtrace
    418 \item the no \red{repeating} addresses property
     453\item the no \blue{repeating} addresses property
    419454\item proof that the same \textbf{stack limit} is observed
    420455\end{itemize}
    421456which the back-end requires, and
    422457\begin{itemize}
    423 \item the observables for the \textbf{prefix} and \red{structured
     458\item the observables for the \textbf{prefix} and \blue{structured
    424459    trace} are the same as their \textbf{Clight} counterparts
    425460\end{itemize}
    … …  
    555590  for simple labelling
    556591\item Replaces with \lstinline[language=C]'if ... then ... else' tree
    557 \item Tricky part of proof memory extension for extra variable
    558 \item Partial proof: validate approach, but not relevant to
    559   intensional properties
     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
    560595\end{itemize}
    561596
    … …  
    604639\item But do have invariants:
    605640  \begin{itemize}
    606   \item Statement well-typed with respect to pseudo-register
     641  \item[$\bullet$] Statements well-typed with respect to pseudo-register
    607642    environment
    608   \item CFG complete
    609   \item Entry and exit nodes complete, unique
     643  \item[$\bullet$] CFG complete
     644  \item[$\bullet$] Entry and exit nodes present, unique
    610645  \end{itemize}
    611646\item Translation function is \emph{total} as a result
    … …  
    714749
    715750\begin{itemize}
    716 \item `Clock' difference in Clight is sum of cost labels
    717 \item Observables, including trace of labels, is preserved to ASM
    718 \item Labelling at bottom level is sound and precise
    719 \item Sum of labels at ASM is equal to difference in real clock
     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
    720759\end{itemize}
    721760
Note: See TracChangeset for help on using the changeset viewer.