diff -r 3cc70bd49588 -r b56616fd88dd Slides/Slides4.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides4.thy	Tue Feb 25 20:01:47 2014 +0000
@@ -0,0 +1,966 @@
+(*<*)
+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}
+  \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 situations 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, not exited, no higher precedences in s - s')
+  \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 needs to be modified, but apart 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 needs to be modified, but apart from th and th' no
+  other precedence needs to be recalculated
+  \item case 2: RAG needs to be pruned, no precedence needs to be recalculated
+  \end{itemize}\bigskip
+  \item Lock event (2 cases: cs is locked, not locked)
+  \begin{itemize}
+  \item case 1: a waiting edge needs to be added to the RAG, precedences of 
+  all dependants need to recalculated (where there is a change)  
+  \item case 2: a holding edge needs to be added to the RAG, no
+  precedences need to be recalculated
+  \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{A Step Back\ldots}
+  \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, e.g.~RT-Linux
+  \end{itemize}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Theorem Provers}
+
+  \begin{itemize} 
+  \item We found a mistake in a refereed paper by Harper \& Pfenning
+  \item I also found a mistake in my PhD thesis
+  \item also a popular textbook book on Computability contained an
+  error\bigskip
+  
+  \item scratching on the surface of an completely ``alien'' subject 
+  to us --- we were able to make progress
+
+  \end{itemize}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Inductive Method / Protocols}
+
+  \begin{itemize} 
+  \item the inductive method was developed/used by Larry Paulson
+  for verifying security protocols\bigskip\bigskip
+  \item we used it for a different `kind' of protocols (scheduling)
+  \item but this was restricted to only single-processors, no timing information
+
+
+  \end{itemize}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Clock Synchronisation}
+
+  \begin{itemize} 
+  \item Mahyar Malekpour introduced a distributed clock-synchronisation
+  algorithm\\ (perfect example for us)\bigskip\bigskip
+
+  \item connected units exchange messages according to a protocol
+  and reach a stable, synchronised state
+  \item messages have to reach the receiver within a time-window\pause
+
+  \item \alert{verification still ongoing}
+  \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}
+  
+  \begin{center}
+  \begin{tabular}{c}
+  \includegraphics[scale=0.13]{isabelle.png}\\[-2mm]
+  \small\url{http://isabelle.in.tum.de}
+  \end{tabular}
+  \end{center}  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+(*<*)
+end
+end
+(*>*)
\ No newline at end of file