Project-Team : ecoo
Section: New Results
Operational transformations
Automatic proving of transformation functions
Participants : Pascal Molli, Gerald Oster, Hala Skaf-Molli, Pascal Urso.
Real-time groupware systems allow a group of users to manipulate the same object (i.e. a text, an image, a graphic, etc.) at the same time from physically dispersed sites that are interconnected by a supposed reliable network. In order to achieve good responsiveness and friendly collaboration, the shared objects are replicated at the local memory of each participating user. One of the most significant issues in building real-time groupware systems with replicated architecture is consistency maintenance of shared objects [38].
Operational transformation is an approach [31], [34] which allows to build real-time groupware like shared editors. Algorithms like aDOPTed [32], GOTO [37], SOCT 2,3,4 [36] are used to maintain the consistency of shared data. However these algorithms rely on the definition of transformation functions. If these functions are not correct then these algorithms cannot ensure the consistency of shared data.Proving the correctness of transformation functions even on a simple typed object like a String is a complex task. If we have more operations on more complex typed objects, the proof is almost impossible without a computer. This is a serious bottleneck for building more complex real-time groupware software. We propose to assist development of transformation functions with SPIKE , an automated theorem prover which is suitable for reasoning about functions defined by conditional rewrite rules [35]. This approach requires specifying the transformation functions in first order logic. Then, SPIKE automatically determines thecorrectness of transformation functions. If correctness is violated, SPIKE returns counter-examples. Since the proofs are automatic, we can handle more (even complex) operations and develop quickly correct transformation functions. We have found this year many counter-examples to existing transformation function [25]. We have proposed new set of correct transformation functions [7], [23].
Perspectives
Collaborative editing allows users to edit the same text from multiple sites across Internet. For example, recently collaborative editing allowed Wikipedia to collect more than 1,600,000 articles in more than 100 languages. Moreover, more than 13 millions of page requests per day and more than 4,000 changes are made every day by more than 12,000 active writers. Thus, Wikipedia is an example of massive collaborative editing. Scalability is one of the key issues for massive collaborative editing. For example, Wikipedia uses a database pessimistic replication approach. Thus all changes are routed on a single master database that propagates changes to slaves within distributed atomic transactions. Consequently, the master database is a congestion point that limits scalability of this approach. Wikipedia relies on ''brutal force'' to handle this load. On the one hand, the optimistic replication approach greatly improves performances. It can be deployed on peer-to-peer network and scales with cheap resources. On the other hand, it is more difficult to ensure consistency. Traditionally, the optimistic replication systems ensure eventual consistency i.e. replicas can diverge but must converge when system is idle. Optimistic replication is suited for collaborative editing. CVS, real-time group editors are good examples of optimistic replication algorithms applied to collaborative editing. However, these systems have not been designed for massive collaborative editing. Consequently, they often require a central site, a total ordering, a consensus or vector clocks. These well known mechanisms or algorithms are not designed for a large number of sites. The main issue for massive collaborative editing systems, based on optimistic replication, is to ensure eventual consistency and scalability. So far, only Usenet and DNS ensure both eventual consistency and scalability. However, they are not suited for collaborative editing. WOOT [23], [4] is an optimistic replication algorithm designed for massive collaborative editing. It does not require the central site, total ordering, consensus or vector clocks. It does not use the number of sites as its parameter. It is designed to be deployed on a very large peer-to-peer network. WOOT can be used to developp collaborative environement for e-learning, software-engineering (P2P configuration management), content management (P2P wiki)...
