Safety and Liveness: What Correctness Actually Promises

A system can avoid every incorrect result by refusing to produce any result. It can also return quickly while producing conflicting answers. A useful specification must say both which outcomes are forbidden and which progress must eventually happen.

These are the roles of safety and liveness. They are properties of executions, not performance labels.

1. Start with a precise promise

For request processing, define whether a terminal result can be success, rejection, or permanent failure. Returning an arbitrary error cannot satisfy a promise that specifically requires successful execution.

“Eventually” gives no fixed deadline. “Within five seconds” is a different, stronger specification and needs a time model.

2. The finite-prefix test

A safety violation has a finite bad prefix: a finite execution history after which no continuation can make that history satisfy the property. Once two conflicting decisions have occurred, later agreement cannot undo the earlier violation.

Pure liveness has no such finite bad prefix. After a finite wait, completion may still happen later; a trace violates “eventually completes” by postponing completion forever. This distinction is formalized by Alpern and Schneider in Defining Liveness.

Consider these histories:

Safety failure:
accept request R → commit R → commit R again
                              ^ finite evidence of duplication

Liveness failure:
accept request R → retry → retry → retry → ... forever

Successful completion:
accept request R → retry → retry → commit R

Observing ten retries is not the same as observing an infinite execution. A timeout can reveal an operational problem or a missed deadline; without a deadline in the specification, elapsed time alone does not prove a violation of eventual completion.

If the contract is “respond within five seconds,” passing the deadline without a response is already a finite counterexample. Bounded response can therefore be expressed as a safety condition over timed executions.

3. One state machine, two different proof obligations

Imagine a simplified worker that processes an admitted request. The effect is committed by an atomic transition that also records completion.

flowchart LR
  A["Admitted"] --> P["Pending"]
  P -->|Transient failure| P
  P -->|Atomic guarded commit| C["Completed once"]
  C -->|Duplicate request returns saved result| C
  C -.->|Forbidden second effect| X["Safety violation"]

A safety proof can use an invariant:

committedEffectCount(requestId) ≤ 1

Check that it holds initially, then show that every permitted transition preserves it. In the model, a guarded atomic commit changes the count only from 0 to 1; duplicate requests return the saved result. A separate “check, then act” across concurrent workers would not establish the same invariant.

The retry loop exposes a different question: what forces the process to leave Pending? Preserving the count does not answer it. A worker that never commits satisfies this invariant while violating the required progress property.

For a real implementation, identify the boundary of the atomic operation. A database transaction does not automatically include an external service’s side effect. The invariant must describe what the implementation can actually enforce.

4. A possible route to completion is not a guarantee

The state graph has a path from Pending to Completed. It also has a path that loops at Pending forever. The existence of the successful path proves that completion is possible; it does not prove the system guarantees it.

A liveness guarantee must hold on every execution admitted by the model and its assumptions. Relevant assumptions might include:

• The worker does not crash permanently.
• A required dependency eventually becomes available.
• Sent messages are eventually delivered.
• A continuously enabled processing step is eventually scheduled.

The last condition is a form of weak fairness. Without it, a scheduler could ignore a ready worker forever. Weak fairness applies to an action that stays enabled; an action enabled only intermittently may require a stronger fairness assumption or a different design.

State these assumptions explicitly. “The retry will work eventually” is not a proof when the model allows the dependency to remain unavailable forever.

For a finite batch, a progress argument might use the number of unfinished tasks: if it never increases and some unfinished task is guaranteed to finish whenever the count is positive, repeated decreases eventually reach zero. Merely defining the counter is insufficient; the guaranteed decrease is the hard part.

5. Why asynchronous failure detection is difficult

Suppose a detector has heard nothing from P. The same observation is compatible with a crashed P and with a correct P whose messages are delayed. If it must eventually suspect the crash, it must do so after some finite observation. In a fully asynchronous system, a correct process can remain indistinguishable for that long.

Thus perfect strong accuracy and strong completeness cannot both be guaranteed in this model with possible crashes and unbounded delays. Timeouts make an operational choice; they do not turn silence into proof of failure.

Consensus has a related boundary. Paxos protects agreement under its fault assumptions, but termination needs additional conditions that permit progress, such as a stable proposer communicating with a quorum. It does not guarantee eventual decision in every fully asynchronous execution. See Consensus and Paxos and the FLP proof.

6. Stable predicates are about what remains true

A predicate P on global states is stable if:

P(S) implies P(S′) for every state S′ reachable from S

Stability is different from safety or liveness. A stable predicate may describe a desirable completed computation or an undesirable deadlock that cannot resolve itself under the model.

flowchart LR
  A["Computation active"] --> B["All processes passive<br/>and no work in transit"]
  B -->|No new external work| B
  C["Processes waiting"] --> D["Closed circular wait"]
  D -->|No abort or recovery action| D

The qualifications on the loops matter:

• Termination is stable for a closed computation with no new external work, when passive processes can reactivate only by receiving work.
• A deadlock is stable only if the model offers no timeout, cancellation, or recovery transition that breaks it.
• An unreachable object may be safely considered for collection only after accounting for references in messages as well as references stored at processes.

A casual label such as “deadlock freedom” can hide different specifications. “Never enter this closed deadlock state” is a safety condition. “Every waiting request eventually proceeds” is a liveness condition. Write the actual claim before classifying it.

7. What a global snapshot can establish

The Chandy-Lamport snapshot records a consistent cut including channel state. Consider termination detection:

When a stable predicate is true in the recorded snapshot, its truth persists to later reachable states. If it is false, it may become true afterward; another snapshot may be needed. A snapshot detects a condition. It does not cause progress or prove all possible future executions satisfy a liveness promise.

Check your understanding

1. Does retrying guarantee liveness? Only with assumptions that ensure retries can succeed and are eventually executed.
2. Can a refund repair an at-most-once safety violation? It may compensate the business outcome, but it cannot erase the duplicate effect from the execution history.
3. Are safety and liveness universally incompatible? No. Impossibility results depend on a specific model and specification. Both can hold under suitable assumptions.
4. Do idle processes prove termination? Only when no work is in transit and no new work can enter the computation.

Based on UIUC Cloud Computing Concepts, Part 1: “Safety and Liveness” and the global-snapshot lectures (slides and transcripts). The finite-prefix distinction follows the linked Alpern–Schneider paper; worker examples are explanatory models.