407 |
527 |
408 \end{frame}} |
528 \end{frame}} |
409 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
529 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
410 |
530 |
411 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
531 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
532 \mode<presentation>{ |
|
533 \begin{frame}[c] |
|
534 \frametitle{Priority Inheritance Protocol} |
|
535 |
|
536 \begin{itemize} |
|
537 \item an algorithm that is widely used in real-time operating systems |
|
538 \item hash been ``proved'' correct by hand in a paper in 1983 |
|
539 \item but the first algorithm turned out to be incorrect, despite the ``proof''\bigskip\pause |
|
540 |
|
541 \item we specified the algorithm and then proved that the specification makes |
|
542 ``sense'' |
|
543 \item we implemented our specification in C on top of PINTOS (Stanford) |
|
544 \item our implementation was much more efficient than their reference implementation |
|
545 \end{itemize} |
|
546 |
|
547 \end{frame}} |
|
548 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
549 |
|
550 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
551 \mode<presentation>{ |
|
552 \begin{frame}[c] |
|
553 \frametitle{Regular Expression Matching} |
|
554 \tiny |
|
555 |
|
556 \begin{tabular}{@ {\hspace{-6mm}}cc} |
|
557 \begin{tikzpicture}[y=.1cm, x=.15cm] |
|
558 %axis |
|
559 \draw (0,0) -- coordinate (x axis mid) (30,0); |
|
560 \draw (0,0) -- coordinate (y axis mid) (0,30); |
|
561 %ticks |
|
562 \foreach \x in {0,5,...,30} |
|
563 \draw (\x,1pt) -- (\x,-3pt) |
|
564 node[anchor=north] {\x}; |
|
565 \foreach \y in {0,5,...,30} |
|
566 \draw (1pt,\y) -- (-3pt,\y) |
|
567 node[anchor=east] {\y}; |
|
568 %labels |
|
569 \node[below=0.3cm] at (x axis mid) {\bl{a}s}; |
|
570 \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; |
|
571 |
|
572 %plots |
|
573 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
574 file {re-python.data}; |
|
575 \only<1->{ |
|
576 \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] |
|
577 file {re1.data};} |
|
578 \only<1->{ |
|
579 \draw[color=green] plot[mark=square*, mark options={fill=white} ] |
|
580 file {re2.data};} |
|
581 |
|
582 %legend |
|
583 \begin{scope}[shift={(4,20)}] |
|
584 \draw[color=blue] (0,0) -- |
|
585 plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
586 node[right]{\footnotesize Python}; |
|
587 \only<1->{\draw[yshift=6mm, color=red] (0,0) -- |
|
588 plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
589 node[right]{\footnotesize Scala V1};} |
|
590 \only<1->{ |
|
591 \draw[yshift=12mm, color=green] (0,0) -- |
|
592 plot[mark=square*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
593 node[right]{\footnotesize Scala V2 with simplifications};} |
|
594 \end{scope} |
|
595 \end{tikzpicture} & |
|
596 |
|
597 \begin{tikzpicture}[y=.35cm, x=.00045cm] |
|
598 %axis |
|
599 \draw (0,0) -- coordinate (x axis mid) (10000,0); |
|
600 \draw (0,0) -- coordinate (y axis mid) (0,6); |
|
601 %ticks |
|
602 \foreach \x in {0,2000,...,10000} |
|
603 \draw (\x,1pt) -- (\x,-3pt) |
|
604 node[anchor=north] {\x}; |
|
605 \foreach \y in {0,1,...,6} |
|
606 \draw (1pt,\y) -- (-3pt,\y) |
|
607 node[anchor=east] {\y}; |
|
608 %labels |
|
609 \node[below=0.3cm] at (x axis mid) {\bl{a}s}; |
|
610 \node[rotate=90, left=0.6cm] at (y axis mid) {secs}; |
|
611 |
|
612 %plots |
|
613 \draw[color=blue] plot[mark=*, mark options={fill=white}] |
|
614 file {re-internal.data}; |
|
615 \only<1->{ |
|
616 \draw[color=red] plot[mark=triangle*, mark options={fill=white} ] |
|
617 file {re3.data};} |
|
618 |
|
619 %legend |
|
620 \begin{scope}[shift={(2000,4)}] |
|
621 \draw[color=blue] (0,0) -- |
|
622 plot[mark=*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
623 node[right]{\footnotesize Scala Internal}; |
|
624 \only<1->{ |
|
625 \draw[yshift=6mm, color=red] (0,0) -- |
|
626 plot[mark=triangle*, mark options={fill=white}] (0.25,0) -- (0.5,0) |
|
627 node[right]{\footnotesize Scala V3};} |
|
628 \end{scope} |
|
629 \end{tikzpicture} |
|
630 \end{tabular}\bigskip\pause |
|
631 \normalsize |
|
632 \begin{itemize} |
|
633 \item I needed a proof in order to make sure my program is correct |
|
634 \end{itemize}\pause |
|
635 |
|
636 \begin{center} |
|
637 \bl{End Digression.\\ (Our small proof is 0.0005\% of the OS-proof.)} |
|
638 \end{center} |
|
639 |
|
640 \end{frame}} |
|
641 |
|
642 |
|
643 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
|
644 |
|
645 |
|
646 |
|
647 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
412 \mode<presentation>{ |
648 \mode<presentation>{ |
413 \begin{frame}[c] |
649 \begin{frame}[c] |
414 \frametitle{Trusted Third Party} |
650 \frametitle{Trusted Third Party} |
415 |
651 |
416 Simple protocol for establishing a secure connection via a mutually |
652 Simple protocol for establishing a secure connection via a mutually |