Dining philosophers, model-checked

The problem

Each philosopher alternates between thinking and eating, and needs both neighbouring forks to eat. In the naive protocol a hungry philosopher picks up the left fork, then the right fork, eats, and puts both down. Each step is one reaction rule: pickLeft i, pickRight i, putDown i.

Why it deadlocks

The trace shown runs pickLeft0, pickLeft1, pickLeft2. Now every philosopher holds a left fork and waits for the right one, but each right fork is a neighbour's left fork, already held. No rule matches, so the system is stuck: a circular wait. The checker finds this state among the 14 reachable ones.

The repair

Philosopher 2 picks up the right fork first (rules pickRightFirst2, pickLeftSecond2). The forks are now taken in one global order, so the circle cannot close: some philosopher can always finish. Of its 12 reachable states none is stuck. The trace shown is a run in which philosopher 2 eats.

The fair protocol

The repair above avoids deadlock, but it does not show that every philosopher keeps a chance to eat. In the fair protocol everyone still picks up the left fork first. A hungry philosopher whose right fork is held by its neighbour puts the left fork back and returns to thinking (rules dropH i and dropE i; the redex says the right fork lies inside the neighbour). The trace runs into the naive deadlock state, philosopher 2 drops its fork, and then philosophers 1, 0 and 2 eat in turn. From every reachable state each philosopher can still go on to eat. A livelock remains: everyone can keep picking up and dropping forever.

What "fair" means here. Nobody is ever locked out: from every reachable state, each philosopher can still come to eat (proved, for each of the three; theorem fair_verdicts). It does not mean that every run feeds everyone: a run in which nobody ever eats exists (proved; the livelock tab). A fair scheduler would exclude that run; that last claim is not proved here.

The state graph and its loop backs

The panel under the player draws every state the checker explored and every move between them, in columns by distance (fewest moves) from the initial state. The unfolding of the reactions is finite: it stops when no move leads to a new state. Even so, many moves lead back to a state already found, at the same or a smaller distance; these loop backs are drawn as dashed curves. They are what makes runs of unbounded length possible in a finite graph: a run that never ends must revisit some state, and if some infinite run avoids eating altogether, then so does a lasso, a finite path out followed by a cycle repeated forever. A state drawn in red has no outgoing move: the system is stuck there. Select a state to show it; a state that is not on the current trace is shown on its own.

The livelock, as a lasso

The livelock tab shows such a lasso in the fair protocol: pickLeft0, pickLeft1, then dropH0 and pickLeft0 repeated. Philosopher 1 holds its left fork, so philosopher 0, whose right fork that is, drops its own left fork and takes it again, forever; nobody eats. The graph for this tab shows only the lasso's four states, not the whole explored graph: the loop-back move (drawn thick) returns from state 3 to state 2, and the states of the cycle are ringed in the loop-back colour. Playing it goes round the cycle until paused, which is the infinite run the lasso stands for.

This is a theorem, not a simulation: M1PrimeDiningLivelock.livelock, proved by checking the lasso as a witness certificate in the Lean kernel, with the checker proved sound (witnessSound).

The alternating bit protocol

The ABP tab is a different system: a protocol that delivers messages in order over channels that may lose them. A sender S passes each message, tagged with one bit, to a channel T, which may deliver it to the replier R or silently lose it. The replier delivers a message whose bit is new, ignores a duplicate, and replies with the bit of the last message it delivered on a second lossy channel K. The sender resends after a timeout, ignores a stale acknowledgement, and on the right one accepts the next message with the other bit. In the drawing the four processes are nodes, each holding its current state, and the channels send, trans, reply and ack are closed links joining the two processes that use them.

Only two moves are seen from outside: accept (the sender takes a message from its user) and deliver (the replier hands it on). Every other move is internal, a τ move. The graph for this tab is the whole state space, all 112 reachable states and 332 moves; visible moves are drawn in their own colour and τ moves lighter. The trace accepts message 0, loses it on the way, times out and resends, ignores a stale acknowledgement, delivers, loses the acknowledgement, ignores the resent duplicate, and only then accepts message 1 and carries it through. Each state's chips give the processes' states and, under buffer, the state of the one-place buffer it corresponds to.

