Constraining the eventual in eventual consistency

CRDTs are highly available replicated data structures which offer strong eventual consistency in the face of concurrent operations [3]. By their definition, CRDTs eventually converge to a consistent state given enough time. However, this is not strict enough for some distributed applications. Current state-of-the-art CRDT implementations fail to provide programmers with the means to specify these constraints. As a result, programmers need to write application-level code which ignores stale or timed-out operations. In this paper, we introduce a leasing model which allows programmers to declaratively specify timing constraints for CRDTs. In short, programmers are able to attach leases to operations on a CRDT instance. When such a lease expires the underlying implementation ensures that the operation is eventually canceled for all replicas.