The calculus and its five theorems

The previous chapters give guarantees about one isolated piece. This one takes them to the whole system, with every piece loading, unloading and interleaving.

For that it defines a lifecycle model with ten rules, and then lifts the comfortable assumptions one by one: that transitions are instantaneous, that they cannot be interrupted and that they never fail. Every relaxation answers to something that happens in real life, including the awkward part of what to do when a load fails halfway.

• Theorem 1 Preservation No rule can leave the system in a malformed state.
• Theorem 2 Exact recovery Removing a piece leaves the system as if that piece had never been there, even if others touched things in the meantime. And a removed piece leaves nothing behind, however it got to the end.
• Theorem 3 Ordering A piece only starts where its dependencies exist, and they keep existing for as long as it needs them.
• Theorem 4 Progress If there are no circular dependencies, the system does not deadlock and always reaches a resting state.
• Theorem 5 Confluence The one that gives the other four their meaning: order does not matter.

What confluence says

Add a piece, remove it, replace a provider, undo the replacement, interleave it all however you like. The final state the system reaches is the same one you would have got by writing the final configuration in one go from the start, never unloading anything.

What the theorem does not say

Two boundaries the paper marks, and which are worth not omitting when popularising it.

• Limit one Failures are outside Deliberately, because they are a real source of divergence. Whether something fails depends on the state it ran against, so one order can fail where another completes. In everything else the two states coincide, because a failed piece contributes nothing to the state.
• Limit two It talks about state, not about what was emitted A sent email does not come back by unmounting the piece that sent it.