Pith. sign in

REVIEW 3 major objections 5 minor 64 references

A Framework for Consistency Models in Distributed Systems

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Pith's one-line read This paper proves that in asynchronous distributed systems, every wait-free implementation of practically any data abstraction admits histories that cannot satisfy closed past, local visibility, arbitration, and monotonic visibility at…

desk verdict The CLAM proof is coherent, but the advertised scope — 'practically all' data abstractions — rests on an unproven classification; the framework itself is still a genuinely useful contribution. read the letter →

arxiv 2411.16355 v1 pith:X3TPHWPV submitted 2024-11-25 cs.DC

classification cs.DC MSC 68M1468Q85
keywords consistencymodelsdistributedsystemswait-freeimplementationsCALtrilemmaCAPtheoremcausalconvergencearbitration
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Distributed systems that must answer queries while partitioned cannot keep all strong consistency guarantees, and this paper explains exactly which guarantees collide. It builds a general axiomatic framework—pairing per-process serializations with a global visibility relation—and isolates four basic axioms: monotonic visibility, local visibility, closed past, and arbitration. Its main theorem, CLAM, states that for any wait-free implementation of practically any data abstraction, some history cannot be explained by an execution satisfying all four axioms simultaneously. Because monotonic visibility is treated as non-negotiable, the result becomes the CAL trilemma: an available partition-tolerant system must give up closed past, local visibility, or arbitration. This matters because it transforms the vague tradeoff of the CAP theorem into a precise design space for replicated data stores.

What carries the argument

The argument turns on the notion of an irredundant pair of updates (Definition 40) and the physical realizability axiom. Two updates are irredundant when no valid execution can make one visible to the local viewers of the other, before the already-visible update, without violating result validity; examples are two increments to a counter or two enqueues to a queue. This property guarantees that 'phantom' visibility edges—edges that add no information—cannot be used to paper over the missing information flow of a partition. The physical realizability axiom ($\mathrm{vispr}$) rules out visibility that would let information travel backward along a process's program order, while still permitting cycles needed by synchronization abstractions such as barriers and consensus. Together these two ingredients force the contradiction in the CLAM proof: a partition, wait-freedom, and the four axioms combine to demand a visibility edge that irredundance says must change a query's result.

What would settle it

Exhibit a data type with an irredundant pair of updates and a wait-free implementation whose every finite two-process history—including the partition history constructed in the proof, with one update and subsequent queries per process—can be explained by a valid execution satisfying closed past, local visibility, arbitration, and monotonic visibility. A mechanical search over small such histories for a counter or queue would either produce the violating history predicted by CLAM or, if none exists, give evidence that the theorem's premise needs re-examination.

Watch

Extended reading notes

Core claim

The paper's central claim is Theorem 1 (CLAM): in an asynchronous distributed system with at least two processes, any wait-free implementation of a data abstraction with an irredundant pair of updates admits a history that no valid execution can explain while simultaneously satisfying Closed past, Local visibility, Arbitration, and Monotonic visibility. The proof isolates two processes under a partition that lasts the whole history; wait-freedom forces each process's queries to return from its own local events alone. Any execution explaining the whole history must then satisfy local visibility (each process sees its own update), arbitration (both processes order the two updates the same way), and closed past (once one process's update is visible to the other's queries, the other update must be visible too), which forces one update into the other side's visible set and breaks result validity because the updates are irredundant. Since monotonic visibility is argued to be too fundamental to sacrifice, the corollary is the CAL trilemma: closed past, arbitration, or local visibility must be forgone in any wait-free highly available system. The paper positions this as practically stronger than the CAP theorem, which only rules out linearizability for a single register; CLAM rules out a much weaker combination for almost all data types, with the single register as the identified exception.

Load-bearing premise

The theorem only covers data abstractions that have an irredundant pair of updates, and the paper does not prove a general characterization of that property; for an abstraction without such a witness history, such as the single register, CLAM simply does not apply.

Editorial extensions

