15.2 Single character insertion and deletion operations

(26 July 2005)

Abstract

This paper describes a new technique for operational transform of single character insertion and deletion operations on a text document that solves the ERV puzzles and TP2 convergence problems in a far simpler, more efficient and elegant fashion than the SDT [1] or SDTO [2] algorithms.

Like the SDT algorithm, IT and ET are based on the effects relation, which is a total ordering on all characters inserted into the text document. The paper provides an easy way to calculate the effects relation.

Introduction

For state S and operation O, S' = S+O denotes the state obtained after executing O on state S. Operation O may only be executed on state S. Therefore we define state_in(O) = S.

Let id(O) denote the site identifier of the site on which O was originally generated. It is assumed there is a total ordering on site identifiers.

Two operations O₁, O₂ are equivalent (written O₁ ~ O₂) if state_in(O₁) = state_in(O₂) = S and S+O₁ = S+O₂. Note that this doesn't imply that the operations are equal. For example, it is possible that id(O₁)≠id(O₂).

[O₁ ... O_n] denotes the list of operations O₁,...,O_n assumed to be contextually serialised - i.e. intended to be performed in the given order on some initial state S. S + [O₁...O_n] denotes the state (((S+O₁)+O₂)+...+O_n).

As in [1], by definition characters in text documents have identity. A character is originally inserted by a particular user at a particular site. The character keeps its unique identity even though its index position in the document changes as characters are inserted or deleted. Note that a character doesn't simply relate to its appearance (eg its ASCII code) - for example each appearance of the letter 'A' in a document represents a different character.

We take the convention that strings use zero-based index positions. Given string s, let s[i] be the i^th character and let s[i,j) denote the substring corresponding to the half-open interval [i,j).

Definition of IT, ET

It has been shown in [3] that if IT satisfies conditions TP1, TP2 (defined below) then sites are able to execute operations in different orders yet achieve convergence at quiescence.

TP1

∀ O₁, O₂ where O₁ || O₂ and state_in(O₁) = state_in(O₂) = S, S + [O₁ IT(O₂, O₁)] = S + [ O₂ IT(O₁, O₂) ]

In the following diagram we require S12 = S21.

TP2

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

System 1: Insert operations

In system 1 we limit ourselves to insert operations that apply to a single text document. Operation O = ins(p,c) inserts character c at position p.

Let each operation contain the following fields.

The following diagram shows two cases of transforming operations Ox, Oy against each other. For each cell the initial state is in the bottom left corner and the final state is in the top right corner. There are two paths from the initial state to the final state - either along the bottom and right edges, or along the left and top edges.

From these two cells we get four cases for IT(O₁,O₂).

The criteria for these four cases are mutually exclusive and cover all possible cases. Therefore the above cells lead to the following well-defined algorithm for IT.

// Assumes O1 || O2
IT(Operation& O1, const Operation& O2)
{
    if (O2.p < O1.p || O2.p == O1.p && O2.id < O1.id) ++O1.p;
}

From the two cells we get four cases for ET(O₁,O₂).

These four criteria are mutually exclusive, but do not cover all cases. The missing cases are

• O₁.p = O₂.p ∧ O₂.id < O₁.id
• O₁.p = O₂.p + 1 ∧ O₁.id < O₂.id

It would seem that these cases can only occur when there is a causal dependence between O₁, O₂. Therefore we argue that this "incompleteness" is acceptable as long as we only ET concurrent operations. Therefore we have the following algorithm for ET

// Assumes O1 || O2
ET(Operation& O1, const Operation& O2)
{
    if (O2.p < O1.p) --O1.p;
}

We may return to this incompleteness issue in a future paper that addresses the support for selective undo - because that requires transpose of causally dependent operations.

Proof of convergence

TP1: Let the initial document state be S. We want to show that

∀O₁,O₂, S + [O₁ IT(O₂, O₁)] = S + [ O₂ IT(O₁, O₂) ].

Let |S| = n and S_i denote the i^th character in S. Let O₁ = ins(p1,c1). O₂ = ins(p2,c2). O₁, O₂ both execute on state S. Let O₁' = IT(O₁,O₂) and O₂' = IT(O₂,O₁).

Let S1 = S + [O₁] = [S0 S1 ... Sp1-1 c1 Sp1 ... Sn-1] and S2 = S + [O₂] = [S0 S1 ... Sp2-1 c2 Sp2 ... Sn-1].

There are four cases to consider

