Changeset 2941


Ignore:
Timestamp:
Mar 22, 2013, 9:46:18 PM (4 years ago)
Author:
campbell
Message:

Update proof slides.

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

Legend:

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

    r2585 r2941  
    178178         transform="scale(-0.6,-0.6)" />
    179179    </marker>
     180    <inkscape:perspective
     181       id="perspective2895"
     182       inkscape:persp3d-origin="0.5 : 0.33333333 : 1"
     183       inkscape:vp_z="1 : 0.5 : 1"
     184       inkscape:vp_y="0 : 1000 : 0"
     185       inkscape:vp_x="0 : 0.5 : 1"
     186       sodipodi:type="inkscape:persp3d" />
     187    <inkscape:perspective
     188       id="perspective2920"
     189       inkscape:persp3d-origin="0.5 : 0.33333333 : 1"
     190       inkscape:vp_z="1 : 0.5 : 1"
     191       inkscape:vp_y="0 : 1000 : 0"
     192       inkscape:vp_x="0 : 0.5 : 1"
     193       sodipodi:type="inkscape:persp3d" />
     194    <marker
     195       inkscape:stockid="Arrow2Mend"
     196       orient="auto"
     197       refY="0"
     198       refX="0"
     199       id="Arrow2Mend-8"
     200       style="overflow:visible">
     201      <path
     202         id="path3678-01"
     203         style="font-size:12px;fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round"
     204         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"
     205         transform="scale(-0.6,-0.6)" />
     206    </marker>
    180207  </defs>
    181208  <sodipodi:namedview
     
    186213     inkscape:pageopacity="0.0"
    187214     inkscape:pageshadow="2"
    188      inkscape:zoom="2"
    189      inkscape:cx="225.5371"
    190      inkscape:cy="536.39819"
     215     inkscape:zoom="4"
     216     inkscape:cx="123.51808"
     217     inkscape:cy="505.66774"
    191218     inkscape:document-units="px"
    192      inkscape:current-layer="layer1"
     219     inkscape:current-layer="layer2"
    193220     showgrid="true"
    194221     showguides="true"
     
    199226     inkscape:window-y="25"
    200227     inkscape:window-maximized="1"
    201      inkscape:snap-global="false">
     228     inkscape:snap-global="true">
    202229    <inkscape:grid
    203230       type="xygrid"
     
    253280    <path
    254281       style="fill:none;stroke:#0000ff;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:3, 1;stroke-dashoffset:0"
    255        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 "
    256        id="rect4273" />
     282       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"
     283       id="rect4273"
     284       sodipodi:nodetypes="cccccccccccccc" />
    257285    <rect
    258286       style="fill:none;stroke:#00ff00;stroke-width:1;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:3, 1;stroke-dashoffset:0"
     
    260288       width="30"
    261289       height="40"
    262        x="40"
     290       x="-5"
    263291       y="542.36218"
    264292       ry="7.5" />
     
    306334       xml:space="preserve"
    307335       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"
    308        x="92.960938"
     336       x="47.960938"
    309337       y="572.36218"
    310338       id="text4310"><tspan
    311339         sodipodi:role="line"
    312340         id="tspan4312"
    313          x="92.960938"
     341         x="47.960938"
    314342         y="572.36218">Cost map</tspan><tspan
    315343         sodipodi:role="line"
    316          x="92.960938"
     344         x="47.960938"
    317345         y="582.36218"
    318346         id="tspan4314">generation</tspan></text>
     
    389417       xml:space="preserve"
    390418       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"
    391        x="133.83789"
     419       x="82.837891"
    392420       y="552.36218"
    393421       id="text2852"><tspan
    394422         sodipodi:role="line"
    395423         id="tspan2854"
    396          x="133.83789"
     424         x="82.837891"
    397425         y="552.36218">LTL</tspan></text>
    398426    <text
    399427       xml:space="preserve"
    400428       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"
    401        x="92.646484"
     429       x="47.646484"
    402430       y="552.36218"
    403431       id="text2856"><tspan
    404432         sodipodi:role="line"
    405433         id="tspan2858"
    406          x="92.646484"
     434         x="47.646484"
    407435         y="552.36218">LIN</tspan></text>
    408436    <text
    409437       xml:space="preserve"
    410438       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"
    411        x="55.498047"
     439       x="10.498047"
    412440       y="552.36218"
    413441       id="text2860"><tspan
    414442         sodipodi:role="line"
    415443         id="tspan2862"
    416          x="55.498047"
     444         x="10.498047"
    417445         y="552.36218">ASM</tspan></text>
    418446    <text
    419447       xml:space="preserve"
    420448       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"
    421        x="55.303047"
     449       x="10.303047"
    422450       y="577.36218"
    423451       id="text2864"><tspan
    424452         sodipodi:role="line"
    425453         id="tspan2866"
    426          x="55.303047"
     454         x="10.303047"
    427455         y="577.36218">8051</tspan></text>
    428456    <path
     
    440468    <path
    441469       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    442        d="m 55.123439,557.36218 0,10"
     470       d="m 10.123439,557.36218 0,10"
    443471       id="path2872-36" />
    444472    <path
     
    456484    <path
    457485       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    458        d="m 115,549.36218 -10,0"
     486       d="m 70,549.36218 -10,0"
    459487       id="path2874-4-4" />
    460488    <path
    461489       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
    462        d="m 79.999996,549.36218 -9.999996,0"
     490       d="m 34.999996,549.36218 -9.999996,0"
    463491       id="path2874-4-1" />
     492    <text
     493       xml:space="preserve"
     494       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"
     495       x="126.44727"
     496       y="552.36218"
     497       id="text2848-0"><tspan
     498         sodipodi:role="line"
     499         id="tspan2850-7"
     500         x="126.44727"
     501         y="552.36218">ERTLptr</tspan></text>
     502    <path
     503       style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Mend)"
     504       d="m 106,549.36218 -10,0"
     505       id="path2874-4-2-6" />
    464506  </g>
    465507</svg>
  • Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex

    r2589 r2941  
    3232\footnotesize Project FP7-ICT-2009-C-243881
    3333}
    34 \date{CerCo workshop, HiPEAC 2013\\23rd January 2013}
     34\date{CerCo workshop\\23rd March 2013}
    3535\maketitle
    3636
     
    5050\end{itemize}
    5151
     52Talk will only mention \alert{time} costs; but also do stack.
     53
    5254\bigskip
    5355\alert{Extract} compiler code from development for practical execution.
     
    8385Concentrate on cost correctness.
    8486\begin{itemize}
    85 \item Keep changes to \alert{extensional} proof minimal
     87\item Keep \alert{extensional} proofs as separate as possible
    8688\end{itemize}
    8789}
     
    9193
    9294\begin{center}
    93 \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
     95\includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
    9496\end{center}
    9597
     
    107109  \begin{itemize}
    108110  \item 8051 machine code
    109   \item Clight code annotated with \alert{cost labels}
    110   \item \alert{Cost map} of cost labels to 8051 clock cycles
    111   \end{itemize}
    112 \end{itemize}
     111  \item Clight code instrumented with costs in 8051 clock cycles
     112  \end{itemize}
     113\end{itemize}
     114Instrumentation updates global cost variable; suitable for further analysis and
     115verification.
    113116}
    114117
     
    337340
    338341\onslide<2->
    339 Need to enforce correct call/return structure.
     342\alert{Need to enforce correct call/return structure.}
    340343
    341344\onslide<3>
     
    369372
    370373\begin{center}
    371 \includegraphics[width=0.7\linewidth]{compiler.pdf}
     374\includegraphics[width=0.8\linewidth]{compiler.pdf}
    372375\end{center}
    373376
     
    404407Split normal simulation proof into three:
    405408\begin{enumerate}
    406 \item \blue{normal} steps become zero or more \blue{normal} steps
    407409\item \blue{call/return} steps become a \blue{call/return} step plus zero or
    408410  more \blue{normal} steps
    409 \item \blue{cost} steps are preserved
     411\item \blue{cost} label steps are preserved
     412\item other \blue{normal} steps become zero or more \blue{normal} steps
    410413\end{enumerate}
    411414
     
    470473
    471474\begin{center}
    472 \includegraphics[width=0.7\linewidth]{compiler.pdf}
     475\includegraphics[width=0.8\linewidth]{compiler.pdf}
    473476\end{center}
    474477
     
    492495\item Preserving trace structure provides correctness in more challenging
    493496  setting
    494 \item Formal proof still in progress
    495   \begin{itemize}
    496   \item key definitions, structured trace lifting, some simulations done
    497   \item increasing confidence in approach
    498   \end{itemize}
    499 \item[$\star$] Don't need huge changes to existing proofs
     497\item Finishing off formal proof
     498  \begin{itemize}
     499  \item axioms for some regular simulation results
     500  \item concentrating on intensional proofs
     501  \end{itemize}
     502\item[$\star$] Don't need huge changes to extensional proof techniques
    500503\end{itemize}
    501504
Note: See TracChangeset for help on using the changeset viewer.