Changeset 2941

Timestamp:

Mar 22, 2013, 9:46:18 PM (8 years ago)

Author:

campbell

Message:

Update proof slides.

Location:

Deliverables/Dissemination/proof-structured-traces

Files:

• compiler-plain.pdf (modified) (previous)
• compiler.pdf (modified) (previous)
• compiler.svg (modified) (9 diffs)
• proof-structured-traces.pdf (modified) (previous)
• proof-structured-traces.tex (modified) (10 diffs)

Deliverables/Dissemination/proof-structured-traces/compiler.svg

@@ -178 +178 @@
          transform="scale(-0.6,-0.6)" />
     </marker>
+    <inkscape:perspective
+       id="perspective2895"
+       inkscape:persp3d-origin="0.5 : 0.33333333 : 1"
+       inkscape:vp_z="1 : 0.5 : 1"
+       inkscape:vp_y="0 : 1000 : 0"
+       inkscape:vp_x="0 : 0.5 : 1"
+       sodipodi:type="inkscape:persp3d" />
+    <inkscape:perspective
+       id="perspective2920"
+       inkscape:persp3d-origin="0.5 : 0.33333333 : 1"
+       inkscape:vp_z="1 : 0.5 : 1"
+       inkscape:vp_y="0 : 1000 : 0"
+       inkscape:vp_x="0 : 0.5 : 1"
+       sodipodi:type="inkscape:persp3d" />
+    <marker
+       inkscape:stockid="Arrow2Mend"
+       orient="auto"
+       refY="0"
+       refX="0"
+       id="Arrow2Mend-8"
+       style="overflow:visible">
+      <path
+         id="path3678-01"
+         style="font-size:12px;fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round"
+         d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+         transform="scale(-0.6,-0.6)" />
+    </marker>
   </defs>
   <sodipodi:namedview
@@ -186 +213 @@
      inkscape:pageopacity="0.0"
      inkscape:pageshadow="2"
-     inkscape:zoom="2"
-     inkscape:cx="225.5371"
-     inkscape:cy="536.39819"
+     inkscape:zoom="4"
+     inkscape:cx="123.51808"
+     inkscape:cy="505.66774"
      inkscape:document-units="px"
-     inkscape:current-layer="layer1"
+     inkscape:current-layer="layer2"
      showgrid="true"
      showguides="true"
@@ -199 +226 @@
      inkscape:window-y="25"
      inkscape:window-maximized="1"
-     inkscape:snap-global="false">
+     inkscape:snap-global="true">
     <inkscape:grid
        type="xygrid"
@@ -253 +280 @@
     <path
        style="fill:none;stroke:#0000ff;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:3, 1;stroke-dashoffset:0"
-       d="M 222.5 512.375 C 218.345 512.375 215 515.72 215 519.875 L 215 537.375 L 47.5 537.375 C 43.345 537.375 40 540.72 40 544.875 L 40 549.875 C 40 554.03 43.345 557.375 47.5 557.375 L 222.5 557.375 L 242.5 557.375 C 246.655 557.375 250 554.03 250 549.875 L 250 544.875 L 250 519.875 C 250 515.72 246.655 512.375 242.5 512.375 L 222.5 512.375 z "
-       id="rect4273" />
+       d="m 222.5,512.375 c -4.155,0 -7.5,3.345 -7.5,7.5 l 0,17.5 -215,0 c -4.155,0 -7.5,3.345 -7.5,7.5 l 0,5 c 0,4.155 3.345,7.5 7.5,7.5 l 222.5,0 20,0 c 4.155,0 7.5,-3.345 7.5,-7.5 l 0,-5 0,-25 c 0,-4.155 -3.345,-7.5 -7.5,-7.5 l -20,0 z"
+       id="rect4273"
+       sodipodi:nodetypes="cccccccccccccc" />
     <rect
        style="fill:none;stroke:#00ff00;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:3, 1;stroke-dashoffset:0"
@@ -260 +288 @@
        width="30"
        height="40"
-       x="40"
+       x="-5"
        y="542.36218"
        ry="7.5" />
@@ -306 +334 @@
        xml:space="preserve"
        style="font-size:8px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;text-align:center;text-anchor:middle;fill:#00b600;fill-opacity:1;stroke:none;font-family:LMRoman8;-inkscape-font-specification:LMRoman8"
-       x="92.960938"
+       x="47.960938"
        y="572.36218"
        id="text4310"><tspan
          sodipodi:role="line"
          id="tspan4312"
-         x="92.960938"
+         x="47.960938"
          y="572.36218">Cost map</tspan><tspan
          sodipodi:role="line"
-         x="92.960938"
+         x="47.960938"
          y="582.36218"
          id="tspan4314">generation</tspan></text>
@@ -389 +417 @@
        xml:space="preserve"
        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"
-       x="133.83789"
+       x="82.837891"
        y="552.36218"
        id="text2852"><tspan
          sodipodi:role="line"
          id="tspan2854"
