equal
deleted
inserted
replaced
848 |
848 |
849 Like in the argument by Sha et al.~our finite bound does not |
849 Like in the argument by Sha et al.~our finite bound does not |
850 guarantee absence of indefinite Priority Inversion. For this we |
850 guarantee absence of indefinite Priority Inversion. For this we |
851 further have to assume that every thread gives up its resources |
851 further have to assume that every thread gives up its resources |
852 after a finite amount of time. We found that this assumption is |
852 after a finite amount of time. We found that this assumption is |
853 awkward to formalise in our model. There are mainly two reasons: |
853 awkward to formalise in our model. There are mainly two reasons for this: |
854 First, we do not specify what ``running'' the code of a thread |
854 First, we do not specify what ``running'' the code of a thread |
855 means, for example by giving an operational semantics for machine |
855 means, for example by giving an operational semantics for machine |
856 instructions. Therefore we cannot characterise what are ``good'' |
856 instructions. Therefore we cannot characterise what are ``good'' |
857 programs that contain for every looking request also a corresponding |
857 programs that contain for every looking request also a corresponding |
858 unlocking request for a resource. Second, we would need to specify a |
858 unlocking request for a resource. Second, we would need to specify a |