hesela.devCALM theorem
The CALM theorem connects monotone queries with consistent, coordination-free distributed computation in a relational-transducer model.
Monotonicity: Adding input facts cannot invalidate an output fact already derived. This concerns program results, not increasing timestamps or the monotonic-reads session guarantee. [1]
Execution: The formal model uses connected networks and fair runs: nodes keep taking steps and buffered messages are eventually delivered. Coordination-free does not mean communication-free or that every node immediately knows the complete answer. [2]
Design: Proving reachability from received edges differs from declaring an object unreachable while edges may still arrive. Reclaiming tombstoned data can require later coordination even when foreground updates do not. [1]
Relations
Citations
- Hellerstein and Alvaro. Keeping CALM: When Distributed Consistency is Easy. arXiv:1901.01930v2 (2019), sections 1.3-2.2 and 3.4.
- Ameloot, Neven and Van den Bussche. Relational transducers for declarative networking. arXiv:1012.2858v1, sections 4-6.
Sources & caveats
- Source synthesis of the specified formal model and its engineering interpretation; not a runtime performance or fault-tolerance guarantee.