Modelling replication protocols with actions and constraints
I will describe a formal model of replicated-data systems, based on actions and constraints. An action models a data transformation, and a constraint models an invariant. The same model describes different levels in a unified fashion:
- A client application requests updates (actions) that are related to one another in various ways, e.g. by causal dependence or atomicity (constraints).
- Concurrent updates may conflict, i.e. violate object invariants (more constraints).
- The replication protocol transfers actions and orders them (adding other constraints).
- Each site executes the actions it knows, according to some serial schedule that satisfies the constraints it knows.
- The whole system must enforce consistency.
Within the model we give three different definitions of consistency: (1) the intuitive, "declarative" notion of eventual consistency, (2) an "operational" definition based on equivalence of local schedules, and (3) a property of local information called mergeability. We show the three definitions are equivalent. If time permits, I will analyse a few well-known replication protocols in the framework.
