1 (*<*)

     1 (*<*)

     2 theory Paper

     2 theory Paper

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

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

     4 begin

     4 begin

     5 

     5 

    19 

     9 

    20 notation (latex output)

    10 notation (latex output)

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

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

    22   vt ("valid'_state") and

    12   vt ("valid'_state") and

    23   runing ("running") and

    13   runing ("running") and

    36   cp ("cprec") and

    26   cp ("cprec") and

    37   holdents ("resources") and

    27   holdents ("resources") and

    38   original_priority ("priority") and

    28   original_priority ("priority") and

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

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

    40 

    30 

    44 (*>*)

    32 (*>*)

    45 

    33 

    46 section {* Introduction *}

    34 section {* Introduction *}

    47 

    35 

    48 text {*

    36 text {*

    94   implemented. This includes VxWorks (a proprietary real-time OS used

    82   implemented. This includes VxWorks (a proprietary real-time OS used

    95   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's

    83   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's

    96   ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for

    84   ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for

    97   example in libraries for FreeBSD, Solaris and Linux. 

    85   example in libraries for FreeBSD, Solaris and Linux. 

    98 

    86 

   105   PIP. For instance, PIP cannot prevent deadlocks when lock

    96   PIP. For instance, PIP cannot prevent deadlocks when lock

   106   dependencies are circular, and also blocking times can be

    97   dependencies are circular, and also blocking times can be

   107   substantial (more than just the duration of a critical section).

    98   substantial (more than just the duration of a critical section).

   108   Though, most criticism against PIP centres around unreliable

    99   Though, most criticism against PIP centres around unreliable

   109   implementations and PIP being too complicated and too inefficient.

   100   implementations and PIP being too complicated and too inefficient.

   158   behaviour for $L$ is to switch to the highest remaining priority of

   149   behaviour for $L$ is to switch to the highest remaining priority of

   159   the threads that it blocks. The advantage of formalising the

   150   the threads that it blocks. The advantage of formalising the

   160   correctness of a high-level specification of PIP in a theorem prover

   151   correctness of a high-level specification of PIP in a theorem prover

   161   is that such issues clearly show up and cannot be overlooked as in

   152   is that such issues clearly show up and cannot be overlooked as in

   162   informal reasoning (since we have to analyse all possible behaviours

   153   informal reasoning (since we have to analyse all possible behaviours

   164 

   158 

   165   \noindent

   159   \noindent

   166   {\bf Contributions:} There have been earlier formal investigations

   160   {\bf Contributions:} There have been earlier formal investigations

   167   into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model

   161   into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model

   168   checking techniques. This paper presents a formalised and

   162   checking techniques. This paper presents a formalised and

   333   \end{isabelle}

   327   \end{isabelle}

   334 

   328 

   335   \noindent

   329   \noindent

   336   If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:

   330   If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:

   337 

   331 

   339   \begin{center}

   333   \begin{center}

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

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

   341   \begin{tikzpicture}[scale=1]

   335   \begin{tikzpicture}[scale=1]

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

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

   343 

   337 

   358 

   352 

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

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

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

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

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

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

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

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

   395 

   389 

   396   \noindent

   390   \noindent

   397   This definition needs to account for all threads that wait for a thread to

   391   This definition needs to account for all threads that wait for a thread to

   398   release a resource. This means we need to include threads that transitively

   392   release a resource. This means we need to include threads that transitively

   399   wait for a resource being released (in the picture above this means the dependants

   393   wait for a resource being released (in the picture above this means the dependants

   404   in a RAG, then clearly

   398   in a RAG, then clearly

   405   we have a deadlock. Therefore when a thread requests a resource,

   399   we have a deadlock. Therefore when a thread requests a resource,

   406   we must ensure that the resulting RAG is not circular. In practice, the 

   400   we must ensure that the resulting RAG is not circular. In practice, the 

   407   programmer has to ensure this.

   401   programmer has to ensure this.

   408 

   402 

   636   @{thm[mode=Rule] thread_V[where thread=th]}

   630   @{thm[mode=Rule] thread_V[where thread=th]}

   637   \end{center}

   631   \end{center}

   638 

   632 

   639   \noindent

   633   \noindent

   640   Note, however, that apart from the circularity condition, we do not make any 

   634   Note, however, that apart from the circularity condition, we do not make any 

   642   other. In our model it is possible that critical sections overlap. This is in 

   636   other. In our model it is possible that critical sections overlap. This is in 

   643   contrast to Sha et al \cite{Sha90} who require that critical sections are 

   637   contrast to Sha et al \cite{Sha90} who require that critical sections are 

   644   properly nested.

   638   properly nested.

   645 

   639 

   646   A valid state of PIP can then be conveniently be defined as follows:

   640   A valid state of PIP can then be conveniently be defined as follows:

   801   The second property is by induction of @{term vt}. The next three

   795   The second property is by induction of @{term vt}. The next three

   802   properties are 

   796   properties are 

   803 

   797 

   804   \begin{isabelle}\ \ \ \ \ %%%

   798   \begin{isabelle}\ \ \ \ \ %%%

   805   \begin{tabular}{@ {}l}

   799   \begin{tabular}{@ {}l}

   809   \end{tabular}

   803   \end{tabular}

   810   \end{isabelle}

   804   \end{isabelle}

   811 

   805 

   812   \noindent

   806   \noindent

   813   The first property states that every waiting thread can only wait for a single

   807   The first property states that every waiting thread can only wait for a single

   902   %The following lemmas show how every node in RAG can be chased to ready threads:

   896   %The following lemmas show how every node in RAG can be chased to ready threads:

   903   %\begin{enumerate}

   897   %\begin{enumerate}

   904   %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):

   898   %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):

   905   %  @   {thm [display] chain_building[rule_format]}

   899   %  @   {thm [display] chain_building[rule_format]}

   906   %\item The ready thread chased to is unique (@{text "dchain_unique"}):

   900   %\item The ready thread chased to is unique (@{text "dchain_unique"}):

   908   %\end{enumerate}

   902   %\end{enumerate}

   909 

   903 

   910   %Some deeper results about the system:

   904   %Some deeper results about the system:

   911   %\begin{enumerate}

   905   %\begin{enumerate}

   912   %\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):

   906   %\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):

  1074   @{thm[mode=IfThen] eq_cp}

  1068   @{thm[mode=IfThen] eq_cp}

  1075   \end{tabular}

  1069   \end{tabular}

  1076   \end{isabelle}

  1070   \end{isabelle}

  1077 

  1071 

  1078   \noindent

  1072   \noindent

  1080   current precedences of the other threads. The current precedence of the created

  1074   current precedences of the other threads. The current precedence of the created

  1081   thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.

  1075   thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.

  1082   \smallskip

  1076   \smallskip

  1083   *}

  1077   *}

  1084 (*<*)

  1078 (*<*)

  1451   the proof of Sha et al.: they require that critical sections nest properly, 

  1445   the proof of Sha et al.: they require that critical sections nest properly, 

  1452   whereas our scheduler allows critical sections to overlap. 

  1446   whereas our scheduler allows critical sections to overlap. 

  1453 

  1447 

  1454   PIP is a scheduling algorithm for single-processor systems. We are

  1448   PIP is a scheduling algorithm for single-processor systems. We are

  1455   now living in a multi-processor world. Priority Inversion certainly

  1449   now living in a multi-processor world. Priority Inversion certainly

  1457   However, there is very little ``foundational''

  1451   However, there is very little ``foundational''

  1458   work about PIP-algorithms on multi-processor systems.  We are not

  1452   work about PIP-algorithms on multi-processor systems.  We are not

  1459   aware of any correctness proofs, not even informal ones. There is an

  1453   aware of any correctness proofs, not even informal ones. There is an

  1460   implementation of a PIP-algorithm for multi-processors as part of the

  1454   implementation of a PIP-algorithm for multi-processors as part of the

  1461   ``real-time'' effort in Linux, including an informal description of the implemented scheduling

  1455   ``real-time'' effort in Linux, including an informal description of the implemented scheduling