You are here

MEMO: Synchronization

Introduction

This document targets the synchronization problem between two or more communicating entities, each having its own copy of the document. The specific application in mind is whiteboarding which is assumed to consist of a number of independent items, such as rectangles, paths, images etc. Each item has a state made up of its features, such as coordinates, colors, etc.

The task of this paper is to describe a method to achieve synchronization between two or more entities without any involvement of a third party. In addition, we show that no extra communication is needed to achive this. In
short, we describe a self-synchronization algorithm.

The application in mind is an XMPP network for transporting SVG graphics (Scalable Vector Graphics (SVG) 1.1 Specification, Mobile SVG Profiles: SVG Tiny and SVG Basic), but the analysis is not limited to this.

Assumptions

A few assumptions go into this discussion:

  • Two or more interacting entities A, B and C etc.
  • Single item at A and B, with no dependencies on other items.
  • Atomic operations which means only a single attribute is changed in an edit operation. There is no loss of generality in this assumption since an edit operation can be defined to be composed of several other atomic operations.
  • Each entity must keep an item specific undo stack to be able to revoke recent edits. Note that this is not the customary application or whiteboard instance specific undo stack.
  • All operations are assumed to be noncommutative, that is, order matters. This is a conservative measure that can be relaxed later. But if a method works for noncommutative operations it works in all situations. The case with commutative operations only is, of course, trivial.
    Commutative: ab = ba,
    Noncommutatitve: ab != ba
  • All edits are transported serially, or in other words, they are received in the same order they are created.

We will start with the simpler case of two interacting entities.

Notations

The state of a particular item is denoted S. An items state consists of all the attributes that describe it, such as coordinates, colors, strokes, fills etc.

The initial state of the item is S_0 and it can safely be assumed that it is identical at both A and B since the entity that creates it just transmits it to the other entity without any intervention.

Each item has a version attribute with an initial value of 0. The state with version i is denoted S_i.

Edit operations also carry a version attribute. Edits are denoted a, b, c,... and with version i they are a_i etc., or with numbers a1, b2, etc. It can be helpful to picture an edit operation in xml as,

<Edit(a) version='i' id='...' .../>

The state after an edit a1 will be S(a1), and after a sequence of edits, S(a1 b2 c3) etc.

Describe a timeline from left to right, for the entities A and B. See below.

  S_0   S_1(a1)            S_2(a1b2)
A ----------------------------------------------------------------------
     \                   /             \      /
    a1\                 /               \    /
       \               /                 \  /
        \             /                   \/
         \         b2/                    /\
          \         /                    /  \
B ----------------------------------------------------------------------
  S_0      S_1(a1)  S_2(a1b2)
                                                  ---> time

Figure 1.

Edit operations are initiated either by A or B, and transported to the other entity, which is pictured by "/" or "\" lines. These are the "edit lines". Each edit line has an operator a_i etc., here indicated by a1 and b2.

In this figure it is important to distinguish between noncrossing sections and crossing sections. It is evident from the figure which is which. Noncrossing sections will never result in any synchronization problems since all edits will be applied in the same order at both A and B. Thus, only crossing sections need to be considered.

Edit operations, or edits, can be of two types:

  • Local edits that the initiating entity applies to its own item.
  • Remote edits that are represented by a remote edit operation that is
    received from the other entity.

Edits can either be:

  • Adopted (accepted)
  • Rejected

Local edits are always trivially adopted. Remote edits can either be adopted or rejected. It is the task of this document to decide which cases to reject and how to change an items state after a rejection to achieve mutual
synchronization.

It is perfectly clear that perfect synchronization between two entities cannot be achieved at any time since travel time (think speed of light plus something) is larger than zero. We relax the task to achieve synchronization between the two entities after all edits from another entity have been received.

Description

An edit operation is constructed locally by the entity that makes it. It always get a version attribute "one plus" the items version attribute, and the items version is incremented by one when the edit is applied.

Before an edit a:

S_2()

After:

S_3(a3)

and the edit is, of course, a3.

We can describe this formally as:

a_i+1 S_i(*) = S_i+1(* a_i+1)

where we have used * for all the (accepted) edits, if any, that have been applied to the item so far.

A remote edit will either be accepted or rejected. In any case the items versionattribute is incremented with one irrespective of the edits version number,

a_i S_j(*) = S_j+1(**)

where we have indicated the new state by ** which we will define below.

Lets start with the normal case with noncrossing sections, thus no conflicting edits. Picture it as:

  S_0  S_1(a1)               S_2(a1b2)
