Changeset 2585


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

Many improvements to proof/structured traces talk.

Location:
Deliverables/Dissemination/proof-structured-traces
Files:
5 edited

Legend:

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

    r2583 r2585  
    1515   version="1.1"
    1616   inkscape:version="0.47 r22583"
    17    sodipodi:docname="New document 1">
     17   sodipodi:docname="compiler.svg">
    1818  <defs
    1919     id="defs4">
     
    188188     inkscape:zoom="2"
    189189     inkscape:cx="225.5371"
    190      inkscape:cy="537.39819"
     190     inkscape:cy="536.39819"
    191191     inkscape:document-units="px"
    192      inkscape:current-layer="layer2"
     192     inkscape:current-layer="layer1"
    193193     showgrid="true"
    194194     showguides="true"
     
    198198     inkscape:window-x="0"
    199199     inkscape:window-y="25"
    200      inkscape:window-maximized="1">
     200     inkscape:window-maximized="1"
     201     inkscape:snap-global="false">
    201202    <inkscape:grid
    202203       type="xygrid"
     
    227228        <dc:type
    228229           rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
    229         <dc:title></dc:title>
     230        <dc:title />
    230231      </cc:Work>
    231232    </rdf:RDF>
     
    269270       id="text4290"><tspan
    270271         sodipodi:role="line"
    271          id="tspan4292"></tspan></text>
     272         id="tspan4292" /></text>
    272273    <text
    273274       xml:space="preserve"
     
    287288       id="text4298"><tspan
    288289         sodipodi:role="line"
    289          id="tspan4300"></tspan></text>
     290         id="tspan4300" /></text>
    290291    <text
    291292       xml:space="preserve"
     
    378379       xml:space="preserve"
    379380       style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:LMSans10;-inkscape-font-specification:LMSans10"
    380        x="132.4039"
     381       x="182.34375"
    381382       y="552.36218"
    382383       id="text2848"><tspan
    383384         sodipodi:role="line"
    384385         id="tspan2850"
    385          x="132.4039"
     386         x="182.34375"
    386387         y="552.36218">ERTL</tspan></text>
    387388    <text
    388389       xml:space="preserve"
    389390       style="font-size:10px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:LMSans10;-inkscape-font-specification:LMSans10"
    390        x="180.16211"
     391       x="133.83789"
    391392       y="552.36218"
    392393       id="text2852"><tspan
    393394         sodipodi:role="line"
    394395         id="tspan2854"
    395          x="180.16211"
     396         x="133.83789"
    396397         y="552.36218">LTL</tspan></text>
    397398    <text
     
    431432    <path
    432433       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    433        d="m 150,522.36218 10,0"
     434       d="m 150,524.36218 10,0"
    434435       id="path2874" />
    435436    <path
     
    443444    <path
    444445       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    445        d="m 200,522.36218 10,0"
     446       d="m 200,524.36218 10,0"
    446447       id="path2874-7" />
    447448    <path
    448449       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    449        d="m 210,547.36218 -10,0"
     450       d="m 210,549.36218 -10,0"
    450451       id="path2874-4" />
    451452    <path
    452453       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    453        d="m 160,547.36218 -10,0"
     454       d="m 160,549.36218 -10,0"
    454455       id="path2874-4-2" />
    455456    <path
    456457       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    457        d="m 115,547.36218 -10,0"
     458       d="m 115,549.36218 -10,0"
    458459       id="path2874-4-4" />
    459460    <path
    460461       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    461        d="m 79.999996,547.36218 -9.999996,0"
     462       d="m 79.999996,549.36218 -9.999996,0"
    462463       id="path2874-4-1" />
    463464  </g>
  • 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.