Changeset 3260
- Timestamp:
- May 9, 2013, 11:04:39 AM (7 years ago)
- Location:
- Deliverables/Dissemination/front-end
- Files:
-
- 13 added
- 9 copied
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/Dissemination/front-end/front-end.tex
r3253 r3260 26 26 \begin{document} 27 27 28 \title{ A certified proof based on structured traces}29 \author{Brian Campbell}28 \title{Front-end Correctness Proofs} 29 \author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark} 30 30 \institute{LFCS, University of Edinburgh\\[1ex] 31 31 \includegraphics[width=.3\linewidth]{cerco_logo.png}\\ … … 90 90 91 91 \frame{ 92 \frametitle{Outline} 93 \tableofcontents 94 } 95 96 \section{CerCo Compiler} 97 98 \frame{ 92 99 \frametitle{CerCo compiler} 93 100 … … 115 122 verification. 116 123 } 124 125 \section{Overall correctness} 117 126 118 127 \begin{frame}[fragile] … … 202 211 203 212 \begin{frame}[fragile] 204 \frametitle{ Goal}213 \frametitle{Overall correctness statement} 205 214 206 215 \begin{center} … … 347 356 \end{frame} 348 357 358 \section{Front-end correctness} 359 360 \frame{ 361 \frametitle{Front-end correctness} 362 363 Recalling the toy compiler, need 364 \begin{enumerate} 365 \item Functional correctness 366 \item Cost labelling sound and precise 367 \item\label{it:return} To demonstrate return addresses are correct 368 \end{enumerate} 369 % TODO: stack space? from obs, from fnl correctness 370 371 \bigskip 372 For~\ref{it:return} we generalise notion of \emph{structured traces} 373 originally introduced for the correctness of timing analysis. 374 } 375 349 376 \begin{frame}[fragile] 350 377 \frametitle{Structured traces} … … 375 402 \end{center} 376 403 377 \onslide<1>378 \green{Assembler} provides part of local cost analysis (CPP'12).379 380 \onslide<2-4>404 %\onslide<1> 405 %\green{Assembler} provides part of local cost analysis (CPP'12). 406 407 %\onslide<2-4> 381 408 Switch at RTLabs: 382 409 \begin{itemize} … … 386 413 \end{itemize} 387 414 388 \onslide<3>389 Changes \blue{syntactic} properties of labelling into \blue{semantic}390 properties.391 392 \onslide<4>415 %\onslide<3> 416 %Changes \blue{syntactic} properties of labelling into \blue{semantic} 417 %properties. 418 419 %\onslide<4> 393 420 Reason for choice: first language with explicit \alert{addresses}, implicit 394 421 \alert{call handling}. 395 422 396 423 \end{frame} 424 425 \frame{ 426 \frametitle{Front-end correctness statement} 427 428 We start with a \blue{measurable} subtrace of an execution, and the 429 \textbf{prefix} of that trace from initial state. 430 431 \medskip 432 Need: 433 \begin{itemize} 434 \item Functional correctness for \textbf{prefix} 435 \item \red{Structured trace} corresponding to \blue{measurable} 436 subtrace 437 \item Proof that no PC \red{repeats} in structured trace,\\ to ensure 438 \blue{sound} labelling 439 \item \textbf{Observables} preserved 440 \item \textbf{Stack limit} observed 441 \end{itemize} 442 443 } 444 445 \section{Correctness proofs} 446 \subsection{Generic lifting result} 397 447 398 448 \begin{frame}[fragile] … … 424 474 \end{frame} 425 475 426 \begin{frame}[fragile] 427 \frametitle{Structured trace simulation} 428 429 Lift \alert{local} simulations to \alert{structured trace} simulations 430 similarly. 431 432 \bigskip 433 \pause 434 \begin{itemize} 435 \item 436 Require local simulations for \alert{normal}, \alert{call} and \alert{return} 437 steps 438 \item allow traces to expand with extra \alert{normal} steps, 439 \item allow us to collapse some \alert{normal} steps 440 \begin{itemize} 441 \item but not collapse \blue{labelled} steps 442 % TODO: why? avoid larger change in structure 443 \item or change call structure 444 \end{itemize} 445 \end{itemize} 446 447 \bigskip 448 Sufficient to calculate structured trace in target. 449 % TODO: pics 450 451 \end{frame} 452 453 \begin{frame}[fragile] 454 \frametitle{Structured trace local simulation example} 455 456 For function call steps: 457 \begin{center} 458 \includegraphics[width=0.7\linewidth]{strcall.pdf} 459 \end{center} 460 461 \begin{itemize} 462 \item May add extra steps before and after 463 \item Extra steps must not be call/return 464 \item Must call the same function 465 \item Cost label must stay at start of function 466 \end{itemize} 467 468 \end{frame} 469 476 %\begin{frame}[fragile] 477 %\frametitle{Structured trace simulation} 478 % 479 %Lift \alert{local} simulations to \alert{structured trace} simulations 480 %similarly. 481 % 482 %\bigskip 483 %\pause 484 %\begin{itemize} 485 %\item 486 %Require local simulations for \alert{normal}, \alert{call} and \alert{return} 487 %steps 488 %\item allow traces to expand with extra \alert{normal} steps, 489 %\item allow us to collapse some \alert{normal} steps 490 % \begin{itemize} 491 % \item but not collapse \blue{labelled} steps 492 % % TODO: why? avoid larger change in structure 493 % \item or change call structure 494 % \end{itemize} 495 %\end{itemize} 496 % 497 %\bigskip 498 %Sufficient to calculate structured trace in target. 499 %% TODO: pics 500 % 501 %\end{frame} 502 % 503 %\begin{frame}[fragile] 504 %\frametitle{Structured trace local simulation example} 505 % 506 %For function call steps: 507 %\begin{center} 508 %\includegraphics[width=0.7\linewidth]{strcall.pdf} 509 %\end{center} 510 % 511 %\begin{itemize} 512 %\item May add extra steps before and after 513 %\item Extra steps must not be call/return 514 %\item Must call the same function 515 %\item Cost label must stay at start of function 516 %\end{itemize} 517 % 518 %\end{frame} 519 520 \subsection{Simulations for compiler passes} 521 522 \frame{ 523 \frametitle{TODO} 524 } 525 526 \section{Checking cost labelling properties} 527 528 \frame{ 529 \frametitle{Checking cost labelling properties} 530 531 Check cost labelling is \red{sound} and \blue{precise} at 532 \textbf{RTLabs}. 533 \begin{itemize} 534 \item Shortcut; similar to translation validation 535 \end{itemize} 536 537 \medskip 538 At \textbf{RTLabs} properties become 539 \begin{description} 540 \item[\red{soundness}] bound on number of instructions in CFG until label\\ 541 label at start of every function 542 \item[\blue{precision}] label after every branch 543 \end{description} 544 545 \medskip 546 Bound is the hard part; the rest is a simple syntactic check. 547 } 548 549 \begin{frame}[fragile] 550 \frametitle{Bound on number of instructions until label} 551 552 \begin{center} 553 \includegraphics<1>[width=.4\linewidth]{loop.pdf} 554 \includegraphics<2>[width=.4\linewidth]{loop1.pdf} 555 \includegraphics<3>[width=.4\linewidth]{loop2.pdf} 556 \includegraphics<4>[width=.4\linewidth]{loop3.pdf} 557 \includegraphics<5>[width=.4\linewidth]{loop4.pdf} 558 \includegraphics<6>[width=.4\linewidth]{loopx.pdf} 559 \end{center} 560 561 \begin{itemize} 562 \item Pick an arbitrary node in the CFG 563 \item<2-> Follow successor instructions 564 \item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots 565 \item<5-> \dots so remove them and pick a new node, continue 566 \item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound, 567 report an error 568 \end{itemize} 569 570 \end{frame} 571 572 \frame{ 573 \frametitle{Checking cost labelling properties} 574 575 This compile-time check is 576 \begin{itemize} 577 \item[$-$] partial 578 \item[$-$] extra work in compilation 579 \item[$\mp$] not proving anything about compilation passes 580 \item[$+$] less proof burden 581 \end{itemize} 582 583 \bigskip 584 Constructing the bound between \textbf{Cminor} and \textbf{RTLabs} 585 likely to be at least as expensive as this check. 586 587 } 588 589 \section{Whole compiler} 470 590 471 591 \begin{frame}[fragile]
Note: See TracChangeset
for help on using the changeset viewer.