pith. machine review for the scientific record. sign in

arxiv: 2605.09114 · v1 · submitted 2026-05-09 · 💻 cs.DC

Recognition: 2 theorem links

· Lean Theorem

Light Cone Consistency: Toward a Unified Theory of Consistency in Message-Passing Systems

Rob Landers , Kaben Kramer
Authors on Pith no claims yet

Pith reviewed 2026-05-12 01:49 UTC · model grok-4.3

classification 💻 cs.DC
keywords distributed consistencymessage-passing systemscausal logsimpossibility theoremsCAP theoremfork resolutiontimelinesslight cone consistency
0
0 comments X

The pith

All consistency models reduce to configurations of three constraints on causal logs that form an entangled impossibility triangle.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper frames every distributed system as a message-passing setup whose observers each see a growing causal log. It defines Light Cone Consistency by three independent constraints on that visible sub-DAG—causal closure C(deps), fork resolution O(π), and timeliness R(δ)—plus a separate return-value function F. These parameters allow every one of the 50+ named models to be expressed as one of 85 concrete configurations. The central observation is that the three classic impossibility results each forbid exactly one pair of parameters, yet the parameters are fully entangled: any attempt to restore one constraint requires messages that are themselves subject to all three constraints. Consequently every system in active use must relax at least one parameter to operate.

Core claim

Our central result is the observation that these three constraints are fully entangled: violation of any one surface cascades to the other two, because restoring any parameter requires messages—and those messages are subject to all three constraints. The three parameters and their pairwise impossibility surfaces form a fully connected triangle. Every distributed system must exit the triangle by relaxing at least one parameter. The triangle activates only when the system is in use: C ≠ none, O ≠ trivial, or R ≠ absent each introduces a constraint that exposes the system to the surfaces.

What carries the argument

Light Cone Consistency framework: the triple of constraints causal closure C(deps), fork resolution O(π), and timeliness R(δ) applied to each observer's visible sub-DAG of the causal log, together with an orthogonal return-value function F.

If this is right

  • Every active system must relax at least one of the three parameters to avoid the impossibility surfaces.
  • The impossibility triangle is active precisely when any of the three constraints is non-trivial.
  • A system that imposes no constraints or writes far slower than propagation delay remains trivially linearizable.
  • The three impossibility results (CAP, FLP, AFC) are minimal and independent.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • New consistency guarantees could be obtained by enumerating the remaining unmapped configurations inside the triangle.
  • The entanglement implies that strengthening one parameter in practice often forces an unintended relaxation of another through added message traffic.
  • Systems that appear to satisfy two parameters may still be forced across the third surface by the messages required to maintain the first two.

Load-bearing premise

Every known consistency model can be expressed exactly as a configuration of the three constraints C(deps), O(π), R(δ) plus the return-value function F.

What would settle it

A consistency model that cannot be expressed as any of the 85 configurations of C, O, R, and F, or an impossibility result that does not align with exactly one of the three pairwise surfaces.

read the original abstract

Every distributed system -- databases, networks, postal services, CPU caches -- is a message-passing system. Every message-passing system is a growing causal log observed by a set of observers. We present Light Cone Consistency (LCC), a framework that describes every known consistency model as a configuration of three constraints on each observer's visible sub-DAG: causal closure $C(\mathrm{deps})$, fork resolution $O(\pi)$, and timeliness $R(\delta)$, plus an orthogonal return-value function $F$. We map 85 configurations, covering all 50+ named models from Viotti and Vukolic's taxonomy, with caveats for fork-based and probabilistic models. We show that three impossibility results of distributed computing -- CAP, FLP, and AFC -- each constrain exactly one pair of parameters, and prove they are minimal and independent. Our central result is the observation that these three constraints are fully entangled: violation of any one surface cascades to the other two, because restoring any parameter requires messages -- and those messages are subject to all three constraints. The three parameters and their pairwise impossibility surfaces form a fully connected triangle. Every distributed system must exit the triangle by relaxing at least one parameter. The triangle activates only when the system is in use: $C \neq \mathrm{none}$, $O \neq \mathrm{trivial}$, or $R \neq \mathrm{absent}$ each introduces a constraint that exposes the system to the surfaces. A system that demands nothing -- or writes far slower than its propagation delay -- is trivially linearizable. We identify open problems including a conjectured fourth surface (log locality), undiscovered constraints, and the universality of the safety-liveness fork as the consequence of crossing any boundary.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper presents Light Cone Consistency (LCC) as a unifying framework for consistency in message-passing systems. Every such system is modeled as a growing causal log observed by observers, with each observer's visible sub-DAG subject to three constraints—causal closure C(deps), fork resolution O(π), and timeliness R(δ)—plus an orthogonal return-value function F. The work maps 85 configurations that cover all 50+ named models in Viotti and Vukolić's taxonomy (with caveats for fork-based and probabilistic models), shows that the CAP, FLP, and AFC impossibility results each constrain exactly one pair of the three parameters, proves those results minimal and independent, and claims as its central result that the three constraints are fully entangled: violating any one cascades to the others because restoring a parameter requires messages that are themselves subject to all three, forming a fully connected triangle with the impossibility surfaces. Every system must exit the triangle by relaxing at least one parameter; the triangle is inactive only for trivial or extremely slow systems.

