A critique of the CAP Theorem

Slides from an unsession given at Strange Loop, 25 September 2015. https://github.com/strangeloop/StrangeLoop2015/wiki/Unsessions#cap

Abstract:

The CAP Theorem, as proposed by Brewer and formalized by Gilbert and Lynch, has been subject of much debate and confusion over the last few years. The confusion arises partly from the definitions of “consistency,” “availability” and “partition tolerance,” which are not as intuitive or precise as one might hope, and which are therefore prone to being misinterpreted. I will also argue that there are some formal problems with Gilbert and Lynch's proof which weaken the result. With so many problems, it is becoming doubtful whether CAP is still useful for reasoning about systems.

The trade-off between consistency guarantees and tolerance of network faults is real, but we need better tools for reasoning about these trade-offs. In this session I will show some formal results from distributed systems theory that I have found useful: they focus the discussion on *latency* (which has been described as the “missing piece of the CAP theorem”). We'll then open up for discussion, and hopefully together we can work towards replacing CAP with something better: something more precise, more intuitive, and more relevant to practice.

Transcript

5. Johnson and Thomas, 1975 (RFC 677)
6. Fischer and Michael, 1982
34. (Alpern and Schneider, 1985)
44. Liveness properties are inherently problematic. The question of whether a real system satisfies a liveness property is meaningless; it can be answered only by observing the system for an infinite length of time, and real systems don’t run forever. Liveness is always an approximation to the property we really care about. We want a program to terminate within 100 years, but proving that it does would require the addition of distracting timing assumptions. So, we prove the weaker condition that the program eventually terminates. This doesn’t prove that the program will terminate within our lifetimes, but it does demonstrate the absence of infinite loops. (Lamport, 2000; emphasis added)