Creating a specification for Map CRDTs
In an eventually consistent system, a replica of an object can execute an operation without synchronizing beforehand with other replicas, the updates between all replicas happen asynchronously. These concurrent updates on different replicas of the same object result in diverging states of the object, but eventual consistency guarantees that all replicas, once they stop executing new operations on their local state and only propagate their updates, eventually reach the same state and no update is lost. Convergent or Commutative Replicated Data Types (CRDTs), which are based on simple formal conditions, provide a way for deterministic conflict resolution. Thus it is useful in an eventually consistent system to use CRDTs. While there are certain CRDTs like sets or counters with an existing specification, there is none yet for maps. The goal of this thesis is to give a specification for Map CRDTs containing the formal conditions to guarantee eventual consistency.