
diff -r 9d667d545e32 -r 0f2d4b78f839 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Thu Dec 06 16:30:57 2012 +0000
+++ b/Slides/Slides2.thy	Mon Dec 10 21:27:22 2012 +0000
@@ -23,6 +23,8 @@
   waiting ("waits") and
   Th ("T") and
   Cs ("C") and
+  P ("Lock") and
+  V ("Unlock") and
   readys ("ready") and
   depend ("RAG") and 
   preced ("prec") and
@@ -38,7 +40,7 @@
 
 
 text_raw {*
-  \renewcommand{\slidecaption}{Nanjing, P.R. China, 1 August 2012}
+  \renewcommand{\slidecaption}{Leicester, 7 December 2012}
   \newcommand{\bl}[1]{#1}                        
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
@@ -46,22 +48,18 @@
   \frametitle{%
   \begin{tabular}{@ {}c@ {}}
   \\[-3mm]
-  \Large Priority Inheritance Protocol \\[-3mm] 
-  \Large Proved Correct \\[0mm]
+  \LARGE A Provably Correct\\[-1mm] 
+  \LARGE Priority Inheritance Protocol\\[-3mm] 
   \end{tabular}}
   
   \begin{center}
-  \small Xingyuan Zhang \\
-  \small \mbox{PLA University of Science and Technology} \\
-  \small \mbox{Nanjing, China}
-  \end{center}
-
+   Christian Urban\\
+  \small King's College London
+  \end{center}\bigskip
+ 
   \begin{center}
-  \small joint work with \\
-  Christian Urban \\
-  Kings College, University of London, U.K.\\
-  Chunhan Wu \\
-  My Ph.D. student now working for Christian\\
+  \small joint work with Xingyuan Zhang and Chunhan Wu from the PLA
+  University of Science and Technology in Nanjing
   \end{center}
 
   \end{frame}}
@@ -72,28 +70,85 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{\large Prioirty Inheritance Protocol (PIP)}
-  \large
+  \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{itemize} 
-  \item Widely used in Real-Time OSs \pause
-  \item One solution of \textcolor{red}{`Priority Inversion'} \pause
-  \item A flawed manual correctness proof (1990)\pause
-        \begin{itemize} \large
-          \item {Notations with no precise definition}
-          \item {Resorts to intuitions}
-        \end{itemize} \pause
-  \item Formal treatments using model-checking \pause
-        \begin{itemize} \large
-          \item {Applicable to small size system models}
-          \item { Unhelpful for human understanding } 
-        \end{itemize} \pause
-  \item Verification of PCP in PVS (2000)\pause
-        \begin{itemize} \large
-           \item {A related protocol}
-           \item {Priority Ceiling Protocol}
-        \end{itemize}
-  \end{itemize}
+  \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}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -101,22 +156,94 @@
 *}
 
 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{Our Motivation}
+  \frametitle{Real-Time OSes}
   \large
 
   \begin{itemize}
-  \item Undergraduate OS course in our university \pause
-        \begin{itemize}
-           \item {\large Experiments using instrutional OSs }
-           \item {\large PINTOS (Stanford) is chosen }
-           \item {\large Core project: Implementing PIP in it}
-        \end{itemize} \pause
-  \item Understanding is crucial for the implemention \pause
-  \item Existing literature of little help \pause
-  \item Some mention the complication
+  \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}}
@@ -129,96 +256,22 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{\mbox{Some excerpts}}
-  
-  \begin{quote}
-  ``Priority inheritance is neither ef$\!$ficient nor reliable. 
-  Implementations are either incomplete (and unreliable) 
-  or surprisingly complex and intrusive.''
-  \end{quote}\medskip
-
-  \pause
-
-  \begin{quote}
-  ``I observed in the kernel code (to my disgust), the Linux 
-  PIP implementation is a nightmare: extremely heavy weight, 
-  involving maintenance of a full wait-for graph, and requiring 
-  updates for a range of events, including priority changes and 
-  interruptions of wait operations.''
-  \end{quote}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Our Aims}
-  \large
-
-  \begin{itemize}
-  \item Formal specification at appropriate abstract level,
-        convenient for:
-  \begin{itemize} \large
-    \item Constructing interactive proofs
-    \item Clarifying the underlying ideas
-  \end{itemize} \pause
-  \item Theorems usable to guide implementation, critical point:
-    \begin{itemize} \large
-      \item Understanding the relationship with real OS code \pause
-      \item Not yet formalized
-    \end{itemize}
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Real-Time OSes}
-  \large
-
-  \begin{itemize}
-  \item Purpose: gurantee the most urgent task to be processed in time
-  \item Processes have priorities\\
-  \item Resources can be locked and unlocked
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Problem}
+  \frametitle{The Problem}
   \Large
 
   \begin{center}
   \begin{tabular}{l}
-  \alert{H}igh-priority process\\[4mm]
+  \alert{H}igh-priority process (waits)\\[4mm]
   \onslide<2->{\alert{M}edium-priority process}\\[4mm]
-  \alert{L}ow-priority process\\[4mm]
+  \alert{L}ow-priority process (has a lock)\\[4mm]
   \end{tabular}
   \end{center}
 
   \onslide<3->{
   \begin{itemize}
-  \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L}
-  \item<4> avoid indefinite priority inversion
+  \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}}
@@ -228,33 +281,22 @@
 
 
 text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Priority Inversion}
-
-  \begin{center}
-  \includegraphics[scale=0.4]{PriorityInversion.png}
-  \end{center}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
-text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
   \frametitle{Mars Pathfinder Mission 1997}
-  \Large
+  \large
 
   \begin{center}
-  \includegraphics[scale=0.2]{marspath1.png}
-  \includegraphics[scale=0.22]{marspath3.png}
-  \includegraphics[scale=0.4]{marsrover.png}
+  \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}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -264,17 +306,17 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Solution}
+  \frametitle{The Solution}
   \Large
 
-  \alert{Priority Inheritance Protocol (PIP):}
+  \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\\[21mm]
-  {\normalsize (temporarily raise its priority)}
+  \alert{L}ow-priority process\\[15mm]
+  {\normalsize (temporarily raise the priority of \alert{L})}
   \end{tabular}
   \end{center}
 
@@ -289,12 +331,12 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{A Correctness ``Proof'' in 1990}
+  \frametitle{A First Correctness ``Proof''}
   \Large
 
   \begin{itemize}
-  \item a paper$^\star$ 
-  in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm]
+  \item the paper$^\star$ first describing  PIP ``proved'' also its 
+  correctness:\\[5mm]
   \end{itemize}
 
   \normalsize
@@ -305,7 +347,7 @@
   \end{quote}\bigskip
 
   \small
-  $^\star$ in IEEE Transactions on Computers
+  $^\star$ in IEEE Transactions on Computers in 1990 by Sha et al.
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
@@ -319,51 +361,32 @@
 
   \begin{center}
   \begin{tabular}{l}
-  \alert{H}igh-priority process 1\\[2mm]
-  \alert{H}igh-priority process 2\\[8mm]
-  \alert{L}ow-priority process
+  \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 highest \alert{remaining} priority
+  \item Solution: return to the highest
+  \phantom{Solution:} \alert{remaining} priority\\
   \end{itemize}}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Event Abstraction}
-
-  \begin{itemize}\large
-     \item Use Inductive Approach of L. Paulson \pause
-     \item System is event-driven \pause
-     \item A \alert{state} is a list of events 
-  \end{itemize}
-
-  \pause
-
-  \begin{center}
-  \includegraphics[scale=0.4]{EventAbstract.png}
-  \end{center}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Events}
+  \frametitle{Specification}
   \Large
+  
+   \begin{itemize}\Large
+  \item Use Inductive Method with events of the form:
+   \end{itemize}
 
   \begin{center}
   \begin{tabular}{l}
@@ -383,13 +406,101 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Precedences}
+  \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{tabular}{l}
-  @{thm preced_def[where thread="th"]} 
-  \end{tabular}
+  \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}
 
   
@@ -403,52 +514,102 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{RAGs}
-
-\begin{center}
-  \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
-  \begin{tikzpicture}[scale=1]
-  %%\draw[step=2mm] (-3,2) grid (1,-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.2) [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"}};
+  \frametitle{The Scheduler}
+  \large
 
-  \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);
-  \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);
-  \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);
-  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);
-  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);
-  \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);
-  \end{tikzpicture}
-  \end{center}\bigskip
-
-  \begin{center}
-  \begin{minipage}{0.8\linewidth}
-  \raggedleft
-  @{thm cs_depend_def}
-  \end{minipage}
-  \end{center}\pause
-
+  \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{Good Next Events}
+  \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
@@ -466,78 +627,17 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Good Next Events}
-  %%\large
+  \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}
-
-  
+  \end{center}\bigskip\pause
 
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-(*<*)
-context extend_highest_gen
-begin
-(*>*)
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\mbox{\large Theorem: ``No indefinite priority inversion''}}
-
-  \pause
-
-  Theorem $^\star$: If th is the thread with the highest precedence in state 
-  @{text "s"}: \pause
-  \begin{center}
-  \textcolor{red}{@{thm highest})}
-  \end{center}
-  \pause
-  and @{text "th"} is blocked by a thread @{text "th'"} in 
-  a future state @{text "s'"} (with @{text "s' = t@s"}): \pause
-  \begin{center}
-  \textcolor{red}{@{text "th' \<in> running (t@s)"} and @{text "th' \<noteq> th"}} \pause
-  \end{center}
-  \fbox{ \hspace{1em} \pause
-  \begin{minipage}{0.95\textwidth}
   \begin{itemize}
-  \item @{text "th'"} did not hold or wait for a resource in s:
-  \begin{center}
-  \textcolor{red}{@{text "\<not>detached s th'"}}  
-  \end{center} \pause
-  \item @{text "th'"} is running with the precedence of @{text "th"}:
-  \begin{center}
-  \textcolor{red}{@{text "cp (t@s) th' = preced th s"}} 
-  \end{center} 
-  \end{itemize}
-  \end{minipage}}
-  \pause
-  \small
-  $^\star$ modulo some further assumptions\bigskip\pause
-  It does not matter which process gets a released lock.
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[t]
-  \frametitle{Implementation}
-  
-  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
-
-  When @{text "e"} = \alert{Create th prio}, \alert{Exit th} 
-  
-  \begin{itemize}
-  \item @{text "RAG s' = RAG s"}
-  \item No precedence needs to be recomputed
+  \item Done with the specification. \ldots
   \end{itemize}
 
   \end{frame}}
@@ -547,45 +647,71 @@
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}[t]
-  \frametitle{Implementation}
-
-  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
+  \begin{frame}[c]
+  \frametitle{Correctness Criterion}
+  \large
   
 
-  When @{text "e"} = \alert{Set th prio}
-  
+  \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 @{text "RAG s' = RAG s"}
-  \item No precedence needs to be recomputed
+  \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}
 
-  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
-
-  When @{text "e"} = \alert{Unlock th cs} where there is a thread to take over
   
   \begin{itemize}
-  \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"}
-  \item we have to recalculate the precedence of the direct descendants
+  \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
-
-  \pause
-
-  When @{text "e"} =  \alert{Unlock th cs} where no thread takes over
-  
+  \item Set event:
   \begin{itemize}
-  \item @{text "RAG s' = RAG s - {(C cs, T th)}"}
-  \item no recalculation of precedences
+  \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}
 
 
@@ -597,24 +723,23 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[t]
-  \frametitle{Implementation}
+  \frametitle{Implementation (2)}
 
-  s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
-
-  When @{text "e"} = \alert{Lock th cs} where cs is not locked
   
   \begin{itemize}
-  \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"}
-  \item no recalculation of precedences
+  \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
-
-  \pause
-
-  When @{text "e"} = \alert{Lock th cs} where cs is locked
-  
+  \item Lock event (2 cases: cs is locked, not locked)
   \begin{itemize}
-  \item @{text "RAG s' = RAG s - {(T th, C cs)}"}
-  \item we have to recalculate the precedence of the descendants
+  \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}
 
 
@@ -627,22 +752,48 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Conclusion}
+  \frametitle{Implementation}
   
-  \begin{itemize} \large
-  \item Aims fulfilled \medskip \pause
-  \item Alternative way \pause
-       \begin{itemize} 
-           \item using Isabelle/HOL in OS code development \medskip
-           \item through the Inductive Approach
-       \end{itemize} \pause
-  \item Future research \pause
-       \begin{itemize}
-           \item scheduler in RT-Linux\medskip
-           \item multiprocessor case\medskip
-           \item other ``nails'' ? (networks, \ldots) \medskip \pause
-           \item Refinement to real code and relation between implementations
-        \end{itemize}
+  \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}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -652,10 +803,58 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \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 listening!
+  \item Thank you for the invitation and for listening!
   \end{itemize}
   
   \end{frame}}




