14.1 Operational Transform Convergence

(May 2005)

Editorial note: This paper presents the conventional 2005 construction in which an inclusion transform on primitive operations is extended to temporal lists of operations. It is retained for its historical role in the convergence argument. Inclusion transform on its own is no longer the fundamental operator in cxOT; the later work instead centres merge and factorisation of composite, spatially represented operations.

Syntactic conventions

O, O₁, O₂ etc are primitive (i.e. indivisible) operations.

L, L₁, L₂ etc are lists of operations.

L = [O₁ , O₂ , O₃ , ... , O_n] is the list of operations O₁ then O₂ ... then O_n.

L = [L₁, L₂, ..., L_n] is the concatenation of lists L₁, ..., L_n.

L = [H | T] is the list with head operation H and tail T.

X_i is either an O_i or L_i.

L = [X₁ X₂ ... X_n] is the concatenation of lists or primitive operations X₁, ..., X_n.

Execution context (editorial clarification)

The empty list acts as the identity at whichever document state it is used; it does not have a single intrinsic input or output state. The list transforms below are understood only where their operation transforms and concatenations are defined.

Definitions

Operations and lists of operations are treated as partial functions on document states. All expressions below are assumed to be executable on the states at which they occur. Consequently, convergence is a congruence: convergent lists may be substituted for one another within an executable concatenation.

Some people call this eventual consistency, but the term "consistent" means different things to different people (e.g. convergent, satisfies integrity constraints, linearisable or serialisable), and therefore probably should be avoided.

Clearly: ∀i, X_i ~ Y_i ⇒ [X₁ ... X_n] ~ [Y₁ ... Y_n]

The following diagram depicts the two operations O₁, O₂ that apply to initial document state S. Condition C₁ states that the path along the left and top edges yields the same final document state F as the path along the bottom and right edges.

Here IT is overloaded for primitive operations and lists. For two primitive operations it has the meaning defined above; the rules extend it recursively to lists. The empty-list rules are the boundary cases of that recursion.

[Note that this definition appears to be ambiguous in the way in which a list is decomposed into smaller sub-lists. However, it turns out that the final result is independent of the order in which the lists are decomposed. A more formal approach could begin with an unambiguous definition then prove the two decomposition rules above.]

Editorial clarification: Independence from the choice of decomposition is not an automatic consequence of writing down these recursive equations. It requires the appropriate coherence properties of the primitive transformation functions. The displayed equations are therefore best read as decomposition laws whose well-definedness must be proved; condition C₂, introduced below for three concurrent operations, expresses the corresponding path-independence requirement.

We can depict IT(L₁,L₂) pictorially as follows. L₂ has three primitive operations and L₁ has four primitive operations. The initial document state S is associated with the bottom left corner of the 3 x 4 grid of "cells".

Starting from the bottom left corner we can apply IT on the primitive operations. This can proceed to adjacent cells until we transform the operations to the top and right boundaries.

Note that IT is quadratic in the size of the lists.

Proof:

A formal proof can be achieved using induction on the length of L₁,L₂. Informally, we can prove the result more easily as follows.

We begin with L_1,2, which is associated with the path along the bottom and right edges. Starting from the bottom right corner we can shift the path using the known convergence property on the cell. This is repeated for adjacent cells until the path is transformed to the left and top edges, corresponding to L_2,1.

This represents one of the six possible paths from "Start" to "Finish" on the following cube.

Note that it is not the case that C₁⇒C₂. On the contrary, C₂ must be independently assumed in order to achieve convergence when there are more than two sites.

There are 6 possible paths on the cube.

Convergence C₁ implies that the 6 paths can be put into 3 groups, illustrated with the dotted ovals on the left side.

Adding condition C₂ implies that all 6 paths are equivalent.

Note that it is not the case that C₁ ⇒ L_1,2,3 ~ L_2,1,3

Proof:

(Informally)

