(*<*)
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\})
  \end{minipage}
  \end{center}

  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{The Scheduler}
  \large

  \begin{itemize}
  \item \underline{Start}: all priorities/precedences are 0, all resources are unlocked
  \item \underline{Create th p}: set precedence of th
  \item \underline{Exit th}: reset precedence to 0
  \item \underline{Set th p}: reset precedence of th
  \item \underline{Lock th cs}: add th to the end of the waiting queue of cs
  \item \underline{Unlock th cs}:\\ delete th from the waiting queue of cs\\
  \hspace{1cm}\alert{and who to give the resource next?}
  \end{itemize}
  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{The Scheduler (2)}
  %%\large

  \begin{itemize}
  \item \large threads ready to run\normalsize

  \begin{center}
  \begin{tabular}{@ {}l}
  @{thm (lhs) readys_def} $\dn$\\
  \;@{thm (rhs) readys_def}
  \end{tabular}
  \end{center}\bigskip

  \item \large the thread that is running in a state:\\[-10mm]\normalsize
  \begin{center}
  \begin{tabular}{@ {}l@ {}}
  @{thm (lhs) runing_def} $\dn$\\
  \;@{thm (rhs) runing_def}
  \end{tabular}
  \end{center}

  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Inductive Method}
  %%\large

  \begin{center}
\begin{tikzpicture}[scale=1.6]
%%\draw[step=2mm] (-4,-1) grid (4,1.4);
\draw (0,0.2) node {\begin{tabular}{l} valid\\[-1mm] scheduler\\[-1mm] states\\ \end{tabular}};
\draw (3,0) node {\begin{tabular}{l} set of invalid\\[-1mm] scheduler states \\[-1mm](e.g., deadlocks)\\ \end{tabular}};
\draw[<-, line width=0.5mm] (1.0,0) -- (1.8,0);
\draw[<-, line width=0.5mm] (-0.2,-0.55) -- (-0.4,-1.3);
\draw (-0.0,-1.5) node {\begin{tabular}{l} inductively defined set \end{tabular}};

\draw[line width=0.5mm, rounded corners=6.3pt] 
  (-0.9,-0.05) -- (-0.8,0.6) -- (-0.3,0.95) -- (0,1) -- (0.5,0.8) -- (0.65,0.5) -- (0.7,0) -- (0.4,-0.5) -- (0,-0.6) -- (-0.5,-0.45) -- cycle;

\draw[line width=0.5mm, rounded corners=15pt] 
 (-1.2,0) -- (-0.9,0.95) -- (0,1.2) -- (1.0,1.0) -- (1.7,0) -- (0.95,-1.0) -- (0,-1.2) -- (-0.9,-0.9) -- cycle;

