diff -r 1dc801552dfd -r 92ca2410b3d9 Journal/Paper.thy --- a/Journal/Paper.thy Wed Jan 13 13:20:45 2016 +0000 +++ b/Journal/Paper.thy Wed Jan 13 14:20:58 2016 +0000 @@ -890,10 +890,10 @@ programs that contain for every looking request also a corresponding unlocking request for a resource. Second, we would need to specify a kind of global clock that tracks the time how long a thread locks a - resource. But this seems difficult, because how do we conveninet + resource. But this seems difficult, because how do we conveniently distinguish between a thread that ``just'' lock a resource for a very long time and one that locks it forever. Therefore we decided - to leave it out this property and let the programmer assume the + to leave out this property and let the programmer assume the responsibility to program threads in such a benign manner (in addition to causing no circularity in the RAG). In this detail, we do not make any progress in comparison with the work by Sha et al. @@ -936,7 +936,7 @@ THENTHEN - @{thm [source] runing_inversion_4} @{thm runing_inversion_4} + (here) %@ {thm [source] runing_inversion_4} @ {thm runing_inversion_4} which explains what the @{term "th'"} looks like. Now, we have found the @{term "th'"} which blocks @{term th}, we need to know more about it. @@ -1166,6 +1166,20 @@ %if every such thread can release all its resources in finite duration, then after finite %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen %then. + + NOTE: about bounds in sha et al and ours: + + There are low priority threads, + which do not hold any resources, + such thread will not block th. + Their Theorem 3 does not exclude such threads. + + There are resources, which are not held by any low prioirty threads, + such resources can not cause blockage of th neither. And similiary, + theorem 6 does not exlude them. + + Our one bound excudle them by using a different formaulation. " + *} (*<*) end