The following cube depicts two operations in L₁, two in L₂ and three operations in L₃.

L_1,2,3 corresponds to the transformation of L₃ along the front face then the right face of the cube. On each of these faces we can depict a regular grid of cells, associated with the simple, two dimensional case. Condition C₁ ensures that convergence is achieved on each face of the cube.

The individual operations allow us to partition the cube into small "cells". In particular the "cell" at the nearest, bottom right corner of the cube (i.e. labelled B in the diagram) is of interest. Consider that we adjust the path on the right face as follows.

We can now apply condition C₂ to the cell at B to yield an equivalent path as follows.

We now adjust the path on the back face of the cell at B.

This allows us to proceed to the cell to the left of B. In this manner we can proceed through the cells until we get the following path.

This corresponds to L_2,1,3.

This shows informally that L_1,2,3 ~ L_2,1,3.

Four sites

There are 4! = 24 paths through the "hypercube". Interestingly it turns out that C₁,C₂ are sufficient for convergence.

The paths can be listed in four groups of 6 as follows:

The same argument extends to n sites by induction. Partition the n! paths into n groups according to their first operation. Within each group, the induction hypothesis applies to the remaining n − 1 operations. Lemma 2 and associativity allow adjacent leading operations to be exchanged, connecting the groups. Thus C₁ and C₂ are sufficient for convergence for any finite number of sites.

Related work (editorial note)

The terminology in this paper belongs to an established line of operational-transformation research. The earliest appearances located in preparing this transcription are summarised here; this is not a claim that no still earlier use exists, particularly where several papers from the same research programme were in circulation at about the same time.

Clarence Ellis and Simon Gibbs introduced the dOPT transformation approach in Concurrency Control in Groupware Systems (June 1989). Their consistency model already required copies of the shared object to converge, as well as preserving precedence. Thus convergence as a system-level requirement of replicated groupware predates this May 2005 paper. Chengzheng Sun, Xiaohua Jia, Yanchun Zhang, Yun Yang and David Chen subsequently gave the familiar convergence, causality-preservation and intention-preservation model in Achieving Convergence, Causality Preservation, and Intention Preservation in Real-Time Cooperative Editing Systems (March 1998).

The 1998 paper also explicitly defined an operation's context: the operations taking the document from its initial state to the state on which that operation is defined. It called two operations context equivalent when their contexts are equal, and called one operation context preceding another when the latter's context is obtained by appending the former. On that basis it specified the inclusion transformation IT for context-equivalent operations, and the complementary exclusion transformation ET for context-preceding operations. The underlying transformation idea therefore dates to Ellis and Gibbs in 1989, while the earliest explicit definitions of IT and ET, with these contextual preconditions, located for this note are in Sun et al. in 1998.

The exact adjective forms contextually equivalent and contextually serialized appear in Rui Li and Du Li's Commutativity-Based Concurrency Control in Groupware (CollaborateCom, December 2005). They defined the first by equality of source document states and the second by the destination state of one operation being the source state of the next. They also expressly related these notions to Sun et al.'s earlier context-equivalence and context-serialization preconditions for IT and ET. The list-level definitions added to this transcription under Execution context are an editorial extension of that operation-level vocabulary: a contextually serialised list is a composable chain, and two such lists are context equivalent when they start in the same state.

An especially close antecedent is Gordon V. Cormack's A Calculus for Concurrent Update (University of Waterloo technical report CS-95-06, January 1995; an abstract was published at PODC in August 1995). Cormack defined a binary operator on update sequences by four recursive equations: two empty-sequence cases, a rule for transforming through a concatenated second sequence, and a rule for decomposing a concatenated first sequence. Apart from notation and Cormack's use of forward and backward transforms selected by a canonical timestamp order, those equations have the same structure as the four list-IT equations above. His Theorem 1 then proves, by induction on the combined lengths of two sequences, that either sequence can be applied first and the other transformed after it without changing the result. This is the earliest directly corresponding two-list construction located for this note, and should be regarded as prior work for both the recursive definition and its inductive convergence proof.

