CAP Theorem, PACELC Trade-Offs & Formal Consistency Models

Executive Summary

Designing resilient distributed systems begins with accepting fundamental physical constraints: network latency is non-zero, packet loss is inevitable, and synchronized global physical clocks do not exist. Eric Brewer's CAP Theorem and Daniel Abadi's PACELC Theorem formalize the immutable trade-offs distributed systems must navigate during normal operations and network partitions.

1. Brewer's CAP Theorem Formalization

Brewer's CAP Theorem states that a distributed data store can simultaneously provide at most two of the following three guarantees:

• Consistency (Linearizability): Every read receives the most recent write or an error.
• Availability: Every non-failing node returns a non-error response for every request (without guarantee it contains the most recent write).
• Partition Tolerance: The system continues to operate despite an arbitrary number of messages being dropped or delayed by the network between nodes.

In any physical distributed network, network partitions ($P$) are unavoidable. Thus, the system is fundamentally forced to choose between CP (Consistency under Partition) and AP (Availability under Partition).

2. Abadi's PACELC Theorem

The PACELC Theorem extends CAP by explicitly modeling system behavior when the network is running normally (no partitions): $$\text{If } P \text{ (Partition)} \rightarrow \text{choose } [A \lor C]; \quad \text{ELSE } \rightarrow \text{choose } [L \lor C]$$

• PC/EC: During partition choose Consistency; Else choose Consistency over Latency (e.g. Apache Kafka KRaft, CockroachDB, Google Spanner).
• PA/EL: During partition choose Availability; Else choose Latency over Consistency (e.g. DynamoDB eventual read, Cassandra, Couchbase).
• PA/EC: During partition choose Availability; Else choose Consistency (e.g. MongoDB primary reads).
• PC/EL: During partition choose Consistency; Else choose Latency (e.g. PostgreSQL sync replica).

3. Hierarchy of Consistency Models

1. Strict Serializability (External Consistency): The gold standard. Transactions appear in real physical-time sequence with linearizable reads.
2. Linearizability (Atomic Consistency): Single-object, single-operation real-time ordering.
3. Sequential Consistency: Operations take effect in some sequential order consistent across all nodes, respecting program order.
4. Causal Consistency: Causally related operations are observed in the same order by all nodes; concurrent operations may be seen in different order.
5. Eventual Consistency: In the absence of new updates, all replicas eventually converge to identical state.

4. Production Architectural Guidelines

• Financial Balances & Inventory: Mandate CP / PC/EC with Raft quorum. Never allow split-brain writes on balance ledgers.
• Telemetry & Social Feeds: Mandate AP / PA/EL with Conflict-Free Replicated Data Types (CRDTs). Low latency and high availability trump instantaneous linearizability.