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]

A liveness property cannot be violated in a finite execution of a distributed system because the "good" event might only theoretically occur at some time after execution ends. Eventual consistency is an example of a liveness property.^[3] All properties can be expressed as the intersection of safety and liveness properties.^[4]

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.^[5]
• 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.^[5]
• 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.^[5]

See also

• Non-blocking algorithm

References

1. Lamport, L. (1977). "Proving the Correctness of Multiprocess Programs". IEEE Transactions on Software Engineering (2): 125–143. 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.
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. doi:10.1007/BF01782772.
5. Raynal, Michel (2012). Concurrent Programming: Algorithms, Principles, and Foundations. Springer Science & Business Media. pp. 10–11. ISBN 3642320279.