# HG changeset patch # User Christian Urban # Date 1355174842 0 # Node ID 0f2d4b78f839b9f649faf99fccd7c5207eefa417 # Parent 9d667d545e32bd057d8a532b81793d627ba634d0 updated diff -r 9d667d545e32 -r 0f2d4b78f839 IsaMakefile --- a/IsaMakefile Thu Dec 06 16:30:57 2012 +0000 +++ b/IsaMakefile Mon Dec 10 21:27:22 2012 +0000 @@ -24,7 +24,7 @@ slides1: session1 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated/root.beamer.pdf Slides/slides.pdf + cp Slides/generated/root.beamer.pdf slides1.pdf ## Slides @@ -36,7 +36,7 @@ slides2: session2 rm -f Slides/generated/*.aux # otherwise latex will fall over cd Slides/generated ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex - cp Slides/generated/root.beamer.pdf Slides/slides.pdf + cp Slides/generated/root.beamer.pdf slides2.pdf # main files diff -r 9d667d545e32 -r 0f2d4b78f839 Slides/Slides2.thy --- 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{ @@ -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{ \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{ + \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{ + \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{ \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{ \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{ - \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{ - \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{ - \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 "\"} \alert{H $<$ L} - \item<4> avoid indefinite priority inversion + \item \alert{priority inversion}\\ \hspace{2cm}@{text "\"} 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{ - \begin{frame}[c] - \frametitle{Priority Inversion} - - \begin{center} - \includegraphics[scale=0.4]{PriorityInversion.png} - \end{center} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode{ \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{ \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{ \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{ - \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{ \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{ \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{ + \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{ + \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{ \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{ \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{ + \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{ + \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{ \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{ - \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' \ running (t@s)"} and @{text "th' \ 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 "\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{ - \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{ - \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{ \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)} \ {(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{ \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 \ {(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{ \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{ + \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{ \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{ + \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{ + \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}} diff -r 9d667d545e32 -r 0f2d4b78f839 Slides/document/beamerthemeplaincu.sty --- a/Slides/document/beamerthemeplaincu.sty Thu Dec 06 16:30:57 2012 +0000 +++ b/Slides/document/beamerthemeplaincu.sty Mon Dec 10 21:27:22 2012 +0000 @@ -1,4 +1,4 @@ -\ProvidesPackage{beamerthemeplaincu}[2003/11/07 ver 0.93] +%%\Providespackage{beamerthemeplainculight}[2003/11/07 ver 0.93] \NeedsTeXFormat{LaTeX2e}[1995/12/01] % Copyright 2003 by Till Tantau . @@ -6,7 +6,7 @@ % This program can be redistributed and/or modified under the terms % of the LaTeX Project Public License Distributed from CTAN % archives in directory macros/latex/base/lppl.txt. - + \newcommand{\slidecaption}{} \mode @@ -43,35 +43,10 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% % Title page -%\usetitlepagetemplate{ -% \vbox{} -% \vfill -% \begin{centering} -% \Large\structure{\textrm{\textit{{\inserttitle}}}} -% \vskip1em\par -% \normalsize\insertauthor\vskip1em\par -% {\scriptsize\insertinstitute\par}\par\vskip1em -% \insertdate\par\vskip1.5em -% \inserttitlegraphic -% \end{centering} -% \vfill -% } - - % Part page -%\usepartpagetemplate{ -% \begin{centering} -% \Large\structure{\textrm{\textit{\partname~\@Roman\c@part}}} -% \vskip1em\par -% \textrm{\textit{\insertpart}}\par -% \end{centering} -% } - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Frametitles -\setbeamerfont{frametitle}{size={\huge}} +\setbeamerfont{frametitle}{size={\LARGE}} \setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}} -\setbeamercolor{frametitle}{fg=gray,bg=white} +\setbeamercolor{frametitle}{fg=ProcessBlue,bg=white} \setbeamertemplate{frametitle}{% \vskip 2mm % distance from the top margin diff -r 9d667d545e32 -r 0f2d4b78f839 Slides/document/isabelle.png Binary file Slides/document/isabelle.png has changed diff -r 9d667d545e32 -r 0f2d4b78f839 Slides/document/root.beamer.tex --- a/Slides/document/root.beamer.tex Thu Dec 06 16:30:57 2012 +0000 +++ b/Slides/document/root.beamer.tex Mon Dec 10 21:27:22 2012 +0000 @@ -1,4 +1,4 @@ -\documentclass[14pt,t]{beamer} +\documentclass[dvipsnames, 14pt,t]{beamer} %%%\usepackage{pstricks} \input{root.tex}