A ----------------------------------------------------------------------
      \                   /    
     a1\                 /     
        \               /      
         \             /       
          \         b2/        
           \         /         
B ----------------------------------------------------------------------
  S_0       S_1(a1)   S_2(a1b2)

Figure 2.

Local edits are always trivially accepted so we only need to describe the remote edits. In our case we get,

b_i+1 S_i(a_i) = S_i+1(a_i b_i+1)

that is, apply the edit and increment the version with one. However, in a more general case the edits may be denoted *,

b_i+1 S_i(*) = S_i+1(* b_i+1)

with the same interpretation as above. Thus, following an entities timeline, the items version number increases monotonically with one for each edit: 1, 2, 3,... This is true for any case, also for rejected edits. Important!

Remote edits that will be adopted will have an edit version which is exactly the items version plus one, that is,

b_i+1 S_i(*) = S_i+1(* b_i+1)

which is identical to a local edit. We can therefore make the likely hypothesis that remote edits with version not one plus the items number shall be rejected since they are "out of sync".

The remaining and most important question is to determine how the items edit state shall be changed when an edit is rejected. Lets start with the normal accepted states to see the patterns:

c3 S_2(a1 b2) = S_3(a1 b2 c3)

while a rejected case will look something like,

c2 S_2(a1 b2) = S_3(???)

where we will define the question marks below.

As an example, consider a state S_3(a1 b2 c3) with an incoming edit d1. Our hypothesis will be to undo all edits with version numbers larger or identical to the remote edits version number. Thus,

d1 S_3(a1 b2 c3) = S_4()

A few more cases to trace out the pattern:

d2 S_3(a1 b2 c3) = S_4(a1)

d3 S_3(a1 b2 c3) = S_4(a1 b2)

to compare with the adopted case,

d4 S_3(a1 b2 c3) = S_4(a1 b2 c3 d4)

It may also happen that the edits version is larger than any of the items edit state numbers. In this case no change of the items state is made,

c3 S_3(a1) = S_4(a1)

If we put this in formal terms it reads,

a_i S_j(..., i-1, i, i+1,...,k) = S_j+1(..., i-1)   for k >= i, i != j+1

where we have simplified the notation slightly. If i is larger than k we get,

a_i S_j(...,k) = S_j+1(...,k)   for k < i, i != j+1

If we take the short description, a remote edit, a_i+1 S_j(q_k), with i != j and k > i will result in a new state S_j+1(q_i) where q_i is a previous edit state. If k <= i the edit state is unchanged.

Use Cases

Before presenting a formal evidence of this method, lets look into a few examples which will make the method plausible. Consider these cases and convince yourself of that the end states are identical despite conflicting edits. We
don't consider noncrossing sections unless to verify that we retain a synchronized state. We denote the initial state S_0 which is the same as S_0().

  S_0 S_1(a1)  S_2()    
A ----------------------------------------------------------------------
      \     /       
     a1\   /        
        \ /         
         \       
        / \        
     b1/   \       
      /     \
B ----------------------------------------------------------------------
  S_0 S_1(b1)  S_2()

Figure 3.

           S_2(a1b2)
  S_0 S_1(a1)          S_3()  S_4()
A ----------------------------------------------------------------------
      \   \          /     /  
     a1\ b2\        /     /   
        \   \-------     /
         \ / \          /
          \   \        /
         / \   \      /
        /   \   -----/
     c1/     \    d3/\
      /       \    /  \
B ----------------------------------------------------------------------
  S_0 S_1(c1)  S_2()    S_4()
                   S_3(d3)

Figure 4.

  S_0 S_1(a1)   S_2()    S_3()    S_4()              S_5(e5)
A ----------------------------------------------------------------------
      \       /        /        /                   \
     a1\     /        /        /                   e5\
        \   /        /        /                       \
         \ /        /        /                         \
          \        /        /                           \
         / \      /        /                             \
        /   --------------/                               \
     b1/      c2/      d3/\                                \
      /        /        /  \                                \
B ----------------------------------------------------------------------
  S_0 S_1(b1)           S_3(b1c2d3)                           S_5(e5)
               S_2(b1c2)      S_4()

Figure 5.

In the above example we also added a nonconflicting edit to the right to verify that a new edit will be accepted.

           S_2(a1b2)
  S_0 S_1(a1)   S_3()         S_4()
A ----------------------------------------------------------------------
      \   \   /             /
     a1\ b2\ /             /
        \   \    ----------
         \ / \  /        
          \   \/
         / \  /\
        /   \/  -----------
     c1/  d2/\             \
      /    /  \             \