Significance. If the formal definitions of C, O, and R and the derivation of the cascade property can be supplied, the unification of 50+ models under three parameters plus the explicit linkage of CAP/FLP/AFC to pairwise surfaces would constitute a substantial conceptual contribution to distributed-systems theory. The explicit mapping of 85 configurations and the identification of open problems (conjectured fourth surface, universality of the safety-liveness fork) are concrete strengths that would remain valuable even if the entanglement claim requires refinement.

major comments (2)
  1. [Abstract (central result paragraph)] The central entanglement claim (abstract, final two paragraphs) is presented as an observation that follows from the definitions of C(deps), O(π), and R(δ) and from the 85 mapped configurations, yet no derivation steps, no explicit formal definitions of the three constraints, and no verification that the cascade is forced rather than assumed are supplied. Without these, it is impossible to determine whether the triangle closes necessarily or only under additional bridging assumptions (e.g., that every restoration must use messages subject to all three constraints simultaneously).
  2. [Abstract (mapping claim)] The claim that every known consistency model (including fork-based and probabilistic ones) can be expressed exactly as a configuration of C, O, R plus F (abstract) is asserted with only “minor caveats.” The weakest-assumption note indicates that the mapping may not be exact for all models; if any model requires an additional independent parameter, the asserted minimality and independence of the three impossibility results (and therefore the triangle) would be undermined. A concrete counter-example or a precise statement of the caveats is needed.
minor comments (2)
  1. [Abstract] The abstract is extremely dense; the three constraints and the return-value function F are introduced without even a one-sentence gloss, making the subsequent claims difficult to parse on first reading.
  2. [Abstract] No section or equation numbers are referenced in the provided text for the proofs of minimality and independence; adding explicit cross-references would improve traceability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback on the Light Cone Consistency framework. The two major comments identify opportunities to strengthen the exposition of the formal definitions and the scope of the mapping. We address each point below and will revise the manuscript accordingly to improve clarity while preserving the core claims.

