642 our criterion is as follows: for all states @{text s}, we know the |
642 our criterion is as follows: for all states @{text s}, we know the |
643 corresponding thread @{text th} with the highest precedence; we show |
643 corresponding thread @{text th} with the highest precedence; we show |
644 that in every future state (denoted by @{text "s' @ s"}) in which |
644 that in every future state (denoted by @{text "s' @ s"}) in which |
645 @{text th} is still alive, either @{text th} is running or it is |
645 @{text th} is still alive, either @{text th} is running or it is |
646 blocked by a thread that was alive in the state @{text s} and was waiting |
646 blocked by a thread that was alive in the state @{text s} and was waiting |
647 or in the possession of a lock in @{text s}. Since in @{text s}, as in |
647 for or in the possession of a lock in @{text s}. Since in @{text s}, as in |
648 every state, the set of alive threads is finite, @{text th} can only |
648 every state, the set of alive threads is finite, @{text th} can only |
649 be blocked a finite number of times. This is independent of how many |
649 be blocked a finite number of times. This is independent of how many |
650 threads of lower priority are created in @{text "s'"}. We will actually prove a |
650 threads of lower priority are created in @{text "s'"}. We will actually prove a |
651 stronger statement where we also provide the current precedence of |
651 stronger statement where we also provide the current precedence of |
652 the blocking thread. However, this correctness criterion hinges upon |
652 the blocking thread. However, this correctness criterion hinges upon |