If this is right

  • Any partition-tolerant, always-available system using a data type with irredundant updates must, on at least one history, violate one of closed past, local visibility, or arbitration; a system that appears to satisfy all three is either not wait-free or not actually using such a data type.
  • Convergent causal consistency survives the trilemma: data types with concurrent specifications, such as CRDTs, can converge without arbitration, so they can be wait-free while keeping local visibility and closed past.
  • The two available ways to converge through arbitration are precisely the two families the paper defines: replay consistency, which keeps local visibility and drops closed past, and prefix consistency, which keeps closed past and drops local visibility.
  • Classic axiomatic definitions of PRAM and causal memory are weaker than their intended behavior and admit physically impossible causality loops; the physical realizability axiom repairs them uniformly.
  • The single register is a genuine exception: it can be wait-free and sequentially consistent, but sequential consistency for one register does not compose to memory, so the exception does not restore the CAP-era picture.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the theorem is right, designers of 'strongly consistent' AP data stores can use the four axioms as an audit checklist: for any finite partition history, at least one axiom must be visibly broken, and the proof predicts precisely where to look.
  • A natural next step the paper leaves open is a full characterization of irredundance; one testable conjecture is that data types whose updates form a join-semilattice or have an overriding zero element are exactly those outside the theorem's reach, with the single register as the prototype.
  • Treating convergence as a safety property with universal quantification over executions, rather than as eventual consistency, suggests that verification tools for replicated types should check convergence against all valid executions of a history, not just one witness execution.
  • An empirical check of the theorem's mechanism would be to run a wait-free counter or queue under a simulated permanent partition and track each side's query results; the recorded history should be unexplainable by any execution satisfying closed past, local visibility, arbitration, and monotonic visibility, showing concretely which axiom the system sacrifices.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper presents an axiomatic, timeless framework for consistency models in asynchronous distributed systems, combining a global visibility relation with per-process serializations. It introduces well-formedness axioms (physical realizability, serialization of visibility), basic consistency axioms (monotonic visibility, local visibility, closed past), and derives serial, pipelined, causal, replay, and prefix consistency models. It defines convergence and arbitration as safety properties and proves the CLAM theorem: in asynchronous systems with at least two processes, no wait-free implementation of a data abstraction with irredundant updates can satisfy closed past, local visibility, arbitration, and monotonic visibility simultaneously, yielding the CAL trilemma. The paper also revisits PRAM and causal memory, presenting corrections to prior axiomatic specifications, and offers a taxonomy of consistency models.

Significance. If the framework and proof are accepted, this is a valuable contribution: it generalizes classic consistency frameworks in several orthogonal dimensions and provides a more refined impossibility statement than CAP for AP systems, with a short proof and a clear design-space taxonomy. The framework itself is a genuine contribution, and several parts, such as the physical realizability axiom and the treatment of convergence as a safety property, are well motivated. The main weakness is that the breadth of the central theorem is not established: the irredundance property is existential and only illustrated, so the advertised "practically all data abstractions" scope is currently a claim rather than a proved result.

major comments (3)
  1. [§9.1, Definition 40; §1 and Abstract] Definition 40 makes "irredundant pair" an existential property over witness histories, and the paper asserts without proof that this holds for practically all abstractions and that the single register is the only exception. Since Theorem 1 quantifies over exactly this class, the CAL trilemma inherits the unproven classification. The examples (counter, queue, set, memory) are plausible, but no syntactic criterion or general argument is given. Please add a theorem characterizing irredundance (e.g., for operations that are non-commutative or affect distinct locations) or explicitly narrow the abstract, introduction, and conclusions to the verified class.
  2. [§9.2, proof of Theorem 1] The proof assumes that the irredundancy witness history has exactly one update at each of two processes and one or more queries after each update, under a partition lasting the whole history. Definition 40 only guarantees existence of some witness history for a pair of updates; it does not guarantee a witness of this two-process partition shape. A lemma is needed showing that any irredundant pair has such a witness history, or Definition 40 must be reformulated to include the shape used in the proof. Without this, Theorem 1 may apply only to a subclass of the abstractions for which it is claimed.
  3. [§9.1, Definition 40] The term "update" is not formally defined, although the framework allows operations that are both queries and updates (e.g., dequeue or pop) and concurrent specifications. All examples of irredundant pairs are pure updates. To make the theorem's scope checkable for a given abstraction, the paper should define updates for arbitrary sequential and concurrent specifications and prove the irredundance examples, including operations with both query and update effects.
minor comments (5)
  1. [§9.2, Theorem 1] The proof never uses monotonic visibility, so the theorem could be stated without M (making it stronger) or the role of M in the CAL framing should be explained explicitly.
  2. [Definitions 26 and 27] The headings contain typos: "Seqential Consistency" and "Set-Seqential Consistency" should be "Sequential Consistency" and "Set-Sequential Consistency".
  3. [Figure 16] The border-color encoding for satisfied axioms (red/blue/green) is not accessible in grayscale; please add textual labels or a legend that does not rely on color alone.
  4. [Section 1, Introduction] The phrase "This is appealing but mat be limiting" contains a typo; it should read "may be limiting".
  5. [Section 6 and Table 3] The model "convergent causal consistency" appears in Table 3 and in the text without a numbered definition; please clarify whether it is defined as causality plus convergence or as serial causal consistency plus convergence.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the CLAM theorem is a conditional impossibility proof built on the paper's own irredundance definition, not a reduction to its inputs; the main weakness is the unsupported breadth of the 'practically all abstractions' claim, which is a scope gap rather than a circular step.

