Learn · All the Ways It Can Break

growing

Say Eventually Precisely

A temporal property constrains whole behaviors, and fairness names which enabled work may not be ignored forever.

formal-methods, tla-plus, tlc, liveness, fairness, learn

You will distinguish state predicates from temporal formulas, read [] and <>, understand stuttering, add weak fairness to the action that needs it, and interpret paired failing and passing liveness runs without turning fairness into a wish.

One formula, two behavior sets

The executable specimen states:

tla code/all-the-ways-it-can-break/publication-liveness/Publication.tla#liveness Publication.tla The property is identical in both runs. Only the admitted behaviors change when fairness is added.

[][Next]_vars allows every Next step and stuttering steps that leave vars unchanged. Stuttering makes specifications insensitive to an implementation's extra invisible work, but it also admits waiting forever. In the unfair model, TLC reports a temporal counterexample that reaches complete and then stutters.

Prediction — identify what weak fairness actually promises.

Weak is not strong, and neither is free

Weak fairness applies when an action eventually stays enabled. Strong fairness is needed to rule out starvation when an action is enabled infinitely often but keeps becoming disabled. Stronger fairness yields fewer admitted behaviors and therefore stronger environmental assumptions.

Ask what mechanism earns the promise: a fair queue, retry loop, scheduler contract, operator intervention, or nothing. If production can drop the job permanently, adding fairness proves a different system. Fairness belongs beside the result's residual risk, not hidden inside Spec.

Run both sides

The two public configurations select SpecUnfair and SpecFair while checking the same EventuallyPublished property. Run them with TLC 1.7.4 as in Chapter

The unfair run must emit a temporal counterexample; the fair run must report

complete exploration with no error. The test harness grades both verdicts, so a future edit that accidentally removes starvation also breaks the negative control.

Under the hood: safety and liveness leave different witnesses

A safety failure has a finite bad prefix. A liveness counterexample is an infinite behavior represented finitely by a stem plus a cycle; pure stuttering is a one-state cycle. That is why the temporal trace names a loop and why a final state alone cannot refute <>.

Lessons

Invariants constrain states; temporal properties constrain behaviors.
<> P means P holds at some future position of the behavior.
Stuttering is admitted deliberately and can witness starvation.
Weak fairness covers continuous enablement, not deadlines or intermittent enablement.
Every fairness assumption needs a real mechanism and remains attached to the claim.

Practice

Retrieval. Explain the difference between [] P and <> P.
Discrimination. A retry is enabled for one step after each timeout, then disabled during backoff. Is weak fairness of retry enough by itself?
Transfer. Model a replicated configuration service and state which action must be fair for every continuously connected replica eventually to apply the chosen version.

Worked answers

[] P requires P at every position; <> P requires it at some future position.
Not necessarily: retry is only intermittently enabled. The model needs a stronger assumption or a different action whose continuous enablement the real mechanism supports.
Fair delivery or apply must be tied to continuous connectivity and pending work; the property must exclude permanently disconnected replicas explicitly.

References

Leslie Lamport. Specifying Systems, Chapters 8 and 16. — temporal formulas, stuttering, and fairness
Bowen Alpern and Fred B. Schneider. Defining Liveness. Information Processing Letters 21(4), 1985. — the safety/liveness distinction

← Make the State Space Pay Rent Types Make the Symbolic World Finite Enough →

Every state may be safe while one job waits forever. TLA+ therefore evaluates liveness over behaviors—state sequences extended indefinitely by real steps or stuttering. <> P says that some future state satisfies P. Without fairness, a behavior may stop choosing an enabled publish action and stutter forever. The checked specimen makes that failure visible. Its unfair configuration reaches a complete job and then stutters, refuting eventual publication. The fair specification adds weak fairness separately to start, complete, and publish for each job. TLC then exhausts the finite model. The green result includes those scheduler promises; it does not discover them from the code.