--- 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