full rationale

The central derivation is not circular. Theorem 1 (CLAM) is a conditional impossibility statement: it assumes wait-freedom, a partition, and the existence of an irredundant pair of updates (Definition 40), then derives that any execution satisfying Closed past, Local visibility, Arbitration, and Monotonic visibility would need extra visibility edges across the partition, which Definition 40 then says would contradict result validity. The proof is a real derivation from the axioms and the semantic property of irredundance; it does not equate the theorem's conclusion with its hypothesis by construction. No fitted parameter is renamed as a prediction, and no load-bearing uniqueness theorem from prior work is imported. The paper does cite the author's own earlier work ([8], [9], [60]), but only for terminology, counter-implementation context, and CRDT discussion; none of these citations carries the CLAM proof. The genuine caveat is scope, not circularity: the paper asserts 'it applies to practically all abstractions, where not every operation overrides every other operation; the single register was the only counter-example we have found' (Section 9.2), but it supplies examples rather than a characterization or proof that most data abstractions have irredundant updates. That is an evidentiary and generality gap, appropriately weighed as a correctness risk, not as a circular step.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

No free parameters are fitted to data. The central theorem rests on domain assumptions about asynchronous distributed systems and wait-free termination, plus the author's physical realizability and irredundance axioms. The framework introduces no new physical entities; terms like phantom visibility are analytical devices, not posited objects.

assumptions (7)
  • domain assumption A distributed history is a family of totally ordered per-process sequences; the next operation of a process starts only after the previous one returns.
    Section 2.1, Definition 1. This underpins program order and the physical realizability axiom; it excludes processes with multiple outstanding operations.
  • ad hoc to paper Operation effects are atomic: an operation is the basic unit of computation and its effects become visible as a whole.
    Section 2.2, discussion before Definition 5. Needed to define physical realizability and to make the CLAM proof's local executions well-defined.
  • ad hoc to paper Physical realizability: a hb b implies not b po a.
    Definition 5, vispr. This is the paper's proposed well-formedness criterion; it rejects causality loops that cross program order while allowing cross-process visibility cycles.
  • ad hoc to paper Serialization of visibility: a vis b_i implies a ser_i b_i.
    Definition 6, servis. Connects the visibility relation to each process's serialization.
  • domain assumption Wait-free operations terminate in finite steps without depending on messages from other processes, even during a partition.
    Section 9, used in Theorem 1 to assert that local queries during a partition return using only local information.
  • ad hoc to paper For a data abstraction covered by CLAM, there exists an irredundancy witness history for some pair of updates.
    Definition 40. This existential scope condition is load-bearing for the theorem; the paper gives examples but no general proof that practically all abstractions satisfy it.
  • standard math Set-theoretic relations, transitive closure, and total orders are used as standard background.
    Throughout the definitions of hb, ser_i, vis, and the proofs.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Framework for Consistency Models in Distributed Systems." pith.science (2026). https://pith.science/paper/X3TPHWPV

@misc{pith2026241116355,
  author       = {Pith},
  title        = {Pith review of: A Framework for Consistency Models in Distributed Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/X3TPHWPV}},
  note         = {Machine review of arXiv:2411.16355}
}
read the original abstract

We define am axiomatic timeless framework for asynchronous distributed systems, together with well-formedness and consistency axioms, which unifies and generalizes the expressive power of current approaches. 1) It combines classic serialization per-process with a global visibility. 2) It defines a physical realizability well-formedness axiom to prevent physically impossible causality cycles, while allowing possible and useful visibility cycles, to allow synchronization-oriented abstractions. 3) Allows adding time-based constraints, from a logical or physical clock, either partially or totally ordered, in an optional and orthogonal way, while keeping models themselves timeless. 4) It simultaneously generalizes from memory to general abstractions, from sequential to concurrent specifications, either total or partial, and beyond serial executions. 5) Defines basic consistency axioms: monotonic visibility, local visibility, and closed past. These are satisfied by what we call serial consistency, but can be used as building blocks for novel consistency models with histories not explainable by any serial execution. 6) Revisits classic pipelined and causal consistency, revealing weaknesses in previous axiomatic models for PRAM and causal memory. 7) Introduces convergence and arbitration as safety properties for consistency models, departing from the use of eventual consistency, which conflates safety and liveness. 8) Formulates and proves the CLAM theorem for asynchronous distributed systems: any wait-free implementation of practically all data abstractions cannot simultaneously satisfy Closed past, Local visibility, Arbitration, and Monotonic visibility. While technically incomparable, the CLAM theorem is practically stronger than the CAP theorem, as it allows reasoning about the design space and possible tradeoffs in highly available partition tolerant systems.

