State the scheduling assumptions that make progress possible

A safety violation has a finite bad prefix: once two mutually exclusive commitments have occurred, later behavior cannot erase that fact. A pure liveness violation instead needs an infinite behavior in which the required progress never occurs. A long pending request is suspicious, but without a deadline or additional assumptions its finite waiting prefix can still be extended by eventual completion. Model checkers can represent infinite nonprogress through a reachable cycle or stuttering suffix when the finite state graph and temporal conditions permit that behavior.

Define whose progress matters. Fairness of an action that serves some request does not imply fairness for each particular request. An implementation can repeatedly serve newer requests while one older request remains pending. Per-request or per-process assumptions can express a stronger requirement, but they need an implementation argument. Likewise an enabled transition is one whose guard permits a nonstuttering step in the chosen variable tuple. An action that merely leaves those variables unchanged does not count as the substantive progress required by a nonstuttering fairness condition.

Weak fairness excludes endless neglect when an action remains continuously enabled. It does not exclude a schedule that repeatedly disables that action before choosing it. Strong fairness rules out endless neglect when the action is enabled infinitely often, even if enabling is intermittent. Consider a ready flag that toggles forever while Process is enabled only when ready is true. A schedule containing only toggles can satisfy weak fairness for Process because readiness never becomes permanent; it violates strong fairness because Process has infinitely many opportunities and never runs.

Stronger fairness is not automatically a better or more realistic model. A scheduler may have no mechanism that guarantees selection during intermittent opportunities. Network delivery, lock ownership, admission, and process scheduling can each have different assumptions. When a claim needs strong fairness, identify which component enforces the required recurring opportunity and selection behavior. If the action becomes permanently disabled because a request is lost or a node never recovers, neither weak nor strong fairness of that disabled action forces completion. The environment must supply the missing possibility.

A replicated service can remain safe during a permanent partition while losing progress for some clients. A liveness theorem might therefore assume a sufficiently connected period, eventual message delivery, a live quorum, and scheduling conditions. State these premises before the conclusion, and distinguish them from probabilistic availability estimates. A fairness theorem also does not bound latency: an action can be delayed for any finite duration and still eventually occur. A finite deadline needs an explicit clock and quantitative execution assumptions in addition to eventual scheduling.

The Markov instrument offers a visible two-state cycle. Reset, set p=1 and q=1, predict state-one probability one after one transition and zero after two, then take two Steps. It starts entirely in state zero and alternates deterministically; each Step advances one transition. This exact distribution model does not contain a scheduler, Process action, or fairness checker. Its repeated states make a cyclic nonprogress illustration possible, but proving that a service cycle violates a liveness requirement requires the service's own actions, enabling conditions, and fairness assumptions.