[marc_shapiro]

The argument of Sun's paper seems to be that CRDTs have hidden performance costs. Perhaps this is true.

This completely misses the main point. OT is complex, the theory is weak, and most OT algorithms have been proven incorrect (see http://hal.inria.fr/inria-00071213/). AFAIK, the only OT algorithm proved correct is TTF, which is actually a CRDT in disguise.

In contrast, the logic of CRDTs is simple and obvious. We know exactly why CRDTs converge. There are several papers proving that specific CRDTs are indeed correct.

Furthermore, I'm somewhat doubtful of the performance discussion, since Attiya et al. proved that there is a lower bound on the complexity of concurrent editing, independently of the technology used. See http://dx.doi.org/10.1145/2933057.2933090.

Disclaimer: I did not read the paper in detail, just skimmed over it.

[marc_shapiro]

"Most OT algorithms have been proved incorrect": a better reference is https://doi.org/10.1016/j.tcs.2005.09.066

[shunza]

Representative CRDTs, at least Logoot and TreeDoc, were never truly proved. The correctness of Logoot and TreeDoc are claimed under the assumption that the required property of ids is preserved by the CRDT design. However, the existing id generation algorithms cannot achieve the desired property.

To be specific, I will enumerate two examples.

First, in Logoot (https://hal.inria.fr/inria-00432368/document", the function generateLinePositions in section 4.2 has a serious error, which could lead to the failure of generating new identifiers. This flawed design can be also found in the following research (Logoot-Undo, https://hal.inria.fr/hal-00450416/)

Second, in TreeDoc (https://hal.inria.fr/inria-00445975/document), the function newPosID described in section 3.2 may generate incorrect ids. This function is to generate an id r between any two ids p and q (p<q) so that p<r<q. However, in line 5, if pn=0, then we would get r<p. Readers can refer to Figure 3, in the tree, the character dY precedes the character dZ in infix order, however, the id of dY (10(0:dY)) is greater than the id of dZ (100(1:dZ)), thus their positions are inconsistent their ids.

In the literature, CRDT researchers always claim their CRDT designs are formally proved.

However, there are various scenarios whereby CRDTs would have inconsistency issues as stated above.

In my opinion, I don't think there are much validity for these claims.

[marc_shapiro]

Well, RGA has been proved formally [DOI 10.1145/2933057.2933090]. Regarding Figure 3 of the Treedoc paper, I believe the IDs of dY and dZ are in the correct order, according to the rules in the paper.

[nused]

This paper follows the same reasoning as in http://hal.inria.fr/inria-00071213/, so it invariably arrives at the same bogus conclusion "Most OT algorithms have been proved incorrect". Please feel free to explain if you feel otherwise, but quoting yet another publication doesn't really help its case here.

What did catch my eye in this paper is that the authors claimed to have used CoWord as a case study (and of course, claimed that the theorem prover showed CoWord doesn't satisfy TP2). I worked on CoWord, and it was never open-sourced so how the authors got hands on CoWord's transformation functions (which were inside a compiled C++ binary OT-engine) for evaluation is truly troubling. Care to explain?

[nused]

No points were missed - the paper just showed why the points are wrong. I'd be happy to discuss them if you care to read it: there are three concrete correctness problems with CRDT (Logoot) in sections 4.2.4 - 4.2.6.

Re: the articles you cited: Molli et al.'s http://hal.inria.fr/inria-00071213/ (A) and their earlier paper: https://www.lri.fr/~mbl/ENS/CSCW/2013/papers/Imine-ECSCW03.p... (B), are unfortunately wrong about OT correctness, demonstrably so.

The formalism can obscure the underlying argument, but both A and B uses the same reasoning, which goes something like this:

1. Assumption: An OT system's transformation functions must always satisfy TP1 and TP2, independent of the OT algorithm or protocol, otherwise they are incorrect.

2. Proof: take any existing OT system, disregard the OT algorithm or protocol, just look at the OT transformation functions in isolation, and show that the functions do not satisfy TP1 and TP2.

3. Conclusion: All known OT systems are incorrect

The starting assumption of the proof is a false premise: OT's transformation functions do not always require TP2. The proof itself, of evaluating correctness on a subset of OT in isolation, then broadly generalize to OT as a whole, is a sleight of hand (and sloppy theory work). Hence, the conclusion is plainly wrong.

TP2 is only required under a very specific pre-condition, and meaning that avoiding this pre-condition means removing the need to preserve TP2 at the level of transformation functions. TP2/CP2-avoidance strategy is commonly used in many OT algorithms and protocols: GOT, JUPITER, G-WAVE/DOCS, COT, TIBOT etc., which are provably correct (see https://www.computer.org/csdl/trans/td/2016/03/07060680-abs..... Transformation functions capable of preserving TP2/CP2 for string-wise text editing (with verified correctness and without tombstones or other meta-data)are also available (see https://dl.acm.org/citation.cfm?doid=2998181.2998252)

What I also find really dubious is the verification method used in A and B: paper B starts with using a theorem prover to definitively prove that all previously known OT systems are wrong. Then the paper proposed new transformation functions that the same theorem prover showed to be definitively correct. Paper A, which came after paper B by the same authors, used another theorem prover to show again that all previously known OT functions to be wrong, definitively, including the ones that they proposed to be "definitely correct" from B. So A basically contradicts the results in B, and both were definitively "proven correct".