read point-by-point responses

  1. Referee: [Abstract (central result paragraph)] The central entanglement claim (abstract, final two paragraphs) is presented as an observation that follows from the definitions of C(deps), O(π), and R(δ) and from the 85 mapped configurations, yet no derivation steps, no explicit formal definitions of the three constraints, and no verification that the cascade is forced rather than assumed are supplied. Without these, it is impossible to determine whether the triangle closes necessarily or only under additional bridging assumptions (e.g., that every restoration must use messages subject to all three constraints simultaneously).

    Authors: We agree that the abstract presents the entanglement at a high level and that explicit derivation steps would strengthen the presentation. The full manuscript supplies formal definitions of C(deps), O(π), and R(δ) in Section 3 and derives the cascade in Section 5 by showing that restoration of any parameter occurs via messages that are themselves governed by the same three constraints under the message-passing model. To address the concern directly, we will insert a new subsection 'Derivation of Entanglement' that enumerates the logical steps: (1) any restoration action requires a message, (2) every message is subject to C, O, and R by definition of the causal log, and (3) therefore violation of one surface forces consideration of the others. This will demonstrate that the cascade follows necessarily from the model without extra bridging assumptions. revision: yes

  2. Referee: [Abstract (mapping claim)] The claim that every known consistency model (including fork-based and probabilistic ones) can be expressed exactly as a configuration of C, O, R plus F (abstract) is asserted with only “minor caveats.” The weakest-assumption note indicates that the mapping may not be exact for all models; if any model requires an additional independent parameter, the asserted minimality and independence of the three impossibility results (and therefore the triangle) would be undermined. A concrete counter-example or a precise statement of the caveats is needed.

    Authors: The caveats are confined to two families and do not introduce a fourth independent parameter. Fork-based models are accommodated by allowing O(π) to take values that leave forks unresolved; probabilistic models are accommodated by interpreting R(δ) as a probabilistic bound rather than a deterministic one. Both remain within the existing three-dimensional space. In the revision we will replace the abstract phrase 'with caveats for fork-based and probabilistic models' with the explicit statement: 'with the exception of fork-based models (e.g., fork-consistency variants) captured by non-resolving O(π) and probabilistic models (e.g., probabilistic eventual consistency) captured by relaxed R(δ)'. We will also add a short appendix listing the 85 configurations and identifying the affected models. No counter-example requiring an independent fourth parameter appears in the mapping. revision: yes

Circularity Check

1 steps flagged

Entanglement claim reduces to definitional property of message-passing systems

specific steps
  1. self definitional [Abstract (central result paragraph)]
    "Our central result is the observation that these three constraints are fully entangled: violation of any one surface cascades to the other two, because restoring any parameter requires messages—and those messages are subject to all three constraints. The three parameters and their pairwise impossibility surfaces form a fully connected triangle."

    The cascade is justified solely by the clause that restoring parameters requires messages subject to all three constraints. Because the paper's foundational premise is that every distributed system is a message-passing system whose observers see sub-DAGs governed by precisely C, O, and R, any restoration step is definitionally subject to the same three constraints. The full entanglement and the closed triangle are therefore logical consequences of the modeling assumptions rather than a derived property of the 85 mappings or the impossibility proofs.

full rationale

The paper defines all systems as message-passing causal logs under exactly the three constraints C(deps), O(π), R(δ) plus F, maps 85 configurations to known models, associates CAP/FLP/AFC to parameter pairs, and proves those pairs minimal and independent. The central result then asserts full entanglement via a cascade whose sole justification is that restoring any parameter requires messages subject to all three constraints. This justification is entailed by the initial modeling choice that every system is a message-passing system whose every message is governed by C, O, and R; no independent derivation from the impossibility mappings or the configuration table is supplied. The triangle therefore follows by construction from the framework's premises rather than from additional reasoning.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The framework rests on the domain assumption that every distributed system is a message-passing system whose state can be represented as a growing causal log visible to observers; the three constraints and the return-value function are introduced as the complete set of primitives.

axioms (1)
  • domain assumption Every distributed system is a message-passing system whose history is a growing causal log observed by a set of observers.
    Stated in the first sentence of the abstract.
invented entities (1)
  • Light Cone Consistency framework no independent evidence
    purpose: Unified description of consistency models via three constraints on observer-visible sub-DAGs
    Newly introduced in the paper; no independent evidence outside the framework itself.

pith-pipeline@v0.9.0 · 5616 in / 1412 out tokens · 46720 ms · 2026-05-12T01:49:47.559363+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