-         x="133.83789"
+         x="82.837891"
          y="552.36218">LTL</tspan></text>
     <text
        xml:space="preserve"
        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"
-       x="92.646484"
+       x="47.646484"
        y="552.36218"
        id="text2856"><tspan
          sodipodi:role="line"
          id="tspan2858"
-         x="92.646484"
+         x="47.646484"
          y="552.36218">LIN</tspan></text>
     <text
        xml:space="preserve"
        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"
-       x="55.498047"
+       x="10.498047"
        y="552.36218"
        id="text2860"><tspan
          sodipodi:role="line"
          id="tspan2862"
-         x="55.498047"
+         x="10.498047"
          y="552.36218">ASM</tspan></text>
     <text
        xml:space="preserve"
        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"
-       x="55.303047"
+       x="10.303047"
        y="577.36218"
        id="text2864"><tspan
          sodipodi:role="line"
          id="tspan2866"
-         x="55.303047"
+         x="10.303047"
          y="577.36218">8051</tspan></text>
     <path
@@ -440 +468 @@
     <path
        style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
-       d="m 55.123439,557.36218 0,10"
+       d="m 10.123439,557.36218 0,10"
        id="path2872-36" />
     <path
@@ -456 +484 @@
     <path
        style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
-       d="m 115,549.36218 -10,0"
+       d="m 70,549.36218 -10,0"
        id="path2874-4-4" />
     <path
        style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
-       d="m 79.999996,549.36218 -9.999996,0"
+       d="m 34.999996,549.36218 -9.999996,0"
        id="path2874-4-1" />
+    <text
+       xml:space="preserve"
+       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"
+       x="126.44727"
+       y="552.36218"
+       id="text2848-0"><tspan
+         sodipodi:role="line"
+         id="tspan2850-7"
+         x="126.44727"
+         y="552.36218">ERTLptr</tspan></text>
+    <path
+       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
+       d="m 106,549.36218 -10,0"
+       id="path2874-4-2-6" />
   </g>
 </svg>

Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex

@@ -32 +32 @@
 \footnotesize Project FP7-ICT-2009-C-243881
 }
-\date{CerCo workshop, HiPEAC 2013\\23rd January 2013}
+\date{CerCo workshop\\23rd March 2013}
 \maketitle
 
@@ -50 +50 @@
 \end{itemize}
 
+Talk will only mention \alert{time} costs; but also do stack.
+
 \bigskip
 \alert{Extract} compiler code from development for practical execution.
@@ -83 +85 @@
 Concentrate on cost correctness.
 \begin{itemize}
-\item Keep changes to \alert{extensional} proof minimal
+\item Keep \alert{extensional} proofs as separate as possible
 \end{itemize}
 }
@@ -91 +93 @@
 
 \begin{center}
-\includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
+\includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
 \end{center}
 
@@ -107 +109 @@
   \begin{itemize}
   \item 8051 machine code
-  \item Clight code annotated with \alert{cost labels}
-  \item \alert{Cost map} of cost labels to 8051 clock cycles
-  \end{itemize}
-\end{itemize}
+  \item Clight code instrumented with costs in 8051 clock cycles
+  \end{itemize}
+\end{itemize}
+Instrumentation updates global cost variable; suitable for further analysis and
+verification.
 }
 
@@ -337 +340 @@
 
 \onslide<2->
-Need to enforce correct call/return structure.
+\alert{Need to enforce correct call/return structure.}
 
 \onslide<3>
@@ -369 +372 @@
 
 \begin{center}
-\includegraphics[width=0.7\linewidth]{compiler.pdf}
+\includegraphics[width=0.8\linewidth]{compiler.pdf}
 \end{center}
 
@@ -404 +407 @@
 Split normal simulation proof into three:
 \begin{enumerate}
-\item \blue{normal} steps become zero or more \blue{normal} steps
 \item \blue{call/return} steps become a \blue{call/return} step plus zero or
   more \blue{normal} steps
-\item \blue{cost} steps are preserved
+\item \blue{cost} label steps are preserved
+\item other \blue{normal} steps become zero or more \blue{normal} steps
 \end{enumerate}
 
@@ -470 +473 @@
 
 \begin{center}
-\includegraphics[width=0.7\linewidth]{compiler.pdf}
+\includegraphics[width=0.8\linewidth]{compiler.pdf}
 \end{center}
 
@@ -492 +495 @@
 \item Preserving trace structure provides correctness in more challenging
   setting
-\item Formal proof still in progress
-  \begin{itemize}
-  \item key definitions, structured trace lifting, some simulations done
-  \item increasing confidence in approach
-  \end{itemize}
-\item[$\star$] Don't need huge changes to existing proofs
+\item Finishing off formal proof
+  \begin{itemize}
+  \item axioms for some regular simulation results
+  \item concentrating on intensional proofs
+  \end{itemize}
+\item[$\star$] Don't need huge changes to extensional proof techniques
 \end{itemize}