B ----------------------------------------------------------------------
  S_0 S_1(c1)  S_3()         S_4()
	   S_2(c1d2)

Figure 6.

It is evident from the examples above that a crossing section revokes all edits for both entities to their original state that they have before the crossing section. With an initial state S_0() we get the final state S_k() with k > 0.

Proof

Use the items version numbers to define a sequence for each entity. By definition all version numbers describe the sequence of natural numbers starting with 0. (Well, 0 is not a natural number but we add 0 to this set.) More precisely, the numbers describe the items version number it receives after the edit has been applied. The number at the edit lines initiator end is the edits version number.

   0  1 2  3 4 5              6           7
A ----------------------------------------------------------------------
      \  \ / \/               \          /
       \  /  /\                \        /
        \/ \/  \                \      /
        /\ /\   \                \    /
B ----------------------------------------------------------------------
   0   1 2 3 4   5                6   7

Figure 7.

Crossing lines will generate unequal numbers at each end of the edit line. Only edit lines with identical numbers at each end will be accepted by both entities. In the above case these are 6 and 7.

Note also that for the edit lines in the crossing section the initiator end will have a strictly lower number than the target end. The first and last edit of each entity in the crossing section must have at least one crossing by
definition. Any edits inbetween must have at least two crossings to "link together" the edits. The difference between an edits target number and its initiator number (its version) is identical to the number of crossings.

Prove that all crossings generate unequal version numbers, and noncrossing lines will give identical numbers.

From the figure it is evident that any noncrossing line (edit) have identical versions, and thus no conflicts. It is also evident that this is the only possibility to generate edits with identical versions.
QED

It must also be proven that both entities states after a crossing section are identical.

Consider, for instance, the entity A. It will make a local edit 1, and possibly zero or more edits after that, before receiving the edit from B, which will have version 1. In any case the receiving edit will be in conflict and thus rejected
since version numbers will not match. Also, all edits made (1, 2,..k ; k>=1) will be revoked taking it back to its original state S_0.

If we denote this slightly more formally as B's first edit a1, and A's state when receiving B's first edit will be S_k(q1,...,q_k) where k >= 1. The operation will be,

a1 S_k(q1,...,q_k) = S_k+1()    with k >= 1

The a1 edit line will have 1 in its initiator end and k+1 at its target end,

1 --- k+1

It remains to be proven that any subsequent edits A receives will revoke any local edits made by A. By assumption none of B's edits will be adopted.

Assume that A makes zero or more edits before receiving B's next edit denoted b. If zero edits made there is nothing to prove. Assume therefore that A has made the local edits q_k+2,...,q_m, and its state is

S_m(q_k+2,...,q_m)    with m >= k+2

The crucial question is the version of B's edit b. In particular we must know its highest version number possible since this gives the largest chance of A's edits to not be revoked.

By assumption it must cross A's last edit before receiving a1. This will give b its max version. Since A has made k edits and B one, its max version must be k+1. Apply the edit to A:

b_k+1 S_m(q_k+2, ..., q_m) = S_m+1()

since all higher edits than k+1 will be revoked. During this discussion it is helpful to consider figure 8 below.

           k   k+1 m   m+1
   0   1   2   3   4   5
A ----------------------------------------------------------------------
       \   \  /    \ /
        \   \/      /
         \  /\     / \
          \/  \   /   \
          /\   \ /     \
         /  \   \       \
        /    \ / \       \
B ----------------------------------------------------------------------
   0    1    2 3  4       5
                  k+2        

Figure 8.

The reasoning above can now be applied to any subsequent edit A will receive from B without loss of generality. This will be described now.

Consider two consecutive edits at B, b and c, and A's edit just before it receives b from B, see figure 9. Give the edit a version k. This means that

           k   k+1
A ----------------------------------------------------------------------
          a\  /   \\\/
            \/      /
            /\     / 
     ...   /  \   /    ...
          /    \ /   
         /      \    
       b/     c/ \   
B ----------------------------------------------------------------------
              k+1 k+2

Figure 9.

the number of edits A has made, including a, plus the number of edits it has received from B, is equal to k. Consider now B when it receives edit a. It must have received all of A's edits up to and including a, as well of all B's
edits plus the two b and c. Thus the index is k+2. If we seek the max version of the edit c, that must be the nearest lower index, k+1. As above, it is the largest edit index which gives A's edits the highest chance to not be revoked.
Convince yourself of that any edits A has made before a, that are received by B after the edit c, will result in a lower edit number of c relative k+2. Assume now that A has made a number of edits after k+1, indicated by \\\ in the figure. This will make A's state just before receiving the edit c as,

