bounded bypass

[Daniel Sadoc Menasche]

Dear All,


while working on exercise 2 of chapter 1, on the distinction between liveness and safety, I came across the problem of explaining why bounded bypass is a liveness property.


It seems clear to me that "if an interrupt occurs, then a message is printed within one second" is a safety property, right? After all, the "bad thing" is "will not print within one second".


The following would still be a safety property, right?


"if an interrupt occurs, then it takes at most one additional interruption before a message is printed"



The following, however, would be a liveness property?


"if an interrupt occurs, then a message will be printed and it takes at most one additional interruption before the message is printed"


The distinction between the liveness property of bounded bypass and the safety property of bounded overtaking seems subtle to me. I've updated Wikipedia with the following. Is that reasonable?


Livelock freedom (processes will not deadlock) together with bounded overtaking implies bounded bypass. Bounded overtaking means that after a tagged process declares the interest in entering the critical section, each other process will overtake the tagged process a bounded number of times before the tagged process enters the critical section. Bounded overtaking, by itself, is not a liveness property. In a deadlocked system, bounded overtaking trivially holds, but bounded bypass doesn't.


Thanks!


Daniel