Note that the relative order of characters is preserved under IT. This relates to the requirement of user intention preservation.

TP2: Need to show ∀ O₁, O₂, O₃, IT( IT( O₃, O₁), IT(O₂, O₁)) = IT( IT( O₃, O₂), IT(O₁, O₂))

Continuing the conventions in the proof of TP1, let O₃ = ins(p3,c3).

Suppose p1 < p2. Then there are seven cases to consider. The following table shows the shifts (i.e. Δp3) applied to p3 as O₃ ITs first past O₁ then O₂' = ins(p2',c2), or alternatively first past O₂ then O₁' = ins(p1',c1). Note that p2' = p2+1, and p1' = p1.

There is a consistency in the relationship between p1,p3 (irrespective of whether O₃ ITs past O₁ first or O₂ first): In the first five rows, when O₃ ITs first past O₂, p3 is not changed (Δp3 = 0). Also p1' = p1 so the relationship between p1,p3 is preserved. In the last two rows, when O₃ ITs past O₂, p3 is incremented. This still means p3 > p1 so again the relationship between p1,p3 is preserved.

There is a consistency in the relationship between p2,p3 (irrespective of whether O₃ ITs past O₁ first or O₂ first): In the first two rows, when O₃ first ITs past O₁, p3 is not changed (Δp3 = 0). In these cases p3 < p2 and also p3 < p2' = p2+1, so the relationship between p2, p3 is preserved. In the last five rows, when O₃ ITs past O₁, p3 is incremented. However O₂' also has its position p2 incremented, so the relationship between p2, p3 is preserved.

In all cases the total shift applied to p3 is the same, and therefore condition TP2 is proven. By symmetry we see that TP2 is also proven when p2 < p1.

Let p = p1 = p2, WLOG assume O₁.id < O₂.id. Therefore O₁' = ins(p1,c1) and O₂' = ins(p2+1,c2). There are five cases to consider. The following table shows the shifts (i.e. Δp3) applied to p3 as O₃ ITs past O₁ then O₂', or alternatively O₂ then O₁'. In all cases the total shift is the same, and therefore condition TP2 is proven.

Alternative proof of convergence

At quiescence all sites have executed all the insert operations. Therefore all sites agree on the set of characters that have been inserted. Therefore to show convergence, it is sufficient to show that all sites agree on a total ordering of the characters.

Consider that we break up the text document into groups of characters, where characters within a group were tied for insertion position during IT (and therefore site ids were used to break the ties). It is claimed that all the following are true

1. All sites agree on the assignment of characters to these groups.
2. There is agreement by all sites on a total ordering of these groups.
3. Within a group, the characters are ordered according to the total ordering on the site identifiers.

Cell 1 relates to the division of the characters into the groups, and cell 2 to the ordering of operations within a group.

It follows that all sites agree on a total ordering of the inserted characters.

System 2: Insert and track operations

System 2 extends System 1 by allowing for "track" operations, in addition to insert operations. That is, System 2 supports the following two operations:

• ins(p, c) — insert character c at position p.
• trk(p) — track the character at position p.

The "track" operation doesn't have any side effects. Its only purpose is to track the location of a character.

The solution is expressed with the following two additional cells

Cell 3 says that tracking operations have no effect on each other. Cell 4 says we need to increment the position of a tracked character when there is an insertion at the same position or to the left.

IT(Operation& O1,const Operation& O2)
{
    if (O2.ins)
    {
        if (O2.p < O1.p || O2.p == O1.p && (O1.trk || O2.id < O1.id))
        {
            ++O1.p;
        }
    }
}

ET(Operation& O1,const Operation& O2)
{
    if (O2.ins && O2.p < O1.p)
    {
        --O1.p;
    }
}

Note that ET assumes O₁ || O₂, so it never sees the case of t(O₁) = trk, t(O₂) = ins and O₁.p = O₂.p.

Proof of convergence: The tracking operations have no effect on the document state; therefore convergence is achieved because we continue to use cells 1,2.

System 3: Insert and delete operations

System 3 extends System 1 by allowing for single character delete operations, in addition to single character insert operations. That is, System 3 supports the following two operations:

• ins(p, c) — insert character c at position p.
• del(p) — delete the character at position p.

A correct solution to IT and ET is surprisingly difficult and there have been many attempts in the last 15 years by researchers that have failed to correctly provide both properties TP1 and TP2. Some researchers have avoided the problem by employing a control algorithm that doesn't require TP2 for convergence. However, [1] points out that it is necessary to address ERV puzzles to preserve user intention correctly, and only the solutions in [1] and [2] have addressed the ERV puzzles.

