Jupiter Made Abstract, and Then Refined
- PDF / 5,657,491 Bytes
- 22 Pages / 595 x 842 pts (A4) Page_size
- 53 Downloads / 138 Views
Jupiter Made Abstract, and Then Refined Heng-Feng Wei, Member, CCF, Rui-Ze Tang, Yu Huang∗ , Member, CCF, and Jian Lv, Fellow, CCF, Member, ACM State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210023, China
E-mail: [email protected]; [email protected]; {yuhuang, lj}@nju.edu.cn Received April 10, 2020; revised October 22, 2020. Abstract Collaborative text editing systems allow multiple users to concurrently edit the same document, which can be modeled by a replicated list object. In the literature, there is a family of operational transformation (OT)-based Jupiter protocols for replicated lists, including AJupiter, XJupiter, and CJupiter. They are hard to understand due to the subtle OT technique, and little work has been done on formal verification of complete Jupiter protocols. Worse still, they use quite different data structures. It is unclear about how they are related to each other, and it would be laborious to verify each Jupiter protocol separately. In this work, we make contributions towards a better understanding of Jupiter protocols and the relation among them. We first identify the key OT issue in Jupiter and present a generic solution. We summarize several techniques for carrying out the solution, including the data structures to maintain OT results and to guide OTs. Then, we propose an implementation-independent AbsJupiter protocol. Finally, we establish the (data) refinement relation among these Jupiter protocols (AbsJupiter included). We also formally specify and verify the family of Jupiter protocols and the refinement relation among them using TLA+ (TLA stands for “Temporal Logic of Actions”) and the TLC model checker. To our knowledge, this is the first work to formally specify and verify a family of OT-based Jupiter protocols and the refinement relation among them. It would be helpful to promote a rigorous study of OT-based protocols. Keywords
1
Jupiter protocol, operational transformation, refinement, replicated list, TLA+
Introduction
Collaborative text editing systems, such as Google 1 2 3 4 Docs○ , Firepad○ , Overleaf○ , and SubEthaEdit○ , allow multiple users to concurrently edit the same document. For availability, such systems often replicate the document at several replicas. For low latency, replicas are required to respond to user operations immediately and updates are propagated asynchronously [1, 2] . The replicated list object is frequently used to model the core functionality (e.g., insertion and deletion) of replicated collaborative text editing systems [1–4] . A common specification for it is strong eventual consis-
tency (SEC) [3] . It requires that whenever two replicas have processed the same set of updates, they have the same list. A family of Jupiter protocols [3] for implementing such a replicated list have been proposed, including XJupiter [4] (a multi-client version of [3] given by Xu et al.), AJupiter [2] (another multi-client version of [3] given by Attiya et al.), and CJupiter [6] (short for Compact Jupiter). They adopt the client/se
Data Loading...
