Work Order Scheduling: Reserving Output at Run Start
Can an operation's output buffer capacity be reserved when its run starts, instead of when the operation is assigned, without the factory locking? This page checks the idea against Work Order Scheduling: counterexamples where it fails, the two amendments that make it work, and proofs.
◎ The answer
| Result | What it shows |
|---|---|
| Theorem 1 | Locks. The proposal as written locks the one-machine factory from the current doc. Its buffers are exactly the minimum the current doc requires, and every assignment passes the check. |
| Theorem 2 | Locks. Checking the start as well, with coverage as the current doc defines it, still locks. An operation's cover ends when its output leaves, and nothing re-checks at that moment. |
| Theorem 3 | Locks. The current algorithm has the same flaw and locks too, with no change to when output is reserved. It needs a capacity above the minimum the current doc requires. |
| Theorem 4 | Locks. Counting coverage in units without checking the start still locks: a start takes the output unit a waiting run was keeping. |
| Theorems 5 & 6 | Never locks. With both amendments the invariant holds in every reachable state, and no reachable state is a lock (under four stated assumptions). |
| Machine check | 9,840 random small factories, every order of events explored. The amended proposal locked 0 times. The proposal as written locked in 584, the current algorithm in 113, and the current algorithm with coverage counted in units in 0. |
What it buys: a machine can gather the inputs of several runs while its output is still busy. On a weld machine with 6 input units and 1 output unit, 3 welds can gather plates at once instead of 1 (details). What it does not buy: smaller buffers. The minimum capacity is unchanged, still one run of each recipe a machine is the only home for.
⇄ The proposal
Today, an assigned operation reserves its recipe's input claim and output claim on its machine at the same moment: when it is assigned. The input reservation starts filling as soon as the first input arrives. The output reservation stays empty until the run resolves. While the inputs are still on their way, that output capacity is reserved and holds nothing. For a recipe with many inputs from far away, that can be most of the operation's life.
The proposal: take the input claim at assignment, as now, and take the output claim only when the run starts. The input ledger is checked at assignment and the output ledger at the start. As written, the refusal check still runs at assignment only.
Aa The model
A proof needs every rule written down. The model follows the current doc; where the doc leaves a choice open, the reading taken is stated here. The same model is what the machine check runs.
Each machine M has input capacity Cin(M), output capacity Cout(M), and the recipes it carries out. A recipe R has an input claim and an output claim: counts per component kind, totalling |inR| and |outR| units. A unit is one buffer slot, room for one component; capacities are counted in units too. Every recipe has at least one input.
A kind no recipe makes comes from a source, unlimited. A kind no recipe consumes goes to a sink as soon as it is made. Components are fungible by kind, across work orders.
planned → waiting on M (assigned, run not started) → running on M → holding on M (run resolved, some output still there) → done (last output gone).
Waiting, running and holding together are what the current doc calls assigned: "from assignment until its last output component has left".
A component departs the moment an operation that needs its kind is waiting, and counts as gone from then on (the current doc's departing rule).
Assign O to M: O is planned; M carries out its recipe; one of its inputs exists (a source kind, or a component held somewhere); the ledger has freein(M) ≥ |inO| (and freeout(M) ≥ |outO| under the current rule); the refusal check passes. Source inputs arrive; held components O needs depart to it.
Start O: waiting, all inputs arrived. Under the proposal the ledger also needs freeout(M) ≥ |outO|. Inputs are consumed.
Resolve O: sink kinds leave; the rest are held; held components a waiting operation needs depart to it.
Transitions interleave in any order. A run may start the moment it can or later, and a component may take any time in transit. Every counterexample below still locks when every run starts the moment it can, unless stated otherwise.
Walk from every assigned operation: from X to Y whenever X still has a component of some kind to put out (all its outputs before it resolves, what it holds after) and Y still needs that kind — in either direction, repeatedly. The needed set is the recipes of the operations reached that have not started.
This is the current doc's closure, with fungibility taken literally: a component can go to any operation that needs its kind. It leaves out recipes whose only operations have already run, as the current doc's steppers do.
∴ What the current argument relies on
The current doc argues in two parts. First, Why checking at assignment is sufficient shows coverage cannot break between assignments. Second, Why one run per recipe is enough argues that coverage keeps work moving. Both parts use two facts about the current rule without stating them, and a third point is missing from the list.
Free capacity decreases only at an assignment.
As listed in the current doc: arrivals convert inbound to held; a start releases input; a resolve converts reserved to held; a departure releases output. None of these takes a unit. ∎
A waiting operation whose inputs have all arrived can start.
Its output claim was reserved when it was assigned, and starting needs nothing else. ∎
Under the proposal both are false. A start now takes output units, so free capacity drops at an event the check does not see. A waiting operation with every input present can find no output free, and while it waits it keeps its inputs in the machine's input buffer. The recycling argument ("a run takes it, resolves, its outputs leave, the capacity returns") assumes the run can take it.
An operation's cover of its recipe ends when its last output leaves. That event is neither an assignment nor a decrease in free capacity, and it can leave the recipe uncovered.
When the last output leaves, the operation stops counting as assigned, and the capacity it releases is output only. Its input reservation was released when its run started. Any assignment made since then was allowed to take that input capacity, because the recipe counted as covered. The current doc says coverage "can break in only two ways"; this is a third. Theorem 2 and Theorem 3 show it breaks in practice. ∎
| Event | Current rule | Proposal |
|---|---|---|
| Assign | takes input and output · needed set may grow · checked | takes input · needed set may grow · checked |
| Start | releases input | releases input · takes output — not checked |
| Resolve | releases what goes to the sink | releases what goes to the sink |
| Last output leaves | releases output · ends that operation's cover — not checked | releases output · ends that operation's cover — not checked |
Every theorem below that ends in a lock comes through one of the two highlighted cells.
⊘ Theorem 1 · the proposal as written locks
With output reserved at the start and the refusal check at assignment only, the one-machine factory from the current doc locks. That is recipe A (1 ore → 1 ingot), recipe B (1 ingot → 1 plate), machine M with input 2 and output 2, and a work order for five plates. The buffers are exactly the precondition's minimum, and every assignment on the way passes both the ledger and the check.
Proof.The stepper is the execution; each step's panel shows what the proposal checks and that it passes. In the final state:
- B2 and A5 are waiting with every input present. Each needs one output unit, and M's output holds two ingots, so freeout(M) = 0 and neither can start.
- The two ingots leave only into a waiting B. B3, B4 and B5 each need one input unit, and freein(M) = 0 (B2's ingot and A5's ore), so the ledger refuses them.
- No operation is running, and every A is assigned or done.
No transition is allowed. ∎
Steps 6 and 9 are where it happens. Each time, an A run and a B run are both ready and one output unit is free, and the A takes it. Nothing prefers the B. A start-order rule that did would be a rule about how this factory is wired, which is exactly what the invariant exists to avoid.
⊘ Theorem 2 · checking the start is not enough
The obvious repair is to put the start through the same check as an assignment, since that is where output is now taken. With coverage as the current doc defines it, that fails, through Observation 3.
With output reserved at the start, and both assignment and start checked against coverage as the current doc states it, the same factory with four plates locks.
Proof.Each step passes its checks, as shown. In the final state:
- A3 and A4 are waiting with their ore, and one output unit is free, so the ledger allows either start. After either start, B, which is needed for A2's ingot, would have no operation assigned and no free output unit, so the check refuses it.
- B2 needs one input unit; freein(M) = 0.
- Nothing is running.
No transition is allowed. ∎
Step 5 is the mistake and step 6 is where it shows. A4 is let in because B counts as covered by B1, but B1's run had already consumed its ingot. What B1 still held was an output unit, not the input unit A4 took. When the plate left, B's cover ended with no check, and the input half of B's headroom was already gone.
⊘ Theorem 3 · the current algorithm locks the same way
Observation 3 does not depend on the proposal. Under the current rule the waiting operations holding input can still always start (Lemma 2), so a lapse is usually harmless. It is not harmless when those waiting operations are short of an input only the uncovered recipe can make.
The current algorithm, unchanged, locks. One machine M with input 6 and output 3 carries out recipe A (1 ore → 1 ingot) and recipe B (1 coal + 2 ingots → 1 plate), with a work order for two plates. The precondition holds: one run each needs 4 input and 2 output.
Proof.Each assignment passes the ledger and the check, as shown. In the final state:
- B1 holds its coal and one ingot and needs a second ingot. B2 holds its coal and needs two ingots. Neither can start.
- Only an A makes ingots. A2, A3 and A4 each need one input unit, and freein(M) = 0, so the ledger refuses them.
- Nothing is running and nothing is held.
No transition is allowed. ∎
At exactly the minimum (input 4, output 2) this factory does not lock, because B2 does not fit the ledger. Capacity beyond the minimum, which the current doc says "buys parallelism", is what lets B2 take the input unit A needs. The same lock appears with two machines and three operations: M (input 3, output 2) carries out A and B, and N (input 3, output 1) carries out B only. B1 goes to M while A1 runs. When A1's ingot moves into B1, A needs M's input and B1 is holding it.
# Coverage counted in units
The repair for Observation 3 is to count what an operation holds, not the fact that it exists. The proposal also needs one more demand: a waiting operation must be able to start where it is.
What a unit is
A unit is one buffer slot: room for one component. A machine with input 6 has six input units. Recipe claims are counted the same way. A (1 ore → 1 ingot) needs 1 input unit and 1 output unit per run, and B (1 coal + 2 ingots → 1 plate) needs 3 input and 1 output.
The invariant's job is the same in both models: for every recipe the factory is waiting on, one run's worth of slots must be available. The models differ in what counts as available.
The old model: a yes or no per recipe
If any operation of A is assigned, A is covered, full stop. The check never asks what that operation is still holding. But an operation holds fewer slots as it goes:
| Moment | A1 holds on M | Old model says A is… |
|---|---|---|
| Assigned | 1 input + 1 output | covered |
| Run starts (ore consumed) | 1 output only; its input slot is released | covered |
| Ingot leaves | nothing; A1 is done | uncovered, suddenly |
In the middle row A counts as fully covered, but A1 holds only half of an A run's slots. The input slot it released is free, and the check lets anyone take it, because "A is covered". When the ingot leaves, A needs an input slot and may not find one. That is Theorem 3:
- 1A1 starts and releases its input slot.
- 2B1 and B2 take all six input slots. This is allowed, because A counts as covered by A1.
- 3A1's ingot leaves, and A needs an input slot. None is free, and B1 and B2 are waiting for ingots only A can make. The factory locks.
The new model: count the slots, per side, per machine
A run of A on M needs 1 input slot and 1 output slot. Each of those slots must be either free, or currently held by an operation of A on M. The same moment, after A1 starts:
| A's next run needs | Old model | New model |
|---|---|---|
| 1 output slot | covered: A1 is assigned | held by A1, so it counts |
| 1 input slot | covered: A1 is assigned | must stay free: A1 released it |
So B2 is refused, because it would take the input slot A's next run needs. There is no sudden drop: when an operation lets go of a slot, that same slot becomes free at the same moment, so it still counts toward the recipe.
The extra piece the proposal needs
Under the proposal, an operation that is assigned but has not started holds input slots and no output slots. It counts on the input side only. One run's worth of output slots must stay available on its machine so it can start: either free, or held by an earlier run of the same recipe there. Theorem 4 is what happens without it.
Formally
A waiting operation of R on M lends its input reservation to R's run on M.
Running and holding operations of R on M lend the output units they still hold: the run's reservation, then its held components. Write heldR(M) for their total. (Under the current rule a waiting operation's output reservation counts too.)
Choose a machine μ(R) that carries out R for each needed recipe R. On each machine M:
Each recipe is counted once per machine, even when both conditions hold.
So when it stops lending some units, it frees those same units, on the same machine, at the same moment. A cover that ends is traded for free capacity of the same size, and Observation 3 cannot happen.
A waiting operation of R on M can start only on M, so one run of R's output is kept there. It can be free, or held by R's own earlier runs. Several waiting operations of R on M share it, because they start one at a time.
⊘ Theorem 4 · counting units is not enough without checking the start
With output reserved at the start, coverage in units, and the check at assignment only, the following factory locks even when every run starts the moment it can. Machine M has input 4 and output 3 and carries out recipe A (1 ore → 2 ingots) and recipe B (3 ingots → 1 plate). The work order is for two plates. The buffers are exactly the precondition's minimum: input 1 + 3, output 2 + 1.
Proof.Each assignment passes the ledger and coverage in units, as shown. In the final state:
- B1 has all three ingots and needs one output unit; freeout(M) = 0 (three held ingots).
- Those ingots leave only into B2, which needs three input units; freein(M) = 1.
- Every A is done or holding, and nothing is running.
No transition is allowed. ∎
Step 7 takes the output unit B1 was keeping. A3 needs two units, two are free, and the ledger is the only thing asked. Under the amended rule this start is refused, and B1 starts instead.
≡ The amended rule
- 1Assign O to M when freein(M) ≥ |inO| and the factory would be covered in units afterwards, after O's source inputs arrive and the held components it needs depart to it. Otherwise refuse.
- 2Start O when its inputs have all arrived, freeout(M) ≥ |outO|, and the factory would be covered in units afterwards. Otherwise the run waits.
- 3Nothing else is checked. Nothing is reserved for unassigned work, nothing is assigned early, nothing is evicted, and refusal is the only action, as today.
∴ Theorem 5 · the invariant holds in every reachable state
Under the amended rule, the factory is covered in units in every reachable state.
Proof.By induction over transitions. In the initial state nothing is assigned, so the needed set is empty, nothing waits, and every demand is 0.
The needed set only grows at an assignment. The walk starts from assigned operations; only an assignment adds one. It follows a link only while one operation still has a kind to put out and another still needs it; starts, resolves and departures only remove such links. An operation that starts leaves the "not started" set. So after a start, a resolve or a departure, the needed set is a subset of what it was, and any choice μ restricted to it still fits: dropping a recipe only drops demand.
Assign, start: refused unless coverage in units holds afterwards.
Resolve O of R on M: the k units that go to the sink raise freeout(M) by k and lower heldR(M) by k, so R's output demand on M rises by at most k. Nothing else changes on any machine.
Departure of one component from M, made by an operation of R: freeout(M) rises by 1, heldR(M) falls by 1, demand rises by at most 1. The receiving operation's input was already reserved. If this was the operation's last component it is now done, and it has already stopped lending anything.
In every case the same μ still fits. ∎
This is the step the current doc's induction cannot make with coverage counted in operations. There, the event that ends a cover ("last output leaves") frees output units but ends a cover that also stood in for input units, which were released long before.
∎ Theorem 6 · the amended rule never locks
Safety is not liveness. A rule that refuses everything keeps any invariant, so Theorem 6 has to show that some transition is always allowed. It uses four assumptions, discussed in Open.
No recipe consumes, directly or through other recipes, a kind it makes. Recycling is the typical recipe cycle: offcuts from cutting smelted back into the ingots being cut (ingot → offcut → ingot).
This is about recipes, not machines. A work order that comes back to a machine it has already used is not a cycle in this sense, and is fully covered. That includes one machine carrying out A then B, or A on M, B on N, then C on M again. It is the shape that causes every lock on this page, and every example here has it.
Write R ≺ Q when a kind R makes is consumed by Q, or by a recipe that is ≺ Q. By A1 this is a strict partial order on recipes, whichever machines they run on.
Under A1–A4 and the precondition P, no reachable state of the amended rule is a lock. Every work order finishes.
Proof.Suppose S is reachable, some operation is not done, and no transition is allowed. By Theorem 5, S is covered in units; fix a choice μ that fits. Call a waiting operation full if all its inputs have arrived and short otherwise. Five facts about S first.
6.1 Nothing is running. A resolve is never refused.
6.2 Nothing held is needed by a waiting operation. It would have departed.
6.3 Conservation. For each kind κ that recipes make and consume: the κ held, plus the κ still to be made by planned, waiting and running operations, equals the κ still needed by planned and waiting operations. Every component made is either held or delivered, and by A2 the totals made and consumed are equal.
6.4 A start is refused only by its own recipe's output. If a full operation O of R waits on M, then some operation of R is holding output on M. Suppose not. Then heldR(M) = 0 and R waits on M, so R's output demand on M is |outR|, and freeout(M) covers it plus every other output demand: the ledger passes. Starting O takes |outR| free units. R's output demand drops by the same amount, since O now holds them. R's input demand on M can rise by |inR| only if μ(R) = M and O was the last of R waiting there, and then O's start has just freed |inR| input units on M. No other demand changes, and the needed set does not grow. The same μ fits, so the start is allowed — a contradiction.
6.5 An assignment is refused only by a waiting operation of the same recipe. Let C be a planned operation of Q that the walk reaches, with an input that exists. Then something of Q waits on μ(Q). Suppose not, and let M = μ(Q). Q's input demand on M is |inQ|, so the ledger passes. Once C is assigned it lends |inQ|: input demand drops by exactly what freein(M) drops. Q now waits on M, but Q's output demand on M was already counted, because μ(Q) = M. The walk already reached C, so the needed set does not grow. Each component that departs to C frees a unit where it was and raises demand there by at most one. The same μ fits, so the assignment is allowed — a contradiction.
Step 1: no waiting operation is short. Suppose one is. Pick a short O whose recipe RO is minimal under ≺ among short operations, and a kind κ it still needs. By 6.2 nothing holds κ, and by 6.1 nothing runs, so by 6.3 some planned or waiting operation makes κ. Its recipe is ≺ RO.
- A waiting operation makes κ. By minimality it is full, so by 6.4 an operation of its recipe holds output, and by A4 that output is κ. This contradicts 6.2.
- Only planned operations make κ. Let Q0 be one; the walk reaches it from O. While Qi has no input that exists, all its inputs are kinds made by recipes that nothing holds. Pick one; by 6.3 something planned or waiting makes it. A waiting maker is excluded as in case 1: it would hold that kind, which would then exist. So a planned Qi+1 makes it, the walk reaches it, and its recipe is ≺ that of Qi. Recipes strictly decrease, so the chain ends at some Qj with an input that exists. By 6.5 an operation of Qj's recipe waits on μ. By minimality it is full, so by 6.4 and A4 its recipe holds its one output kind. That kind is κ if j = 0, which contradicts 6.2. Otherwise it is the kind Qj−1 needs, which then exists — a contradiction.
Step 2: nothing is held. Suppose something is. Among the recipes of holding operations pick one, RP, maximal under ≺, with operation P holding a kind κ. By 6.2 no waiting operation needs κ, so by 6.3 a planned C needs it. C's input exists and the walk reaches C from P. By 6.5 an operation of C's recipe Q waits on μ(Q); by Step 1 it is full, so by 6.4 an operation of Q holds output. But RP ≺ Q, which contradicts the choice of RP.
Step 3: nothing waits. By Step 1 every waiting operation is full; by 6.4 it needs a holding operation; by Step 2 there is none.
Step 4: nothing is assigned, and yet an assignment is allowed. By 6.1 and Steps 2–3 every operation is planned or done, so every machine is empty and the needed set is empty. Pick a planned C whose recipe Q is minimal under ≺ among planned operations. By 6.3, any made kind C needs would have to be made by a planned operation of a recipe ≺ Q, and there is none. So all of C's inputs come from sources and exist. Assign C to the machine P chooses for Q. The ledger passes, and P's choice fits the result: on each machine the demand is at most P's claims there, less the |inQ| that C now lends. The assignment is allowed — a contradiction.
So S is not a lock. Every transition moves an operation or a component forward, so every execution is finite, and each ends with every operation done. ∎
The current rule, counted in units
The current rule, output reserved at assignment, with the refusal check counting coverage in units, never locks under A1–A4 and P.
Proof.Theorem 5 holds as before. A start needs no check, because it releases input and leaves output where it was. In Theorem 6, 6.4 becomes "a full waiting operation can always start" (Lemma 2), which makes Step 1 case 1 and Step 3 immediate. 6.5 gains an output side: C's assignment is refused only if something of Q waits on μ(Q) or an operation of Q holds output there, because either one can hold back the output ledger. In Step 1 case 2 and in Step 2, a waiting operation of Q leads to the same contradictions as before, and a holding one leads to them directly. Step 4 is unchanged. ∎
▶ Theorem 1's schedule, under the amended rule
The same factory, the same five plates, and the same order of requests as Theorem 1. The first eight steps are allowed as before. The start that locked the factory is refused, B2 starts instead, and all five plates are made.
Step 9 is the whole difference. Under the proposal as written, A4's start passes the ledger and nothing else is asked. Under the amendment, the start asks whether the factory is still covered afterwards, and it is not: B2 is waiting on M and keeping that output unit. The refusal has moved from assignment to the start, because the start is now where output is taken.
± What it buys, what it costs
| Press, machine P | 1 ore → 1 plate · input 2, output 2 |
| Weld, machine W | 2 plates → 1 frame · input 6, output 1 |
| Paint, machine T | 1 frame → 1 painted frame · input 1, output 1 |
| Work | three painted frames |
| Rule | Most welds gathering plates at once | States explored | Locks |
|---|---|---|---|
| Current rule | 1 | 108,404 | 0 |
| Current rule, coverage in units | 1 | 108,404 | 0 |
| Amended proposal | 3 | 189,696 | 0 |
Under the current rule the first weld assigned reserves W's only output unit. The second weld cannot be assigned, and its plates cannot be sent, until the first frame has left for Paint. Under the amended proposal W's input fills with the next two welds' plates while the first frame waits, and the one output unit serves them in turn.
Wherever output capacity, not input, is what holds back assignment. The gain grows with the number of inputs per run and how long they take to arrive.
Precondition P is unchanged. Output must still fit one run of each recipe a machine is the only home for, and runs of one recipe still pass through that output one at a time.
Every start runs the same predicate as an assignment, and a run with all its inputs present can be told to wait, as A4 was above. A player will sometimes see a machine idle with a full input buffer, waiting on its own output.
Coverage in units needs, per machine and recipe, the input units lent by waiting operations and the output units held by running and holding ones. These are counters, updated on the events that already update the ledger.
An operation pre-empted before its run starts holds no output under the proposal, so pre-empting it frees only input. The following assignment still goes through the check, as today.
Theorem 3 is a lock in the current algorithm, so the coverage wording should change whether or not output moves to the start. Corollary 7 is the current rule with that change alone.
⚙ Machine check
An explicit-state model checker implements the model on this page, and each rule is a switch in it. For each factory it explores every order of transitions, breadth first, and reports any reachable lock with the shortest trace that reaches it. It is a cross-check, not part of the proofs. Every stepper on this page was produced by replaying its events through the checker. The source is in checker.py.
| Rule | Factories with a lock | Factories fully explored |
|---|---|---|
| Current rule, as documented | 113 | 9,784 |
| Current rule, coverage in units (Corollary 7) | 0 | 9,779 |
| Proposal as written (Theorem 1) | 584 | 9,759 |
| Proposal, start checked (Theorem 2) | 913 | 9,771 |
| Proposal, coverage in units (Theorem 4) | 203 | 9,756 |
| Amended proposal (Theorems 5, 6) | 0 | 9,758 |
- Factories. 9,840 in all, generated at random: 2–4 recipes with no cycles, 1–2 input kinds each with counts 1–2, and an output count of 1–2. There are 1–3 machines, and each recipe is carried out by 1–2 of them. Buffers are sized from a random choice of one machine per recipe (so P holds), plus 0 or 1 spare unit per side. The work is balanced by kind, with 2–9 operations.
- Fully explored. Exploration stops at 40,000–60,000 states. Factories that hit the cap are left out of that rule's count.
- Outside A4. In 3,600 of the factories a recipe may also put out a second kind, and 193 of them use one. The amended proposal locked in none of these (0 of 3,599 explored).
- A different needed set. With recipes of operations that have already started kept in the needed set, the amended proposal still locked in 0 of 9,758.
- Runs starting the moment they can. Theorem 4's rule also locks when no ready run is ever held back: 4 of 600 factories.
? Open
- Routing restrictions (A3). With restrictions, needed entries are recipe × reach, and the choice μ must stay inside each entry's reach. Lemma 6.5 is where this bites: μ(Q) must be a machine the planned consumer can actually reach. Neither the proof nor the checker covers it.
- Recipes with several output kinds (A4). A4 is used once, in Step 1, to say that a maker's held output is the missing kind. The checker found no lock without it, but there is no proof.
- Recipe cycles (A1). A kind that is, directly or indirectly, an input to its own recipe, such as recycled offcuts, is outside the proof. Machines revisited by a work order are not recipe cycles and are covered.
- The cheap superset. A larger needed set refuses more. Whether it can lock by refusal is not covered here, under either rule.
- Eviction after a factory edit. Re-check coverage in units and evict until it holds. Theorems 5 and 6 start from any covered state, so they apply from there.
- The current doc. Independent of the proposal, Work Order Scheduling should count coverage in units (Theorem 3, Corollary 7).