`jupiter-refinement-project`

Overview

It is devoted to "formal specification and verification of a family of Jupiter protocols for implementing replicated lists".

Jupiter protocol is a core of many collaborative editing systems.

Papers

See paper-jupiter-refinement.

How to Run?

Run separately.

Create and run TLC models in the usual way.

Run in batch (Recommended).

We write scripts to automatically conduct a batch of experiments; see tangruize/jupiter-experiments.

TLA+ Modules

Note: The TLA+ code in this repository may be different from that in papers we wrote in formatting, naming, and modularity.

The following figure shows the key TLA+ modules in this project, where the solid line from module A to module B indicates that B "extends" A, and the dashed line from module A to module B indicates that B contains an "instance" of A.

These modules fall into four categories:

System Model: It describes the client/server architecture of collaborative editing systems.

It also models a replica as an abstract state machine and provides the interface for implementing such a state machine.
Jupiter Family: This contains several techniques for all Jupiter protocols.
- JupiterCtx is for context-based Jupiter protocols.
- JupiterSerial helps to establish the serialization order at the server.
- BufferStateSpace, GraphStateSpace, SetStateSpace are data structures for supporting OTs in Jupiter protocols.
Jupiter Protocols: Formal TLA+ specifications of four Jupiter protocols, i.e., AJupiter, XJupiter, CJupiter, and AbsJupiter.
Refinement: The (data) refinement relations among Jupiter protocols are established. Specifically,
- AJupiter is a refinement (a.k.a implementation) of XJupiter,
- XJupiter is a refinement of CJupiter,
- CJupiter is a refinement of AbsJupiter.