1 (*<*)

     2 theory Slides1

     3 imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 ML {*

    11   open Printer;

    12   show_question_marks_default := false;

    13   *}

    14 

    15 notation (latex output)

    16   Cons ("_::_" [78,77] 73) and

    17   vt ("valid'_state") and

    18   runing ("running") and

    19   birthtime ("last'_set") and

    20   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and

    21   Prc ("'(_, _')") and

    22   holding ("holds") and

    23   waiting ("waits") and

    24   Th ("T") and

    25   Cs ("C") and

    26   readys ("ready") and

    27   depend ("RAG") and 

    28   preced ("prec") and

    29   cpreced ("cprec") and

    30   dependents ("dependants") and

    31   cp ("cprec") and

    32   holdents ("resources") and

    33   original_priority ("priority") and

    34   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

    35 

    36 (*>*)

    37 

    38 

    39 

    40 text_raw {*

    41   \renewcommand{\slidecaption}{London, 28 June 2012}

    42   \newcommand{\bl}[1]{#1}                        

    43   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    44   \mode<presentation>{

    45   \begin{frame}

    46   \frametitle{%

    47   \begin{tabular}{@ {}c@ {}}

    48   \\[8mm]

    49   \Large A Provably Correct Implementation\\[-3mm] 

    50   \Large of the Priority Inheritance Protocol\\[0mm]

    51   \end{tabular}}

    52   

    53   \begin{center}

    54   \small Christian Urban\\

    55   \end{center}

    56 

    57   \begin{center}

    58   \small joint work with Xingyuan Zhang and Chunhan Wu\medskip \\

    59   \small \mbox{from the PLA University of Science and Technology in Nanjing}

    60   \end{center}

    61 

    62   \end{frame}}

    63   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    64 

    65 *}

    66 

    67 text_raw {*

    68   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    69   \mode<presentation>{

    70   \begin{frame}[c]

    71   \frametitle{Isabelle Theorem Prover}

    72   My background:

    73 

    74   \begin{itemize}

    75   \item mechanical reasoning about languages with binders (Nominal)\medskip

    76   \item Barendregt's variable convention can lead to \alert{false}\medskip

    77   \item found a bug in a proof by Bob Harper and Frank Pfenning (CMU) on

    78   LF (ACM TOCL, 2005)

    79   \end{itemize}

    80 

    81   \begin{textblock}{6}(6.5,12.5)

    82   \includegraphics[scale=0.28]{isabelle1.png}

    83   \end{textblock}

    84 

    85   \end{frame}}

    86   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    87 

    88 *}

    89 

    90 text_raw {*

    91   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    92   \mode<presentation>{

    93   \begin{frame}[c]

    94   \frametitle{Real-Time OSes}

    95   \large

    96 

    97   \begin{itemize}

    98   \item Processes have priorities\\[5mm]

    99   \item Resources can be locked and unlocked

   100   \end{itemize}

   101 

   102   \end{frame}}

   103   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   104 

   105 *}

   106 

   107 text_raw {*

   108   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   109   \mode<presentation>{

   110   \begin{frame}[c]

   111   \frametitle{Problem}

   112   \Large

   113 

   114   \begin{center}

   115   \begin{tabular}{l}

   116   \alert{H}igh-priority process\\[4mm]

   117   \onslide<2->{\alert{M}edium-priority process}\\[4mm]

   118   \alert{L}ow-priority process\\[4mm]

   119   \end{tabular}

   120   \end{center}

   121 

   122   \onslide<3->{

   123   \begin{itemize}

   124   \item \alert{Priority Inversion} @{text "\<equiv>"} \alert{H $<$ L}

   125   \item<4> avoid indefinite priority inversion

   126   \end{itemize}}

   127 

   128   \end{frame}}

   129   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   130 

   131 *}

   132 

   133 text_raw {*

   134   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   135   \mode<presentation>{

   136   \begin{frame}[c]

   137   \frametitle{Mars Pathfinder Mission 1997}

   138   \Large

   139 

   140   \begin{center}

   141   \includegraphics[scale=0.26]{pathfinder.jpg}

   142   \end{center}

   143 

   144   \end{frame}}

   145   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   146 *}

   147 

   148 text_raw {*

   149   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   150   \mode<presentation>{

   151   \begin{frame}[c]

   152   \frametitle{Solution}

   153   \Large

   154 

   155   \alert{Priority Inheritance Protocol (PIP):}

   156 

   157   \begin{center}

   158   \begin{tabular}{l}

   159   \alert{H}igh-priority process\\[4mm]

   160   \textcolor{gray}{Medium-priority process}\\[4mm]

   161   \alert{L}ow-priority process\\[21mm]

   162   {\normalsize (temporarily raise its priority)}

   163   \end{tabular}

   164   \end{center}

   165 

   166   \end{frame}}

   167   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   168 *}

   169 

   170 

   171 text_raw {*

   172   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   173   \mode<presentation>{

   174   \begin{frame}[c]

   175   \frametitle{\mbox{}}

   176   

   177   \begin{quote}

   178   ``Priority inheritance is neither ef$\!$ficient nor reliable. 

   179   Implementations are either incomplete (and unreliable) 

   180   or surprisingly complex and intrusive.''

   181   \end{quote}\medskip

   182 

   183   \begin{quote}

   184   ``I observed in the kernel code (to my disgust), the Linux 

   185   PIP implementation is a nightmare: extremely heavy weight, 

   186   involving maintenance of a full wait-for graph, and requiring 

   187   updates for a range of events, including priority changes and 

   188   interruptions of wait operations.''

   189   \end{quote}

   190 

   191   \end{frame}}

   192   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   193 *}

   194 

   195 

   196 text_raw {*

   197   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   198   \mode<presentation>{

   199   \begin{frame}[c]

   200   \frametitle{A Correctness ``Proof'' in 1990}

   201   \Large

   202 

   203   \begin{itemize}

   204   \item a paper$^\star$ 

   205   in 1990 ``proved'' the correctness of an algorithm for PIP\\[5mm]

   206   \end{itemize}

   207 

   208   \normalsize

   209   \begin{quote}

   210   \ldots{}after the thread (whose priority has been raised) completes its 

   211   critical section and releases the lock, it ``returns to its original 

   212   priority level''.

   213   \end{quote}\bigskip

   214 

   215   \small

   216   $^\star$ in IEEE Transactions on Computers

   217   \end{frame}}

   218   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   219 *}

   220 

   221 text_raw {*

   222   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   223   \mode<presentation>{

   224   \begin{frame}[c]

   225   \frametitle{}

   226   \Large

   227 

   228   \begin{center}

   229   \begin{tabular}{l}

   230   \alert{H}igh-priority process 1\\[2mm]

   231   \alert{H}igh-priority process 2\\[8mm]

   232   \alert{L}ow-priority process

   233   \end{tabular}

   234   \end{center}

   235 

   236   \onslide<2->{

   237   \begin{itemize}

   238   \item Solution: \\Return to highest \alert{remaining} priority

   239   \end{itemize}}

   240 

   241   \end{frame}}

   242   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   243 *}

   244 

   245 

   246 text_raw {*

   247   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   248   \mode<presentation>{

   249   \begin{frame}[c]

   250   \frametitle{Events}

   251   \Large

   252 

   253   \begin{center}

   254   \begin{tabular}{l}

   255   Create \textcolor{gray}{thread priority}\\

   256   Exit \textcolor{gray}{thread}\\

   257   Set \textcolor{gray}{thread priority}\\

   258   Lock \textcolor{gray}{thread cs}\\

   259   Unlock \textcolor{gray}{thread cs}\\

   260   \end{tabular}

   261   \end{center}\pause\medskip

   262 

   263   \large

   264   A \alert{state} is a list of events (that happened so far).

   265 

   266   \end{frame}}

   267   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   268 *}

   269 

   270 text_raw {*

   271   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   272   \mode<presentation>{

   273   \begin{frame}[c]

   274   \frametitle{Precedences}

   275   \large

   276 

   277   \begin{center}

   278   \begin{tabular}{l}

   279   @{thm preced_def[where thread="th"]}

   280   \end{tabular}

   281   \end{center}

   282 

   283   

   284 

   285   \end{frame}}

   286   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   287 *}

   288 

   289 

   290 text_raw {*

   291   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   292   \mode<presentation>{

   293   \begin{frame}[c]

   294   \frametitle{RAGs}

   295 

   296 \begin{center}

   297   \newcommand{\fnt}{\fontsize{7}{8}\selectfont}

   298   \begin{tikzpicture}[scale=1]

   299   %%\draw[step=2mm] (-3,2) grid (1,-1);

   300 

   301   \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};

   302   \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};

   303   \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};

   304   \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};

   305   \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};

   306   \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};

   307   \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};

   308 

   309   \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);

   310   \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);

   311   \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);

   312   \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);

   313   \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);

   314   \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);

   315   \end{tikzpicture}

   316   \end{center}\bigskip

   317 

   318   \begin{center}

   319   \begin{minipage}{0.8\linewidth}

   320   \raggedleft

   321   @{thm cs_depend_def}

   322   \end{minipage}

   323   \end{center}\pause

   324 

   325   

   326 

   327   \end{frame}}

   328   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   329 

   330 *}

   331 

   332 text_raw {*

   333   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   334   \mode<presentation>{

   335   \begin{frame}[c]

   336   \frametitle{Good Next Events}

   337   %%\large

   338 

   339   \begin{center}

   340   @{thm[mode=Rule] thread_create[where thread=th]}\bigskip

   341 

   342   @{thm[mode=Rule] thread_exit[where thread=th]}\bigskip

   343 

   344   @{thm[mode=Rule] thread_set[where thread=th]}

   345   \end{center}

   346 

   347   

   348 

   349   \end{frame}}

   350   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   351 *}

   352 

   353 text_raw {*

   354   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   355   \mode<presentation>{

   356   \begin{frame}[c]

   357   \frametitle{Good Next Events}

   358   %%\large

   359 

   360   \begin{center}

   361   @{thm[mode=Rule] thread_P[where thread=th]}\bigskip

   362   

   363   @{thm[mode=Rule] thread_V[where thread=th]}\bigskip

   364   \end{center}

   365 

   366   

   367 

   368   \end{frame}}

   369   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   370 *}

   371 

   372 text_raw {*

   373   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   374   \mode<presentation>{

   375   \begin{frame}[c]

   376   \frametitle{Theorem}

   377   

   378   \textcolor{gray}{``No indefinite priority inversion''}\bigskip

   379 

   380   Theorem:$^\star$ If th is the thread with the highest precedence in state s,

   381   then in every future state @{text "s'"} in which th is still

   382   alive\smallskip

   383 

   384 

   385   \begin{itemize}

   386   \item th is blocked by a thread @{text "th'"} that was alive in s 

   387   \item @{text "th'"} held a resource in s, and

   388   \item @{text "th'"} is running with the precedence of th.\bigskip

   389   \end{itemize}

   390 

   391   \small

   392   $^\star$ modulo some further assumptions\bigskip\pause

   393 

   394   It does not matter which process gets a released lock.

   395 

   396   \end{frame}}

   397   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   398 *}

   399 

   400 text_raw {*

   401   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   402   \mode<presentation>{

   403   \begin{frame}[t]

   404   \frametitle{Implementation}

   405   

   406   s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip

   407 

   408   \alert{Create th prio}, \alert{Exit th} 

   409   

   410   \begin{itemize}

   411   \item @{text "RAG s' = RAG s"}

   412   \item precedences of descendants stay all the same

   413   \end{itemize}

   414 

   415   \end{frame}}

   416   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   417 *}

   418 

   419 text_raw {*

   420   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   421   \mode<presentation>{

   422   \begin{frame}[t]

   423   \frametitle{Implementation}

   424   

   425   s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip

   426 

   427   \alert{Set th prio}

   428   

   429   \begin{itemize}

   430   \item @{text "RAG s' = RAG s"}

   431   \item we have to recalculate the precedence of the direct descendants

   432   \end{itemize}

   433 

   434   \end{frame}}

   435   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   436 *}

   437 

   438 text_raw {*

   439   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   440   \mode<presentation>{

   441   \begin{frame}[t]

   442   \frametitle{Implementation}

   443   

   444   s $=$ current state; @{text "s'"} $=$ next state\bigskip

   445 

   446   \alert{Unlock th cs} where there is a thread to take over

   447   

   448   \begin{itemize}

   449   \item @{text "RAG s' = RAG s - {(C cs, T th), (T th', C cs)} \<union> {(C cs, T th')}"}

   450   \item we have to recalculate the precedence of the direct descendants

   451   \end{itemize}\bigskip

   452 

   453   \alert{Unlock th cs} where no thread takes over

   454   

   455   \begin{itemize}

   456   \item @{text "RAG s' = RAG s - {(C cs, T th)}"}

   457   \item no recalculation of precedences

   458   \end{itemize}

   459 

   460 

   461   \end{frame}}

   462   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   463 *}

   464 

   465 text_raw {*

   466   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   467   \mode<presentation>{

   468   \begin{frame}[t]

   469   \frametitle{Implementation}

   470   

   471   s $=$ current state; @{text "s'"} $=$ next state\bigskip\bigskip

   472 

   473   \alert{Lock th cs} where cs is not locked

   474   

   475   \begin{itemize}

   476   \item @{text "RAG s' = RAG s \<union> {(C cs, T th')}"}

   477   \item no recalculation of precedences

   478   \end{itemize}\bigskip

   479 

   480   \alert{Lock th cs} where cs is locked

   481   

   482   \begin{itemize}

   483   \item @{text "RAG s' = RAG s - {(T th, C cs)}"}

   484   \item we have to recalculate the precedence of the descendants

   485   \end{itemize}

   486 

   487 

   488   \end{frame}}

   489   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   490 *}

   491 

   492 text_raw {*

   493   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   494   \mode<presentation>{

   495   \begin{frame}[c]

   496   \frametitle{PINTOS}

   497 

   498   \begin{itemize}

   499   \item \ldots{}small operating system developed at Stanford for teaching;

   500   written in C\bigskip 

   501   \end{itemize}

   502   

   503   \begin{center}

   504   \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}

   505   \hline

   506   {\bf Event} & {\bf PINTOS function} \\

   507   \hline

   508   @{text Create} & @{text "thread_create"}\\

   509   @{text Exit}   & @{text "thread_exit"}\\

   510   @{text Set}    & @{text "thread_set_priority"}\\

   511   @{text Lock}   & @{text "lock_acquire"}\\

   512   @{text Unlock} & @{text "lock_release"}\\ 

   513   \hline

   514   \end{tabular}

   515   \end{center}

   516 

   517 

   518   \end{frame}}

   519   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   520 *}

   521 

   522 text_raw {*

   523   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   524   \mode<presentation>{

   525   \begin{frame}[c]

   526   \frametitle{Conclusion}

   527   

   528   \begin{itemize}

   529   \item surprised how pleasant the experience was\medskip

   530 

   531   \item no real specification existed for PIP\medskip

   532 

   533   \item general technique (a ``hammer''):\\[2mm]

   534   events, separation of good and bad configurations\medskip

   535 

   536   \item scheduler in RT-Linux\medskip

   537 

   538   \item multiprocessor case\medskip

   539 

   540   \item other ``nails'' ? (networks, \ldots)

   541   \end{itemize}

   542 

   543 

   544   \end{frame}}

   545   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   546 *}

   547 

   548 (*<*)

   549 end

   550 (*>*)