Figures

Figures reproduced from arXiv: 2411.16355 by the authors.

Figure 1
Figure 1. Three multi-threaded programs; x and y are shared variables, l1 and l2 local variables. (a) reads can [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Operations from each process from left to right. Well-formedness of visibility relations according to [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Past and future light cones of event 𝑜, space-like and time-like intervals. must satisfy. The stronger the consistency model, the more constrained those relations. For the remainder of the article we only consider valid executions, unless otherwise stated. 3 TIME AND CONSISTENCY MODELS Most classic consistency models (Cache, Processor, Pipelined, Causal, and Sequential Consistency) do not refer to time, and can be s… view at source ↗
Figures from the paper (16 more)
Figure 4
Figure 4. Figure 4: Causal broadcast implemented by buffering messages with missing dependencies; abstraction events: [PITH_FULL_IMAGE:figures/full_fig_p016_4.png]
Figure 5
Figure 5. Figure 5: Candidate executions are checked: first for validity ( [PITH_FULL_IMAGE:figures/full_fig_p017_5.png]
Figure 6
Figure 6. Figure 6: Operation 𝑎 can be visible to 𝑏 only if clock 𝐶(𝑎) at start of 𝑎 is less than clock 𝐶 ′ (𝑏) at completion of 𝑏, whether for logical or physical clocks, either partially or totally ordered. 𝐿(𝑜), and when it completes, 𝐿 ′ (𝑜). As illustrated by [PITH_FULL_IMAGE:figure…
Figure 7
Figure 7. Figure 7: Examples about basic visibility axioms, considering a single counter object. Operations from each [PITH_FULL_IMAGE:figures/full_fig_p019_7.png]
Figure 8
Figure 8. Figure 8: Example without closed past considering a queue object. Operations from each process placed in [PITH_FULL_IMAGE:figures/full_fig_p020_8.png]
Figure 9
Figure 9. Figure 9: Example satisfying basic axioms but not serial consistency, considering a stack object. Operations [PITH_FULL_IMAGE:figures/full_fig_p022_9.png]
Figure 10
Figure 10. Figure 10: Monotonic visibility: subsequent operations to [PITH_FULL_IMAGE:figures/full_fig_p023_10.png]
Figure 11
Figure 11. Figure 11: History acceptable by the PRAM axiomatic specification but not the original operational definition, [PITH_FULL_IMAGE:figures/full_fig_p024_11.png]
Figure 12
Figure 12. Figure 12: History acceptable by the causal memory specification, where the final read of each process can only [PITH_FULL_IMAGE:figures/full_fig_p026_12.png]
Figure 13
Figure 13. Figure 13: Executions a) with a counter, convergent; b) a queue, with closed past, not convergent); c) alternative [PITH_FULL_IMAGE:figures/full_fig_p027_13.png]
Figure 14
Figure 14. Figure 14: Executions vacuously satisfying convergence, for queue and stack, with closed past. Operations from [PITH_FULL_IMAGE:figures/full_fig_p029_14.png]
Figure 15
Figure 15. Figure 15: Executions satisfying serial consistency and either (a) satisfying arbitration or (b) not satisfying [PITH_FULL_IMAGE:figures/full_fig_p033_15.png]
Figure 16
Figure 16. Figure 16: A taxonomy of consistency axioms (dashed border) and models (solid border), partially ordered [PITH_FULL_IMAGE:figures/full_fig_p037_16.png]
Figure 17
Figure 17. Figure 17: History only explainable by a per-operation serialization, allowing an infinite sequence of apparently [PITH_FULL_IMAGE:figures/full_fig_p041_17.png]
Figure 18
Figure 18. Figure 18: Convergent execution through last-write-wins. Whatever the value of [PITH_FULL_IMAGE:figures/full_fig_p044_18.png]
Figure 19
Figure 19. Figure 19: Execution for concurrent set data type where [PITH_FULL_IMAGE:figures/full_fig_p046_19.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

64 extracted references · 34 canonical work pages

  1. [1]

    Consistency Tradeoffs in Modern Distributed Database System Design: CAP is Only Part of the Story

    D. Abadi. “Consistency Tradeoffs in Modern Distributed Database System Design: CAP is Only Part of the Story”. In: Computer 45.2 (2012), pp. 37–42. doi: 10.1109/MC.2012.33

  2. [2]

    Shared Memory Consistency Models: A Tutorial

    S. V. Adve and K. Gharachorloo. “Shared Memory Consistency Models: A Tutorial”. In: Computer 29.12 (1996), pp. 66–76. doi: 10.1109/2.546611

  3. [3]

    Weak Ordering - A New Definition

    S. V. Adve and M. D. Hill. “Weak Ordering - A New Definition”. In: Proceedings of the 17th Annual International Symposium on Computer Architecture, Seattle, W A, USA, June 1990. Ed. by J. Baer, L. Snyder, and J. R. Goodman. ACM, 1990, pp. 2–14. doi: 10.1145/325164.325100

  4. [4]

    The Power of Processor Consistency

    M. Ahamad, R. A. Bazzi, R. John, P. Kohli, and G. Neiger. “The Power of Processor Consistency”. In: Proceedings of the 5th Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA ’93, Velen, Germany, June 30 - July 2,

  5. [5]

    Causal Memory: Definitions, Implementation, and Programming

    M. Ahamad, G. Neiger, J. E. Burns, P. Kohli, and P. W. Hutto. “Causal Memory: Definitions, Implementation, and Programming”. In: Distributed Comput. 9.1 (1995), pp. 37–49. doi: 10.1007/BF01784241

  6. [6]

    A formal hierarchy of weak memory models

    J. Alglave. “A formal hierarchy of weak memory models”. In: Formal Methods Syst. Des. 41.2 (2012), pp. 178–210. doi: 10.1007/S10703-012-0161-5

  7. [7]

    Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory

    J. Alglave, L. Maranget, and M. Tautschnig. “Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory”. In: ACM Trans. Program. Lang. Syst. 36.2 (2014), 7:1–7:74. doi: 10.1145/2627752

  8. [8]

    Approaches to Conflict-free Replicated Data Types

    P. S. Almeida. “Approaches to Conflict-free Replicated Data Types”. In: ACM Comput. Surv. 57.2 (Nov. 2024). issn: 0360-0300. doi: 10.1145/3695249

Show all 64 references
  1. [9]

    Scalable eventually consistent counters over unreliable networks

    P. S. Almeida and C. Baquero. “Scalable eventually consistent counters over unreliable networks”. In: Distributed Comput. 32.1 (2019), pp. 69–89. doi: 10.1007/s00446-017-0322-2

  2. [10]

    The network is reliable

    P. Bailis and K. Kingsbury. “The network is reliable”. In: Commun. ACM 57.9 (2014), pp. 48–55. doi: 10.1145/2643130

  3. [11]

    Synchronized DSM Models

    J. Bataller and J. M. Bernabéu-Aubán. “Synchronized DSM Models”. In: Euro-Par ’97 Parallel Processing, Third International Euro-Par Conference, Passau, Germany, August 26-29, 1997, Proceedings . Ed. by C. Lengauer, M. Griebl, and S. Gorlatch. Vol. 1300. Lecture Notes in Comput...

  4. [12]

    Mathematizing C++ concurrency

    M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. “Mathematizing C++ concurrency”. In:Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011. Ed. by T. Ball and M. Sagiv. ACM, 2011, pp....

  5. [13]

    An optimized conflict-free replicated set

    A. Bieniusa, M. Zawirski, N. M. Preguiça, M. Shapiro, C. Baquero, V. Balegas, and S. Duarte. “An optimized conflict-free replicated set”. In: CoRR abs/1210.3368 (2012). arXiv: 1210.3368

  6. [14]

    Brief Announcement: Semantics of Eventually Consistent Replicated Sets

    A. Bieniusa, M. Zawirski, N. M. Preguiça, M. Shapiro, C. Baquero, V. Balegas, and S. Duarte. “Brief Announcement: Semantics of Eventually Consistent Replicated Sets”. In:Distributed Computing - 26th International Symposium, DISC 2012, Salvador, Brazil, October 16-18, 2012. Pro...

  7. [15]

    Lightweigt Causal and Atomic Group Multicast

    K. P. Birman, A. Schiper, and P. Stephenson. “Lightweigt Causal and Atomic Group Multicast”. In: ACM Trans. Comput. Syst. 9.3 (1991), pp. 272–314. doi: 10.1145/128738.128742

  8. [16]

    Foundations of the C++ concurrency memory model

    H. Boehm and S. V. Adve. “Foundations of the C++ concurrency memory model”. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008 . Ed. by R. Gupta and S. P. Amarasinghe. ACM, 2008, pp. 68–78. doi...

  9. [17]

    Outlawing ghosts: avoiding out-of-thin-air results

    H. Boehm and B. Demsky. “Outlawing ghosts: avoiding out-of-thin-air results”. In: Proceedings of the workshop on Memory Systems Performance and Correctness, MSPC ’14, Edinburgh, United Kingdom, June 13, 2014 . Ed. by J. Singer, M. Kulkarni, and T. Harris. ACM, 2014, 7:1–7:6. d...

  10. [18]

    On verifying causal consistency

    A. Bouajjani, C. Enea, R. Guerraoui, and J. Hamza. “On verifying causal consistency”. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 . Ed. by G. Castagna and A. D. Gordon. ACM, 2017, pp. 6...

  11. [19]

    Principles of Eventual Consistency

    S. Burckhardt. “Principles of Eventual Consistency”. In: Found. Trends Program. Lang. 1.1-2 (2014), pp. 1–150. doi: 10.1561/2500000011

  12. [20]

    Replicated data types: specification, verification, optimality

    S. Burckhardt, A. Gotsman, H. Yang, and M. Zawirski. “Replicated data types: specification, verification, optimality”. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 . Ed. by S. Jaganna...

  13. [21]

    Unifying Concurrent Objects and Distributed Tasks: Interval-Linearizability

    A. Castañeda, S. Rajsbaum, and M. Raynal. “Unifying Concurrent Objects and Distributed Tasks: Interval-Linearizability”. In: J. ACM 65.6 (2018), 45:1–45:42. doi: 10.1145/3266457

  14. [22]

    Dynamo: amazon’s highly available key-value store

    G. DeCandia, D. Hastorun, M. Jampani, G. Kakulapati, A. Lakshman, A. Pilchin, S. Sivasubramanian, P. Vosshall, and W. Vogels. “Dynamo: amazon’s highly available key-value store”. In:Proceedings of the 21st ACM Symposium on Operating Systems Principles 2007, SOSP 2007, Stevenso...

  15. [23]

    Harvest, Yield and Scalable Tolerant Systems

    A. Fox and E. A. Brewer. “Harvest, Yield and Scalable Tolerant Systems”. In: Proceedings of The Seventh Workshop on Hot Topics in Operating Systems, HotOS-VII, Rio Rico, Arizona, USA, March 28-30, 1999 . Ed. by P. Druschel. IEEE Computer Society, 1999, pp. 174–178. doi: 10.110...

  16. [24]

    Retrospective: Memory Consistency and Event Ordering in Scalable Shared-Memory Multipro- cessors

    K. Gharachorloo. “Retrospective: Memory Consistency and Event Ordering in Scalable Shared-Memory Multipro- cessors”. In: 25 Years of the International Symposia on Computer Architecture (Selected Papers) . Ed. by G. S. Sohi. ACM, 1998, pp. 67–70. doi: 10.1145/285930.285957

  17. [25]

    Information storage in a decentralized computer system

    D. K. Gifford. “Information storage in a decentralized computer system”. PhD thesis. Stanford, CA, USA, 1981

  18. [26]

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

    S. Gilbert and N. A. Lynch. “Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services”. In: SIGACT News 33.2 (2002), pp. 51–59. doi: 10.1145/564585.564601

  19. [27]

    Monotonic Prefix Consistency in Distributed Systems

    A. Girault, G. Gößler, R. Guerraoui, J. Hamza, and D. Seredinschi. “Monotonic Prefix Consistency in Distributed Systems”. In: Formal Techniques for Distributed Objects, Components, and Systems - 38th IFIP WG 6.1 International Conference, FORTE 2018, Held as Part of the 13th In...

  20. [28]

    J. R. Goodman. Cache Consistency and Sequential Consistency . Tech. rep. TR1006. University of Wisconsin-Madison, Department of Computer Sciences, 1991

  21. [29]

    Notes on Data Base Operating Systems

    J. Gray. “Notes on Data Base Operating Systems”. In: Operating Systems, An Advanced Course . Ed. by M. J. Flynn, J. Gray, A. K. Jones, K. Lagally, H. Opderbeck, G. J. Popek, B. Randell, J. H. Saltzer, and H. Wiehle. Vol. 60. Lecture Notes in Computer Science. Springer, 1978, p...

  22. [30]

    Wait-Free Synchronization

    M. Herlihy. “Wait-Free Synchronization”. In: ACM Trans. Program. Lang. Syst. 13.1 (1991), pp. 124–149. doi: 10.1145/ 114005.102808

  23. [31]

    Linearizability: A Correctness Condition for Concurrent Objects

    M. Herlihy and J. M. Wing. “Linearizability: A Correctness Condition for Concurrent Objects”. In: ACM Trans. Program. Lang. Syst. 12.3 (1990), pp. 463–492. doi: 10.1145/78969.78972

  24. [32]

    Slow Memory: Weakening Consistency to Enchance Concurrency in Distributed Shared Memories

    P. W. Hutto and M. Ahamad. “Slow Memory: Weakening Consistency to Enchance Concurrency in Distributed Shared Memories”. In: 10th International Conference on Distributed Computing Systems (ICDCS 1990), May 28 - June 1, 1990, Paris, France . IEEE Computer Society, 1990, pp. 302–...

  25. [33]

    A Generic Specification Framework for Weakly Consistent Replicated Data Types

    X. Jiang, H. Wei, and Y. Huang. “A Generic Specification Framework for Weakly Consistent Replicated Data Types”. In: International Symposium on Reliable Distributed Systems, SRDS 2020, Shanghai, China, September 21-24, 2020 . IEEE, 2020, pp. 143–154. doi: 10.1109/SRDS51746.2020.00022

  26. [34]

    A Critique of the CAP Theorem

    M. Kleppmann. “A Critique of the CAP Theorem”. In: CoRR abs/1509.05393 (2015). arXiv: 1509.05393

  27. [35]

    OpSets: Sequential Specifications for Replicated Datatypes (Extended Version)

    M. Kleppmann, V. B. F. Gomes, D. P. Mulligan, and A. R. Beresford. “OpSets: Sequential Specifications for Replicated Datatypes (Extended Version)”. In: CoRR abs/1805.04263 (2018). arXiv: 1805.04263

  28. [36]

    How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs

    L. Lamport. “How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs”. In: IEEE Trans. Computers 28.9 (1979), pp. 690–691. doi: 10.1109/TC.1979.1675439. 50 Paulo Sérgio Almeida

  29. [37]

    Time, Clocks, and the Ordering of Events in a Distributed System

    L. Lamport. “Time, Clocks, and the Ordering of Events in a Distributed System”. In: Commun. ACM 21.7 (1978), pp. 558–565. doi: 10.1145/359545.359563

  30. [38]

    R. J. Lipton and J. S. Sandberg. PRAM: A scalable shared memory . Tech. rep. CS-TR-180-88. Princeton University, Department of Computer Science, 1988

  31. [39]

    Mahajan, L

    P. Mahajan, L. Alvisi, and M. Dahlin. Consistency, A vailability, and Convergence. Tech. rep. UTCS TR-11-22. Depart- ment of Computer Science, The University of Texas at Austin, 2011

  32. [40]

    Space and Time

    H. Minkowski. “Space and Time”. In: Space and Time: Minkowski’s Papers on Relativity . Ed. by V. Petkov. Minkowski Institute Press, Montreal, 2012

  33. [41]

    Axioms for Memory Access in Asynchronous Hardware Systems

    J. Misra. “Axioms for Memory Access in Asynchronous Hardware Systems”. In: ACM Trans. Program. Lang. Syst. 8.1 (1986), pp. 142–153. doi: 10.1145/5001.5007

  34. [42]

    Set-Linearizability

    G. Neiger. “Set-Linearizability”. In: Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, Los Angeles, California, USA, August 14-17, 1994 . Ed. by J. H. Anderson, D. Peleg, and E. Borowsky. ACM, 1994, p. 396. doi: 10.1145/197917.198176

  35. [43]

    Causal consistency: beyond memory

    M. Perrin, A. Mostéfaoui, and C. Jard. “Causal consistency: beyond memory”. In: Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, March 12-16,

  36. [44]

    Update Consistency for Wait-Free Concurrent Objects

    M. Perrin, A. Mostéfaoui, and C. Jard. “Update Consistency for Wait-Free Concurrent Objects”. In: 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, Hyderabad, India, May 25-29, 2015 . IEEE Computer Society, 2015, pp. 219–228. doi: 10.1109/IPDPS.2015.39

  37. [45]

    ECROs: building global scale systems from sequential code

    K. D. Porre, C. Ferreira, N. M. Preguiça, and E. G. Boix. “ECROs: building global scale systems from sequential code”. In: Proc. ACM Program. Lang. 5.OOPSLA (2021), pp. 1–30. doi: 10.1145/3485484

  38. [46]

    From Causal Consistency to Sequential Consistency in Shared Memory Systems

    M. Raynal and A. Schiper. “From Causal Consistency to Sequential Consistency in Shared Memory Systems”. In: Foundations of Software Technology and Theoretical Computer Science, 15th Conference, Bangalore, India, December 18-20, 1995, Proceedings . Ed. by P. S. Thiagarajan. Vol...

  39. [47]

    Replicated abstract data types: Building blocks for collaborative applications

    H. Roh, M. Jeon, J. Kim, and J. Lee. “Replicated abstract data types: Building blocks for collaborative applications”. In: J. Parallel Distributed Comput. 71.3 (2011), pp. 354–368. doi: 10.1016/j.jpdc.2010.12.006

  40. [48]

    Optimistic replication

    Y. Saito and M. Shapiro. “Optimistic replication”. In:ACM Comput. Surv. 37.1 (2005), pp. 42–81. doi: 10.1145/1057977. 1057980

  41. [49]

    R. Salgado. Relativity on Rotated Graph Paper . 2016. url: https://www.geogebra.org/m/HYD7hB9v

  42. [50]

    x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors

    P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. “x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors”. In: Commun. ACM 53.7 (2010), pp. 89–97. doi: 10.1145/1785414.1785443

  43. [51]

    Consistency in 3D

    M. Shapiro, M. S. Ardekani, and G. Petri. “Consistency in 3D”. In: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada . Ed. by J. Desharnais and R. Jagadeesan. Vol. 59. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Inform...

  44. [52]

    Conflict-Free Replicated Data Types

    M. Shapiro, N. M. Preguiça, C. Baquero, and M. Zawirski. “Conflict-Free Replicated Data Types”. In: Stabilization, Safety, and Security of Distributed Systems - 13th International Symposium, SSS 2011, Grenoble, France, October 10-12,

  45. [53]

    A unified theory of shared memory consistency

    R. C. Steinke and G. J. Nutt. “A unified theory of shared memory consistency”. In: J. ACM 51.5 (2004), pp. 800–849. doi: 10.1145/1017460.1017464

  46. [54]

    Achieving Convergence, Causality Preservation, and Intention Preservation in Real-Time Cooperative Editing Systems

    C. Sun, X. Jia, Y. Zhang, Y. Yang, and D. Chen. “Achieving Convergence, Causality Preservation, and Intention Preservation in Real-Time Cooperative Editing Systems”. In: ACM Trans. Comput. Hum. Interact. 5.1 (1998), pp. 63–

  47. [55]

    Replicated data consistency explained through baseball

    D. Terry. “Replicated data consistency explained through baseball”. In: Commun. ACM 56.12 (2013), pp. 82–89. doi: 10.1145/2500500

  48. [56]

    Session Guarantees for Weakly Consistent Replicated Data

    D. B. Terry, A. J. Demers, K. Petersen, M. Spreitzer, M. Theimer, and B. B. Welch. “Session Guarantees for Weakly Consistent Replicated Data”. In: Proceedings of the Third International Conference on Parallel and Distributed Infor- mation Systems (PDIS 94), Austin, Texas, USA,...

  49. [57]

    Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System

    D. B. Terry, M. Theimer, K. Petersen, A. J. Demers, M. Spreitzer, and C. Hauser. “Managing Update Conflicts in Bayou, a Weakly Connected Replicated Storage System”. In: Proceedings of the Fifteenth ACM Symposium on Operating System Principles, SOSP 1995, Copper Mountain Resort...

  50. [58]

    Consistency in Non-Transactional Distributed Storage Systems

    P. Viotti and M. Vukolic. “Consistency in Non-Transactional Distributed Storage Systems”. In: ACM Comput. Surv. 49.1 (2016), 19:1–19:34. doi: 10.1145/2926965

  51. [59]

    Eventually consistent

    W. Vogels. “Eventually consistent”. In: Commun. ACM 52.1 (2009), pp. 40–44. doi: 10.1145/1435417.1435432. A Framework for Consistency Models in Distributed Systems 51

  52. [60]

    An oblivious observed-reset embeddable replicated counter

    M. Weidner and P. S. Almeida. “An oblivious observed-reset embeddable replicated counter”. In: PaPoC@EuroSys 2022: Proceedings of the 9th Workshop on Principles and Practice of Consistency for Distributed Data, Rennes, France, April 5 - 8, 2022. Ed. by A. Szekeres and K. C. Si...

  53. [108]

    doi: 10.1145/274444.274447

  54. [1993]

    Ed. by L. Snyder. ACM, 1993, pp. 251–260. doi: 10.1145/165231.165264

  55. [2011]

    Proceedings. Ed. by X. Défago, F. Petit, and V. Villain. Vol. 6976. Lecture Notes in Computer Science. Springer, 2011, pp. 386–400. doi: 10.1007/978-3-642-24550-3_29

  56. [2016]

    Ed. by R. Asenjo and T. Harris. ACM, 2016, 26:1–26:12. doi: 10.1145/2851141.2851170

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.