(*<*)

theory Slides4

imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"

begin

notation (latex output)

  set ("_") and

  Cons  ("_::/_" [66,65] 65) 

(*

ML {*

  open Printer;

  show_question_marks_default := false;

  *}

*)

notation (latex output)

  Cons ("_::_" [78,77] 73) and

  vt ("valid'_state") and

  runing ("running") and

  birthtime ("last'_set") and

  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and

  Prc ("'(_, _')") and

  holding ("holds") and

  waiting ("waits") and

  Th ("T") and

  Cs ("C") and

  P ("Lock") and

  V ("Unlock") and

  readys ("ready") and

  depend ("RAG") and 

  preced ("prec") and

  cpreced ("cprec") and

  dependents ("dependants") and

  cp ("cprec") and

  holdents ("resources") and

  original_priority ("priority") and

  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

(*>*)

text_raw {*

  \renewcommand{\slidecaption}{NASA, 20 June 2013}

  \newcommand{\bl}[1]{#1}                        

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}

  \frametitle{%

  \begin{tabular}{@ {}c@ {}}

  \\[-3mm]

  \LARGE Formalisations and the\\[-1mm] 

  \LARGE Isabelle Theorem Prover\\[-3mm] 

  \end{tabular}}

  \begin{center}

   Christian Urban\\[1mm]

  \small King's College London

  \end{center}\bigskip

  \begin{center}

  many thanks to Mahyar Malekpour and Cesar Munoz for the invitation and 

  hospitality

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<2->[c]

  \frametitle{Isabelle Theorem Prover}

  \begin{center}

  \includegraphics[scale=0.23]{isabelle.png}

  \end{center}  

  \only<2>{

  \begin{textblock}{12}(2,13.6)

  \begin{tikzpicture}

  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

  {\normalsize\color{darkgray}

  \begin{minipage}{9cm}\raggedright

  \ldots to make sure large proofs are correct

  \end{minipage}};

  \end{tikzpicture}

  \end{textblock}}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

  \tikzstyle{node1}=[rectangle, minimum size=8mm, rounded corners=3mm, very thick, 

                     draw=black!50, top color=white, bottom color=black!20]

  \tikzstyle{node2}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

                     draw=red!70, top color=white, bottom color=red!50!black!20]

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{}

  \begin{tabular}{@ {}c@ {\hspace{2mm}}c}

  \\[6mm]

  \begin{tabular}{c}

  \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

  {\footnotesize Bob Harper}\\[-2.5mm]

  {\footnotesize (CMU)}

  \end{tabular}

  \begin{tabular}{c@ {}}

  \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

  {\footnotesize Frank Pfenning}\\[-2.5mm]

  {\footnotesize (CMU)}

  \end{tabular} &

  \begin{tabular}{@ {\hspace{-3mm}}p{7cm}}

  \begin{tikzpicture}[remember picture, scale=0.5]

  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

  { \& \& \node (desc) {\makebox[0mm]{\begin{tabular}{l}published in a journal\\ 

    \small (ACM ToCL, 31 pages, 2005)\\[3mm]\end{tabular}}};\\

    \&[-10mm] 

    \node (def1)   [node1] {\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

    \node (proof1) [node1] {Proof}; \&

    \node (alg1)   [node1] {\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);

  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

  \draw[<-,black,line width=0.5mm] (proof1) -- (desc);

  \end{tikzpicture}

  \end{tabular}\\

  \pause

  \\[0mm]

  \multicolumn{2}{c}{

  \begin{tabular}{p{6cm}}

  \raggedright

  \color{black}{relied on their proof in a\\ {\bf security} critical application}

  \end{tabular}

  \begin{tabular}{c}

  \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

  {\footnotesize Andrew Appel}\\[-2.5mm]

  {\footnotesize (Princeton)}

  \end{tabular}}

  \end{tabular} 

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<4-> 

  \frametitle{\LARGE\begin{tabular}{c}An Example for a Small TCB\end{tabular}}

  \mbox{}\\[-14mm]\mbox{}

  \begin{columns}

  \begin{column}{0.2\textwidth}

  \begin{tabular}{@ {} c@ {}}

  \includegraphics[scale=0.3]{appel.jpg}\\[-2mm] 

  {\footnotesize Andrew Appel}\\[-2.5mm]

  {\footnotesize (Princeton)}

  \end{tabular}

  \end{column}

  \begin{column}{0.8\textwidth}

  \begin{textblock}{10}(4.5,3.95)

  \begin{block}{Proof-Carrying Code:}

  \begin{center}

  \begin{tikzpicture}

  \draw[help lines,cream] (0,0.2) grid (8,4);

  \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);

  \node[anchor=base] at (6.5,2.8) 

     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user can run untrusted code\end{tabular}};

  \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);

  \node[anchor=base] at (1.5,2.3) 

     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  code developer/ web server/ Apple 

  Store\end{tabular}};

  \onslide<4->{

  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);

  \node[anchor=base,white] at (6.5,1.1) 

     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}

  \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};

  \onslide<3->{

  \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};

  \node at (3.8,1.9) {\small certificate};

  }

  \onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}

  % Code Developer

  % User (runs untrusted code)

  % transmits a proof that the code is safe

  % 

  \end{tikzpicture}

  \end{center}

  \end{block}

  \end{textblock}

  \end{column}

  \end{columns}

  \small\mbox{}\\[3.2cm]

  \begin{itemize}

  \item<4-> TCB of the checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 

  803 loc in C including 2 library functions)\\[-3mm]

  \item<4-> 167 loc in C implement a type-checker

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

                     draw=black!50, top color=white, bottom color=black!20]

  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

                     draw=red!70, top color=white, bottom color=red!50!black!20]

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}<2->[squeeze]

  \frametitle{} 

  \begin{columns}

  \begin{column}{0.8\textwidth}

  \begin{textblock}{0}(1,2)

  \begin{tikzpicture}

  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

  { \&[-10mm] 

    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

    \node (proof1) [node1] {\large Proof}; \&

    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);

  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}

  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}

  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}

  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}

  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 

  \end{tikzpicture}

  \end{textblock}

  \end{column}

  \end{columns}

  \begin{textblock}{3}(12,3.6)

  \onslide<4->{

  \begin{tikzpicture}

  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

  \end{tikzpicture}}

  \end{textblock}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Other Formalisations}

  \begin{itemize} 

  \item I also found a (fixable) mistake in my PhD thesis\bigskip

  \item Nominal Isabelle: found out that the variable convention 

  can be used to prove false (a surprising result in PL-research)\bigskip

  \item Computability and Logic Book (5th ed.)\\ by Boolos, Burgess and Jeffrey ---

  two definitions about halting computations in UTMs are inconsistent

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Scheduling in RTOS}

  \begin{itemize}

  \item RTOS: priorities and resource locking

  \item Purpose:\\

  guarantee tasks to be completed in time\medskip\pause

  \item \alert{this already results into a surprisingly non-trivial algorithmic problem}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{The Problem}

  \Large

  \begin{center}

  \begin{tabular}{l}

  \alert{H}igh-priority process (waits)\\[4mm]

  \onslide<2->{\alert{M}edium-priority process}\\[4mm]

  \alert{L}ow-priority process (has a lock)\\[4mm]

  \end{tabular}

  \end{center}

  \onslide<3->{

  \begin{itemize}

  \item \alert{priority inversion}\\ \hspace{2cm}@{text "\<equiv>"} H waits for a process\\ 

  \mbox{}\hfill with lower priority

  \item<4> avoid \alert{indefinite} priority inversion

  \end{itemize}}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Mars Pathfinder Mission 1997}

  \large

  \begin{center}

  \includegraphics[scale=0.15]{marspath1.png}

  \includegraphics[scale=0.16]{marspath3.png}

  \includegraphics[scale=0.3]{marsrover.png}

  \end{center}

  \begin{itemize}

  \item the lander reset frequently on Mars

  \item the problem: priority inversion

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{The Solution}

  \Large

  \alert{Priority Inheritance Protocol (PIP):}\bigskip

  \begin{center}

  \begin{tabular}{l}

  \alert{H}igh-priority process\\[4mm]

  \textcolor{gray}{Medium-priority process}\\[4mm]

  \alert{L}ow-priority process\\[15mm]

  {\normalsize (temporarily raise the priority of \alert{L})}

  \end{tabular}

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{A First Correctness ``Proof''}

  \Large

  \begin{itemize}

  \item the paper$^\star$ first describing  PIP ``proved'' also its 

  correctness:\\[5mm]

  \end{itemize}

  \normalsize

  \begin{quote}

  \ldots{}after the thread (whose priority has been raised) completes its 

  critical section and releases the lock, it ``returns to its original 

  priority level''.

  \end{quote}\bigskip

  \small

  $^\star$ in IEEE Transactions on Computers in 1990 by Sha et al.

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{}

  \Large

  \begin{center}

  \begin{tabular}{l}

  \alert{H}igh-priority process 1 (waits)\\[2mm]

  \alert{H}igh-priority process 2 (waits)\\[8mm]

  \alert{L}ow-priority process (has a lock)

  \end{tabular}

  \end{center}

  \onslide<2->{

  \begin{itemize}

  \item Solution: return to the highest

  \phantom{Solution:} \alert{remaining} priority\\

  \end{itemize}}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Specification}

  \Large

   \begin{itemize}\Large

  \item Use Inductive Method with events of the form:

   \end{itemize}

  \begin{center}

  \begin{tabular}{l}

  Create \textcolor{gray}{thread priority}\\

  Exit \textcolor{gray}{thread}\\

  Set \textcolor{gray}{thread priority}\\

  Lock \textcolor{gray}{thread cs}\\

  Unlock \textcolor{gray}{thread cs}\\

  \end{tabular}

  \end{center}\medskip

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Scheduling States}

  \Large

  \begin{itemize}

  \item A \alert{state s} is a list of events\bigskip

  \begin{center}

  \begin{tikzpicture}

  \draw [->, line width=1.5mm] (-4,0) -- (4, 0);

  \draw [line width=0.8mm] (-4, 0.3) -- (-4, -0.3);

  \draw [line width=0.8mm] (1, 0.3) -- (1, -0.3);

  \node at (1,-0.7) {\large s};

  \node at (-4,-0.7) {\large 0};

  \node at (3.2,-0.7) {\large time};

  \end{tikzpicture}

  \end{center}\pause

  \item Scheduling according to \alert{precedences}:

  \begin{center}

  \begin{tabular}{@ {}l@ {}}

  \large @{thm preced_def[where thread="th"]} 

  \end{tabular}

  \end{center}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Waiting Queues}

  \large

  \begin{itemize}