diff -r 2c56b20032a7 -r 0679a84b11ad prio/Slides/Slides1.thy --- a/prio/Slides/Slides1.thy Mon Dec 03 08:16:58 2012 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,669 +0,0 @@ -(*<*) -theory Slides1 -imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar" -begin - -notation (latex output) - set ("_") and - Cons ("_::/_" [66,65] 65) - -ML {* - open Printer; - show_question_marks_default := false; - *} - -notation (latex output) - Cons ("_::_" [78,77] 73) and - vt ("valid'_state") and - runing ("running") and - birthtime ("last'_set") and - If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and - Prc ("'(_, _')") and - holding ("holds") and - waiting ("waits") and - Th ("T") and - Cs ("C") and - readys ("ready") and - depend ("RAG") and - preced ("prec") and - cpreced ("cprec") and - dependents ("dependants") and - cp ("cprec") and - holdents ("resources") and - original_priority ("priority") and - DUMMY ("\<^raw:\mbox{$\_\!\_$}>") - -(*>*) - - - -text_raw {* - \renewcommand{\slidecaption}{Nanjing, P.R. China, 1 August 2012} - \newcommand{\bl}[1]{#1} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame} - \frametitle{% - \begin{tabular}{@ {}c@ {}} - \\[-3mm] - \Large Priority Inheritance Protocol \\[-3mm] - \Large Proved Correct \\[0mm] - \end{tabular}} - - \begin{center} - \small Xingyuan Zhang \\ - \small \mbox{PLA University of Science and Technology} \\ - \small \mbox{Nanjing, China} - \end{center} - - \begin{center} - \small joint work with \\ - Christian Urban \\ - Kings College, University of London, U.K.\\ - Chunhan Wu \\ - My Ph.D. student now working for Christian\\ - \end{center} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{\large Prioirty Inheritance Protocol (PIP)} - \large - - \begin{itemize} - \item Widely used in Real-Time OSs \pause - \item One solution of \textcolor{red}{`Priority Inversion'} \pause - \item A flawed manual correctness proof (1990)\pause - \begin{itemize} \large - \item {Notations with no precise definition} - \item {Resorts to intuitions} - \end{itemize} \pause - \item Formal treatments using model-checking \pause - \begin{itemize} \large - \item {Applicable to small size system models} - \item { Unhelpful for human understanding } - \end{itemize} \pause - \item Verification of PCP in PVS (2000)\pause - \begin{itemize} \large - \item {A related protocol} - \item {Priority Ceiling Protocol} - \end{itemize} - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Our Motivation} - \large - - \begin{itemize} - \item Undergraduate OS course in our university \pause - \begin{itemize} - \item {\large Experiments using instrutional OSs } - \item {\large PINTOS (Stanford) is chosen } - \item {\large Core project: Implementing PIP in it} - \end{itemize} \pause - \item Understanding is crucial for the implemention \pause - \item Existing literature of little help \pause - \item Some mention the complication - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \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} - \Large - - \begin{center} - \begin{tabular}{l} - \alert{H}igh-priority process\\[4mm] - \onslide<2->{\alert{M}edium-priority process}\\[4mm] - \alert{L}ow-priority process\\[4mm] - \end{tabular} - \end{center} - - \onslide<3->{ - \begin{itemize} - \item \alert{Priority Inversion} @{text "\"} \alert{H $<$ L} - \item<4> avoid indefinite priority inversion - \end{itemize}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - - -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 - - \begin{center} - \includegraphics[scale=0.2]{marspath1.png} - \includegraphics[scale=0.22]{marspath3.png} - \includegraphics[scale=0.4]{marsrover.png} - \end{center} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Solution} - \Large - - \alert{Priority Inheritance Protocol (PIP):} - - \begin{center} - \begin{tabular}{l} - \alert{H}igh-priority process\\[4mm] - \textcolor{gray}{Medium-priority process}\\[4mm] - \alert{L}ow-priority process\\[21mm] - {\normalsize (temporarily raise its priority)} - \end{tabular} - \end{center} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{A Correctness ``Proof'' in 1990} - \Large - - \begin{itemize} - \item a paper$^\star$ - in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm] - \end{itemize} - - \normalsize - \begin{quote} - \ldots{}after the thread (whose priority has been raised) completes its - critical section and releases the lock, it ``returns to its original - priority level''. - \end{quote}\bigskip - - \small - $^\star$ in IEEE Transactions on Computers - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{} - \Large - - \begin{center} - \begin{tabular}{l} - \alert{H}igh-priority process 1\\[2mm] - \alert{H}igh-priority process 2\\[8mm] - \alert{L}ow-priority process - \end{tabular} - \end{center} - - \onslide<2->{ - \begin{itemize} - \item Solution: \\Return to highest \alert{remaining} priority - \end{itemize}} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \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} - \Large - - \begin{center} - \begin{tabular}{l} - Create \textcolor{gray}{thread priority}\\ - Exit \textcolor{gray}{thread}\\ - Set \textcolor{gray}{thread priority}\\ - Lock \textcolor{gray}{thread cs}\\ - Unlock \textcolor{gray}{thread cs}\\ - \end{tabular} - \end{center}\medskip - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Precedences} - \large - - \begin{center} - \begin{tabular}{l} - @{thm preced_def[where thread="th"]} - \end{tabular} - \end{center} - - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{RAGs} - -\begin{center} - \newcommand{\fnt}{\fontsize{7}{8}\selectfont} - \begin{tikzpicture}[scale=1] - %%\draw[step=2mm] (-3,2) grid (1,-1); - - \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}}; - \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}}; - \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}}; - \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}}; - \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}}; - \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}}; - \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}}; - - \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B); - \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B); - \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B); - \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E); - \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (E1); - \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E); - \end{tikzpicture} - \end{center}\bigskip - - \begin{center} - \begin{minipage}{0.8\linewidth} - \raggedleft - @{thm cs_depend_def} - \end{minipage} - \end{center}\pause - - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Good Next Events} - %%\large - - \begin{center} - @{thm[mode=Rule] thread_create[where thread=th]}\bigskip - - @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip - - @{thm[mode=Rule] thread_set[where thread=th]} - \end{center} - - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Good Next Events} - %%\large - - \begin{center} - @{thm[mode=Rule] thread_P[where thread=th]}\bigskip - - @{thm[mode=Rule] thread_V[where thread=th]}\bigskip - \end{center} - - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} -(*<*) -context extend_highest_gen -begin -(*>*) -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \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 - \end{itemize} - - \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{Set th prio} - - \begin{itemize} - \item @{text "RAG s' = RAG s"} - \item No precedence needs to be recomputed - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \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 - \end{itemize}\bigskip - - \pause - - When @{text "e"} = \alert{Unlock th cs} where no thread takes over - - \begin{itemize} - \item @{text "RAG s' = RAG s - {(C cs, T th)}"} - \item no recalculation of precedences - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[t] - \frametitle{Implementation} - - s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip - - When @{text "e"} = \alert{Lock th cs} where cs is not locked - - \begin{itemize} - \item @{text "RAG s' = RAG s \ {(C cs, T th')}"} - \item no recalculation of precedences - \end{itemize}\bigskip - - \pause - - When @{text "e"} = \alert{Lock th cs} where cs is locked - - \begin{itemize} - \item @{text "RAG s' = RAG s - {(T th, C cs)}"} - \item we have to recalculate the precedence of the descendants - \end{itemize} - - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Conclusion} - - \begin{itemize} \large - \item Aims fulfilled \medskip \pause - \item Alternative way \pause - \begin{itemize} - \item using Isabelle/HOL in OS code development \medskip - \item through the Inductive Approach - \end{itemize} \pause - \item Future research \pause - \begin{itemize} - \item scheduler in RT-Linux\medskip - \item multiprocessor case\medskip - \item other ``nails'' ? (networks, \ldots) \medskip \pause - \item Refinement to real code and relation between implementations - \end{itemize} - \end{itemize} - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - -text_raw {* - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - \mode{ - \begin{frame}[c] - \frametitle{Questions?} - - \begin{itemize} \large - \item Thank you for listening! - \end{itemize} - - \end{frame}} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*} - - -(*<*) -end -end -(*>*) \ No newline at end of file