Changeset 3266


Ignore:
Timestamp:
May 10, 2013, 6:59:06 PM (4 years ago)
Author:
campbell
Message:

Some f.e. revisions.

File:
1 edited

Legend:

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

    r3264 r3266  
    3232\footnotesize Project FP7-ICT-2009-C-243881
    3333}
    34 \date{CerCo workshop\\23rd March 2013}
     34\date{CerCo review meeting\\16th May 2013}
    3535\maketitle
    3636
     
    3838\frametitle{Introduction}
    3939
    40 The \emph{Matita} proof assistant supports writing and verification of
    41 functional programs.
    42 
    43 \bigskip
    44 
    45 We
    46 \begin{itemize}
    47 \item formalise the CerCo compiler in Matita,
    48 \item prove usual \red{extensional} result: \blue{functional correctness}
    49 \item also prove \red{intensional} properties: \blue{cost bound correctness}
    50 \end{itemize}
    51 
    52 Talk will only mention \alert{time} costs; but also do stack.
    53 
    54 \bigskip
    55 \alert{Extract} compiler code from development for practical execution.
    56 
    57 \bigskip
    58 Informed by earlier formal experiment with a toy compiler.
    59 }
    60 
    61 \frame{
    62 \frametitle{Motivation for formalisation}
    63 
    64 \begin{enumerate}
    65 \item Provide \alert{assurance} about labelling approach
    66   \begin{itemize}
    67   \item more complex setting than toy compiler
    68   \end{itemize}
    69 \item demonstrate feasibility of \alert{certified} WCET toolchain
    70 % Future: proof translating compiler to provide checkable WCET certificate?
    71 \item new experiments with certified compilation:
    72   \begin{itemize}
    73   \item deeper use of \alert{dependent types}
    74   \item \alert{executable} semantics in type theory
    75   \item certification of \alert{optimising assembler}
    76   \end{itemize}
    77 \end{enumerate}
    78 
    79 \bigskip
    80 \pause
     40D3.4 is the front-end correctness proofs:
     41
     42\begin{description}
     43\item[Primary focus:] novel \red{intensional} properties: \blue{cost
     44    bound correctness}
     45\item[Secondary:] usual \red{extensional} result: \blue{functional correctness}
     46\end{description}
     47
    8148Functional correctness for similar compilers already studied in
    8249Leroy et al.'s \blue{CompCert}.
    83 
    84 \bigskip
    85 Concentrate on cost correctness.
    86 \begin{itemize}
    87 \item Keep \alert{extensional} proofs as separate as possible
    88 \end{itemize}
    89 }
     50\begin{itemize}
     51\item Axiomatize similar results
     52\end{itemize}
     53
     54\medskip
     55Now 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
     64Informed by earlier formal experiment with a toy compiler.
     65}
     66
     67% TODO: could reuse some of this to make stronger intro?
     68% \frame{
     69% \frametitle{Motivation for formalisation}
     70
     71% \begin{enumerate}
     72% \item Provide \alert{assurance} about labelling approach
     73%   \begin{itemize}
     74%   \item more complex setting than toy compiler
     75%   \end{itemize}
     76% \item demonstrate feasibility of \alert{certified} WCET toolchain
     77% % Future: proof translating compiler to provide checkable WCET certificate?
     78% \item new experiments with certified compilation:
     79%   \begin{itemize}
     80%   \item deeper use of \alert{dependent types}
     81%   \item \alert{executable} semantics in type theory
     82%   \item certification of \alert{optimising assembler}
     83%   \end{itemize}
     84% \end{enumerate}
     85
     86% \bigskip
     87% \pause
     88
     89% \bigskip
     90% Concentrate on cost correctness.
     91% \begin{itemize}
     92% \item Keep \alert{extensional} proofs as separate as possible
     93% \end{itemize}
     94% }
    9095
    9196\frame{
     
    116121  \begin{itemize}
    117122  \item 8051 machine code
    118   \item Clight code instrumented with costs in 8051 clock cycles
     123  \item Clight code instrumented with costs in 8051 clock cycles and
     124    bytes of stack space
    119125  \end{itemize}
    120126\end{itemize}
     
    179185\end{tabular}
    180186
    181 From experiments with toy compiler:
     187From experiments with toy compiler [D2.1, FMICS'12]:
    182188\begin{enumerate}
    183189\item Functional correctness, \emph{including trace of labels}
     
    334340  emit _cost2
    335341  ...
    336   %\only<2->{\blue{reduce return address}}%
     342  %\only<2->{\blue{increase return address}}%
    337343  return
    338344\end{lstlisting}
     
    344350
    345351\begin{itemize}
    346 \item<2-> Changing return address reexecutes code from \lstinline'f'
     352\item<2-> Changing return address skips code from \lstinline'f'
    347353\item<2-> Cost no longer equals sum of cost labels
    348354\end{itemize}
    349355
    350356\onslide<2->
    351 \alert{Need to enforce correct call/return structure.}
     357\alert{Need to observe correct call/return structure.}
    352358
    353359\onslide<3>
    354 \emph{Not easy to observe at ASM.}
     360\emph{Not easy at ASM --- observe earlier in compiler \& maintain.}
    355361
    356362\end{frame}
     
    387393\item Invariants on positions of cost labels enforced
    388394\item Steps are \alert{grouped} according to cost label
    389 \end{itemize}
    390 
    391 \onslide<2>
    392 Construct by folding up \alert{measurable} subtrace, using soundness
    393 and preciseness of labelling.
     395\item Forbid \alert{repeating} addresses in grouped steps for
     396  \blue{sound} labelling
     397\end{itemize}
     398
     399% moved later
     400%\onslide<2>
     401%Construct by folding up \alert{measurable} subtrace, using soundness
     402%and preciseness of labelling.
    394403
    395404\end{frame}
     
    398407\frametitle{Front-end correctness statement}
    399408
    400 We start with a \blue{measurable} subtrace of an execution, and the
    401 \textbf{prefix} of that trace from initial state.
     409Given a \blue{measurable} subtrace of a \textbf{Clight} execution, including
     410the \textbf{prefix} of that trace from initial state,
    402411
    403412\medskip
    404 Need:
    405 \begin{itemize}
    406 \item Functional correctness for \textbf{prefix}
    407 \item \red{Structured trace} corresponding to \blue{measurable}
     413we have in \textbf{RTLabs}
     414\begin{itemize}
     415\item a new \textbf{prefix}
     416\item a \red{structured trace} corresponding to \blue{measurable}
    408417  subtrace
    409 \item Proof that no PC \red{repeats} in structured trace,\\ to ensure
    410   \blue{sound} labelling
    411 \item \textbf{Observables} preserved
    412 \item \textbf{Stack limit} observed
    413 \end{itemize}
    414 
     418\item the no \red{repeating} addresses property
     419\item proof that the same \textbf{stack limit} is observed
     420\end{itemize}
     421which the back-end requires, and
     422\begin{itemize}
     423\item the observables for the \textbf{prefix} and \red{structured
     424    trace} are the same as their \textbf{Clight} counterparts
     425\end{itemize}
     426which links the behaviour and costs to the original program.
    415427}
    416428
     
    447459
    448460\begin{frame}[fragile]
    449 \frametitle{Front-end measurable traces (Clight to RTLabs)}
    450 
    451 There is a \alert{measurable} RTLabs subtrace \alert{equivalent} to any
    452 \alert{measurable} Clight subtrace.
     461\frametitle{Lifting measurable traces}
     462
     463For each pass find a target \alert{measurable} subtrace
     464\alert{equivalent} to any source \alert{measurable} subtrace.
    453465
    454466\bigskip
    455467
    456468\onslide<2->
    457 Split normal simulation proof into three:
     469\begin{center}
     470\includegraphics{meassim.pdf}
     471\end{center}
     472
     473Split normal simulation proof:
    458474\begin{enumerate}
    459 \item \blue{call/return} steps become a \blue{call/return} step plus zero or
     475\item each \blue{call} becomes a \blue{call} step plus zero or
     476  more \blue{normal} steps;\\
     477  following cost labels should stay next to the call step
     478\item each \blue{return} becomes a \blue{return} plus zero or
    460479  more \blue{normal} steps
    461480\item \blue{cost} label steps are preserved
     
    465484\bigskip
    466485\onslide<3->
    467 Preserves the essential termination property for \alert{measurable} subtraces.
    468 
    469 \bigskip
    470 \onslide<4->
    471 Due to time pressures, check \alert{soundness} and \alert{precision} of cost
    472 labels at RTLabs.
     486Preserves the defining termination property for \alert{measurable} subtraces.
     487
     488% \bigskip
     489% \onslide<4->
     490% Due to time pressures, check \alert{soundness} and \alert{precision} of cost
     491% labels at RTLabs.
    473492
    474493\end{frame}
     
    654673
    655674\bigskip
    656 Constructing the bound between \textbf{Cminor} and \textbf{RTLabs}
    657 likely to be at least as expensive as this check.
     675In a full proof would go from
     676\begin{quote}
     677  cost labels at the head of loops in \textbf{Cminor}
     678\end{quote}
     679to
     680\begin{quote}
     681  bound on instructions to cost label in \textbf{RTLabs}
     682\end{quote}
     683Showing existence of the bound alone likely to require at least as much
     684proof effort as this check.
    658685
    659686}
     
    688715\begin{itemize}
    689716\item `Clock' difference in Clight is sum of cost labels
    690 \item Trace of labels is preserved to ASM
     717\item Observables, including trace of labels, is preserved to ASM
    691718\item Labelling at bottom level is sound and precise
    692719\item Sum of labels at ASM is equal to difference in real clock
    693720\end{itemize}
    694721
    695 Also preserve observables.
    696 
    697722\end{frame}
    698723
     
    700725\frametitle{Conclusion}
    701726
    702 Sketched proof for formalised CerCo compiler
    703 
    704 \begin{itemize}
    705 \item Preserving trace structure provides correctness in more challenging
    706   setting
    707 \item Finishing off formal proof
    708   \begin{itemize}
    709   \item axioms for some regular simulation results
    710   \item concentrating on intensional proofs
    711   \end{itemize}
     727Sketched proof for formalised CerCo front-end
     728
     729\begin{itemize}
     730\item Intensional proofs can be layered on top of extensional results
     731\item Preserving call-structure key ingredient
     732\item Compile-time cost labelling checks can reduce proof burden
    712733\item[$\star$] Don't need huge changes to extensional proof techniques
    713734\end{itemize}
Note: See TracChangeset for help on using the changeset viewer.