The specification is that one-place buffer, Buff = accept . deliver . Buff. However the channels behave, the visible moves come in the order accept, deliver, accept, deliver, and the protocol can always go on: each state is weakly bisimilar to the buffer, empty or full, shown in its chips (56 states each).

Two theorems stand behind this. ABP.abp_wbisim_buff: this finite ABP, with one-place channels, is weakly bisimilar to the one-place buffer; untrusted code explores the 112 states and writes a certificate (the relation and the answering paths), which a checker proved sound (certWeakBisimSound) validates in the Lean kernel. ABPInf.abpInf_wbisim_buff: the same holds with unbounded lossy FIFO channels, an infinite-state system, proved by an abstraction to a finite system, a certificate for that, and deduction. Both are weak bisimilarity to accept.deliver.Buff. The chips' buffer states are recomputed by the certificate producer for this page, not read from the checked certificate.

The ABP with tracked messages

The tab ABP: tracked messages draws the same protocol with the messages themselves as nodes. A message node msg lies inside whoever holds it: the sender S, the channel T, the replier R, or a fifth node U, the user, who holds a delivered message until consuming it. Tracking answers a question that a picture of states cannot: is the message here, later, the same message as the one there, earlier? Each reaction rule says which nodes and links of its redex survive into its reactum, and so each move carries a tracking map from the old state to the new one. A formula can then name a message in one state and follow it along the moves.

A message's identity is a link, not a node. When the sender accepts a message the rule creates a node on a fresh link. When it retransmits, the copy put into the channel cannot be the same node (the sender keeps its own), so it is a new node on the same link. A copy moving from T into R, and on into U, is the same node. Losing or discarding a copy deletes a node; the link survives while it still has nodes, and goes with its last one. So "the same message" means "a node on the same link", and the link is followed through the moves by the tracking maps. In the drawing each message link and its nodes have one colour for the whole trace, carried by those maps: the link and node numbers in the states are renumbered at almost every step, which is why the colour is not taken from them. Under each step, tracking says where each message's link went.

The trace accepts message A, sends it, and the copy is lost. A stale acknowledgement makes the sender send again: a new copy, on the same link. The replier takes it, the sender times out and sends a third copy, and A is delivered to the user while that copy is still in the channel. The acknowledgement lets the sender drop A and accept message B, on a new link, while the user still holds A. The replier discards the stale copy of A, the user consumes A, and B is sent, delivered, and its lost acknowledgement repeated, until the user consumes B. The graph is the whole state space: 224 reachable states and 828 moves.

Each verdict is a theorem at the initial state, in Bigraph.Logic.ABPTrackCert (Logic/Examples/M1Prime/ABPTrackCert.lean, built on demand outside the library build): sameMessage_holds, heldNow_false, noDuplicate_holds, canDeliver_holds, noStray_holds, copyGone_false. Untrusted compiled code explores the states and writes certificates (closed sets for the invariants, paths to a counterexample for the failures, attractor paths for μ, an invariant table for ν); checkers proved sound (agCheck_sound, agFalseP, muWalk_sound, nuCheck_sound, plugAG_sound) validate them in the Lean kernel. The trace, the chips and the tracking notes on this page are recomputed by the same kind of untrusted exploration for the page, not read from the checked certificate.

What was checked

How sure we are. Each verdict above is a theorem about the library's bigraphs, checked by the Lean kernel (naive_verdicts, repaired_verdicts). Untrusted code explores the states and writes a certificate (the states, the moves between them, and a renumbering for each move); a checker proved correct (m1Prime) validates it in about 30 seconds and evaluates the formulas on the certified graph. The fair protocol's verdicts are proved the same way (fair_verdicts).