--- a/Slides/Slides2.thy Thu Dec 06 16:30:57 2012 +0000
+++ b/Slides/Slides2.thy Mon Dec 10 21:27:22 2012 +0000
@@ -23,6 +23,8 @@
waiting ("waits") and
Th ("T") and
Cs ("C") and
+ P ("Lock") and
+ V ("Unlock") and
readys ("ready") and
depend ("RAG") and
preced ("prec") and
@@ -38,7 +40,7 @@
text_raw {*
- \renewcommand{\slidecaption}{Nanjing, P.R. China, 1 August 2012}
+ \renewcommand{\slidecaption}{Leicester, 7 December 2012}
\newcommand{\bl}[1]{#1}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
@@ -46,22 +48,18 @@
\frametitle{%
\begin{tabular}{@ {}c@ {}}
\\[-3mm]
- \Large Priority Inheritance Protocol \\[-3mm]
- \Large Proved Correct \\[0mm]
+ \LARGE A Provably Correct\\[-1mm]
+ \LARGE Priority Inheritance Protocol\\[-3mm]
\end{tabular}}
\begin{center}
- \small Xingyuan Zhang \\
- \small \mbox{PLA University of Science and Technology} \\
- \small \mbox{Nanjing, China}
- \end{center}
-
+ Christian Urban\\
+ \small King's College London
+ \end{center}\bigskip
+
\begin{center}
- \small joint work with \\
- Christian Urban \\
- Kings College, University of London, U.K.\\
- Chunhan Wu \\
- My Ph.D. student now working for Christian\\
+ \small joint work with Xingyuan Zhang and Chunhan Wu from the PLA
+ University of Science and Technology in Nanjing
\end{center}
\end{frame}}
@@ -72,28 +70,85 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{\large Prioirty Inheritance Protocol (PIP)}
- \large
+ \frametitle{Interactive Theorem Proving}
+
+ \begin{center}
+ \includegraphics[scale=0.23]{isabelle.png}
+ \end{center}
+
+ \only<2>{
+ \begin{textblock}{12}(2,13.6)
+ \begin{tikzpicture}
+ \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ {\normalsize\color{darkgray}
+ \begin{minipage}{10cm}\raggedright
+ \ldots more often than not, thinking is only Plan B
+
+ \end{minipage}};
+ \end{tikzpicture}
+ \end{textblock}}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+*}
+
+text_raw {*
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ \tikzstyle{node1}=[rectangle, minimum size=8mm, rounded corners=3mm, very thick,
+ draw=black!50, top color=white, bottom color=black!20]
+ \tikzstyle{node2}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
+ draw=red!70, top color=white, bottom color=red!50!black!20]
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{}
- \begin{itemize}
- \item Widely used in Real-Time OSs \pause
- \item One solution of \textcolor{red}{`Priority Inversion'} \pause
- \item A flawed manual correctness proof (1990)\pause
- \begin{itemize} \large
- \item {Notations with no precise definition}
- \item {Resorts to intuitions}
- \end{itemize} \pause
- \item Formal treatments using model-checking \pause
- \begin{itemize} \large
- \item {Applicable to small size system models}
- \item { Unhelpful for human understanding }
- \end{itemize} \pause
- \item Verification of PCP in PVS (2000)\pause
- \begin{itemize} \large
- \item {A related protocol}
- \item {Priority Ceiling Protocol}
- \end{itemize}
- \end{itemize}
+ \begin{tabular}{@ {}c@ {\hspace{2mm}}c}
+ \\[6mm]
+ \begin{tabular}{c}
+ \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
+ {\footnotesize Bob Harper}\\[-2.5mm]
+ {\footnotesize (CMU)}
+ \end{tabular}
+ \begin{tabular}{c@ {}}
+ \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
+ {\footnotesize Frank Pfenning}\\[-2.5mm]
+ {\footnotesize (CMU)}
+ \end{tabular} &
+
+ \begin{tabular}{@ {\hspace{-3mm}}p{7cm}}
+ \begin{tikzpicture}[remember picture, scale=0.5]
+ \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+ { \& \& \node (desc) {\makebox[0mm]{\begin{tabular}{l}published in a journal\\
+ \small (ACM ToCL, 31 pages, 2005)\\[3mm]\end{tabular}}};\\
+ \&[-10mm]
+ \node (def1) [node1] {\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+ \node (proof1) [node1] {Proof}; \&
+ \node (alg1) [node1] {\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+ };
+ \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+ \draw[<-,black,line width=0.5mm] (proof1) -- (desc);
+ \end{tikzpicture}
+ \end{tabular}\\
+
+ \pause
+ \\[0mm]
+
+ \multicolumn{2}{c}{
+ \begin{tabular}{p{6cm}}
+ \raggedright
+ \color{black}{relied on their proof in a\\ {\bf security} critical application}
+ \end{tabular}
+
+ \begin{tabular}{c}
+ \includegraphics[scale=0.36]{appel.jpg}\\[-2mm]
+ {\footnotesize Andrew Appel}\\[-2.5mm]
+ {\footnotesize (Princeton)}
+ \end{tabular}}
+ \end{tabular}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -101,22 +156,94 @@
*}
text_raw {*
+ \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
+ draw=black!50, top color=white, bottom color=black!20]
+ \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
+ draw=red!70, top color=white, bottom color=red!50!black!20]
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}<2->[squeeze]
+ \frametitle{}
+
+ \begin{columns}
+
+ \begin{column}{0.8\textwidth}
+ \begin{textblock}{0}(1,2)
+
+ \begin{tikzpicture}
+ \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+ { \&[-10mm]
+ \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+ \node (proof1) [node1] {\large Proof}; \&
+ \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+
+ \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \&
+ \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+ \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+
+ \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+ \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\
+
+ \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+ \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+ };
+
+ \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+ \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+ \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+ \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+
+ \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);}
+ \end{tikzpicture}
+
+ \end{textblock}
+ \end{column}
+ \end{columns}
+
+
+ \begin{textblock}{3}(12,3.6)
+ \onslide<4->{
+ \begin{tikzpicture}
+ \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+ \end{tikzpicture}}
+ \end{textblock}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+
+text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Our Motivation}
+ \frametitle{Real-Time OSes}
\large
\begin{itemize}
- \item Undergraduate OS course in our university \pause
- \begin{itemize}
- \item {\large Experiments using instrutional OSs }
- \item {\large PINTOS (Stanford) is chosen }
- \item {\large Core project: Implementing PIP in it}
- \end{itemize} \pause
- \item Understanding is crucial for the implemention \pause
- \item Existing literature of little help \pause
- \item Some mention the complication
+ \item Purpose of a general OS:\\
+ give access to various resources\\
+ $\Rightarrow$ access needs to be moderated by\\
+ $\phantom{\Rightarrow}$ locking and unlocking\medskip \\
+
+ \item Purpose of a real-time OS:\\
+ gurantee tasks to be completed in time\medskip\pause
+
+ \item \alert{this already results into a surprisingly non-trivial scheduling problem}
\end{itemize}
\end{frame}}
@@ -129,96 +256,22 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{\mbox{Some excerpts}}
-
- \begin{quote}
- ``Priority inheritance is neither ef$\!$ficient nor reliable.
- Implementations are either incomplete (and unreliable)
- or surprisingly complex and intrusive.''
- \end{quote}\medskip
-
- \pause
-
- \begin{quote}
- ``I observed in the kernel code (to my disgust), the Linux
- PIP implementation is a nightmare: extremely heavy weight,
- involving maintenance of a full wait-for graph, and requiring
- updates for a range of events, including priority changes and
- interruptions of wait operations.''
- \end{quote}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Our Aims}
- \large
-
- \begin{itemize}
- \item Formal specification at appropriate abstract level,
- convenient for:
- \begin{itemize} \large
- \item Constructing interactive proofs
- \item Clarifying the underlying ideas
- \end{itemize} \pause
- \item Theorems usable to guide implementation, critical point:
- \begin{itemize} \large
- \item Understanding the relationship with real OS code \pause
- \item Not yet formalized
- \end{itemize}
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Real-Time OSes}
- \large
-
- \begin{itemize}
- \item Purpose: gurantee the most urgent task to be processed in time
- \item Processes have priorities\\
- \item Resources can be locked and unlocked
- \end{itemize}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Problem}
+ \frametitle{The Problem}
\Large
\begin{center}
\begin{tabular}{l}
- \alert{H}igh-priority process\\[4mm]
+ \alert{H}igh-priority process (waits)\\[4mm]
\onslide<2->{\alert{M}edium-priority process}\\[4mm]
- \alert{L}ow-priority process\\[4mm]
+ \alert{L}ow-priority process (has a lock)\\[4mm]
\end{tabular}
\end{center}
\onslide<3->{
\begin{itemize}
- \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L}
- \item<4> avoid indefinite priority inversion
+ \item \alert{priority inversion}\\ \hspace{2cm}@{text "\<equiv>"} H waits for a process\\
+ \mbox{}\hfill with lower priority
+ \item<4> avoid \alert{indefinite} priority inversion
\end{itemize}}
\end{frame}}
@@ -228,33 +281,22 @@
text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Priority Inversion}
-
- \begin{center}
- \includegraphics[scale=0.4]{PriorityInversion.png}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
-
-text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
\frametitle{Mars Pathfinder Mission 1997}
- \Large
+ \large
\begin{center}
- \includegraphics[scale=0.2]{marspath1.png}
- \includegraphics[scale=0.22]{marspath3.png}
- \includegraphics[scale=0.4]{marsrover.png}
+ \includegraphics[scale=0.15]{marspath1.png}
+ \includegraphics[scale=0.16]{marspath3.png}
+ \includegraphics[scale=0.3]{marsrover.png}
\end{center}
+
+ \begin{itemize}
+ \item despite NASA's famous testing procedure, the lander reset frequently on Mars
+ --- problem: priority inversion
+ \end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -264,17 +306,17 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Solution}
+ \frametitle{The Solution}
\Large
- \alert{Priority Inheritance Protocol (PIP):}
+ \alert{Priority Inheritance Protocol (PIP):}\bigskip
\begin{center}
\begin{tabular}{l}
\alert{H}igh-priority process\\[4mm]
\textcolor{gray}{Medium-priority process}\\[4mm]
- \alert{L}ow-priority process\\[21mm]
- {\normalsize (temporarily raise its priority)}
+ \alert{L}ow-priority process\\[15mm]
+ {\normalsize (temporarily raise the priority of \alert{L})}
\end{tabular}
\end{center}
@@ -289,12 +331,12 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{A Correctness ``Proof'' in 1990}
+ \frametitle{A First Correctness ``Proof''}
\Large
\begin{itemize}
- \item a paper$^\star$
- in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm]
+ \item the paper$^\star$ first describing PIP ``proved'' also its
+ correctness:\\[5mm]
\end{itemize}
\normalsize
@@ -305,7 +347,7 @@
\end{quote}\bigskip
\small
- $^\star$ in IEEE Transactions on Computers
+ $^\star$ in IEEE Transactions on Computers in 1990 by Sha et al.
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
@@ -319,51 +361,32 @@
\begin{center}
\begin{tabular}{l}
- \alert{H}igh-priority process 1\\[2mm]
- \alert{H}igh-priority process 2\\[8mm]
- \alert{L}ow-priority process
+ \alert{H}igh-priority process 1 (waits)\\[2mm]
+ \alert{H}igh-priority process 2 (waits)\\[8mm]
+ \alert{L}ow-priority process (has a lock)
\end{tabular}
\end{center}
\onslide<2->{
\begin{itemize}
- \item Solution: \\Return to highest \alert{remaining} priority
+ \item Solution: return to the highest
+ \phantom{Solution:} \alert{remaining} priority\\
\end{itemize}}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{Event Abstraction}
-
- \begin{itemize}\large
- \item Use Inductive Approach of L. Paulson \pause
- \item System is event-driven \pause
- \item A \alert{state} is a list of events
- \end{itemize}
-
- \pause
-
- \begin{center}
- \includegraphics[scale=0.4]{EventAbstract.png}
- \end{center}
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-*}
-
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Events}
+ \frametitle{Specification}
\Large
+
+ \begin{itemize}\Large
+ \item Use Inductive Method with events of the form:
+ \end{itemize}
\begin{center}
\begin{tabular}{l}
@@ -383,13 +406,101 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Precedences}
+ \frametitle{Scheduling States}
+ \Large
+
+ \begin{itemize}
+ \item A \alert{state} is a list of event\bigskip
+ \begin{center}
+ \begin{tikzpicture}
+ \draw [->, line width=1.5mm] (-4,0) -- (4, 0);
+ \draw [line width=0.8mm] (-4, 0.3) -- (-4, -0.3);
+ \draw [line width=0.8mm] (1, 0.3) -- (1, -0.3);
+ \node at (1,-0.7) {\large s};
+ \node at (-4,-0.7) {\large 0};
+ \node at (3.2,-0.7) {\large time};
+ \end{tikzpicture}
+ \end{center}\pause
+
+ \item Scheduling according to \alert{precedences}:
+ \begin{center}
+ \begin{tabular}{@ {}l@ {}}
+ \large @{thm preced_def[where thread="th"]}
+ \end{tabular}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Waiting Queues}
\large
+ \begin{itemize}
+ \item A \alert{waiting queue} function returns a list of threads
+ associated with every resource
+ \item The head of the list is the thread holding the resource.
+ \medskip
+
+ \begin{center}\normalsize
+ \begin{tabular}{@ {}l}
+ @{thm cs_holding_def[where thread="th"]}\\
+ @{thm cs_waiting_def[where thread="th"]}
+ \end{tabular}
+ \end{center}
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Resource Allocation Graphs}
+
+\begin{center}
+ \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
+ \begin{tikzpicture}[scale=1]
+
+ \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
+ \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
+ \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
+ \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
+ \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+ \node (E1) at (6, 0.3) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
+ \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+
+ \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds} (B);
+ \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waits} (B);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waits} (B);
+ \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holds} (E);
+ \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holds} (E1);
+ \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waits} (E);
+ \end{tikzpicture}
+ \end{center}\bigskip
+
\begin{center}
- \begin{tabular}{l}
- @{thm preced_def[where thread="th"]}
- \end{tabular}
+ \begin{minipage}{0.8\linewidth}
+ \raggedleft
+ @{thm cs_depend_def}
+ \end{minipage}\medskip\\
+ \begin{minipage}{1\linewidth}
+ @{thm cs_dependents_def}
+ \end{minipage}\medskip\\\pause
+ \begin{minipage}{1\linewidth}
+ \alert{cprec wq s th} $\dn$\\
+ \mbox{}\hspace{1cm}Max(\{prec th s\} $\cup$\\
+ \mbox{}\hspace{1cm}\phantom{Max(}\{prec th' s $\mid$ th' $\in$ dependants wq th\})
+ \end{minipage}
\end{center}
@@ -403,52 +514,102 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{RAGs}
-
-\begin{center}
- \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
- \begin{tikzpicture}[scale=1]
- %%\draw[step=2mm] (-3,2) grid (1,-1);
-
- \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
- \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
- \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
- \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
- \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
- \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
- \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
+ \frametitle{The Scheduler}
+ \large
- \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B);
- \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
- \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B);
- \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E);
- \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (E1);
- \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E);
- \end{tikzpicture}
- \end{center}\bigskip
-
- \begin{center}
- \begin{minipage}{0.8\linewidth}
- \raggedleft
- @{thm cs_depend_def}
- \end{minipage}
- \end{center}\pause
-
+ \begin{itemize}
+ \item \underline{Start}: all priorities/precedences are 0, all resources are unlocked
+ \item \underline{Create th p}: set precedence of th
+ \item \underline{Exit th}: reset precedence to 0
+ \item \underline{Set th p}: reset precedence of th
+ \item \underline{Lock th cs}: add th to the end of the waiting queue of cs
+ \item \underline{Unlock th cs}:\\ delete th from the waiting queue of cs\\
+ \hspace{1cm}\alert{and who to give the resource next?}
+ \end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
*}
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Good Next Events}
+ \frametitle{The Scheduler (2)}
+ %%\large
+
+ \begin{itemize}
+ \item \large threads ready to run\normalsize
+
+ \begin{center}
+ \begin{tabular}{@ {}l}
+ @{thm (lhs) readys_def} $\dn$\\
+ \;@{thm (rhs) readys_def}
+ \end{tabular}
+ \end{center}\bigskip
+
+ \item \large the thread that is running in a state:\\[-10mm]\normalsize
+ \begin{center}
+ \begin{tabular}{@ {}l@ {}}
+ @{thm (lhs) runing_def} $\dn$\\
+ \;@{thm (rhs) runing_def}
+ \end{tabular}
+ \end{center}
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Inductive Method}
%%\large
\begin{center}
+\begin{tikzpicture}[scale=1.6]
+%%\draw[step=2mm] (-4,-1) grid (4,1.4);
+\draw (0,0.2) node {\begin{tabular}{l} valid\\[-1mm] scheduler\\[-1mm] states\\ \end{tabular}};
+\draw (3,0) node {\begin{tabular}{l} set of invalid\\[-1mm] scheduler states \\[-1mm](e.g., deadlocks)\\ \end{tabular}};
+\draw[<-, line width=0.5mm] (1.0,0) -- (1.8,0);
+\draw[<-, line width=0.5mm] (-0.2,-0.55) -- (-0.4,-1.3);
+\draw (-0.0,-1.5) node {\begin{tabular}{l} inductively defined set \end{tabular}};
+
+\draw[line width=0.5mm, rounded corners=6.3pt]
+ (-0.9,-0.05) -- (-0.8,0.6) -- (-0.3,0.95) -- (0,1) -- (0.5,0.8) -- (0.65,0.5) -- (0.7,0) -- (0.4,-0.5) -- (0,-0.6) -- (-0.5,-0.45) -- cycle;
+
+\draw[line width=0.5mm, rounded corners=15pt]
+ (-1.2,0) -- (-0.9,0.95) -- (0,1.2) -- (1.0,1.0) -- (1.7,0) -- (0.95,-1.0) -- (0,-1.2) -- (-0.9,-0.9) -- cycle;
+
+\end{tikzpicture}
+\end{center}
+
+ \begin{itemize}
+ \item We have to exclude situation where there is a deadlock,
+ a thread exited before created, \ldots
+
+ \end{itemize}
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{Valid Next Events}
+ \large
+
+ \begin{itemize}
+ \item In a state s, the following events can occur:
+ \end{itemize}
+
+ \begin{center}
@{thm[mode=Rule] thread_create[where thread=th]}\bigskip
@{thm[mode=Rule] thread_exit[where thread=th]}\bigskip
@@ -466,78 +627,17 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Good Next Events}
- %%\large
+ \frametitle{Valid Next Events (2)}
+ \large
\begin{center}
@{thm[mode=Rule] thread_P[where thread=th]}\bigskip
@{thm[mode=Rule] thread_V[where thread=th]}\bigskip
- \end{center}
-
-
+ \end{center}\bigskip\pause
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-(*<*)
-context extend_highest_gen
-begin
-(*>*)
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[c]
- \frametitle{\mbox{\large Theorem: ``No indefinite priority inversion''}}
-
- \pause
-
- Theorem $^\star$: If th is the thread with the highest precedence in state
- @{text "s"}: \pause
- \begin{center}
- \textcolor{red}{@{thm highest})}
- \end{center}
- \pause
- and @{text "th"} is blocked by a thread @{text "th'"} in
- a future state @{text "s'"} (with @{text "s' = t@s"}): \pause
- \begin{center}
- \textcolor{red}{@{text "th' \<in> running (t@s)"} and @{text "th' \<noteq> th"}} \pause
- \end{center}
- \fbox{ \hspace{1em} \pause
- \begin{minipage}{0.95\textwidth}
\begin{itemize}
- \item @{text "th'"} did not hold or wait for a resource in s:
- \begin{center}
- \textcolor{red}{@{text "\<not>detached s th'"}}
- \end{center} \pause
- \item @{text "th'"} is running with the precedence of @{text "th"}:
- \begin{center}
- \textcolor{red}{@{text "cp (t@s) th' = preced th s"}}
- \end{center}
- \end{itemize}
- \end{minipage}}
- \pause
- \small
- $^\star$ modulo some further assumptions\bigskip\pause
- It does not matter which process gets a released lock.
-
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-*}
-
-text_raw {*
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \mode<presentation>{
- \begin{frame}[t]
- \frametitle{Implementation}
-
- s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
-
- When @{text "e"} = \alert{Create th prio}, \alert{Exit th}
-
- \begin{itemize}
- \item @{text "RAG s' = RAG s"}
- \item No precedence needs to be recomputed
+ \item Done with the specification. \ldots
\end{itemize}
\end{frame}}
@@ -547,45 +647,71 @@
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
- \begin{frame}[t]
- \frametitle{Implementation}
-
- s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
+ \begin{frame}[c]
+ \frametitle{Correctness Criterion}
+ \large
- When @{text "e"} = \alert{Set th prio}
-
+ \begin{center}
+ \begin{tikzpicture}
+ \draw [->, line width=1.5mm] (-4,0) -- (4, 0);
+ \draw [line width=0.8mm] (-4, 0.3) -- (-4, -0.3);
+ \draw [line width=0.8mm] (1, 0.3) -- (1, -0.3);
+ \draw [line width=0.8mm] (0, 0.3) -- (0, -0.3);
+ \node at (1,-0.7) {\large s'};
+ \node at (0,-0.7) {\large s};
+ \node at (1,-1.5) {\small(th')};
+ \node at (0,-1.5) {\small(th)};
+ \node at (-4,-0.7) {\large 0};
+ \node at (3.2,-0.7) {\large time};
+ \end{tikzpicture}
+ \end{center}
+
+ \normalsize
\begin{itemize}
- \item @{text "RAG s' = RAG s"}
- \item No precedence needs to be recomputed
+ \item {\bf If} th is alive in s and has the highest precedence
+ \item plus some further assumption (like th not reset, exited, no higher precedences)
+ \item and th is {\bf not} running in s', \\ {\bf then} the running
+ thread th' (in s') is a thread that was alive in {\bf s} and has in s' the same
+ precedence as th in s.
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}
+
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
+
text_raw {*
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
\frametitle{Implementation}
- s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
-
- When @{text "e"} = \alert{Unlock th cs} where there is a thread to take over
\begin{itemize}
- \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"}
- \item we have to recalculate the precedence of the direct descendants
+ \item Create/Exit events:
+ \begin{itemize}
+ \item we do not have to recalculate the RAG
+ \item we do not have to recalculate the other precedences
\end{itemize}\bigskip
-
- \pause
-
- When @{text "e"} = \alert{Unlock th cs} where no thread takes over
-
+ \item Set event:
\begin{itemize}
- \item @{text "RAG s' = RAG s - {(C cs, T th)}"}
- \item no recalculation of precedences
+ \item we do not have to recalculate the RAG
+ \item also the other precedences do not have to be recalculated
+ (since this is the currently running thread, it cannot affect
+ other threads)
+ \end{itemize}
+ \item Unlock event (2 cases: a thread to take over, no thread to take over)
+ \begin{itemize}
+ \item case 1: RAG need to be modified, but appart from th and th' no
+ other precedence needs to be recalculated
+ \item case 2: RAG needs to be prunned, no precedence needs to be recalculated
+ \end{itemize}
\end{itemize}
@@ -597,24 +723,23 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[t]
- \frametitle{Implementation}
+ \frametitle{Implementation (2)}
- s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip
-
- When @{text "e"} = \alert{Lock th cs} where cs is not locked
\begin{itemize}
- \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"}
- \item no recalculation of precedences
+ \item Unlock event (2 cases: a thread to take over, no thread to take over)
+ \begin{itemize}
+ \item case 1: RAG need to be modified, but appart from th and th' no
+ other precedence needs to be recalculated
+ \item case 2: RAG needs to be prunned, no precedence needs to be recalculated
\end{itemize}\bigskip
-
- \pause
-
- When @{text "e"} = \alert{Lock th cs} where cs is locked
-
+ \item Lock event (2 cases: cs is locked, not locked)
\begin{itemize}
- \item @{text "RAG s' = RAG s - {(T th, C cs)}"}
- \item we have to recalculate the precedence of the descendants
+ \item case 1: an waiting edge needs to be added to the RAG, precedences of
+ all dependants need to recalculated (where there is a change)
+ \item case 2: an holding edge needs to be added to the RAG, no
+ precedences need to be recalculuated
+ \end{itemize}
\end{itemize}
@@ -627,22 +752,48 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
- \frametitle{Conclusion}
+ \frametitle{Implementation}
- \begin{itemize} \large
- \item Aims fulfilled \medskip \pause
- \item Alternative way \pause
- \begin{itemize}
- \item using Isabelle/HOL in OS code development \medskip
- \item through the Inductive Approach
- \end{itemize} \pause
- \item Future research \pause
- \begin{itemize}
- \item scheduler in RT-Linux\medskip
- \item multiprocessor case\medskip
- \item other ``nails'' ? (networks, \ldots) \medskip \pause
- \item Refinement to real code and relation between implementations
- \end{itemize}
+ \begin{itemize}
+ \item in PINTOS (Stanford), written in C for educational purposes\bigskip
+ \begin{center}
+ \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}
+ \hline
+ {\bf Event} & {\bf PINTOS function} \\
+ \hline
+ @{text Create} & @{text "thread_create"}\\
+ @{text Exit} & @{text "thread_exit"}\\
+ @{text Set} & @{text "thread_set_priority"}\\
+ @{text Lock} & @{text "lock_acquire"}\\
+ @{text Unlock} & @{text "lock_release"}\\
+ \hline
+ \end{tabular}
+ \end{center}\pause\bigskip
+
+ \item \alert{We did not verify our C-code!}\pause
+ \item We were much faster: we gave an unlocked resource to
+ the thread with the highest precedence
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{What Next?}
+ \large
+
+ \begin{itemize}
+ \item Did we make any impact? No!\medskip\pause
+
+ \item real-time scheduling on multiprocessors seems to be a very
+ underdeveloped area.
+ \item implementations exist: RT-Linux\bigskip
+
+ \item The inductive approach can deal with distributed
+ algorithms\\ \normalsize(a clock syncronisation algorithm developed by NASA)
\end{itemize}
\end{frame}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -652,10 +803,58 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]
+ \frametitle{Theorem Provers}
+ \large
+
+ \begin{itemize}
+ \item We found a mistake in a refereed paper by Harper \& Pfenning
+ \item I also found a mistake in my PhD thesis\bigskip
+
+ \item scratching on the surface of an completely ``alien'' subject
+ to us --- we were able to make progress
+ \item a string algorithm about suffix sorting (appeared at ICALP 2005)\smallskip\\
+ \small no implementation exists, claim: ``we are the best'';
+ we found an error the {\bf old-fashioned way}; now we need to verify our fix :(
+ \end{itemize}
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
+ \frametitle{State of the Art}
+ \large
+
+ theorem provers are bad with:
+
+ \begin{itemize}
+ \item real number arithmetic (Big-O stuff)
+ \item C-programs
+ \end{itemize}\bigskip
+
+ what others(we) are working on:
+
+ \begin{itemize}
+ \item write your programs inside your theorem prover, verify it,
+ compile it to efficient machine code (compilation is verified)
+ \end{itemize}
+
+
+ \end{frame}}
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+
+text_raw {*
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \mode<presentation>{
+ \begin{frame}[c]
\frametitle{Questions?}
\begin{itemize} \large
- \item Thank you for listening!
+ \item Thank you for the invitation and for listening!
\end{itemize}
\end{frame}}