\end{tikzpicture}
\end{center}

  \begin{itemize}
  \item We have to exclude situation where there is a deadlock,
  a thread exited before created, \ldots
  
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Valid Next Events}
  \large

  \begin{itemize}
  \item In a state s, the following events can occur:
  \end{itemize}

  \begin{center}
  @{thm[mode=Rule] thread_create[where thread=th]}\bigskip

  @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip

  @{thm[mode=Rule] thread_set[where thread=th]}
  \end{center}

  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Valid Next Events (2)}
  \large

  \begin{center}
  @{thm[mode=Rule] thread_P[where thread=th]}\bigskip
  
  @{thm[mode=Rule] thread_V[where thread=th]}\bigskip
  \end{center}\bigskip\pause

  \begin{itemize}
  \item Done with the specification. \ldots
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Correctness Criterion}
  \large
  

  \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);
  \draw [line width=0.8mm] (0, 0.3) -- (0, -0.3);
  \node at (1,-0.7) {\large s'};
  \node at (0,-0.7) {\large s};
  \node at (1,-1.5) {\small(th')};
  \node at (0,-1.5) {\small(th)};
  \node at (-4,-0.7) {\large 0};
  \node at (3.2,-0.7) {\large time};
  \end{tikzpicture}
  \end{center}

  \normalsize
  \begin{itemize}
  \item {\bf If} th is alive in s and has the highest precedence
  \item plus some further assumption (like th not reset, exited, no higher precedences)
  \item and th is {\bf not} running in s', \\ {\bf then} the running
  thread th' (in s') is a thread that was alive in {\bf s} and has in s' the same 
  precedence as th in s.
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


(*<*)
context extend_highest_gen
begin
(*>*)

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{Implementation}

  
  \begin{itemize}
  \item Create/Exit events:
  \begin{itemize}
  \item we do not have to recalculate the RAG
  \item we do not have to recalculate the other precedences
  \end{itemize}\bigskip
  \item Set event:
  \begin{itemize}
  \item we do not have to recalculate the RAG
  \item also the other precedences do not have to be recalculated
  (since this is the currently running thread, it cannot affect
  other threads)
  \end{itemize}
  \item Unlock event (2 cases: a thread to take over, no thread to take over)
  \begin{itemize}
  \item case 1: RAG need to be modified, but appart from th and th' no
  other precedence needs to be recalculated
  \item case 2: RAG needs to be prunned, no precedence needs to be recalculated
  \end{itemize}
  \end{itemize}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{Implementation (2)}

  
  \begin{itemize}
  \item Unlock event (2 cases: a thread to take over, no thread to take over)
  \begin{itemize}
  \item case 1: RAG need to be modified, but appart from th and th' no
  other precedence needs to be recalculated
  \item case 2: RAG needs to be prunned, no precedence needs to be recalculated
  \end{itemize}\bigskip
  \item Lock event (2 cases: cs is locked, not locked)
  \begin{itemize}
  \item case 1: an waiting edge needs to be added to the RAG, precedences of 
  all dependants need to recalculated (where there is a change)  
  \item case 2: an holding edge needs to be added to the RAG, no
  precedences need to be recalculuated
  \end{itemize}
  \end{itemize}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Implementation}
  
  \begin{itemize} 
  \item in PINTOS (Stanford), written in C for educational purposes\bigskip
  \begin{center}
  \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
  \hline
  {\bf Event} & {\bf PINTOS function} \\
  \hline
  @{text Create} & @{text "thread_create"}\\
  @{text Exit}   & @{text "thread_exit"}\\
  @{text Set}    & @{text "thread_set_priority"}\\
  @{text Lock}      & @{text "lock_acquire"}\\
  @{text Unlock}      & @{text "lock_release"}\\ 
  \hline
  \end{tabular}
  \end{center}\pause\bigskip

  \item \alert{We did not verify our C-code!}\pause
  \item We were much faster: we gave an unlocked resource to
  the thread with the highest precedence
  \end{itemize}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{What Next?}
  \large

  \begin{itemize} 
  \item Did we make any impact? No!\medskip\pause
  
  \item real-time scheduling on multiprocessors seems to be a very
  underdeveloped area. 
  \item implementations exist: RT-Linux\bigskip

  \item The inductive approach can deal with distributed
  algorithms\\ \normalsize(a clock syncronisation algorithm developed by NASA)
  \end{itemize}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Theorem Provers}
  \large

  \begin{itemize} 
  \item We found a mistake in a refereed paper by Harper \& Pfenning
  \item I also found a mistake in my PhD thesis\bigskip
  
  \item scratching on the surface of an completely ``alien'' subject 
  to us --- we were able to make progress
  \item a string algorithm about suffix sorting (appeared at ICALP 2005)\smallskip\\
  \small no implementation exists, claim: ``we are the best'';
  we found an error the {\bf old-fashioned way}; now we need to verify our fix :(
  \end{itemize}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{State of the Art}
  \large

  theorem provers are bad with:

  \begin{itemize} 
  \item real number arithmetic (Big-O stuff)
  \item C-programs
  \end{itemize}\bigskip
 
  what others(we) are working on:

  \begin{itemize} 
  \item write your programs inside your theorem prover, verify it,
  compile it to efficient machine code (compilation is verified)
  \end{itemize}
 

 \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Questions?}
  
  \begin{itemize} \large
  \item Thank you for the invitation and for listening!
  \end{itemize}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


(*<*)
end
end
(*>*)