Detail

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.