S_m(q_k+2,q_k+3,...,q_m)   with m >= k+2

Note that when the edit q_k+2 is applied, the state is identical to the initial state. It is now a simple matter to apply edit c as,

c_k+1 S_m(q_k+2,q_k+3,...,q_m) = S_m+1()    with m >= k+2

All edits will be revoked once again.

Thus, A's state after the crossing section will be identical to its initial state at the start of the crossing section. By symmetry, the same will be true for entity B.
QED

Alternative Proof

Show that an edit line a from A that is being crossed by at least one edit from B will have its local edit revoked and its remote edit rejected.

Since its target end will have a number larger than its init end, the edit a at B will not be accepted.

By assumption there is at least one edit from B that crosses a. Assume that there are m >= 1 crosses of a, see figure 10. We have arbitrarily denoted a's version with k, and also denoted the first crossing edit with b. The last of
these edits that A will recive will have an index k+m+... where ... will be the number of local edits made after a but before k+m+...

           k   k+1   k+m+...
A ----------------------------------------------------------------------
          a\  / ... /
            \/     / 
            /\    /  
     ...   /  \  /      ...
          /    \/    
         /     /\    
       b/ ... /  \   
B ----------------------------------------------------------------------
	i         k+m

Figure 10.

The edit a will have its target index k+m since there are m crossings. Denote the number of crossings of edit b in addition to the edit a with n, n >= 0. This is equal to the number of edits B will receive between its local edit b and
receiving edit a. Thus there are n+1 crossings of edit b. It is now a simple matter of arithmetic to find b's version number i,

i = (k+m) - m - n = k-n   with n >= 0

or

i <= k

We can now apply edit b at A as,

b_i S_k(a_k) = S_k+1()     since i <= k

Thus, also a's local edit will be revoked.

By symmetry this is valid for all edits that are being crossed, independently of A or B.
QED

Multiple Entities

(with Joonas Govenius)

It is important to consider seriality in this case, or in other words, edits are transported sequentially through a server. Consider figure 11 where we have shown two entities, A and B, between which an edit a takes place, and a third
arbitrary entity C. We may consider entity C to comprise all other entities not A or B because:

  1. We do not consider individual version numbers for edits from C.
  2. Edits not from A or B will be delivered to A and B via the same point on the server.
			P1
A ----------o-------o---o---o-------------------------------------------
           /  ...  /    a\ /
          /       /       /     P2
B -------o-------o-------o------o---------------------------------------
        /       /       /   \  /
       /       /       /     \/
  ====*=======*=======*=======*=========================================
     /       /       /         \
    /  ...  /       /           \
C -o-------o-------o-------------o--------------------------------------

Figure 11.

We have symbolically shown the server, or sequencer, with ===. Each actual edit, local or remote, are indicated with -o-. Sequencing implies that the number of C's edits that reach A before P1 is smaller or equal to the number of its edits that reaches B before P2. Thus, an edit a between two entitites divides the edits from a third entity into two sets.

Edit a is any edit from A that is being crossed by one or more edits from B. We denote the first edit of B that crosses a with b. The formal proof makes use of the following notations and figure 12 below.

Notations:

Points: P1 is where edit a is made by A
	      P2 is where edit b is made by B
	      P3 is where edit a is received by B
	      P4 is where edit b is received by A

A: The edits up to and including P1:
     kA is the number of local edits made by A, a included
     kB is the number of edits received from B
     kC is the number of edits received from C

B: m is the number of B's edits that cross edit a, with b being the first one;
   m > 0
   n+1 is the number of A's edits that cross b, edit a included; n >= 0
   p is the number of C's edits received by B up to P3
   r is the number of C's edits received by B up to P2
   i is the unknown version (index) of edit b
				 (P4)
		     (P1)        kA+kB+kC+1
		     kA+kB+kC    |
A -----o-----o-o-----o--o--------o-----o--------------------------------
      / kC  /   \  n  \  \      /     /
     / ... /     \ ... \ a\    /  m  /
                           \  / ... /
                            \/     / 
                            /\    /  
                     ...   /  \  /      ...
                          /    \/    
                        b/     /\    
                        / ... /  \   
B ------o------------o-o-----o--o-o-------------------------------------
       /      r     /  i       /  kA+kB+m+p 
      /     ...    /  (P2)    /   (P3)
     /       p               /
    /       ...             /
