equal
deleted
inserted
replaced
401 |
401 |
402 \noindent |
402 \noindent |
403 We also use the abbreviation |
403 We also use the abbreviation |
404 |
404 |
405 \begin{isabelle}\ \ \ \ \ %%% |
405 \begin{isabelle}\ \ \ \ \ %%% |
406 ???%%@ { thm preceds_def} |
406 @{abbrev "preceds ths s"} |
407 \end{isabelle} |
407 \end{isabelle} |
408 |
408 |
409 \noindent |
409 \noindent |
410 for the set of precedences of threads @{text ths} in state @{text s}. |
410 for the set of precedences of threads @{text ths} in state @{text s}. |
411 The point of precedences is to schedule threads not according to priorities (because what should |
411 The point of precedences is to schedule threads not according to priorities (because what should |
1085 all ready threads, that is |
1085 all ready threads, that is |
1086 |
1086 |
1087 \begin{center} |
1087 \begin{center} |
1088 @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"} |
1088 @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"} |
1089 \end{center} |
1089 \end{center} |
|
1090 |
|
1091 \noindent |
|
1092 We also know that this is equal to all threads, that is |
|
1093 |
|
1094 \begin{center} |
|
1095 @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"} |
|
1096 \end{center} |
|
1097 |
|
1098 \noindent |
|
1099 But the maximum of all threads is the @{term "cp"} of @{text "th"}, |
|
1100 which is the @{term preced} of @{text th}. |
1090 \end{proof} |
1101 \end{proof} |
1091 |
1102 |
1092 @{thm "th_blockedE_pretty"} -- thm-blockedE?? |
1103 @{thm "th_blockedE_pretty"} -- thm-blockedE?? |
1093 |
1104 |
1094 |
1105 |