Safety and Liveness
Summary: Two fundamental types of properties used to reason about the correctness of distributed algorithms.
Sources: chapter8
Last updated: 2026-04-17
To define what it means for an algorithm to be correct, we can describe its properties in terms of safety and liveness.
Safety Properties
Informally: “nothing bad happens.”
- If a safety property is violated, we can point to a specific point in time where it happened (e.g., two requests were granted the same fencing token).
- Once a safety property is violated, it cannot be undone.
(source: chapter8, p. 308)
Liveness Properties
Informally: “something good eventually happens.”
- A liveness property might not hold at some point in time, but there is always hope that it will be satisfied in the future (e.g., a node eventually receives a response).
- Liveness properties often include the word “eventually” (source: chapter8, p. 308).
Why the Distinction?
Distributed algorithms are often required to maintain their safety properties even under extreme conditions (e.g., all nodes crash). However, for liveness properties, caveats are allowed (e.g., a request only eventually succeeds if a majority of nodes recover) (source: chapter8, p. 309).