C -o-----------------------o--------------------------------------------

      ... \    \    \    \    \    \    \ ...

R ----------------------------------------------------------------------

Figure 12.

A few notes on the indices of figure 12. At P1 the index is kA+kB+kC by our definitions. At P3 we have received exactly kA edits from A, and the kB of B's edits received by A at P1 must be added with B's local edits not yet received
by A, which we have denoted m. In addition, B has received p edits from C. This makes kA+kB+m+p.

We now need to prove that edit a is revoked locally and rejected remotely.

If we impose seriality on edit a we get

kC <= p, or kC-p <= 0.

The condition for edit a to be accepted by B is,

kA+kB+kC = kA+kB+m+p

or

kC = m+p     with m > 0

or

kC-p = m     with m > 0

but this is inconsistent with the seriality condition above. Thus, any edit that crosses any other edit line will be rejected remotely.

We also need to prove that edit a will be revoked locally by edit b. The edit b's version number i is,

i = (kB+1) + (kA - (n+1)) + r = kA+kB+r-n,    with n >= 0

if we add the local edits, edits from A, and edits from C. If we impose seriality on edit b we get r <= kC since by assumption b is the first edit A receives after P1, and thus no edits from C between P1 and P4.

To revoke edit a locally we require,

i <= kA+kB+kC

or

kB+kA+r-n <= kA+kB+kC

which is simplified to,

r-kC <= n,     with n >= 0

By the seriality condition, r <= kC, or, r-kC <= 0, this is always true.

QED

It now remains to be proven that an entity R that makes no local edits will be consistent with any other entity. In particular, we need to prove that any edits between two other entities that cross will be revoked or rejected by R.

Consider figure 13 below where we have added the servers (sequencers) timeline in addition to A, B, C, and R. Let b be any edit made by B, and a an edit by A that crosses b, not necessarily the first crossing of b, but we make sure that A generates the first edit that crosses b. We denote edit u the last edit R receives before edit a. If edit a is the first edit that crosses b then edit u is identical to edit b.

		   k P1
A  ----------------o------------o-----------------------------------------
                   /\a         /
                  /  \        /
                 /    \      /
                /      \    /
B -------------/--o--------------o----------------------------------------
              /    \b    \/     /
             /      \    /\    /
            /        \  /  \  /
           /          \/    \/P5
  ========*============*==*==*============================================
         P2           P3 P4\  \
                            \  \
C ........................................................................
                              \  \
                               \  \
R ------------------------------o--o--------------------------------------
			     P6 u

Figure 13.

Note that the line P2->P1 is only a guideline. Any edits from B or C at P1 must have passed the server before P2.

There are two logical possibilities for a and b to cross; P3 < P5 or P5 < P3. Lets start by considering P3 < P5 as indicated in the figure. In this case we get in addition P3 <= P4 by assumption. We define the number of edits at P1 and P6 as

k = kA+kB+kC

u = uA+uB+uC

where the indices A, B, and C, indicate the origin of these edits. Since u is defined to be the last edit R receives before receiving edit a, we have

kA = uA+1

Since a and b cross we have P2 < P3. Therefore we get (with P3 <= P4),

kB+kC <= uB+uC-1

or

kB+kC+1 <= uB+uC

where the 1 comes from edit b. We now get,

k = kA+kB+kC = uA+1+kB+kC <= uA+uB+uC = u

or

k <= u

Thus, edit a will be rejected by R and edit u will be revoked. Note that this is true for edits coming from any entity that crosses b. This will also be true when a is the first edit to cross b, and thus edit b is identical to edit u and will therefore be revoked.

The other case where P5 < P3, and edit a reaches the server before edit b, follows directly from the above case if we just switch A <-> B and a <-> b using the symmetry.

QED

Short

  • Create an item edit of an item with version i as a_i+1 and increment the items version number by one, to i+1.
  • Accept a received edit a_i+1 only if our state is S_i. Increment items version by one to i+1.
  • Reject a received edit a_i+1 for our state S_j if i!=j. Increment items version by one to j+1. Remove all items edit state if any that are larger than i.

Generalizations

It may be possible to relax the assumption that all operations are noncommutative. The algorithmic complexity increases and it will probably be necessary that all implementations agree on an edit matrix of operations where each entry describes if any two edits commute or not.

Revisions

  1. 2006-06-13 initial version
  2. 2006-06-14 added alternative proof
  3. 2006-06-22 added proof for multiple entities

Copyright

Mats Bengtsson (June, 2006)
(parts with Joonas Govenius)