7 declare [[show_question_marks = false]]

     7 declare [[show_question_marks = false]]

     8 

     8 

     9 

     9 

    10 notation (latex output)

    10 notation (latex output)

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

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

    12   vt ("valid'_state") and

    13   vt ("valid'_state") and

    13   runing ("running") and

    14   runing ("running") and

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

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

    16   holding ("holds") and

    16   holding ("holds") and

    17   waiting ("waits") and

    17   waiting ("waits") and

    18   Th ("T") and

    18   Th ("T") and

    19   Cs ("C") and

    19   Cs ("C") and

    20   readys ("ready") and

    20   readys ("ready") and

    22   preced ("prec") and

    21   preced ("prec") and

    23   cpreced ("cprec") and

    23   cpreced ("cprec") and

    24   cp ("cprec") and

    24   cp ("cprec") and

    25   holdents ("resources") and

    25   holdents ("resources") and

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

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

    27  

    27  

    29 (*>*)

    28 (*>*)

    30 

    29 

    31 section {* Introduction *}

    30 section {* Introduction *}

    32 

    31 

    33 text {*

    32 text {*

   184   to the thread with the highest priority so that it terminates more

   183   to the thread with the highest priority so that it terminates more

   185   quickly.  We were also being able to generalise the scheduler of Sha

   184   quickly.  We were also being able to generalise the scheduler of Sha

   186   et al.~\cite{Sha90} to the practically relevant case where critical 

   185   et al.~\cite{Sha90} to the practically relevant case where critical 

   187   sections can overlap; see Figure~\ref{overlap} below for an example of 

   186   sections can overlap; see Figure~\ref{overlap} below for an example of 

   188   this restriction. In the existing literature there is no 

   187   this restriction. In the existing literature there is no 

   190 

   189 

   191   \begin{figure}

   190   \begin{figure}

   192   \begin{center}

   191   \begin{center}

   193   \begin{tikzpicture}[scale=1]

   192   \begin{tikzpicture}[scale=1]

   194   %%\draw[step=2mm] (0,0) grid (10,2);

   193   %%\draw[step=2mm] (0,0) grid (10,2);

   326   \begin{isabelle}\ \ \ \ \ %%%

   325   \begin{isabelle}\ \ \ \ \ %%%

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

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

   328   \end{isabelle}

   327   \end{isabelle}

   329 

   328 

   330   \noindent

   329   \noindent

   331   The point of precedences is to schedule threads not according to priorities (because what should

   338   The point of precedences is to schedule threads not according to priorities (because what should

   332   we do in case two threads have the same priority), but according to precedences. 

   339   we do in case two threads have the same priority), but according to precedences. 

   333   Precedences allow us to always discriminate between two threads with equal priority by 

   340   Precedences allow us to always discriminate between two threads with equal priority by 

   334   taking into account the time when the priority was last set. We order precedences so 

   341   taking into account the time when the priority was last set. We order precedences so 

   335   that threads with the same priority get a higher precedence if their priority has been 

   342   that threads with the same priority get a higher precedence if their priority has been 

   388   \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a 

   395   \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a 

   389   datatype for vertices). Given a waiting queue function, a RAG is defined 

   396   datatype for vertices). Given a waiting queue function, a RAG is defined 

   390   as the union of the sets of waiting and holding edges, namely

   397   as the union of the sets of waiting and holding edges, namely

   391 

   398 

   392   \begin{isabelle}\ \ \ \ \ %%%

   399   \begin{isabelle}\ \ \ \ \ %%%

   394   \end{isabelle}

   401   \end{isabelle}

   395 

   402 

   396 

   403 

   397   \begin{figure}[t]

   404   \begin{figure}[t]

   398   \begin{center}

   405   \begin{center}

   476   @{thm cpreced_def2}\hfill\numbered{cpreced}

   483   @{thm cpreced_def2}\hfill\numbered{cpreced}

   477   \end{isabelle}

   484   \end{isabelle}

   478 

   485 

   479   \noindent

   486   \noindent

   480   where the dependants of @{text th} are given by the waiting queue function.

   487   where the dependants of @{text th} are given by the waiting queue function.

   482   (for example when the thread is

   489   (for example when the thread is

   483   created), the point of the current precedence is to let the scheduler increase this

   490   created), the point of the current precedence is to let the scheduler increase this

   484   precedence, if needed according to PIP. Therefore the current precedence of @{text th} is

   491   precedence, if needed according to PIP. Therefore the current precedence of @{text th} is

   485   given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 

   492   given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 

   486   threads that are dependants of @{text th}. Since the notion @{term "dependants"} is

   493   threads that are dependants of @{text th}. Since the notion @{term "dependants"} is

   487   defined as the transitive closure of all dependent threads, we deal correctly with the 

   494   defined as the transitive closure of all dependent threads, we deal correctly with the 

   488   problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is

   495   problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is

   490   

   498   

   491   The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined

   499   The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined

   492   by recursion on the state (a list of events); this function returns a \emph{schedule state}, which 

   500   by recursion on the state (a list of events); this function returns a \emph{schedule state}, which 

   493   we represent as a record consisting of two

   501   we represent as a record consisting of two

   494   functions:

   502   functions:

   595   \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\

   603   \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\

   596   \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}

   604   \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}

   597   \end{tabular}

   605   \end{tabular}

   598   \end{isabelle}

   606   \end{isabelle}

   599 

   607 

   603 

   612 

   604   \begin{isabelle}\ \ \ \ \ %%%

   613   \begin{isabelle}\ \ \ \ \ %%%

   605   \begin{tabular}{@ {}rcl}

   614   \begin{tabular}{@ {}rcl}

   610   \end{tabular}

   620   \end{tabular}

   611   \end{isabelle}

   621   \end{isabelle}

   612 

   622 

   613   \noindent

   623   \noindent

   614   With these abbreviations in place we can introduce 

   624   With these abbreviations in place we can introduce 

   623   @{thm runing_def}

   633   @{thm runing_def}

   624   \end{tabular}

   634   \end{tabular}

   625   \end{isabelle}

   635   \end{isabelle}

   626 

   636 

   627   \noindent

   637   \noindent

   629   Note that in the initial state, that is where the list of events is empty, the set 

   639   Note that in the initial state, that is where the list of events is empty, the set 

   630   @{term threads} is empty and therefore there is neither a thread ready nor running.

   640   @{term threads} is empty and therefore there is neither a thread ready nor running.

   631   If there is one or more threads ready, then there can only be \emph{one} thread

   641   If there is one or more threads ready, then there can only be \emph{one} thread

   632   running, namely the one whose current precedence is equal to the maximum of all ready 

   642   running, namely the one whose current precedence is equal to the maximum of all ready 

   633   threads. We use sets to capture both possibilities.

   643   threads. We use sets to capture both possibilities.

   789   has the highest precedence of all alive threads in @{text s}. Furthermore the

   799   has the highest precedence of all alive threads in @{text s}. Furthermore the

   790   priority of @{text th} is @{text prio} (we need this in the next assumptions).

   800   priority of @{text th} is @{text prio} (we need this in the next assumptions).

   791   \begin{isabelle}\ \ \ \ \ %%%

   801   \begin{isabelle}\ \ \ \ \ %%%

   792   \begin{tabular}{l}

   802   \begin{tabular}{l}

   793   @{term "th \<in> threads s"}\\

   803   @{term "th \<in> threads s"}\\

   795   @{term "prec th s = (prio, DUMMY)"}

   805   @{term "prec th s = (prio, DUMMY)"}

   796   \end{tabular}

   806   \end{tabular}

   797   \end{isabelle}

   807   \end{isabelle}

   798   \end{quote}

   808   \end{quote}

   799   

   809   

   834   one resource---that means the thread was not \emph{detached} in @{text s}. 

   844   one resource---that means the thread was not \emph{detached} in @{text s}. 

   835   As we shall see shortly, that means there are only finitely 

   845   As we shall see shortly, that means there are only finitely 

   836   many threads that can block @{text th} in this way and then they 

   846   many threads that can block @{text th} in this way and then they 

   837   need to run with the same precedence as @{text th}.

   847   need to run with the same precedence as @{text th}.

   838 

   848 

   847   programs that contain for every looking request also a corresponding

   857   programs that contain for every looking request also a corresponding

   857   However, we are able to combine their two separate bounds into a

   867   However, we are able to combine their two separate bounds into a

   858   single theorem improving their bound.

   868   single theorem improving their bound.

   859 

   869 

   860   In what follows we will describe properties of PIP that allow us to prove 

   870   In what follows we will describe properties of PIP that allow us to prove 

   861   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 

   871   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 

   863 

   873 

   864   \begin{isabelle}\ \ \ \ \ %%%

   874   \begin{isabelle}\ \ \ \ \ %%%

   865   \begin{tabular}{@ {}l}

   875   \begin{tabular}{@ {}l}

   866   @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\

   876   @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\

   867   @{thm[mode=IfThen]  finite_threads}

   877   @{thm[mode=IfThen]  finite_threads}

   868   \end{tabular}

   878   \end{tabular}

   869   \end{isabelle}

   879   \end{isabelle}

   870 

   880 

   871   \noindent

   881   \noindent

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

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

   874 

   884 

   875   \begin{isabelle}\ \ \ \ \ %%%

   885   \begin{isabelle}\ \ \ \ \ %%%

   876   \begin{tabular}{@ {}l}

   886   \begin{tabular}{@ {}l}

   877   @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\

   887   @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\

   878   @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\

   888   @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\

   888   at most one running thread. We can also show the following properties 

   898   at most one running thread. We can also show the following properties 

   889   about the @{term RAG} in @{text "s"}.

   899   about the @{term RAG} in @{text "s"}.

   890 

   900 

   891   \begin{isabelle}\ \ \ \ \ %%%

   901   \begin{isabelle}\ \ \ \ \ %%%

   892   \begin{tabular}{@ {}l}

   902   \begin{tabular}{@ {}l}

   896   @{thm (concl) wf_dep_converse},\\

   906   @{thm (concl) wf_dep_converse},\\

   898   and\\

   908   and\\

   899   \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.

   909   \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.

   900   \end{tabular}

   910   \end{tabular}

   901   \end{isabelle}

   911   \end{isabelle}

   902 

   912 

  1111   \end{center}

  1121   \end{center}

  1112   \end{lemma}

  1122   \end{lemma}

  1113   

  1123   

  1114   \noindent

  1124   \noindent

  1115   That means the current precedence of a thread @{text th} can be

  1125   That means the current precedence of a thread @{text th} can be

  1117   effect, it only needs to be recomputed for @{text th} when one of

  1127   effect, it only needs to be recomputed for @{text th} when one of

  1118   its children changes its current precedence.  Once the current 

  1128   its children changes its current precedence.  Once the current 

  1119   precedence is computed in this more efficient manner, the selection

  1129   precedence is computed in this more efficient manner, the selection

  1120   of the thread with highest precedence from a set of ready threads is

  1130   of the thread with highest precedence from a set of ready threads is

  1121   a standard scheduling operation implemented in most operating

  1131   a standard scheduling operation implemented in most operating

  1122   systems.

  1132   systems.

  1123 

  1137 

  1124   Of course the main work for implementing PIP involves the

  1138   Of course the main work for implementing PIP involves the

  1125   scheduler and coding how it should react to events.  Below we

  1139   scheduler and coding how it should react to events.  Below we

  1126   outline how our formalisation guides this implementation for each

  1140   outline how our formalisation guides this implementation for each

  1127   kind of events.\smallskip

  1141   kind of events.\smallskip

  1240   in turn. Suppose in state @{text s}, the thread @{text th'} takes over

  1254   in turn. Suppose in state @{text s}, the thread @{text th'} takes over

  1241   resource @{text cs} from thread @{text th}. We can prove

  1255   resource @{text cs} from thread @{text th}. We can prove

  1242 

  1256 

  1243 

  1257 

  1244   \begin{isabelle}\ \ \ \ \ %%%

  1258   \begin{isabelle}\ \ \ \ \ %%%

  1246   \end{isabelle}

  1260   \end{isabelle}

  1247   

  1261   

  1248   \noindent

  1262   \noindent

  1249   which shows how the @{text RAG} needs to be changed. The next lemma suggests

  1263   which shows how the @{text RAG} needs to be changed. The next lemma suggests

  1250   how the current precedences need to be recalculated. For threads that are

  1264   how the current precedences need to be recalculated. For threads that are

  1263   to recalculate the @{text RAG} and also show that no current precedence needs

  1277   to recalculate the @{text RAG} and also show that no current precedence needs

  1264   to be recalculated.

  1278   to be recalculated.

  1265 

  1279 

  1266   \begin{isabelle}\ \ \ \ \ %%%

  1280   \begin{isabelle}\ \ \ \ \ %%%

  1267   \begin{tabular}{@ {}l}

  1281   \begin{tabular}{@ {}l}

  1269   @{thm eq_cp}

  1283   @{thm eq_cp}

  1270   \end{tabular}

  1284   \end{tabular}

  1271   \end{isabelle}

  1285   \end{isabelle}

  1272   *}

  1286   *}

  1273 (*<*)

  1287 (*<*)

  1282   the one where @{text cs} is not locked, and one where it is. We treat the former case

  1296   the one where @{text cs} is not locked, and one where it is. We treat the former case

  1283   first by showing that

  1297   first by showing that

  1284   

  1298   

  1285   \begin{isabelle}\ \ \ \ \ %%%

  1299   \begin{isabelle}\ \ \ \ \ %%%

  1286   \begin{tabular}{@ {}l}

  1300   \begin{tabular}{@ {}l}

  1288   @{thm eq_cp}

  1302   @{thm eq_cp}

  1289   \end{tabular}

  1303   \end{tabular}

  1290   \end{isabelle}

  1304   \end{isabelle}

  1291 

  1305 

  1292   \noindent

  1306   \noindent

  1295   \noindent

  1309   \noindent

  1296   In the second case we know that resource @{text cs} is locked. We can show that

  1310   In the second case we know that resource @{text cs} is locked. We can show that

  1297   

  1311   

  1298   \begin{isabelle}\ \ \ \ \ %%%

  1312   \begin{isabelle}\ \ \ \ \ %%%

  1299   \begin{tabular}{@ {}l}

  1313   \begin{tabular}{@ {}l}

  1301   @{thm[mode=IfThen] eq_cp}

  1315   @{thm[mode=IfThen] eq_cp}

  1302   \end{tabular}

  1316   \end{tabular}

  1303   \end{isabelle}

  1317   \end{isabelle}

  1304 

  1318 

  1305   \noindent

  1319   \noindent