Waiting is not yet a failure

The safety claim “capacity never falls below zero” can fail in one state. The liveness claim “every accepted job eventually settles” cannot be settled by inspecting one state or any fixed number of states.

For every finite waiting trace, append Settle(job). The extended trace now satisfies the particular job's eventuality. A liveness violation is therefore about a behavior that continues without the promised event.

The model may admit a simple infinite behavior:

Wait → Wait → Wait → Wait → …

Sometimes the repeated step is explicit. Sometimes nothing relevant changes; the behavior stutters. TLA+ deliberately permits stuttering so a specification does not depend on how many invisible implementation steps occur between visible actions.

Fairness says which neglect is forbidden

Suppose Start(job) is enabled whenever the job is queued and a credit is free. Two useful intuitions differ:

• Weak fairness: if Start(job) remains enabled continuously, it eventually occurs.
• Strong fairness: if Start(job) becomes enabled infinitely often, even with interruptions, it eventually occurs.

Strong fairness rules out more behaviors and therefore makes a stronger claim about the scheduler. Neither is automatically true of production.

Decompose the promise

“Every accepted job eventually finishes” hides several claims:

1. an accepted job eventually obtains capacity;
2. an enabled start action eventually runs;
3. the worker either completes or reports failure;
4. a completion or failure message is eventually delivered;
5. settlement processing eventually runs.

Each step may require a different assumption. A scheduler can promise fair local execution but cannot promise that a crashed remote process recovers. A retry policy can promise repeated attempts under a timer model but cannot promise that the network eventually delivers a packet unless the network model says so.

The decomposition is useful even when the final answer is “no liveness guarantee.” The system may honestly guarantee safety under arbitrary message loss while offering progress only when the network eventually delivers and at least one worker remains available.

Under the hood: stronger assumptions buy stronger theorems

A liveness theorem has the form “under assumptions $A$, every admitted behavior satisfies progress property $L$.” If $A$ includes reliable delivery, fair scheduling, bounded retries, and eventual recovery, the theorem may be provable. It also applies only to environments satisfying all four.

Adding fairness can make a checker green by deleting the counterexample where the scheduler starves the job. That is correct only if starvation is genuinely outside the promised environment. The negative control is to remove or weaken the fairness assumption and confirm that the starvation behavior returns.

Experienced engineers should treat fairness like an interface contract. Name the component that provides it, the condition under which it applies, and the operational evidence that watches the assumption after deployment. A formal model does not cause a production scheduler to become fair.

Safety without liveness, liveness without safety

A system can satisfy “no canceled job publishes” by never publishing anything. It is safe and useless. Another system can guarantee that every job publishes eventually while occasionally publishing canceled jobs. It is live and unsafe.

Real specifications normally need both. Keeping the properties distinct makes failures actionable: a safety counterexample identifies a forbidden finite prefix; a liveness counterexample identifies an infinite pattern or cycle plus the assumptions that permitted it.

Lessons

• A finite delay cannot by itself refute an eventuality.
• Liveness properties constrain whole behaviors rather than individual states.
• Fairness assumptions rule out specified forms of permanent neglect.
• Weak and strong fairness make different promises and must not be chosen for convenience.
• Formal proof of liveness does not establish that the production environment satisfies its assumptions.

Practice

1. Retrieval. Complete the sentence: possibility comes from _; eventuality additionally requires _.
2. Discrimination. “Every lock acquisition eventually succeeds” and “two threads never hold the lock together” fail in different evidence shapes. Name them.
3. Transfer. Decompose “every submitted email is eventually delivered” into at least three steps and state one environmental assumption for each.

References

1. Bowen Alpern and Fred B. Schneider. “Defining Liveness.” Information Processing Letters, 1985. — formal safety/liveness decomposition
2. Leslie Lamport. “Specifying Systems.” Addison-Wesley, 2002. — behaviors, stuttering, temporal properties, and fairness in TLA+