Liveness

In concurrent computing, liveness refers to a set of properties of concurrent systems, that require a system to make progress despite the fact that its concurrently executing components ("processes") may have to "take turns" in critical sections, parts of the program that cannot be simultaneously run by multiple processes.^[1] Liveness guarantees are important properties in operating systems and distributed systems.^[2]

More generally, a liveness property states that "something good will eventually occur", contrasting a safety property which states that "something bad does not occur". If a safety property is violated there is always a finite execution that shows the violation (the "bad" event occurring), but a liveness property cannot be violated in a finite execution of a distributed system because the "good" event might still occur at some later time. Eventual consistency is an example of a liveness property.^[3] All linear time properties can be expressed as the intersection of safety and liveness properties.^[4] Whereas the violation of a given safety property admits a finite witness, violation of liveness properties may be harder to establish as no finite witness can be used as proof.^[5]

Forms of liveness

Several forms of liveness are recognized. The following ones are defined in terms of a multi-process system that has a critical section, protected by some mutual exclusion (mutex) device. All processes are assumed to correctly use the mutex; progress is defined as finishing execution of the critical section.

Freedom from deadlock is a form of liveness, although a weak one. Consider a system with multiple processes and a single critical section, protected by some mutual exclusion device. Such a system is said to be deadlock-free if, when a group of processes is competing for access to the critical section at some point in time, then some process eventually makes progress at a later point in time. That process need not belong to the aforementioned group; it might have gained access at an earlier or even later moment.^[6]
Freedom from starvation (or "finite bypass") is a stronger liveness guarantee than deadlock-freedom. It states that all processes vying for access to the critical region eventually make progress. Any starvation-free system is also deadlock-free.^[6]
Stronger still is the requirement of bounded bypass. This means that, if $n$ processes are competing for access to the critical region, then each process makes progress after being bypassed at most $f (n)$ times by other processes for some function $f$ .^[6]

Liveness and safety

According to B. Alpern, deadlock-freedom is a safety property.^[7] Alpern presumes that the states of the system can be split between states wherein deadlock is present (red states) and states wherein no deadlock is in place (green states). The property that states that the system remains forever in green states (or, alternatively, that the system never reaches red states) is a safety property. If one cannot distinguish between green and red states, however, the property that says that eventually one of the processes in the system will evolve is a liveness property.

Formal distinction

The distinction between safety and liveness can be formally established through a predicate $P(t)$ , where $t$ refers to time. Let $t_{0}$ be the instant of time starting from which the liveness and safety properties are evaluated. In the examples below, let $x$ be a process (or thread) that one wants to assure that is deadlock free.

Safety: $\forall t\geq t_{0}:P(t)={\textrm {False}}.$

Example: $P(t)$ means " $x$ is in a deadlock state at time $t$ ".

Liveness: $\forall t_{1}\geq t_{0},\exists t\geq t_{1},t<\infty :P(t)={\textrm {True}}.$

Example: $P(t)$ means " $x$ stops waiting at time $t$ ".

Bounded bypass and bounded overtaking

It is also worth noting that the distinction between the liveness property of bounded bypass and the safety property of bounded overtaking is subtle. Starvation freedom together with bounded overtaking implies bounded bypass (i.e., even though bounded bypass is classified as a liveness property, in reality it is a mix of a liveness property and a safety property). 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. Note that if the tagged process is never granted the permission to enter its critical section, bounded overtaking may still hold. Therefore, bounded overtaking, by itself, is not a liveness property. In a deadlocked system, bounded overtaking trivially holds, as no process overtakes the other, but bounded bypass doesn't.^[8]

References

^ Lamport, L. (1977). "Proving the Correctness of Multiprocess Programs". IEEE Transactions on Software Engineering (2): 125–143. CiteSeerX 10.1.1.137.9454. doi:10.1109/TSE.1977.229904.
^ Luís Rodrigues, Christian Cachin; Rachid Guerraoui (2010). Introduction to reliable and secure distributed programming (2. ed.). Berlin: Springer Berlin. pp. 22–24. ISBN 978-3-642-15259-7.{{cite book}}: CS1 maint: multiple names: authors list (link)
^ Bailis, P.; Ghodsi, A. (2013). "Eventual Consistency Today: Limitations, Extensions, and Beyond". Queue. 11 (3): 20. doi:10.1145/2460276.2462076.
^ Alpern, B.; Schneider, F. B. (1987). "Recognizing safety and liveness". Distributed Computing. 2 (3): 117. CiteSeerX 10.1.1.20.5470. doi:10.1007/BF01782772.
^ Gouda, Mohamed G. (1993). "Protocol verification made simple: a tutorial". Computer Networks and ISDN Systems. 25 (9): 969–980. doi:10.1016/0169-7552(93)90094-k.
^ ^a ^b ^c Raynal, Michel (2012). Concurrent Programming: Algorithms, Principles, and Foundations. Springer Science & Business Media. pp. 10–11. ISBN 978-3642320262.
^ Alpern, B. (1985). "Defining liveness". Information Processing Letters. 21 (4): 181–185. doi:10.1016/0020-0190(85)90056-0.
^ Fang, Y. (2006). Liveness by invisible invariants. Lecture Notes in Computer Science. Vol. 4229. pp. 356–371. doi:10.1007/11888116_26. ISBN 978-3-540-46219-4. {{cite book}}: |journal= ignored (help)

[1] Lamport, L. (1977). "Proving the Correctness of Multiprocess Programs". IEEE Transactions on Software Engineering (2): 125–143. CiteSeerX 10.1.1.137.9454. doi:10.1109/TSE.1977.229904.

[2] Luís Rodrigues, Christian Cachin; Rachid Guerraoui (2010). Introduction to reliable and secure distributed programming (2. ed.). Berlin: Springer Berlin. pp. 22–24. ISBN 978-3-642-15259-7.{{cite book}}: CS1 maint: multiple names: authors list (link)

[3] Bailis, P.; Ghodsi, A. (2013). "Eventual Consistency Today: Limitations, Extensions, and Beyond". Queue. 11 (3): 20. doi:10.1145/2460276.2462076.

[4] Alpern, B.; Schneider, F. B. (1987). "Recognizing safety and liveness". Distributed Computing. 2 (3): 117. CiteSeerX 10.1.1.20.5470. doi:10.1007/BF01782772.

[5] Gouda, Mohamed G. (1993). "Protocol verification made simple: a tutorial". Computer Networks and ISDN Systems. 25 (9): 969–980. doi:10.1016/0169-7552(93)90094-k.

[raynal-6] Raynal, Michel (2012). Concurrent Programming: Algorithms, Principles, and Foundations. Springer Science & Business Media. pp. 10–11. ISBN 978-3642320262.

[7] Alpern, B. (1985). "Defining liveness". Information Processing Letters. 21 (4): 181–185. doi:10.1016/0020-0190(85)90056-0.

[8] Fang, Y. (2006). Liveness by invisible invariants. Lecture Notes in Computer Science. Vol. 4229. pp. 356–371. doi:10.1007/11888116_26. ISBN 978-3-540-46219-4. {{cite book}}: |journal= ignored (help)

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

Forms of liveness

Liveness and safety

Formal distinction

Bounded bypass and bounded overtaking

See also

References