(*<*)

theory Slides2

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}{Leicester, 7 December 2012}

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

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

  \mode<presentation>{

  \begin{frame}

  \frametitle{%

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

  \\[-3mm]

  \LARGE A Provably Correct\\[-1mm] 

  \LARGE Priority Inheritance Protocol\\[-3mm] 

  \end{tabular}}

  \begin{center}

   Christian Urban\\

  \small King's College London

  \end{center}\bigskip

  \begin{center}

  \small joint work with Xingyuan Zhang and Chunhan Wu from the PLA

  University of Science and Technology in Nanjing

  \end{center}

  \end{frame}}

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

*}

text_raw {*

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

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Interactive Theorem Proving}

  \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}{10cm}\raggedright

  \ldots more often than not, thinking is only Plan B

  \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 {*

  \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{Real-Time OSes}

  \large

  \begin{itemize}

  \item Purpose of a general OS:\\ 

  give access to various resources\\

  $\Rightarrow$ access needs to be moderated by\\ 

  $\phantom{\Rightarrow}$ locking and unlocking\medskip \\

  \item Purpose of a real-time OS:\\

  gurantee tasks to be completed in time\medskip\pause

  \item \alert{this already results into a surprisingly non-trivial scheduling 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 despite NASA's famous testing procedure, the lander reset frequently on Mars

  --- 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} is a list of event\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}

  \item A \alert{waiting queue} function returns a list of threads

  associated with every resource

  \item The head of the list is the thread holding the resource.

  \medskip

  \begin{center}\normalsize

  \begin{tabular}{@ {}l}

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

  @{thm cs_waiting_def[where thread="th"]}

  \end{tabular}

  \end{center}

  \end{itemize}

  \end{frame}}

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

*}

text_raw {*

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

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Resource Allocation Graphs}

\begin{center}

  \newcommand{\fnt}{\fontsize{7}{8}\selectfont}

  \begin{tikzpicture}[scale=1]

  \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};

  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};

  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};

  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};

  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};

  \node (E1) at (6, 0.3) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};

  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};

  \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds}  (B);

  \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waits}  (B);

  \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waits}  (B);

  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holds}  (E);

  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds}  (E1);

  \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waits}  (E);

  \end{tikzpicture}

  \end{center}\bigskip

  \begin{center}

  \begin{minipage}{0.8\linewidth}

  \raggedleft

  @{thm cs_depend_def}

  \end{minipage}\medskip\\

  \begin{minipage}{1\linewidth}

  @{thm cs_dependents_def}

  \end{minipage}\medskip\\\pause

  \begin{minipage}{1\linewidth}

  \alert{cprec wq s th} $\dn$\\

  \mbox{}\hspace{1cm}Max(\{prec th s\} $\cup$\\ 

  \mbox{}\hspace{1cm}\phantom{Max(}\{prec th' s $\mid$ th' $\in$ dependants wq th\})