Journal/Paper.thy
changeset 70 92ca2410b3d9
parent 64 b4bcd1edbb6d
child 75 2aa37de77f31
equal deleted inserted replaced
69:1dc801552dfd 70:92ca2410b3d9
   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