A liveness property prescribes good things for every execution or, equivalently, describes something that must happen during an execution.[1] The good thing need not be discrete—it might involve an infinite number of steps. Examples of a good thing used to define a liveness property include:[5]
- Termination of an execution that is started in a suitable state;
- Non-termination of an execution that is started in a suitable state;
- Guaranteed eventual entry to a critical section whenever entry is attempted;
- Fair access to a resource in the presence of contention.
The good thing in the first example is discrete but not in the others.
Producing an answer within a specified real-time bound is a safety property rather than a liveness property.
This is because a discrete bad thing is being proscribed: a partial execution that reaches a state where the answer still has not been produced and the value of the clock (a state variable) violates the bound. Deadlock freedom is a safety property: the "bad thing" is a deadlock (which is discrete).
Most of the time, knowing that a program eventually does some "good thing" is not satisfactory; we want to know that the program performs the "good thing" within some number of steps or before some deadline. A property that gives a specific bound to the "good thing" is a safety property (as noted above), whereas the weaker property that merely asserts the bound exists is a liveness property. Proving such a liveness property is likely to be easier than proving the tighter safety property because proving the liveness property doesn't require the kind of detailed accounting that is required for proving the safety property.
To differ from a safety property, a liveness property cannot rule
out any finite prefix
[8] of an execution (since such
an would be a "bad thing" and, thus, would be defining a safety property).
That leads to defining a liveness property to be a property that does not rule out any finite prefix.[5]
This definition does not restrict a good thing to being discrete—the
good thing can involve all of , which is an infinite-length execution.
Lamport used the terms safety property and liveness property
in his 1977 paper[1] on proving the correctness of multiprocess (concurrent) programs.
He borrowed the terms from Petri net theory, which was using the terms
liveness and boundedness for describing how the assignment of a Petri net's "tokens"
to its "places" could evolve; Petri net safety was a specific form of boundedness.
Lamport subsequently developed a formal definition of safety for a
NATO short course on distributed systems in Munich.[9]
It assumed that properties are invariant under stuttering.
The formal definition of safety given above appears in a paper by Alpern and
Schneider;[5]
the connection between the two formalizations of safety properties
appears in a paper by Alpern, Demers, and Schneider.[10]
Alpern and Schneider[5] gives the formal definition for liveness, accompanied by a proof that all properties can be constructed using safety properties and liveness properties. That proof was inspired by Gordon Plotkin's insight that safety properties correspond to closed sets and liveness properties correspond to dense sets in a natural topology on the set of infinite sequences of program states.[11] Subsequently, Alpern and Schneider[12] not only gave a Büchi automaton characterization for the formal definitions of safety properties and liveness properties but used these automata formulations to show that verification of safety properties would require an invariant and verification of liveness properties would require a well-foundedness argument. The correspondence between the kind of property (safety vs liveness) with kind of proof (invariance vs well-foundedness) was a strong argument that the decomposition of properties into safety and liveness (as opposed to some other partitioning) was a
useful one—knowing the type of property to be proved dictated the type of proof that is required.
i.e. it has finite duration
Alford, Mack W.; Lamport, Leslie; Mullery, Geoff P. (3 April 1984). "Basic concepts". Distributed Systems: Methods and Tools for Specification, An Advanced Course. Lecture Notes in Computer Science. Vol. 190. Munich, Germany: Springer Verlag. pp. 7–43. ISBN 3-540-15216-4. The paper[5] received the 2018 Dijkstra Prize ("for outstanding papers on the principles of distributed computing whose significance and impact on the theory and/or practice of distributed computing have been evident for at least a decade"), for the formal decomposition into safety and liveness properties was crucial to future research into proving properties of programs. denotes the set of finite sequences of program states
and the set of infinite sequences of program states. Alford, Mack W.; Lamport, Leslie; Mullery, Geoff P. (3 April 1984). "Basic concepts". Distributed Systems: Methods and Tools for Specification, An Advanced Course. Lecture Notes in Computer Science. Vol. 190. Munich, Germany: Springer Verlag. pp. 7–43. ISBN 3-540-15216-4. Private communication from Plotkin to Schneider.