1201 

  1202 section {* An overview of priority inversion and priority inheritance \label{overview} *}

  1203 

  1204 text {*

  1205 

  1206   Priority inversion refers to the phenomenon when a thread with high priority is blocked 

  1207   by a thread with low priority. Priority happens when the high priority thread requests 

  1208   for some critical resource already taken by the low priority thread. Since the high 

  1209   priority thread has to wait for the low priority thread to complete, it is said to be 

  1210   blocked by the low priority thread. Priority inversion might prevent high priority 

  1211   thread from fulfill its task in time if the duration of priority inversion is indefinite 

  1212   and unpredictable. Indefinite priority inversion happens when indefinite number 

  1213   of threads with medium priorities is activated during the period when the high 

  1214   priority thread is blocked by the low priority thread. Although these medium 

  1215   priority threads can not preempt the high priority thread directly, they are able 

  1216   to preempt the low priority threads and cause it to stay in critical section for 

  1217   an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. 

  1218   

  1219   Priority inheritance is one protocol proposed to avoid indefinite priority inversion. 

  1220   The basic idea is to let the high priority thread donate its priority to the low priority 

  1221   thread holding the critical resource, so that it will not be preempted by medium priority 

  1222   threads. The thread with highest priority will not be blocked unless it is requesting 

  1223   some critical resource already taken by other threads. Viewed from a different angle, 

  1224   any thread which is able to block the highest priority threads must already hold some 

  1225   critical resource. Further more, it must have hold some critical resource at the 

  1226   moment the highest priority is created, otherwise, it may never get change to run and 

  1227   get hold. Since the number of such resource holding lower priority threads is finite, 

  1228   if every one of them finishes with its own critical section in a definite duration, 

  1229   the duration the highest priority thread is blocked is definite as well. The key to 

  1230   guarantee lower priority threads to finish in definite is to donate them the highest 

  1231   priority. In such cases, the lower priority threads is said to have inherited the 

  1232   highest priority. And this explains the name of the protocol: 

  1233   {\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay.

  1234 

  1235   The objectives of this paper are:

  1236   \begin{enumerate}

  1237   \item Build the above mentioned idea into formal model and prove a series of properties 

  1238     until we are convinced that the formal model does fulfill the original idea. 

  1239   \item Show how formally derived properties can be used as guidelines for correct 

  1240     and efficient implementation.

  1241   \end{enumerate}

  1242   The proof is totally formal in the sense that every detail is reduced to the 

  1243   very first principles of Higher Order Logic. The nature of interactive theorem 

  1244   proving is for the human user to persuade computer program to accept its arguments. 

  1245   A clear and simple understanding of the problem at hand is both a prerequisite and a 

  1246   byproduct of such an effort, because everything has finally be reduced to the very 

  1247   first principle to be checked mechanically. The former intuitive explanation of 

  1248   Priority Inheritance is just such a byproduct. 

  1249   *}

  1250 

  1251 section {* General properties of Priority Inheritance \label{general} *}

  1252 

  1253 text {*

  1254  

  1255   *}

  1419 section {* Conclusions \label{conclusion} *}

  1420 

  1421 text {*

  1422  

  1423 

  1424 *}