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}{Nanjing, P.R. China, 1 August 2012}

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

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

    44   \mode<presentation>{

    45   \begin{frame}

    46   \frametitle{%

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

    48   \\[-3mm]

    49   \Large Priority Inheritance Protocol \\[-3mm] 

    50   \Large Proved Correct \\[0mm]

    51   \end{tabular}}

    52   

    53   \begin{center}

    54   \small Xingyuan Zhang \\

    55   \small \mbox{PLA University of Science and Technology} \\

    56   \small \mbox{Nanjing, China}

    57   \end{center}

    58 

    59   \begin{center}

    60   \small joint work with \\

    61   Christian Urban \\

    62   Kings College, University of London, U.K.\\

    63   Chunhan Wu \\

    64   My Ph.D. student now working for Christian\\

    65   \end{center}

    66 

    67   \end{frame}}

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

    69 *}

    70 

    71 text_raw {*

    72   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    73   \mode<presentation>{

    74   \begin{frame}[c]

    75   \frametitle{\large Prioirty Inheritance Protocol (PIP)}

    76   \large

    77 

    78   \begin{itemize} 

    79   \item Widely used in Real-Time OSs \pause

    80   \item One solution of \textcolor{red}{`Priority Inversion'} \pause

    81   \item A flawed manual correctness proof (1990)\pause

    82         \begin{itemize} \large

    83           \item {Notations with no precise definition}

    84           \item {Resorts to intuitions}

    85         \end{itemize} \pause

    86   \item Formal treatments using model-checking \pause

    87         \begin{itemize} \large

    88           \item {Applicable to small size system models}

    89           \item { Unhelpful for human understanding } 

    90         \end{itemize} \pause

    91   \item Verification of PCP in PVS (2000)\pause

    92         \begin{itemize} \large

    93            \item {A related protocol}

    94            \item {Priority Ceiling Protocol}

    95         \end{itemize}

    96   \end{itemize}

    97 

    98   \end{frame}}

    99   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   100 

   101 *}

   102 

   103 text_raw {*

   104   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   105   \mode<presentation>{

   106   \begin{frame}[c]

   107   \frametitle{Our Motivation}

   108   \large

   109 

   110   \begin{itemize}

   111   \item Undergraduate OS course in our university \pause

   112         \begin{itemize}

   113            \item {\large Experiments using instrutional OSs }

   114            \item {\large PINTOS (Stanford) is chosen }

   115            \item {\large Core project: Implementing PIP in it}

   116         \end{itemize} \pause

   117   \item Understanding is crucial for the implemention \pause

   118   \item Existing literature of little help \pause

   119   \item Some mention the complication

   120   \end{itemize}

   121 

   122   \end{frame}}

   123   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   124 

   125 *}

   126 

   127 

   128 text_raw {*

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

   130   \mode<presentation>{

   131   \begin{frame}[c]

   132   \frametitle{\mbox{Some excerpts}}

   133   

   134   \begin{quote}

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

   136   Implementations are either incomplete (and unreliable) 

   137   or surprisingly complex and intrusive.''

   138   \end{quote}\medskip

   139 

   140   \pause

   141 

   142   \begin{quote}

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

   144   PIP implementation is a nightmare: extremely heavy weight, 

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

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

   147   interruptions of wait operations.''

   148   \end{quote}

   149 

   150   \end{frame}}

   151   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   152 *}

   153 

   154 

   155 text_raw {*

   156   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   157   \mode<presentation>{

   158   \begin{frame}[c]

   159   \frametitle{Our Aims}

   160   \large

   161 

   162   \begin{itemize}

   163   \item Formal specification at appropriate abstract level,

   164         convenient for:

   165   \begin{itemize} \large

   166     \item Constructing interactive proofs

   167     \item Clarifying the underlying ideas

   168   \end{itemize} \pause

   169   \item Theorems usable to guide implementation, critical point:

   170     \begin{itemize} \large

   171       \item Understanding the relationship with real OS code \pause

   172       \item Not yet formalized

   173     \end{itemize}

   174   \end{itemize}

   175 

   176   \end{frame}}

   177   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   178 

   179 *}

   180 

   181 

   182 

   183 

   184 text_raw {*

   185   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   186   \mode<presentation>{

   187   \begin{frame}[c]

   188   \frametitle{Real-Time OSes}

   189   \large

   190 

   191   \begin{itemize}

   192   \item Purpose: gurantee the most urgent task to be processed in time

   193   \item Processes have priorities\\

   194   \item Resources can be locked and unlocked

   195   \end{itemize}

   196 

   197   \end{frame}}

   198   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   199 

   200 *}

   201 

   202 

   203 text_raw {*

   204   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   205   \mode<presentation>{

   206   \begin{frame}[c]

   207   \frametitle{Problem}

   208   \Large

   209 

   210   \begin{center}

   211   \begin{tabular}{l}

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

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

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

   215   \end{tabular}

   216   \end{center}

   217 

   218   \onslide<3->{

   219   \begin{itemize}

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

   221   \item<4> avoid indefinite priority inversion

   222   \end{itemize}}

   223 

   224   \end{frame}}

   225   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   226 

   227 *}

   228 

   229 

   230 text_raw {*

   231   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   232   \mode<presentation>{

   233   \begin{frame}[c]

   234   \frametitle{Priority Inversion}

   235 

   236   \begin{center}

   237   \includegraphics[scale=0.4]{PriorityInversion.png}

   238   \end{center}

   239 

   240   \end{frame}}

   241   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   242 

   243 *}

   244 

   245 

   246 text_raw {*

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

   248   \mode<presentation>{

   249   \begin{frame}[c]

   250   \frametitle{Mars Pathfinder Mission 1997}

   251   \Large

   252 

   253   \begin{center}

   254   \includegraphics[scale=0.2]{marspath1.png}

   255   \includegraphics[scale=0.22]{marspath3.png}

   256   \includegraphics[scale=0.4]{marsrover.png}

   257   \end{center}

   258 

   259   \end{frame}}

   260   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   261 *}

   262 

   263 text_raw {*

   264   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   265   \mode<presentation>{

   266   \begin{frame}[c]

   267   \frametitle{Solution}

   268   \Large

   269 

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

   271 

   272   \begin{center}

   273   \begin{tabular}{l}

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

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

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

   277   {\normalsize (temporarily raise its priority)}

   278   \end{tabular}

   279   \end{center}

   280 

   281   \end{frame}}

   282   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   283 *}

   284 

   285 

   286 

   287 

   288 text_raw {*

   289   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   290   \mode<presentation>{

   291   \begin{frame}[c]

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

   293   \Large

   294 

   295   \begin{itemize}

   296   \item a paper$^\star$ 

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

   298   \end{itemize}

   299 

   300   \normalsize

   301   \begin{quote}

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

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

   304   priority level''.

   305   \end{quote}\bigskip

   306 

   307   \small

   308   $^\star$ in IEEE Transactions on Computers

   309   \end{frame}}

   310   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   311 *}

   312 

   313 text_raw {*

   314   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   315   \mode<presentation>{

   316   \begin{frame}[c]

   317   \frametitle{}

   318   \Large

   319 

   320   \begin{center}

   321   \begin{tabular}{l}

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

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

   324   \alert{L}ow-priority process

   325   \end{tabular}

   326   \end{center}

   327 

   328   \onslide<2->{

   329   \begin{itemize}

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

   331   \end{itemize}}

   332 

   333   \end{frame}}

   334   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   335 *}

   336 

   337 

   338 text_raw {*

   339   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   340   \mode<presentation>{

   341   \begin{frame}[c]

   342   \frametitle{Event Abstraction}

   343 

   344   \begin{itemize}\large

   345      \item Use Inductive Approach of L. Paulson \pause

   346      \item System is event-driven \pause

   347      \item A \alert{state} is a list of events 

   348   \end{itemize}

   349 

   350   \pause

   351 

   352   \begin{center}

   353   \includegraphics[scale=0.4]{EventAbstract.png}

   354   \end{center}

   355 

   356   \end{frame}}

   357   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   358 

   359 *}

   360 

   361 text_raw {*

   362   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   363   \mode<presentation>{

   364   \begin{frame}[c]

   365   \frametitle{Events}

   366   \Large

   367 

   368   \begin{center}

   369   \begin{tabular}{l}

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

   371   Exit \textcolor{gray}{thread}\\

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

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

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

   375   \end{tabular}

   376   \end{center}\medskip

   377 

   378   \end{frame}}

   379   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   380 *}

   381 

   382 text_raw {*

   383   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   384   \mode<presentation>{

   385   \begin{frame}[c]

   386   \frametitle{Precedences}

   387   \large

   388 

   389   \begin{center}

   390   \begin{tabular}{l}

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

   392   \end{tabular}

   393   \end{center}

   394 

   395   

   396 

   397   \end{frame}}

   398   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   399 *}

   400 

   401 

   402 text_raw {*

   403   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   404   \mode<presentation>{

   405   \begin{frame}[c]

   406   \frametitle{RAGs}

   407 

   408 \begin{center}

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

   410   \begin{tikzpicture}[scale=1]

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

   412 

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

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

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

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

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

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

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

   420 

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

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

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

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

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

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

   427   \end{tikzpicture}

   428   \end{center}\bigskip

   429 

   430   \begin{center}

   431   \begin{minipage}{0.8\linewidth}

   432   \raggedleft

   433   @{thm cs_depend_def}

   434   \end{minipage}

   435   \end{center}\pause

   436 

   437   

   438 

   439   \end{frame}}

   440   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   441 

   442 *}

   443 

   444 text_raw {*

   445   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   446   \mode<presentation>{

   447   \begin{frame}[c]

   448   \frametitle{Good Next Events}

   449   %%\large

   450 

   451   \begin{center}

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

   453 

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

   455 

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

   457   \end{center}

   458 

   459   

   460 

   461   \end{frame}}

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

   463 *}

   464 

   465 text_raw {*

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

   467   \mode<presentation>{

   468   \begin{frame}[c]

   469   \frametitle{Good Next Events}

   470   %%\large

   471 

   472   \begin{center}

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

   474   

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

   476   \end{center}

   477 

   478   

   479 

   480   \end{frame}}

   481   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   482 *}

   483 (*<*)

   484 context extend_highest_gen

   485 begin

   486 (*>*)

   487 text_raw {*

   488   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   489   \mode<presentation>{

   490   \begin{frame}[c]

   491   \frametitle{\mbox{\large Theorem: ``No indefinite priority inversion''}}

   492 

   493   \pause

   494 

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

   496   @{text "s"}: \pause

   497   \begin{center}

   498   \textcolor{red}{@{thm highest})}

   499   \end{center}

   500   \pause

   501   and @{text "th"} is blocked by a thread @{text "th'"} in 

   502   a future state @{text "s'"} (with @{text "s' = t@s"}): \pause

   503   \begin{center}

   504   \textcolor{red}{@{text "th' \<in> running (t@s)"} and @{text "th' \<noteq> th"}} \pause

   505   \end{center}

   506   \fbox{ \hspace{1em} \pause

   507   \begin{minipage}{0.95\textwidth}

   508   \begin{itemize}

   509   \item @{text "th'"} did not hold or wait for a resource in s:

   510   \begin{center}

   511   \textcolor{red}{@{text "\<not>detached s th'"}}  

   512   \end{center} \pause

   513   \item @{text "th'"} is running with the precedence of @{text "th"}:

   514   \begin{center}

   515   \textcolor{red}{@{text "cp (t@s) th' = preced th s"}} 

   516   \end{center} 

   517   \end{itemize}

   518   \end{minipage}}

   519   \pause

   520   \small

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

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

   523 

   524   \end{frame}}

   525   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   526 *}

   527 

   528 text_raw {*

   529   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   530   \mode<presentation>{

   531   \begin{frame}[t]

   532   \frametitle{Implementation}

   533   

   534   s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip

   535 

   536   When @{text "e"} = \alert{Create th prio}, \alert{Exit th} 

   537   

   538   \begin{itemize}

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

   540   \item No precedence needs to be recomputed

   541   \end{itemize}

   542 

   543   \end{frame}}

   544   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   545 *}

   546 

   547 text_raw {*

   548   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   549   \mode<presentation>{

   550   \begin{frame}[t]

   551   \frametitle{Implementation}

   552 

   553   s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip

   554   

   555 

   556   When @{text "e"} = \alert{Set th prio}

   557   

   558   \begin{itemize}

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

   560   \item No precedence needs to be recomputed

   561   \end{itemize}

   562 

   563   \end{frame}}

   564   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   565 *}

   566 

   567 text_raw {*

   568   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   569   \mode<presentation>{

   570   \begin{frame}[t]

   571   \frametitle{Implementation}

   572 

   573   s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip

   574 

   575   When @{text "e"} = \alert{Unlock th cs} where there is a thread to take over

   576   

   577   \begin{itemize}

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

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

   580   \end{itemize}\bigskip

   581 

   582   \pause

   583 

   584   When @{text "e"} =  \alert{Unlock th cs} where no thread takes over

   585   

   586   \begin{itemize}

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

   588   \item no recalculation of precedences

   589   \end{itemize}

   590 

   591 

   592   \end{frame}}

   593   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   594 *}

   595 

   596 text_raw {*

   597   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   598   \mode<presentation>{

   599   \begin{frame}[t]

   600   \frametitle{Implementation}

   601 

   602   s $=$ current state; @{text "s'"} $=$ next state $=$ @{text "e#s"}\bigskip\bigskip

   603 

   604   When @{text "e"} = \alert{Lock th cs} where cs is not locked

   605   

   606   \begin{itemize}

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

   608   \item no recalculation of precedences

   609   \end{itemize}\bigskip

   610 

   611   \pause

   612 

   613   When @{text "e"} = \alert{Lock th cs} where cs is locked

   614   

   615   \begin{itemize}

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

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

   618   \end{itemize}

   619 

   620 

   621   \end{frame}}

   622   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   623 *}

   624 

   625 

   626 text_raw {*

   627   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   628   \mode<presentation>{

   629   \begin{frame}[c]

   630   \frametitle{Conclusion}

   631   

   632   \begin{itemize} \large

   633   \item Aims fulfilled \medskip \pause

   634   \item Alternative way \pause

   635        \begin{itemize} 

   636            \item using Isabelle/HOL in OS code development \medskip

   637            \item through the Inductive Approach

   638        \end{itemize} \pause

   639   \item Future research \pause

   640        \begin{itemize}

   641            \item scheduler in RT-Linux\medskip

   642            \item multiprocessor case\medskip

   643            \item other ``nails'' ? (networks, \ldots) \medskip \pause

   644            \item Refinement to real code and relation between implementations

   645         \end{itemize}

   646   \end{itemize}

   647   \end{frame}}

   648   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   649 *}

   650 

   651 text_raw {*

   652   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   653   \mode<presentation>{

   654   \begin{frame}[c]

   655   \frametitle{Questions?}

   656   

   657   \begin{itemize} \large

   658   \item Thank you for listening!

   659   \end{itemize}

   660   

   661   \end{frame}}

   662   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   663 *}

   664 

   665 

   666 (*<*)

   667 end

   668 end

   669 (*>*)