equal
deleted
inserted
replaced
360 @{thm (rhs) threads.simps(3)}\\ |
360 @{thm (rhs) threads.simps(3)}\\ |
361 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\ |
361 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\ |
362 \end{tabular}} |
362 \end{tabular}} |
363 \end{isabelle} |
363 \end{isabelle} |
364 |
364 |
365 \noindent |
365 \noindent In this definition @{term "DUMMY # DUMMY"} stands for |
366 In this definition @{term "DUMMY # DUMMY"} stands for list-cons and @{term "[]"} for the empty list. |
366 list-cons and @{term "[]"} for the empty list. We use @{term "DUMMY"} |
367 Another function calculates the priority for a thread @{text "th"}, which is |
367 to match any pattern, like in functional programming. |
368 defined as |
368 Another function |
|
369 calculates the priority for a thread @{text "th"}, which is defined |
|
370 as |
369 |
371 |
370 \begin{isabelle}\ \ \ \ \ %%% |
372 \begin{isabelle}\ \ \ \ \ %%% |
371 \mbox{\begin{tabular}{lcl} |
373 \mbox{\begin{tabular}{lcl} |
372 @{thm (lhs) priority.simps(1)} & @{text "\<equiv>"} & |
374 @{thm (lhs) priority.simps(1)} & @{text "\<equiv>"} & |
373 @{thm (rhs) priority.simps(1)}\\ |
375 @{thm (rhs) priority.simps(1)}\\ |
1172 If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}. |
1174 If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}. |
1173 \end{lemma} |
1175 \end{lemma} |
1174 |
1176 |
1175 \begin{proof} Let us assume otherwise, that is @{text "th'"} is detached in state |
1177 \begin{proof} Let us assume otherwise, that is @{text "th'"} is detached in state |
1176 @{text "s"}, then, according to the definition of detached, @{text |
1178 @{text "s"}, then, according to the definition of detached, @{text |
1177 "th’"} does not hold or wait for any resource. Hence the @{text |
1179 "th'"} does not hold or wait for any resource. Hence the @{text |
1178 cp}-value of @{text "th'"} in @{text s} is not boosted, that is |
1180 cp}-value of @{text "th'"} in @{text s} is not boosted, that is |
1179 @{term "cp s th' = prec th' s"}, and is therefore lower than the |
1181 @{term "cp s th' = prec th' s"}, and is therefore lower than the |
1180 precedence (as well as the @{text "cp"}-value) of @{term "th"}. This |
1182 precedence (as well as the @{text "cp"}-value) of @{term "th"}. This |
1181 means @{text "th'"} will not run as long as @{text "th"} is a live |
1183 means @{text "th'"} will not run as long as @{text "th"} is a live |
1182 thread. In turn this means @{text "th'"} cannot take any action in |
1184 thread. In turn this means @{text "th'"} cannot take any action in |
1697 we have that if \mbox{@{term "\<not>(detached (es @ s) th')"}}, then |
1699 we have that if \mbox{@{term "\<not>(detached (es @ s) th')"}}, then |
1698 \[@{text "len (actions_of {th'} es) < BND(th')"}\] |
1700 \[@{text "len (actions_of {th'} es) < BND(th')"}\] |
1699 \end{quote} |
1701 \end{quote} |
1700 |
1702 |
1701 \noindent By this assumption we enforce that any thread potentially |
1703 \noindent By this assumption we enforce that any thread potentially |
1702 blocking @{term th} must become detached (that is lock no resource |
1704 blocking @{term th} must become detached (that is it owns no resource |
1703 anymore) after a finite number of events in @{text "es @ s"}. Again |
1705 anymore) after a finite number of events in @{text "es @ s"}. Again |
1704 we have to state this bound to hold in all valid states after @{text |
1706 we have to state this bound to hold in all valid states after @{text |
1705 s}. The bound reflects how each thread @{text "th'"} is programmed: |
1707 s}. The bound reflects how each thread @{text "th'"} is programmed: |
1706 Though we cannot express what instructions a thread is executing, |
1708 Though we cannot express what instructions a thread is executing, |
1707 the events in our model correspond to the system calls made by |
1709 the events in our model correspond to the system calls made by |