The solutions that appear in [1] (SDT) and [2] (SDTO) appear correct but are quite complex and this paper describes a far simpler solution. Importantly the proposed approach leads to a far more economical implementation, and doesn't require a change to the control algorithm as required by both [1] and [2].

Note firstly that (in System 1 or 2) we have a working solution that satisfies both TP1 and TP2 when we limit ourselves to insertion operations only. It seems that delete operations are the "fly in the ointment". This leads to the following central idea: to imagine that all delete operations on the document have been disabled! The result would be that the document contains all characters that have ever been inserted into the document. The useful thing here is that we get a total ordering on all characters. This forms the basis of correctly determining the effects relation between any two operations.

The Effects Document is only a theoretical tool - it is not actually stored. For each operation we keep track of both the position p in the normal document (in which deletes are allowed to take effect) as well as the position q in the Effects Document (in which all delete operations are ignored). The effects relation is then as simple as comparing q positions instead of p positions. The "false ties" according to [1] are precisely the cases where p positions are tied but q positions are not.

So by comparing q positions, we correctly determine when one operation is to the left of another, avoiding the problem of prematurely resorting to site ids to break the tie. This is used to update both the p and q positions as required. Note that because delete operations never occur on the Effects Document, a q position is never shifted to the left.

Let each operation contain the following fields.

Let ins(p,q,c) represent the operation to insert character c at the given p-position and q-position. Let del(p,q) represent the operation to delete the character at the given p-position and q-position. Let ~del(p,q) represent a disabled deletion operation. Insertion operations cannot be disabled.

Analysis using cells

The following sections provide an analysis using our "cells".

Insert with insert

Cells 5,6 account for transforming insertion operations with insertion operations, and are analogous to cells 1,2 described previously. Note that only the q-position is tested, while both the p-position and q-position are shifted.

Delete with insert

In cell 7 we have a delete on the left of an insert, causing the insertion position to be shifted to the left. Note that the p-position is adjusted, but not the q-position.

In cell 8 we have an insert on the left of a delete, causing the deletion position to be shifted to the right. Note that both the p-position and q-position are shifted.

Delete with delete

In cell 11 we have a delete on the left of another delete, causing the deletion on the right to shift to the left. Note that the p-value is adjusted, but not the q-value.

In cell 12 we have two delete operations that delete the same character. Both of the operations are disabled after transformation.

The Boolean enable flag is sufficient for contextually valid operations. As established by the reachability invariant below, a valid history buffer contains exactly one enabled delete of a given character—the first—and all subsequent deletes of that character are disabled. The transformation functions are defined on these reachable operation states, rather than arbitrary combinations of field values.

Algorithm

The following tables provide the implementations of IT and ET (in C++) based on the types of operations O₁ and O₂.

Comments on use of enable flag

This algorithm makes use of an enable flag to avoid deleting a character twice. Note that the first operation in a linear history buffer to delete the character is enabled, and all subsequent delete operations are disabled. Therefore, sites may disagree about which operation actually deleted the character! This is reasonable because we are only interested in convergence of the final document state.

Reachability invariant (editorial note)

The following invariant supplies a condition that was implicit in the original account but is needed to justify the Boolean enable flag precisely:

For each character identity, if a valid linear history buffer contains one or more delete operations targeting that character, exactly the first such delete is enabled and every subsequent such delete is disabled.

The invariant holds for an empty history buffer. A locally generated delete targets a visible character and is initially enabled, so its causal context contains no effective delete of that character. When an enabled incoming delete is IT'd through the concurrent suffix, it remains enabled if the suffix has no same-target delete. Otherwise the first same-target delete in the suffix is enabled and disables the incoming delete; later same-target deletes are disabled and have no further effect. If an already-disabled delete is forwarded, its enabled predecessor occurs earlier in the sender's valid serialisation and is included in the operation's context, so it occurs in the receiver's prefix. Appending the received delete therefore preserves the invariant.

It remains to check history-buffer transposition. For adjacent same-target deletes the only reachable enable states are [enabled, disabled], when they are the first two such deletes, and [disabled, disabled], when an enabled predecessor occurs earlier. In the first case, ET re-enables the second delete and IT disables the first, after which swapping them again gives [enabled, disabled]. In the second case neither ET nor IT changes an enable flag and the pair remains [disabled, disabled]. A pair [disabled, enabled] is unreachable. Transpositions involving an insertion or deletes of different characters do not change how many deletes target a character. Thus local generation, remote integration, and every adjacent transposition preserve the invariant, and induction establishes it for every reachable history buffer.

