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. Liveness guarantees are important properties in operating systems and distributed systems. 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. Liveness guarantees are important properties in operating systems and distributed systems. 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. All properties can be expressed as the intersection of safety and liveness properties. Whereas safety properties admit a finite witness, liveness properties may be harder to establish as no finite witness can be used to prove that they do not hold. 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. According to B. Alpern, deadlock-freedom is a safety property. 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. The distinction between safety and liveness can be formally established through a predicate P ( t ) {displaystyle P(t)} , where t {displaystyle t} refers to time. Let t 0 {displaystyle t_{0}} be the instant of time starting from which the liveness and safety properties are evaluated. In the examples below, let x {displaystyle x} be a process (or thread) that one wants to assure that is deadlock free. Safety: ∀ t ≥ t 0 : P ( t ) = False . {displaystyle forall tgeq t_{0}:P(t)={ extrm {False}}.} Example: P ( t ) {displaystyle P(t)} means ' x {displaystyle x} is in a deadlock state at time t {displaystyle t} '. Liveness: ∀ t 1 ≥ t 0 , ∃ t ≥ t 1 , t < ∞ : P ( t ) = True . {displaystyle forall t_{1}geq t_{0},exists tgeq t_{1},t<infty :P(t)={ extrm {True}}.} Example: P ( t ) {displaystyle P(t)} means ' x {displaystyle x} stops waiting at time t {displaystyle t} '.