30 extracted references · 30 canonical work pages

  1. [1]

    A framework for consistency models in distributed systems

    Paulo S\' e rgio Almeida. A framework for consistency models in distributed systems. arXiv:2411.16355 , 2024. URL: https://arxiv.org/abs/2411.16355

    work page arXiv 2024

  2. [2]

    Ameloot, Frank Neven, and Jan Van den Bussche

    Tom J. Ameloot, Frank Neven, and Jan Van den Bussche. Relational transducers for declarative networking. Journal of the ACM , 60(2):15:1--15:38, 2013. https://doi.org/10.1145/2450142.2450151 doi:10.1145/2450142.2450151

    work page doi:10.1145/2450142.2450151 2013

  3. [3]

    Specification and complexity of collaborative text editing

    Hagit Attiya, Sebastian Burckhardt, Alexey Gotsman, Adam Morrison, Hongseok Yang, and Marek Zawirski. Specification and complexity of collaborative text editing. In ACM Symposium on Principles of Distributed Computing (PODC) , pages 259--268, 2016

    work page 2016

  4. [4]

    Arbitration-free consistency is available (and vice versa)

    Hagit Attiya, Constantin Enea, and Enrique Rom\' a n-Calvo. Arbitration-free consistency is available (and vice versa). Proc. ACM Program. Lang. , 10(POPL):1183--1211, 2026. Article 41

    work page 2026

  5. [5]

    Michael, and Martin Vechev

    Hagit Attiya, Rachid Guerraoui, Danny Hendler, Petr Kuznetsov, Maged M. Michael, and Martin Vechev. Laws of order: Expensive synchronization in concurrent algorithms cannot be eliminated. In 38th ACM Symposium on Principles of Programming Languages (POPL) , pages 487--498, 2011

    work page 2011

  6. [6]

    Are wait-free algorithms fast? Journal of the ACM , 41(4):725--763, 1994

    Hagit Attiya, Nancy Lynch, and Nir Shavit. Are wait-free algorithms fast? Journal of the ACM , 41(4):725--763, 1994

    work page 1994

  7. [7]

    Another advantage of free choice: Completely asynchronous agreement protocols

    Michael Ben-Or. Another advantage of free choice: Completely asynchronous agreement protocols. In ACM Symposium on Principles of Distributed Computing (PODC) , pages 27--30, 1983

    work page 1983

  8. [8]

    Luca Bombelli, Joohan Lee, David Meyer, and Rafael D. Sorkin. Space-time as a causal set. Physical Review Letters , 59(5):521--524, 1987

    work page 1987

  9. [9]

    Engineered simultaneity: The physical impossibility of consolidated price discovery across spacelike-separated exchanges

    Paul Borrill. Engineered simultaneity: The physical impossibility of consolidated price discovery across spacelike-separated exchanges. arXiv:2602.22350 , 2026. URL: https://arxiv.org/abs/2602.22350

    work page arXiv 2026

  10. [10]

    Principles of eventual consistency

    Sebastian Burckhardt. Principles of eventual consistency. Foundations and Trends in Programming Languages , 1(1--2):1--150, 2014

    work page 2014

  11. [11]

    Bergstra

    Mark Burgess and Jan A. Bergstra. Promise Theory: Principles and Applications . 2014

    work page 2014

  12. [12]

    Concerning the size of logical clocks in distributed systems

    Bernadette Charron-Bost. Concerning the size of logical clocks in distributed systems. Information Processing Letters , 39(1):11--16, 1991

    work page 1991

  13. [13]

    Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, J

    James C. Corbett, Jeffrey Dean, Michael Epstein, Andrew Fikes, Christopher Frost, J. J. Furman, Sanjay Ghemawat, Andrey Gubarev, Christopher Heiser, Peter Hochschild, et al. Spanner: G oogle's globally-distributed database. In 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI) , pages 251--264, 2012

    work page 2012

  14. [14]

    Dynamo: A mazon's highly available key-value store

    Giuseppe DeCandia, Deniz Hastorun, Madan Jampani, Gunavardhan Kakulapati, Avinash Lakshman, Alex Pilchin, Swaminathan Sivasubramanian, Peter Vosshall, and Werner Vogels. Dynamo: A mazon's highly available key-value store. In 21st ACM Symposium on Operating Systems Principles (SOSP) , pages 205--220, 2007. https://doi.org/10.1145/1294261.1294281 doi:10.114...

    work page doi:10.1145/1294261.1294281 2007

  15. [15]

    Fischer, Nancy A

    Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM , 32(2):374--382, 1985. https://doi.org/10.1145/3149.214121 doi:10.1145/3149.214121

    work page doi:10.1145/3149.214121 1985

  16. [16]

    Making sense of relativistic distributed systems

    Seth Gilbert and Wojciech Golab. Making sense of relativistic distributed systems. In 28th International Symposium on Distributed Computing (DISC) , volume 8784 of LNCS , pages 361--375, 2014

    work page 2014

  17. [17]

    Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services,

    Seth Gilbert and Nancy Lynch. Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News , 33(2):51--59, 2002. https://doi.org/10.1145/564585.564601 doi:10.1145/564585.564601

    work page doi:10.1145/564585.564601 2002

  18. [18]

    The LAW theorem: Local reads and linearizable asynchronous replication

    Emmanouil Giortamis, Antonios Katsarakis, Vasilis Gavrielatos, Pramod Bhatotia, Aleksandar Dragojevic, Boris Grot, Vijay Nagarajan, and Panagiota Fatourou. The LAW theorem: Local reads and linearizable asynchronous replication. Proceedings of the VLDB Endowment , 18(9):2831--2845, 2025. https://doi.org/10.14778/3746405.3746411 doi:10.14778/3746405.3746411

    work page doi:10.14778/3746405.3746411 2025

  19. [19]

    Proving PACELC

    Wojciech Golab. Proving PACELC . ACM SIGACT News , 49(1):73--81, 2018

    work page 2018

  20. [20]

    Hellerstein and Peter Alvaro

    Joseph M. Hellerstein and Peter Alvaro. Keeping CALM : When distributed consistency is easy. Communications of the ACM , 63(9):72--81, 2020

    work page 2020

  21. [21]

    Junqueira, and Benjamin Reed

    Patrick Hunt, Mahadev Konar, Flavio P. Junqueira, and Benjamin Reed. ZooKeeper : Wait-free coordination for internet-scale systems. In USENIX Annual Technical Conference , 2010

    work page 2010

  22. [22]

    Time, clocks, and the ordering of events in a distributed system

    Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM , 21(7):558--565, 1978. https://doi.org/10.1145/359545.359563 doi:10.1145/359545.359563

    work page doi:10.1145/359545.359563 1978

  23. [23]

    Lower bounds for asynchronous consensus

    Leslie Lamport. Lower bounds for asynchronous consensus. Distributed Computing , 19(2):104--125, 2006

    work page 2006

  24. [24]

    Freedman, Michael Kaminsky, and David G

    Wyatt Lloyd, Michael J. Freedman, Michael Kaminsky, and David G. Andersen. Don't settle for eventual: Scalable causal consistency for wide-area storage with COPS . In 23rd ACM Symposium on Operating Systems Principles (SOSP) , pages 401--416, 2011. https://doi.org/10.1145/2043556.2043593 doi:10.1145/2043556.2043593

    work page doi:10.1145/2043556.2043593 2011

  25. [25]

    Building secure file systems out of B yzantine storage

    David Mazi\` e res and Dennis Shasha. Building secure file systems out of B yzantine storage. In ACM Symposium on Principles of Distributed Computing (PODC) , pages 108--117, 2002

    work page 2002

  26. [26]

    In search of an understandable consensus algorithm

    Diego Ongaro and John Ousterhout. In search of an understandable consensus algorithm. In USENIX Annual Technical Conference (ATC) , pages 305--320, 2014

    work page 2014

  27. [27]

    Detecting causal relationships in distributed computations: In search of the holy grail

    Reinhard Schwarz and Friedemann Mattern. Detecting causal relationships in distributed computations: In search of the holy grail. Distributed Computing , 7(3):149--174, 1994

    work page 1994

  28. [28]

    Conflict-free replicated data types

    Marc Shapiro, Nuno Pregui c a, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS) , pages 386--400, 2011. https://doi.org/10.1007/978-3-642-24550-3_29 doi:10.1007/978-3-642-24550-3_29

    work page doi:10.1007/978-3-642-24550-3_29 2011

  29. [29]

    Consistency in non-transactional distributed storage systems

    Paolo Viotti and Marko Vukoli\' c . Consistency in non-transactional distributed storage systems. ACM Computing Surveys , 49(1), 2016

    work page 2016

  30. [30]

    Design and evaluation of a conit-based continuous consistency model for replicated services

    Haifeng Yu and Amin Vahdat. Design and evaluation of a conit-based continuous consistency model for replicated services. ACM Transactions on Computer Systems , 20(3):239--282, 2002

    work page 2002