Development
- Bug tracker - To report bugs and feature requests
- Download development version - For bug hunting
- CIA.vc & coccinella-commits - To watch development progress
- List of supported XEPs
Building Coccinella Dependencies
These are build instructions for a typical unix/linux system which is not MacOSX since you need some special configure switches in that case.
I currently have a kind of ad-hoc rule to keep packages which should be binary compatible in a common directory, but this method may prove wrong, so please give me a note in that case. The following code should be easy to understand for anyone if you also have a look at the possible values of the tcl_platform array:
if {$this(platform) eq "unix"} {
set machine $tcl_platform(machine)
if {[regexp {[2-9]86} $tcl_platform(machine)]} {
set machine "i686"
} elseif {$tcl_platform(machine) eq "x86_64"} {
# x86_64
set machine "i686"
}
set machineSpecPath [file join $tcl_platform(os) $machine]
You can look into the coccinella/bin/ directory tree for a few examples.
Mandatory Packages
Tcl/Tk
First of all you need Tcl/Tk 8.5 if you do not already have it. Typically you do not get it from cvs HEAD since that usually points to an experimental version. Instead download it from Tcl Developer Xchange and follow the README.
Some notes on the directory layout. Place all sources dirs in a common directory like:
tcl/ tk/ tkpng/ tktreectrl/ ...-
TkTreeCtrl
cvs -d:pserver:[email protected]:/cvsroot/tktreectrl login cvs -z3 -d:pserver:[email protected]:/cvsroot/tktreectrl co -P tktreectrl ./configure make make install
The last step is not necessary but makes it easier to identify which components, *.so, pkgIndex.tcl, other .tcl support files, are needed.
TkPNG
cvs -d:pserver:[email protected]:/cvsroot/tkpng login cvs -z3 -d:pserver:[email protected]:/cvsroot/tkpng co -P tkpng ./configure make make install
Optional Packages
tls
Useful to obtain safer connections using TLS is the tls package.
cvs -d:pserver:[email protected]:/cvsroot/tls login cvs -z3 -d:pserver:[email protected]:/cvsroot/tls co -P tls ./configure make make install
Depending on how your SSL installation looks like you may need to specify certain configure flags which points to the wanted SSL system. I have noted that some linux users aren't able to load the standard i686 build, but have no idea why. You may find prebuilt binaries for your system here.
iaxclient
The voip system is using the iaxclient which you can grab at:
svn co https://iaxclient.svn.sourceforge.net/svnroot/iaxclient/trunk iaxclient
It depends on portaudio and speex and you may consult the README or mailing lists which versions match since there have been some incompatible changes. Build and install all three, first speex and portaudio, then iaxclient. That done you need to build my tcl package, you can find instructions here.
Tcl UDP extension
Iaxclient typically needs the Tcl UDP extension to penetrate NATs amongst others.
cvs -d:pserver:[email protected]:/cvsroot/tcludp login cvs -z3 -d:pserver:[email protected]:/cvsroot/tcludp co -P tcludp ./configure make make install
Tk Img extension
Support for additional image formats in whiteboards. TODO
Building Coccinella Executables
Coccinella, like most other Tcl/Tk based applications, is deployed using tclkits and starpacks. There is a very good tutorial describing all this. In short, a starpack is a Tcl/Tk application wrapped up together with a complete Tcl/Tk runtime into a single executable file. At the core there is only one command:
sdx wrap coccinella.exe -runtime tclkit-win32.upx.exe
This line is at the core of the build script, see below. Execute this only if you are not using the build script. See the tutorial for how sdx works.
You can build for any platform on any platform. That is, for instance, I build both linux-x86 and Windows versions on my Mac. You just need to have the proper tclkits to wrap up with. I recommend you use either a unix/linux or a mac system for building. Although it is possible to build on Windows, I have no experience with that.
Important:
Tclkit 8.5.x or later is required.
That said there are essentially two ways to build:
Using ActiveState
This method I've never tried myself, but Marion Bates has written
a detailed page of how to do it. I think there is a time limited trial download.
Using Build Script
I use a simple script on my Mac that builds the Windows and Linux versions. You can use this script for the Mac version as well, but I prefer to use Apples native way of doing this using application bundles, see below.
There are three things you need to download to start with:
- The sdx utility. See also here for more info.
- The tclkits
- My special tclkit for Windows
This assumes that you have an ActiveState Tcl/Tk installation or something compatible. This distro may include a sdx program, I don't know.
Next you need to get Coccinella's source code from either one of two places:
- directly from the Coccinella Subversion repository (for the brave ones)
- released source distro (do not forget to rename to coccinella)
And then there is, of course, my build script. You need to edit it at the indicated places to suit your directory setup. Note that Coccinella has a separate Subversion directory for tools which also contain build tools.
Then do:
- Put the tclkits in a directory, perhaps with sub directories indicating version numbers since the kit names lack version information. As an example:
tclkits/8.4.1/tclkit-coci.upx.exe
TclKits/8.4.11/tclkit-linux-x86.upx.bin - From your console, change directory so that you are in the same directory as Coccinella's source code coccinella/
- Put the build script
BuildCoccinella.tclthere also. May need to chmod u+x BuildCoccinella.tcl - Edit the build script where indicated (
@@@ Edit) so the paths point at your downloaded tclkits for each platform. - Run script as
tclsh BuildCoccinella.tcl - It takes a minute or so and status info is printed to the console.
After that you get a build/ directory with source distros and binary distros for Windows and Linux. You need to cleanup manually.
Mac OS X
On Mac I use Apples native packaging as an application bundle. Either take the latest released Coccinella, open the application bundle by control clicking, replace the coccinella folder with your own.
You can also get any other later TkAqua. Pick the self contained one (TclTkAquaStandalone). You need to copy the Info.plist file, the icon and the PkgInfo file from the original released Coccinella. Replace also the Contents/lib folder with the one in the Coccinella bundle since you do not need all of them. You can also get more detailed info from
(broken URL).
Other Platforms
The Subversion and the source distros are complete for Linux-x86, Windows, and Mac OS X, in the sense that no extra packages need to be obtained.
If you build for any other platform you need to obtain and build the
following packages:
Some more fixes are probably needed. Just contact me so we can sort out this.
Custom Builds
The simplest way to make custom builds is just to replace parts of the
sources with your own. Typically icons in the images/ directory. My build script has some support for custom builds. You need to edit the script to suit your needs. I have a test example. Just place it in the same directory as coccinella and edit the build script.
The custom build procedure is a bit out of date and will probably be revised, so beware!
How to Translate
- Log in to post comments
This tutorial will help you to translate Coccinella to a new language or to update an existing language catalog.
Instructions
-
To avoid double work, you first should contact the current translator(s) of your language, or ask in the forum if you would like to start a new translation. Wait a few days to see whether or not you get a response.
-
Then, download the latest translation sources and translation template and extract this file.
-
Proceed by installing a good computer-assisted translation (CAT) program with gettext support, such as Poedit, Lokalize, Kbabel, gtranslator, and Virtaal. Use this program to open the existing XX.po file for your language code. Or use this program to create a new translation using the template.pot file.
-
Translate untranslated strings, improve strings which are already translated, and/or review fuzzy strings (do not forget to remove the fuzzy status after reviewal). Please do not hesitate to ask in the forum if you have any questions about using the computer-assisted translation program.
-
Finaly, contribute your new or updated translation XX.po file by filing a new bug entry with attachment.
-
Your translation will be added to the development version and we will notify you about this. Less than 24 hours later, you can test your translation in the daily build.
Useful remarks
-
Note that some of the menu strings, have an ampersand "&" in their text string. This means that the character following it will be underlined and the "&" be removed from display text. The underlined character corresponds to a keyboard shortcut for that entry. You are free to pick the underlined character which suits your language yourself, but remember that each character may be underlined only once in a menu.
For an outstanding translation usability, we would suggest you to first simply translate all menu entries. Then, you should look at which letters are used for similar menu entries in popular software like Firefox and try to be as consistent as possible when selecting letters, without using letters more than once. Although this will take a lot longer, the quality of your translation will be much higher!
-
Some of the strings contain one or more "%s". These will be replaced by variables when the string is displayed. You need to see the code if you want to know the replacement variable.
In some cases your language may have a different grammar than English, and there may be situations where the order of the replacement variables must change. In such situations you need to add positional codes. An example describes it best:
{This is the %s and %s attempt} FIRST SECOND This is the FIRST and SECOND attempt {This is the %2$s and %1$s attempt} FIRST SECOND This is the SECOND and FIRST attemptYou just replace "%s" with "%#$s" where # is an integer describing the position.
Issues in Third Party Software
This page is to track issues with third-party software that have negative consequences for users who are using Coccinella. Issues may be trivial usability problems, critical compliance bugs, strange behaviour, crashes, amongst others. The final goal is to get these issues fixed in the third party software so that Coccinella users can benefit from a better end user experience.
| Software | Problem | Cause |
|---|---|---|
| PyMSNt | Ugly MSN JIDs in Coccinella's GUI | Lacks support for XEP-0106: JID Escaping |
| Tlen Transport | Tlen not available as option when adding contact | Patch to fix wrong disco of Tlen transport |
| jGGtrans | Automatic login does not work | ? |
| JJIGW | Wrong disco registrar type: 'x-irc' instead of 'irc' | Patch to fix wrong disco of JJIGW transport |
JabberLib
- Log in to post comments
One of the core parts of Coccinella is JabberLib, a BSD licensed library written in Tcl. Although the library is included in Coccinella, you also can download JabberLib as a separate download. The development version of the library is available in the Coccinella development repository. JabberLib hides all XML used by the Jabber/XMPP protocols. Additionally, a few test files are included to get you started, and although no documentation is available, there is a brief summary of commands in the prefix header of each source file.
Also a patched TclXML package, needed for XML parsing in Tcl, is included.
Projects Using JabberLib
- Coccinella - Advanced instant messaging application with whiteboard
- TkChat - The chat application for the Tcl Chatroom
- tclxmppd - Implementation of the XMPP server to server communications protocol
- Eggdrop Jabber Bot - Link IRC and Jabber IM together
MEMO: Synchronization
- Log in to post comments
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)
---> timeFigure 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 7Figure 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+2Figure 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+mFigure 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:
- We do not consider individual version numbers for edits from C.
- 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 uFigure 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
- 2006-06-13 initial version
- 2006-06-14 added alternative proof
- 2006-06-22 added proof for multiple entities
Copyright
Mats Bengtsson (June, 2006)
(parts with Joonas Govenius)
Porting
If you want to run Coccinella on a machine architecture not presently supported (MacOSX/Windows/Linux-x86/NetBSD) there are two extensions to Tcl/Tk itself which you need to build from their C sources. These are:
They are built the usual way using configure/make/make install but I'm unsure if you need to have Tcl/Tk sources available. This is under the assumption you are running Tcl/Tk 8.5 or later. This will be required before Coccinella version 0.96.10. Then you just get Coccinella sources and execute it from the console (./Coccinella.tcl).