Another weekend, another weekend read, this time all about Defining Liveness
My book Thinking in Distributed Systems is now available. 12 chapters, full of mental models, diagrams, illustrations, and examples, all about distributed systems.
In their paper Defining Liveness, the authors provide a formal definition of safety and liveness properties for software systems.
As I advanced in my career, I realized that my understanding of correctness was fuzzy at best: a system was correct if it did what it was supposed to do.
However, this definition does not provide any objective criteria for determining if a system is correct or not. I wanted to be able to rigorously think about the system's guarantees, capabilities, and limitations.
My favorite definition was coined by Leslie Lamport. Leslie Lamport defines the correctness of a system in terms of its safety and liveness properties:
Safety Informally, a safety property guarantees that something bad will never happen.
Liveness Informally, a liveness property guarantees that something good will eventually happen.
Alpern and Schneider present a tangible definition－and mental model－of Safety and Liveness properties.
Safety
This means if σ violates P, there exists a point i in the execution such that for every possible continuation β, the concatenated sequence starting from σi (the prefix up to i) does not satisfy P.
Essentially, a bad thing happens at a distinct point in time, which makes the violation detectable by examining a finite prefix.
Liveness
This means for every prefix α, there exists an extension β such that the concatenated sequence αβ satisfies P.
Essentially, regardless of the progress made, there is always a possibility that a good thing may occur in the future.
The authors conclude the paper with a proof that any system property can be expressed as a combination of a Safety and Liveness property.
An enlightening and foundational weekend read.
Happy Reading
Defining Liveness
Bowen Alpern and Fred B. Schneider
A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that 'something good' eventually happens during execution. A topological characterization of safety and liveness is given. Every property is shown to be the intersection of a safety property and a liveness property.