Eventual Consistency Formalized

Distribution of computation is well-known, and there are several frameworks, including some formal frameworks, that capture distributed computation. As yet, however, models of distributed computation are based on the idea that data is conceptually centralized. That is, they assume that data, even if it is distributed, is consistent. This assumption is not valid for many of the database systems in use today, where consistency is compromised to ensure availability and partition tolerance. Starting with an informal definition of eventual consistency, this paper explores several measures of inconsistency that quantify how far from consistency a system is. These measures capture key aspects of eventual consistency in terms of distributed abstract state machines. The definitions move from the traditional binary definition of consistency to more quantitative definitions, where the classical consistency is given by the highest possible level of consistency. Expressing eventual consistency in terms of abstract state machines allows models to be developed that capture distributed computation and highly available distributed data within a single framework.