  Internet-scale distributed systems often replicate data at multiple
geographic locations to provide low latency and high availability. The
Conflict-free Replicated Data Type (CRDT) is a framework that provides a
principled approach to maintaining eventual consistency among data replicas.
CRDTs have been notoriously difficult to design and implement correctly. Subtle
deep bugs lie in the complex and tedious handling of all possible cases of
conflicting data updates. We argue that the CRDT design should be formally
specified and model-checked to uncover deep bugs. The implementation further
needs to be systematically tested. On the one hand, the testing needs to
inherit the exhaustive nature of the model checking and ensures the coverage of
testing. On the other hand, the testing is expected to find coding errors which
cannot be detected by design level verification.
  Towards the challenges above, we propose the Model Checking-driven
Explorative Testing (MET) framework. At the design level, MET uses TLA+ to
specify and model check CRDT designs. At the implementation level, MET conducts
model checking-driven explorative testing, in the sense that the test cases are
automatically generated from the model checking traces. The system execution is
controlled to proceed deterministically, following the model checking trace.
The explorative testing systematically controls and permutes all
nondeterministic message reorderings.
  We apply MET in our practical development of CRDTs. The bugs in both designs
and implementations of CRDTs are found. As for bugs which can be found by
traditional testing techniques, MET greatly reduces the cost of fixing the
bugs. Moreover, MET can find subtle deep bugs which cannot be found by existing
techniques at a reasonable cost. We further discuss how MET provides us with
sufficient confidence in the correctness of our CRDT designs and
implementations.
