Guaranteeing Correctness for Collaboration on Documents Using an Optimal Locking Protocol

Collaboration on documents has been supported for several decades through a variety of systems and tools; recently a renewed interest is apparent through the appearance of new collaborative editors and applications. Some distributed groupware systems are plug-ins for standalone word processors while others have a purely web-based existence. Most exemplars of the new breed of systems are based on Operational Transformations, although some are using traditional version management tools and still others utilize document-level locking techniques. All existing techniques have their drawbacks, creating opportunities for new methods. The authors present a novel collaborative technique for documents which is based on transactions, schedulers, conflicts, and locks. It is not meant to replace existing techniques; rather, it can be used in specific situations where a strict form of concurrency control is required. While the approach of presentation in this article is highly formal with an emphasis on proving desirable properties such as guaranteed correctness, the work is part of a project which aims to fully implement the technique.