A formalism for consistency and partial replication



Replication protocols are complex and it is difficult to compare their consistency properties. To this effect, we propose a formalism where a replica executes actions subject to constraints in its local view or multilog. Schedules are selected non-deterministically from the set of sound schedules. This set grows with the number of actions and shrinks as the number of constraints increases. If the size of the set is one, the state is completely determined; if every site runs the same schedule, they converge; if applications encode their semantics with constraints, states are correct. We formalise this intuitive concept of consistency in four different ways, which generalise classical consistency criteria and which expose different aspects of consistency protocols. We prove them equivalent. We provide the first formal definition of partial consistency. In general, achieving consistency entails global consensus; we exhibit sufficient conditions for deciding locally and derive a new decentralised protocol.