Talk:Liveness

Reason for removing content and redirecting this page

The contents of this "liveness" page were removed and the page redirected to "Safety and liveness properties" for several reasons, shown below. It is clear from these reasons that this page was out of date, incorrect in many ways, and not easily fixed.

1. The formal defns of safety and liveness are not equivalent to the now commonly accepted defns. They rule out many properties that are safety and that are liveness. For example, the use of "state predicate" P means that P is not expressive enough to handle properties involving a sequence of states, such as "x is monotonically non decreasing".

2. In the section on "Forms of Liveness", freedom from deadlock is not a form of liveness despite what this article says. It is a form of safety (as the page "Safety and liveness properties" explains). The "bad thing" is a deadlocked state.

3. Bounded bypass is also not a form of liveness despite what this article says. It is a form of safety. The "bad thing" is being bypassed more than f(n) times. The article "Safety and liveness properties" doesn't talk about bounded bypass because it is not a widely discussed property.

4. The whole discussion on "Bounded bypass and bounded overtaking" is based on the wrong premise that Bounded bypass is a form of liveness, so the discussion is wrong. DavidGries (talk) 16:21, 28 October 2022 (UTC)