Alternative exposition

Definition 1:

For operation O, let shiftp(O) and shiftq(O) be defined as follows:

Algorithm

IT(O1,O2)
{
    if (O2.enabled && !O1.ins && !O2.ins && O1.q == O2.q && O1.enabled)
    {
        O1.enabled = false;
    }
    else if (O2 < O1)
    {
        O1.q += shiftq(O2);
        O1.p += shiftp(O2);
    }
}

ET(O1,O2)
{
    if (O2.enabled && !O1.ins && !O2.ins && O1.q == O2.q && !O1.enabled)
    {
        O1.enabled = true;
    }
    else if (O2 < O1)
    {
        O1.q -= shiftq(O2);
        O1.p -= shiftp(O2);
    }
}

Proof of correctness

There is a useful mapping from system 3 to system 2, where delete operations are mapped to tracking operations, and the effects document is mapped to a document in which delete operations are never performed. This immediately gives us two useful results - that convergence of the effects document is achieved, and delete operations correctly track the location of the character within the effects document.

Completion of the convergence proof (editorial note)

The preceding lemmas can be strengthened into a direct argument that transformation through a valid set of concurrent operations is independent of the order in which that set is serialised. Give every inserted character its operation identity. The insertion rules place these identities in one total effects order: q-position is primary, and the total order on site identifiers breaks a genuine tie between concurrent insertions. Deletes do not alter that order.

For an operation O transformed through a context A, its resulting fields have the following interpretation:

1. O.q is its boundary or target position after inserting the members of A that precede O in the total effects order.
2. O.p is the corresponding visible rank after omitting the distinct character identities deleted to its left by A.
3. If O is a delete, O.enabled is true exactly when A contains no earlier delete of O's target identity; once the first same-target delete has been encountered, O is disabled and later disabled representatives have no further effect.

The first item follows from the insertion-only result for System 1. The second follows because an enabled delete shifts precisely the operations whose visible positions lie to its right, while the reachability invariant ensures that several deletes of one identity contribute only one such shift. The third is exactly the enable invariant. Each item is therefore a function of the context's inserted identities and distinct deleted identities, rather than of the chosen valid serialisation of that context.

Consequently, for three concurrent operations O₁, O₂, O₃, transforming O₃ through O₁ followed by IT(O₂,O₁) gives the same q-position, visible p-position and enable state as transforming it through O₂ followed by IT(O₁,O₂). Its type, identity and character are never changed. The resulting operations are equal, establishing TP2 on the contextually valid domain. TP1 follows from the same canonical interpretation for a context containing two operations: both execution paths construct the same effects order and omit the same set of deleted identities.

At quiescence every site has received the same insert operations and hence, by Lemma 5, has the same effects document. Every site has also received the same delete operations. By Lemma 4 they target the same character identities, and by the reachability invariant each identity targeted one or more times is omitted exactly once. The visible document at every site is therefore the common effects document filtered by the same set of deleted identities. Lemma 7 preserves the order of the remaining characters, so all sites have the same visible document. This completes the convergence proof for System 3.

Intention preservation (editorial note)

“Intention” cannot mean an unrecorded subjective purpose of the user. In the CSM model of [1] it has an operational meaning: preserve the effect of each operation and the effects relation between operations. For the operations in this paper, the effect of an insertion is to introduce its fresh character identity at a particular boundary in the effects order; the effect of a deletion is to make the character identity selected at generation invisible. The effects relation is the relative order of the character identities. Concurrent insertions at the same boundary did not previously have a relative order, so ordering them by site identifier completes, rather than contradicts, the recorded intention.

Correctness status (editorial note): Systems 1 and 2 have the convergence arguments given above. For System 3, the reachability invariant and canonical-context argument complete the TP1, TP2 and quiescent-convergence argument for contextually valid operations processed by the stated history-buffer control algorithm. This does not define IT or ET on arbitrary combinations of field values that cannot arise in a valid history. Lemma 8 completes intention preservation for the CSM effects-and-effects-relation meaning applicable to these primitive operations; it does not claim to formalise arbitrary subjective user intention or provide a general selective-undo theory.

