--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides3.thy Thu Jun 20 13:50:01 2013 -0400
@@ -0,0 +1,966 @@
+(*<*)
+theory Slides3
+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