888 means, for example by giving an operational semantics for machine |
888 means, for example by giving an operational semantics for machine |
889 instructions. Therefore we cannot characterise what are ``good'' |
889 instructions. Therefore we cannot characterise what are ``good'' |
890 programs that contain for every looking request also a corresponding |
890 programs that contain for every looking request also a corresponding |
891 unlocking request for a resource. Second, we would need to specify a |
891 unlocking request for a resource. Second, we would need to specify a |
892 kind of global clock that tracks the time how long a thread locks a |
892 kind of global clock that tracks the time how long a thread locks a |
893 resource. But this seems difficult, because how do we conveninet |
893 resource. But this seems difficult, because how do we conveniently |
894 distinguish between a thread that ``just'' lock a resource for a |
894 distinguish between a thread that ``just'' lock a resource for a |
895 very long time and one that locks it forever. Therefore we decided |
895 very long time and one that locks it forever. Therefore we decided |
896 to leave it out this property and let the programmer assume the |
896 to leave out this property and let the programmer assume the |
897 responsibility to program threads in such a benign manner (in |
897 responsibility to program threads in such a benign manner (in |
898 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 |
899 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. |
900 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 |
901 single theorem improving their bound. |
901 single theorem improving their bound. |
934 @{thm [source] th_cp_max th_cp_preced th_kept} |
934 @{thm [source] th_cp_max th_cp_preced th_kept} |
935 @{thm th_cp_max th_cp_preced th_kept} |
935 @{thm th_cp_max th_cp_preced th_kept} |
936 |
936 |
937 THENTHEN |
937 THENTHEN |
938 |
938 |
939 @{thm [source] runing_inversion_4} @{thm runing_inversion_4} |
939 (here) %@ {thm [source] runing_inversion_4} @ {thm runing_inversion_4} |
940 |
940 |
941 which explains what the @{term "th'"} looks like. Now, we have found the |
941 which explains what the @{term "th'"} looks like. Now, we have found the |
942 @{term "th'"} which blocks @{term th}, we need to know more about it. |
942 @{term "th'"} which blocks @{term th}, we need to know more about it. |
943 To see what kind of thread can block @{term th}. |
943 To see what kind of thread can block @{term th}. |
944 |
944 |
1164 |
1164 |
1165 %Since there are only finite many threads live and holding some resource at any moment, |
1165 %Since there are only finite many threads live and holding some resource at any moment, |
1166 %if every such thread can release all its resources in finite duration, then after finite |
1166 %if every such thread can release all its resources in finite duration, then after finite |
1167 %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen |
1167 %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen |
1168 %then. |
1168 %then. |
|
1169 |
|
1170 NOTE: about bounds in sha et al and ours: |
|
1171 |
|
1172 There are low priority threads, |
|
1173 which do not hold any resources, |
|
1174 such thread will not block th. |
|
1175 Their Theorem 3 does not exclude such threads. |
|
1176 |
|
1177 There are resources, which are not held by any low prioirty threads, |
|
1178 such resources can not cause blockage of th neither. And similiary, |
|
1179 theorem 6 does not exlude them. |
|
1180 |
|
1181 Our one bound excudle them by using a different formaulation. " |
|
1182 |
1169 *} |
1183 *} |
1170 (*<*) |
1184 (*<*) |
1171 end |
1185 end |
1172 (*>*) |
1186 (*>*) |
1173 |
1187 |