Generation of operations

When generating an operation it is necessary to correctly initialise both the p-position and q-position stored in the operation. To support this it is necessary to be able to map from p-position to q-position. Therefore a document needs to maintain information about where characters have been deleted. An efficient implementation can store run-length encoded information. However, for the purposes of easily understanding the requirements, consider that an array B[] of booleans flags is stored, indexed by q-position. Let B[q] be false to indicate that the qth character has been deleted, otherwise B[q] = true.

To generate an operation to delete the pth character, we calculate the q-position as follows

int Getq(int p)
{
    int n = B.size();
    int pi = 0;
    for (int i=0 ; i < n ; ++i)
    {
        if (B[i])
        {
            if (pi == p)
            {
                return i;
            }
            ++pi;
        }
    }
    return n;
}

When operation O = del(p,q) is executed, B[] is updated as follows

void UpdateBForDelete(int p,int q)
{
    B[q] = false;
}

When operation O = ins(p,q,c) is executed, B[] is updated as follows

void UpdateBForInsert(int p,int q)
{
    B.insert(B.begin() + q, true);
}

Note that the q-positions (not the p-positions) stored within the operation are used to update B.

Tests

The algorithm was tested by simulating between two and nine sites making randomly generated single-character insertions and deletions and exchanging them in arbitrary causally valid orders. Convergence was checked repeatedly between sites during each simulation and across all sites after every operation had been exchanged. Sites were required to agree on the complete effects document, including character identities and visibility.

A total of 10,000 simulations of 1,000 events each completed without a convergence failure. The number and variety of operations, sites and exchange orders covered by this testing provide very high confidence in the correctness of the algorithm.

Browse the test files.

Related work (editorial note)

During 2004, David Barrett-Lennard was studying the TP2 puzzles, including examples like the one described in Operational Transformation On Text. He observed that there were no such puzzles when all sites performed only insertions, and none when all sites performed only deletions: the puzzles arose when insertions and deletions were both present.

In early 2005 he read Du Li and Rui Li's work on the operation effects relation. Their idea led directly to the realisation that positions could be tracked as though deletions had not taken place. This preserves the correctness of the insertion ordering by preventing deletions from destroying the positional information on which that ordering depends. Li and Li's effects relation was therefore the key inspiration for the Effects Document introduced in this paper, and their contribution to the idea deserves explicit credit. Their work identifies preservation of the effects relation between concurrent operations as a consistency requirement for group editors; see Preserving Operation Effects Relation in Group Editors, published in November 2004.

The Effects Document is a hypothetical document containing every inserted character while treating all delete operations as disabled. It provides a simple way to calculate the effects relation while retaining the ordering information needed by insertion operations.

This line of work was subsequently examined by Gérald Oster, Pascal Urso, Pascal Molli and Abdessamad Imine in the INRIA research report Proving Correctness of Transformation Functions in Collaborative Editing Systems, published in December 2005. They used the SPIKE automated theorem prover to find counterexamples in several existing operational transformation algorithms, including Li and Li's SDT and SDTO algorithms. The counterexamples helped them develop Tombstone Transformation Functions (TTF), which retain deleted characters as invisible tombstones and were formally checked against TP1 and TP2.

TTF preserves the operation effects relation. Conceptually, it shares the central insight of the Effects Document: deleted characters remain available as stable ordering landmarks. The INRIA authors also explicitly describe their use of tombstones as an adaptation of the WOOT approach, developed in Real Time Group Editors Without Operational Transformation. TTF should therefore be understood as connecting Li and Li's effects relation with the tombstone representation used by WOOT, rather than as deriving solely from either one.

References

1. Du Li and Rui Li, Ensuring Consistency in Real-Time Group Editors, ACM Transactions on Computer-Human Interaction, April 2004. Under review at the time of writing.
2. Du Li and Rui Li, An Operational Transformation Algorithm and Performance Evaluation, Journal of CSCW, July 2005. Under review at the time of writing.
3. Matthias Ressel, Doris Nitsche-Ruhland and Rul Gunzenhäuser, An Integrating, Transformation-Oriented Approach to Concurrency Control and Undo in Group Editors, Proceedings of CSCW 1996, pages 288–297, 1996.

Source code

The historical C++ implementation is retained as a documentation resource. It implements the Boolean enable-flag algorithm described above. Its transformation functions assume the contextually valid operation states characterised by the reachability invariant in the editorial completion of the proof. Browse the source files.