1 (*<*)

     1 (*<*)

     2 theory Paper

     2 theory Paper

     4 begin

     6 begin

     5 

     7 

     6 

     8 

     7 declare [[show_question_marks = false]]

     9 declare [[show_question_marks = false]]

     8 

    10 

    17   waiting ("waits") and

    19   waiting ("waits") and

    18   Th ("T") and

    20   Th ("T") and

    19   Cs ("C") and

    21   Cs ("C") and

    20   readys ("ready") and

    22   readys ("ready") and

    21   preced ("prec") and

    23   preced ("prec") and

    23   cpreced ("cprec") and

    25   cpreced ("cprec") and

    24   cp ("cprec") and

    26   cp ("cprec") and

    25   holdents ("resources") and

    27   holdents ("resources") and

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

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

    27  

    29  

   359 

   361 

   360   \noindent

   362   \noindent

   361   We also use the abbreviation 

   363   We also use the abbreviation 

   362 

   364 

   363   \begin{isabelle}\ \ \ \ \ %%%

   365   \begin{isabelle}\ \ \ \ \ %%%

   365   \end{isabelle}

   367   \end{isabelle}

   366 

   368 

   367   \noindent

   369   \noindent

   368   for the set of precedences of threads @{text ths} in state @{text s}.

   370   for the set of precedences of threads @{text ths} in state @{text s}.

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

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

   896   addition to causing no circularity in the RAG). In this detail, we

   898   addition to causing no circularity in the RAG). In this detail, we

   897   do not make any progress in comparison with the work by Sha et al.

   899   do not make any progress in comparison with the work by Sha et al.

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

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

   899   single theorem improving their bound.

   901   single theorem improving their bound.

   900 

   902 

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

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

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

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

   903   It is relatively easy to see that:

   952   It is relatively easy to see that:

   904 

   953 

   905   \begin{isabelle}\ \ \ \ \ %%%

   954   \begin{isabelle}\ \ \ \ \ %%%

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

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

   914   properties are: 

   963   properties are: 

   915 

   964 

   916   \begin{isabelle}\ \ \ \ \ %%%

   965   \begin{isabelle}\ \ \ \ \ %%%

   917   \begin{tabular}{@ {}l}

   966   \begin{tabular}{@ {}l}

   921   \end{tabular}

   971   \end{tabular}

   922   \end{isabelle}

   972   \end{isabelle}

   923 

   973 

   924   \noindent

   974   \noindent

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

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

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

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

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

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

   931 

   981 

   932   \begin{isabelle}\ \ \ \ \ %%%

   982   \begin{isabelle}\ \ \ \ \ %%%

   933   \begin{tabular}{@ {}l}

   983   \begin{tabular}{@ {}l}

   935   \hspace{5mm}@{thm (concl) acyclic_RAG},

   985   \hspace{5mm}@{thm (concl) acyclic_RAG},

   936   @{thm (concl) finite_RAG} and

   986   @{thm (concl) finite_RAG} and

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

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

   939   and\\

   989   and\\

   941   \end{tabular}

   991   \end{tabular}

   942   \end{isabelle}

   992   \end{isabelle}

   943 

   993 

   944   \noindent

   994   \noindent

   945   The acyclicity property follows from how we restricted the events in

   995   The acyclicity property follows from how we restricted the events in

  1134   We can however improve upon this. For this let us define the notion

  1184   We can however improve upon this. For this let us define the notion

  1135   of @{term children} of a thread @{text th} in a state @{text s} as

  1185   of @{term children} of a thread @{text th} in a state @{text s} as

  1136 

  1186 

  1137   \begin{isabelle}\ \ \ \ \ %%%

  1187   \begin{isabelle}\ \ \ \ \ %%%

  1138   \begin{tabular}{@ {}l}

  1188   \begin{tabular}{@ {}l}

  1140   \end{tabular}

  1190   \end{tabular}

  1141   \end{isabelle}

  1191   \end{isabelle}

  1142 

  1192 

  1143   \noindent

  1193   \noindent

  1144   where a child is a thread that is only one ``hop'' away from the thread

  1194   where a child is a thread that is only one ``hop'' away from the thread

  1145   @{text th} in the @{term RAG} (and waiting for @{text th} to release

  1195   @{text th} in the @{term RAG} (and waiting for @{text th} to release

  1146   a resource). We can prove the following lemma.

  1196   a resource). We can prove the following lemma.

  1147 

  1197 

  1148   \begin{lemma}\label{childrenlem}

  1198   \begin{lemma}\label{childrenlem}

  1150   \begin{center}

  1200   \begin{center}

  1152   \end{center}

  1202   \end{center}

  1153   \end{lemma}

  1203   \end{lemma}

  1154   

  1204   

  1155   \noindent

  1205   \noindent

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

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

  1182   the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event

  1232   the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event

  1183   is allowed to occur). In this situation we can show that

  1233   is allowed to occur). In this situation we can show that

  1184 

  1234 

  1185   \begin{isabelle}\ \ \ \ \ %%%

  1235   \begin{isabelle}\ \ \ \ \ %%%

  1186   \begin{tabular}{@ {}l}

  1236   \begin{tabular}{@ {}l}

  1188   @{thm eq_cp_th}, and\\

  1238   @{thm eq_cp_th}, and\\

  1189   @{thm[mode=IfThen] eq_cp}

  1239   @{thm[mode=IfThen] eq_cp}

  1190   \end{tabular}

  1240   \end{tabular}

  1191   \end{isabelle}

  1241   \end{isabelle}

  1192 

  1242 

  1206   \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 

  1256   \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 

  1207   the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that

  1257   the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that

  1208 

  1258 

  1209   \begin{isabelle}\ \ \ \ \ %%%

  1259   \begin{isabelle}\ \ \ \ \ %%%

  1210   \begin{tabular}{@ {}l}

  1260   \begin{tabular}{@ {}l}

  1212   @{thm[mode=IfThen] eq_cp}

  1262   @{thm[mode=IfThen] eq_cp}

  1213   \end{tabular}

  1263   \end{tabular}

  1214   \end{isabelle}

  1264   \end{isabelle}

  1215 

  1265 

  1216   \noindent

  1266   \noindent

  1255   %that this procedure can actually stop often earlier without having to consider all

  1305   %that this procedure can actually stop often earlier without having to consider all

  1256   %dependants.

  1306   %dependants.

  1257   %

  1307   %

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

  1308   %\begin{isabelle}\ \ \ \ \ %%%

  1259   %\begin{tabular}{@ {}l}

  1309   %\begin{tabular}{@ {}l}

  1263   %\end{tabular}

  1313   %\end{tabular}

  1264   %\end{isabelle}

  1314   %\end{isabelle}

  1265   %

  1315   %

  1266   %\noindent

  1316   %\noindent

  1267   %The first lemma states that if the current precedence of @{text th} is unchanged,

  1317   %The first lemma states that if the current precedence of @{text th} is unchanged,

  1328   first by showing that

  1378   first by showing that

  1329   

  1379   

  1330   \begin{isabelle}\ \ \ \ \ %%%

  1380   \begin{isabelle}\ \ \ \ \ %%%

  1331   \begin{tabular}{@ {}l}

  1381   \begin{tabular}{@ {}l}

  1332   @{thm RAG_s}\\

  1382   @{thm RAG_s}\\

  1334   \end{tabular}

  1384   \end{tabular}

  1335   \end{isabelle}

  1385   \end{isabelle}

  1336 

  1386 

  1337   \noindent

  1387   \noindent

  1338   This means we need to add a holding edge to the @{text RAG} and no

  1388   This means we need to add a holding edge to the @{text RAG} and no

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

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

  1342   

  1392   

  1343   \begin{isabelle}\ \ \ \ \ %%%

  1393   \begin{isabelle}\ \ \ \ \ %%%

  1344   \begin{tabular}{@ {}l}

  1394   \begin{tabular}{@ {}l}

  1345   @{thm RAG_s}\\

  1395   @{thm RAG_s}\\

  1347   \end{tabular}

  1397   \end{tabular}

  1348   \end{isabelle}

  1398   \end{isabelle}

  1349 

  1399 

  1350   \noindent

  1400   \noindent

  1351   That means we have to add a waiting edge to the @{text RAG}. Furthermore

  1401   That means we have to add a waiting edge to the @{text RAG}. Furthermore

  1360   dependants.

  1410   dependants.

  1361 

  1411 

  1362   \begin{isabelle}\ \ \ \ \ %%%

  1412   \begin{isabelle}\ \ \ \ \ %%%

  1363   \begin{tabular}{@ {}l}

  1413   \begin{tabular}{@ {}l}

  1364   %%@ {t hm[mode=IfThen] eq_up_self}\\

  1414   %%@ {t hm[mode=IfThen] eq_up_self}\\

  1367   \end{tabular}

  1418   \end{tabular}

  1368   \end{isabelle}

  1419   \end{isabelle}

  1369  

  1420  

  1370   \noindent

  1421   \noindent

  1371   This lemma states that if an intermediate @{term cp}-value does not change, then

  1422   This lemma states that if an intermediate @{term cp}-value does not change, then