
diff -r 2c56b20032a7 -r 0679a84b11ad prio/Slides/Slides1.thy
--- a/prio/Slides/Slides1.thy	Mon Dec 03 08:16:58 2012 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,669 +0,0 @@
-(*<*)
-theory Slides1
-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
-  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}{Nanjing, P.R. China, 1 August 2012}
-  \newcommand{\bl}[1]{#1}                        
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}
-  \frametitle{%
-  \begin{tabular}{@ {}c@ {}}
-  \\[-3mm]
-  \Large Priority Inheritance Protocol \\[-3mm] 
-  \Large Proved Correct \\[0mm]
-  \end{tabular}}
-  
-  \begin{center}
-  \small Xingyuan Zhang \\
-  \small \mbox{PLA University of Science and Technology} \\
-  \small \mbox{Nanjing, China}
-  \end{center}
-
-  \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\\
-  \end{center}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\large Prioirty Inheritance Protocol (PIP)}
-  \large
-
-  \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}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Our Motivation}
-  \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
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \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}
-  \Large
-
-  \begin{center}
-  \begin{tabular}{l}
-  \alert{H}igh-priority process\\[4mm]
-  \onslide<2->{\alert{M}edium-priority process}\\[4mm]
-  \alert{L}ow-priority process\\[4mm]
-  \end{tabular}
-  \end{center}
-
-  \onslide<3->{
-  \begin{itemize}
-  \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L}
-  \item<4> avoid indefinite priority inversion
-  \end{itemize}}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-
-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
-
-  \begin{center}
-  \includegraphics[scale=0.2]{marspath1.png}
-  \includegraphics[scale=0.22]{marspath3.png}
-  \includegraphics[scale=0.4]{marsrover.png}
-  \end{center}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Solution}
-  \Large
-
-  \alert{Priority Inheritance Protocol (PIP):}
-
-  \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)}
-  \end{tabular}
-  \end{center}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{A Correctness ``Proof'' in 1990}
-  \Large
-
-  \begin{itemize}
-  \item a paper$^\star$ 
-  in 1990 ``proved'' the correctness of an algorithm for PIP\\[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
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{}
-  \Large
-
-  \begin{center}
-  \begin{tabular}{l}
-  \alert{H}igh-priority process 1\\[2mm]
-  \alert{H}igh-priority process 2\\[8mm]
-  \alert{L}ow-priority process
-  \end{tabular}
-  \end{center}
-
-  \onslide<2->{
-  \begin{itemize}
-  \item Solution: \\Return to highest \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}
-  \Large
-
-  \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{Precedences}
-  \large
-
-  \begin{center}
-  \begin{tabular}{l}
-  @{thm preced_def[where thread="th"]} 
-  \end{tabular}
-  \end{center}
-
-  
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \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"}};
-
-  \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
-
-  
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Good Next Events}
-  %%\large
-
-  \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{Good Next Events}
-  %%\large
-
-  \begin{center}
-  @{thm[mode=Rule] thread_P[where thread=th]}\bigskip
-  
-  @{thm[mode=Rule] thread_V[where thread=th]}\bigskip
-  \end{center}
-
-  
-
-  \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
-  \end{itemize}
-
-  \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{Set th prio}
-  
-  \begin{itemize}
-  \item @{text "RAG s' = RAG s"}
-  \item No precedence needs to be recomputed
-  \end{itemize}
-
-  \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{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
-  \end{itemize}\bigskip
-
-  \pause
-
-  When @{text "e"} =  \alert{Unlock th cs} where no thread takes over
-  
-  \begin{itemize}
-  \item @{text "RAG s' = RAG s - {(C cs, T th)}"}
-  \item no recalculation of precedences
-  \end{itemize}
-
-
-  \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{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
-  \end{itemize}\bigskip
-
-  \pause
-
-  When @{text "e"} = \alert{Lock th cs} where cs is locked
-  
-  \begin{itemize}
-  \item @{text "RAG s' = RAG s - {(T th, C cs)}"}
-  \item we have to recalculate the precedence of the descendants
-  \end{itemize}
-
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Conclusion}
-  
-  \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}
-  \end{itemize}
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Questions?}
-  
-  \begin{itemize} \large
-  \item Thank you for listening!
-  \end{itemize}
-  
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-
-(*<*)
-end
-end
-(*>*)
\ No newline at end of file




