Skip navigation

12/16/2010: final version of CALM/Bloom paper for CIDR now posted

Conventional Wisdom:
In large distributed systems, perfect data consistency is too expensive to guarantee in general. “Eventually consistent” approaches are often a better choice, since temporary inconsistencies work out in most cases. Consistency mechanisms (transactions, quorums, etc.) should be reserved for infrequent, small-scale, mission-critical tasks.

Most computer systems designers agree on this at some level (once you get past the NoSQL vs. ACID sloganeering). But like lots of well-intentioned design maxims, it’s not so easy to translate into practice — all kinds of unavoidable tactical questions pop up:

Questions:

  • Exactly where in my multifaceted system is eventual consistency “good enough”?
  • How do I know that my “mission-critical” software isn’t tainted by my “best effort” components?
  • How do I maintain my design maxim as software evolves? For example, how can the junior programmer in year n of a project reason about whether their piece of the code maintains the system’s overall consistency requirements?

If you think you have answers to those questions, I’d love to hear them. And then I’ll raise the stakes, because I have a better challenge for you: can you write down your answers in an algorithm?

Challenge:
Write a program checker that will either “bless” your code’s inconsistency as provably acceptable, or identify the locations of unacceptable consistency bugs.

The CALM Conjecture is my initial answer to that challenge.

CALM stands for “Consistency As Logical Monotonicity”. The idea is that the family of eventually consistent programs are exactly those that can be expressed in monotonic logic. By contrast, distributed non-monotonicity (e.g. destructive state modification, aggregation or “reduce”) can and must be resolved via distributed coordination logic (e.g. two-phase-commit, Paxos). The idea that “temporary inconsistencies work out” amounts to ensuring that the data in question is contained within a properly-protected monotonic component of the system.

Presuming that CALM can be proven with sufficient generality (restricted formal versions of it are obvious, but I’m quite sure there’s more that can be done), the next step is to translate this idea into a useful program checker. Like many other verification tasks, this is only tractable in a sufficiently high-level language — in this case, one where the constructs of the language can be translated into an underlying logic. Bloom is our language along these lines, and we have the initial program checks in place. Given a Bloom program, we can do the following:

  1. bless programs as monotonic, and hence safe to run coordination-free
  2. identify non-monotonic “Points of Order” in Bloom programs. These can be resolved by either of the following (which we intend to automate):
    • add coordination logic (e.g. quorum consensus) to enforce the ordering, or
    • augment the program to tag downstream data as “tainted” with potential inconsistency
  3. visualize the Points of Order in a dependency graph, to help programmers reason about restructuring their code for more efficient consistency enforcement.

We wrote up our initial ideas on this topic in a short submission to CIDR 2010 CIDR 2010 paper, including an intro to the current state of the Bloom language, and an example of analyzing a replicated shopping-cart application.  This follows from the discussion in my companion paper to my PODS keynote talk [slides].

I’d love feedback on these ideas, which are still a work in progress.

Advertisements

3 Comments

  1. The obvious question is What is a logically monotonic program?

    • Good! Also need to answer specifically what is Consistency and what is Coordination. There have been a variety of formal papers on this since the time of the post … see this survey paper for an overview:http://dl.acm.org/citation.cfm?id=2694415.

    • Monotonic programs are the programs that can be implemented by streaming algorithms that incrementally produce output elements as they receive input elements.e.g., programs expressible via selection, projection and join (even with recursion).
      The final order or contents of the input will never cause any earlier output to be “revoked” once it has been generated. Non-monotonic programs on the other hand can only be implemented correctly via blocking algorithms that do not produce any output until they have received all tuples in logical partitions of an input set. e.g., those that contain aggregation or negation operations


10 Trackbacks/Pingbacks

  1. By Not even eventually consistent on 31 Jan 2011 at 10:11 am

    […] that the Web is not inconsistent is in any random way: it has its own viable logic.Further reading: The CALM Conjecture: Reasoning about Consistency Comments (0)No Comments »No comments yet.Leave a comment Name Mail (will not be published) […]

  2. […] The CALM Conjecture: Reasoning about Consistency « Data Beta (tags: database consistency nosql) […]

  3. By Quora on 11 Aug 2011 at 11:08 pm

    What are some active uses of weakly consistent, read-any/write-any distributed systems like Bayou?…

    Theoretically speaking (ideal use cases for weakly consistent systems): Eventual consistency allows for high availability, even if majority of nodes are unable to communicate with each other e.g., disconnected operations. It also allows low latency be …

  4. […] you’ve been following our Bloom work, you know where this discussion is coming from: the CALM Theorem says that the real reason to use coordination is to manage non-monotonic reasoning.  Many (most?) […]

  5. […] in the past couple years formalizing eventual consistency (EC) for distributed programs, via the CALM theorem and practical tools for analyzing Bloom […]

  6. […] la complexité, le réseau et vive l’asynchronisme.Jonas souhaite attirer notre attention sur « The CALM Conjecture » sans plus de détail si ce n’est que la donnée temps n’est plus prise en compte.Go BIG […]

  7. […] article by Bailis and Ghodsi, if a programmer follows a certain set of guidelines (expressed by CALM theorem) on which operations and programs are safe to use in eventually consistent system, he can build a […]

  8. […] notifications when all records for a given round of input or loop iteration have been received. Asynchronous processing is great for some algorithms, but others require synchronization, including such simple algorithms as counting all of the […]

  9. […] draws inspiration from the CALM theorem, but Blazes is much more than a formalism—it’s a tool for analyzing working code.  In […]

  10. By BOOM, Bloom Language, CALM | Note To Self on 21 May 2014 at 8:07 am

    […] this blog post […]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: