Journal/Paper.thy
changeset 134 8a13b37b4d95
parent 130 0f124691c191
child 135 9b5da0327d43
equal deleted inserted replaced
133:4b717aa162fa 134:8a13b37b4d95
   182   remaining priority of the threads that it blocks.  A similar error
   182   remaining priority of the threads that it blocks.  A similar error
   183   is made in the textbook \cite[Section 2.3.1]{book} which specifies
   183   is made in the textbook \cite[Section 2.3.1]{book} which specifies
   184   for a process that inherited a higher priority and exits a critical
   184   for a process that inherited a higher priority and exits a critical
   185   section ``{\it it resumes the priority it had at the point of entry
   185   section ``{\it it resumes the priority it had at the point of entry
   186   into the critical section}''.  This error can also be found in the
   186   into the critical section}''.  This error can also be found in the
       
   187   textbook \cite[Section 16.4.1]{LiYao03} where the authors write
       
   188   ``{\it its priority is immediately lowered to the level originally assigned}'';
       
   189   or in the 
   187   more recent textbook \cite[Page 119]{Laplante11} where the authors
   190   more recent textbook \cite[Page 119]{Laplante11} where the authors
   188   state: ``{\it when [the task] exits the critical section that caused
   191   state: ``{\it when [the task] exits the critical section that caused
   189   the block, it reverts to the priority it had when it entered that
   192   the block, it reverts to the priority it had when it entered that
   190   section}''. The textbook \cite[Page 286]{Liu00} contains a simlar
   193   section}''. The textbook \cite[Page 286]{Liu00} contains a simlar
   191   flawed specification and even goes on to develop pseudo-code based
   194   flawed specification and even goes on to develop pseudo-code based
   205   example on Page 254 the authors write: ``{\it Upon releasing the
   208   example on Page 254 the authors write: ``{\it Upon releasing the
   206   lock, the [low-priority] thread will revert to its original
   209   lock, the [low-priority] thread will revert to its original
   207   priority.}'' The same error is also repeated later in this textbook.
   210   priority.}'' The same error is also repeated later in this textbook.
   208 
   211 
   209   
   212   
   210   While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
   213   While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only
   211   formal publications we have found that specify the incorrect
   214   formal publications we have found that specify the incorrect
   212   behaviour, it seems also many informal descriptions of PIP overlook
   215   behaviour, it seems also many informal descriptions of PIP overlook
   213   the possibility that another high-priority might wait for a
   216   the possibility that another high-priority might wait for a
   214   low-priority process to finish.  A notable exception is the texbook
   217   low-priority process to finish.  A notable exception is the texbook
   215   \cite{buttazzo}, which gives the correct behaviour of resetting the
   218   \cite{buttazzo}, which gives the correct behaviour of resetting the