Liveness and Fairness in Temporal Specifications

Safety properties and liveness properties fail in structurally different ways, and the difference determines how they must be specified and tested. A safety property asserts that nothing bad ever happens; it is violated by a finite execution prefix, and a single reachable bad state is a counterexample. A liveness property asserts that something good eventually happens; no finite prefix can violate it, because the good event may still occur later. Proving a liveness property therefore requires reasoning about infinite executions, which is a different kind of argument and introduces a different class of specification error.

The classification is due to Lamport, and the asymmetry is exact: if a property is violated by some execution, either the violation is detectable in a finite prefix or it is not. The first case is safety, the second liveness, and every property decomposes into a conjunction of a safety part and a liveness part. Most real requirements are exactly that conjunction: “no order ships before payment, and every paid order eventually ships”.

Why the good event cannot be checked at a deadline

A test that waits for a timeout and declares failure is testing liveness approximately. It observes that the good event did not occur within $n$ steps, which is consistent with both a genuine violation and a merely slow system. The test cannot distinguish them, because the property quantifies over all time.

This is not a limitation of testing tools; it is the property’s definition. Consider a queue that guarantees every enqueued item is eventually dequeued. An execution that enqueues one item and then idles forever violates it. An execution that enqueues one item and dequeues it after a billion steps satisfies it. No finite observation separates the two, and any monitor with a bound is really checking a stronger, different property: “the item is dequeued within $n$ steps”. That stronger property is often the one operations actually need, a latency bound rather than eventual delivery, and stating it as a bound is more useful than stating it as liveness. The mistake is to write the bound in the test and the liveness claim in the specification, then treat a test pass as evidence for the specification.

Bounded liveness is sometimes called responsiveness, and it is a safety property in disguise: the violation “not dequeued within $n$ steps” is detectable in a finite prefix. Converting an eventual guarantee into a bounded one is a strengthening, and it costs the implementer freedom. Whether that cost is acceptable is a design decision that should be made explicitly, because an unbounded liveness claim is cheap to state and expensive to verify.

Fairness: the assumption that makes progress possible

A scheduler that never runs a ready thread is a legal execution of most concurrency models. Under such a scheduler, no thread makes progress, so no liveness property holds. The system is not wrong; the environment is adversarial. Liveness proofs therefore require an assumption about the environment, and that assumption is a fairness condition.

Weak fairness over an action $A$ says: if $A$ remains continuously enabled from some point onward, then $A$ is eventually taken. Strong fairness says: if $A$ is enabled infinitely often, then $A$ is eventually taken. The distinction matters for actions that are enabled intermittently. A lock acquisition is enabled only while the lock is free; under weak fairness, a thread that is repeatedly enabled and disabled by competing acquirers may never acquire it, and that is a legal execution. Strong fairness excludes that execution, at the cost of a stronger assumption about the scheduler.

Choosing between them is a specification decision with a real consequence. Weak fairness is a reasonable assumption for a scheduler that must not permanently ignore a runnable thread. Strong fairness is a reasonable assumption for a network that must not permanently drop a repeatedly retransmitted message. Assuming strong fairness where only weak fairness holds makes a liveness proof succeed on paper and fail in practice, which is the worst of the outcomes: the specification claims a guarantee the environment does not provide.

def weakly_fair(suffix, enabled, fired):
    # suffix: states along an execution; enabled(s): the guard holds at s;
    # fired: indices in suffix where the transition is taken.
    if not all(enabled(s) for s in suffix):
        return True                    # not continuously enabled: no obligation
    return any(i in fired for i in range(len(suffix)))

The code above is a sketch of the obligation rather than an implementation, and that is the point: fairness is not a runtime check. It is a hypothesis under which the proof is conducted, and it must be written down next to the property it supports, because a liveness claim without its fairness assumption is unfalsifiable — any counterexample can be dismissed by blaming the scheduler.

Starvation, and the requirement hidden inside it

Starvation is the practical face of a fairness violation. A thread waits forever because others keep arriving and taking the resource. The system satisfies every safety property — no invariant is broken — and violates the liveness property that each waiting thread eventually proceeds.

The interesting cases are the ones where the design must choose between fairness and throughput. A strict first-in-first-out lock is fair and admits no starvation, but it forces every acquirer to wait behind every earlier one, including a thread that holds the lock only briefly. A barging lock lets a newly arriving thread take the lock ahead of waiters, which improves throughput and permits indefinite postponement of a slow waiter. Both are correct implementations of different specifications, and the choice cannot be made by the implementer, because it changes an observable guarantee.

Specifications often omit this choice, and the omission surfaces as a bug report from one user whose request was repeatedly overtaken. The fix is a sentence in the specification: either the acquisition order is FIFO, or a waiter that has been ready for $n$ attempts is given priority. The second form is a bounded fairness guarantee, which is checkable and which composes: a scheduler with a bounded bypass count has a computable worst-case wait in terms of the number of competing threads.

Proving liveness with a ranking function

For finite-state systems, liveness can be established by showing that every cycle in the reachable state graph contains a transition that makes progress on some measure. For systems with unbounded state, the standard technique is a ranking function: a map from states to a well-founded ordered set, strictly decreased by every step that does not achieve the goal, and never increased. Since a well-founded order has no infinite descending chain, the goal is reached in finitely many steps.

Well-foundedness is what makes the argument work for infinite state spaces, and it is also where the argument usually breaks. A ranking function into the natural numbers proves termination in finitely many steps; a ranking function into the ordinals extends the technique to recursive or nested structures, at the cost of a harder proof obligation. A function that merely decreases on average, or decreases except when a retry occurs, is not a ranking function, and the resulting liveness claim is unsupported.

The composition of liveness properties is worth noting, because it is not free. Two components each guaranteed to make progress do not, in general, compose into a system that makes progress: the components may each be waiting for the other, a cycle that no individual fairness assumption rules out. This is the same shape as the deadlock question, and the specification has to state the cross-component ordering explicitly. The obligation to do so is what separates a liveness claim that has been thought through from one that has been asserted, and it connects to the invariant reasoning in inductive invariants over reachable states: a deadlock is a reachable state where no progress transition is enabled, which is a safety violation whose consequence is a liveness violation.

What temporal specifications cannot deliver

Temporal logic can state the property; it cannot state the cost of achieving it. “Eventually” says nothing about latency, and a system that satisfies eventual delivery after an hour satisfies the formula. Any operational requirement therefore needs a bounded form, and the bound belongs in the specification as a number rather than as an adjective.

The second limitation is that liveness proofs assume the model. If the model omits a transition that the implementation can take — a retry that resets a counter, a timer that fires early — the proof is about a different system. Model and implementation drift in the direction of the model being simpler, because the model is written first and revised less often. A liveness claim is only as good as the fidelity of the transition relation it was proved over, which is why the same discipline that produces a complete transition table in state machine specification is a prerequisite for any temporal argument rather than an alternative to it.