prio/Paper/Paper.thy
changeset 276 a821434474c9
parent 275 22b6bd498419
child 277 541bfdf1fa36
equal deleted inserted replaced
275:22b6bd498419 276:a821434474c9
   497 text {*
   497 text {*
   498   The properties (especially @{text "runing_inversion_2"}) convinced us that the model defined 
   498   The properties (especially @{text "runing_inversion_2"}) convinced us that the model defined 
   499   in Section \ref{model} does prevent indefinite priority inversion and therefore fulfills 
   499   in Section \ref{model} does prevent indefinite priority inversion and therefore fulfills 
   500   the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper 
   500   the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper 
   501   is to show how this model can be used to guide a concrete implementation. As discussed in
   501   is to show how this model can be used to guide a concrete implementation. As discussed in
   502   Section 5.6.5 of \cite{Vahalia:1996:UI}, the implementation of Priority Inheritance in Solaris 
   502   Section 5.6.5 of \cite{Vahalia96}, the implementation of Priority Inheritance in Solaris 
   503   uses sophisticated linking data structure. Except discussing two scenarios to show how
   503   uses sophisticated linking data structure. Except discussing two scenarios to show how
   504   the data structure should be manipulated, a lot of details of the implementation are missing. 
   504   the data structure should be manipulated, a lot of details of the implementation are missing. 
   505   In \cite{Faria08,conf/fase/JahierHR09,WellingsBSB07} the protocol is described formally 
   505   In \cite{Faria08,conf/fase/JahierHR09,WellingsBSB07} the protocol is described formally 
   506   using different notations, but little information is given on how this protocol can be 
   506   using different notations, but little information is given on how this protocol can be 
   507   implemented efficiently, especially there is no information on how these data structure 
   507   implemented efficiently, especially there is no information on how these data structure