22 Operational Transform Convergence

(May 2005)

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

Xi is either an Oi or Li.

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

Definitions

Definition: We write X₁ ~ X₂ if X₁ and X₂ are executed on the same initial document state and produce the same final document state. This is called convergence.

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]

Definition: IT(O₂, O₁) is the inclusion transform of O₂ against O₁. O₁,O₂ are assumed to be concurrent operations on the same initial document state. IT(O₂, O₁) is a transformed version of O₂ that can be executed after O₁.

Definition: Let O_1,2 = [O₁ , IT(O₂, O₁) ]

Definition: Convergence condition C₁ : ∀ O₁,O₂, O_1,2 ~ O_2,1

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.

Definition: IT(L₁, L₂) is defined recursively as follows

1. IT([], []) = []
2. IT([L₁, L₂], L₃) = [ IT(L₁ ,L₃) , IT(L₂, IT(L₃, L₁)) ]
3. IT(L₁, [L₂ , L₃]) = IT(IT(L₁, L₂), L₃)

[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 decomposition rules 2,3 above]

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.

Definition : L_1,2 = L₁ IT(L₂, L₁)

Lemma 1: C₁ ⇒ ∀ L₁,L₂, L_1,2 ~ L_2,1

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.

Definition: O_1,2,3 = O_{(1,2), 3} = [O_1,2 IT(O₃, O_1,2) ]

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

Definition: Condition C₂: ∀ O₁,O₂,O₃, O_1,2,3 ~ O_2,1,3

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.

Lemma : C₁ ⇒ L_1,2,3 ~ L_1,3,2

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

Lemma 2: C₁, C₂ ⇒ ∀ L₁,L₂,L₃, 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 (ie labeled 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

which corresponds to L_2,1,3

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

RTP. C₁, C₂ ⇒ L_{(1,2), 3} ~ L_{1, (2,3)} (associativity)

Proof :

L_{(1,2), 3} ~ L_(2,1),3 (Lemma 2)

= L_2,1 IT(L₃, L_2,1)

~ L_1,2 IT(L₃, L_2,1) (Lemma 1)

= L_1,2 IT(L₃, [L₂ IT(L₁, L₂)] )

= L_1,2 IT(IT(L₃,L₂), IT(L₁, L₂))

= L₁ IT(L₂,L₁) IT(IT(L₃,L₂), IT(L₁, L₂))

= L₁ IT([L₂ IT(L₃,L₂) ], L₁)

= L₁ IT(L_2,3, L₁)

= L_{1, (2,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

Claim

• Each group contains equivalent paths because they all begin with the same operation which can therefore be disregarded, reducing the problem to the 3-site case which has already been proven
• As an example G1 ~ G2 because L_1,2,3,4 ~ L_2,1,3,4. This follows by letting M = L_3,4. By associativity L_1,2,3,4 ~ L_1,2,M ~ L_2,1,M ~ L_2,1,3,4.

This pattern extends into n sites.