There was also closely related contemporary work on lifting transformation from one operation to a sequence. Abdessamad Imine, Pascal Molli, Gérald Oster and Michaël Rusinowitch's Towards Synchronizing Linear Collaborative Objects with Operational Transformation (FORTE, October 2005) defined T^*(O,L) recursively: transforming against the empty sequence returns O, while transforming against a non-empty sequence transforms O against its head and continues with its tail. The paper proves results about this sequence extension by induction on the length of the sequence, and uses the induction-based theorem prover SPIKE for its larger correctness obligations. This is directly relevant to the one-operation-against-a-list case of IT above. It does not, however, by itself give the symmetric two-list grid construction used here; that construction additionally transforms the operations of both lists to the opposite boundaries.

There are also two related meanings of convergence to keep apart. In the earlier consistency models, convergence is the system property that replicas which have executed the same operations contain identical documents. The relation X₁ ~ X₂ used here is a local algebraic relation between operations or lists: from a common input, they have the same effect. Li and Li called the corresponding relation effects equivalence. That local relation is what permits the grid and cube arguments to establish the system-level result; it is not itself a new definition of replicated-system convergence.

Relationship to Ressel's TP1 and TP2

This treatment is closely related to the convergence framework presented by Matthias Ressel, Doris Nitsche-Ruhland and Rul Gunzenhäuser in their 1996 paper An Integrating, Transformation-Oriented Approach to Concurrency Control and Undo in Group Editors. That work introduced the adOPTed control algorithm and identified two transformation properties, now generally called TP1 and TP2, that make transformation along different paths converge. The grids, cube and hypercube used above express the same geometric idea: alternative paths represent different orders in which concurrent operations can be incorporated.

The condition C₁ above is essentially Ressel's TP1. In the notation of this document it is

[O₁, IT(O₂, O₁)] ~ [O₂, IT(O₁, O₂)].

TP1 says that two concurrent operations can be executed in either order, after transforming the second operation against the first, without changing the resulting document state. It is therefore the convergence condition on each two-dimensional cell in the diagrams above.

The condition called C₂ above is related to, but is not identical to, Ressel's TP2. C₂ requires the two complete three-operation paths to converge:

O_1,2,3 ~ O_2,1,3.

Ressel's TP2 places the stronger requirement on the transformed third operation itself:

IT(IT(O₃, O₁), IT(O₂, O₁)) = IT(IT(O₃, O₂), IT(O₁, O₂)).

Using the list extension of IT, this can be written more compactly as

IT(O₃, O_1,2) = IT(O₃, O_2,1).

Thus TP2 says that transforming O₃ against two equivalent orderings of O₁ and O₂ produces the same operation, not merely operations that happen to produce the same state in a particular execution. TP1 together with TP2 implies the C₂ path-convergence condition used above. The converse need not hold: two distinct transformed operations may have the same effect in one context while behaving differently when they are subsequently transformed or composed with other operations.

This distinction is important for the extension to arbitrary numbers of sites. The standard Ressel result uses TP1 and TP2 to make the transformed operation independent of the transformation path. That path independence supports further transformations and allows all paths through the n-dimensional interaction model to be connected. The cube argument above captures the intuition of that result, but its state-based C₂ is formally weaker than TP2. Accordingly, the final n-site conclusion agrees with Ressel's result if C₂ is understood as TP2, or if an additional assumption ensures that convergent transformed operations are interchangeable under every later transformation.

For alignment with the standard OT literature, one could reserve the name C₂ or TP2 for the transformed-operation equality above and present O_1,2,3 ~ O_2,1,3 as a consequence of C₁ and TP2. The existing diagrams and list lemmas would then serve as an informal illustration of Ressel's convergence theorem rather than as a different definition of its second transformation property.