A Formal Analysis of the Global Sequence Protocol

Cloud infrastructures provide data storages that are virtually unlimited, elastic (i.e., scalable at run-time), highly available and partition tolerant. This is achieved by replicating data over multiple servers. A client may perform update and read operations over any of these replicas and the store is responsible for keeping them synchronised. However, it is known (CAP theorem [7]) that any system cannot simultaneously provide availability, partition tolerance, and consistency. Thus, one of these properties has to be discarded. Today’s popular data storages, such as Dynamo [6] and Cassandra [9], ensure availability and offer weaker notions of consistency, called eventual consistency. Roughly, eventual consistency guarantees that all updates will be delivered to the different replicas, which will eventually converge to the same state [1]. The storages adopt different strategies to achieve eventual consistency, which impact on the guarantees provided by the system, i.e., on the kind of inconsistencies or anomalies that are allowed to happen. For instance, a storage may resolve automatically conflicts introduced be concurrent updates (e.g., by using timestamps or causality) or may leave the problem to applications that read the database (like in Cassandra). In this way, the consistency model supported by a data store becomes crucial when writing applications.

Consequently, there has been a growing interest on establishing programming abstractions to help developers to deal with eventual consistent stores. For instance, commutative replicated data types [10] and cloud types [3] provide programmers with suitable data type abstractions that encapsulate issues related to eventual consistency. Recent proposals advocate declarative approaches for programming with eventual consistency, e.g., to automatically select the consistency level required from a store provided with a consistency contract for the application [11] or to prove that a given consistency level is adequate for preserving some data invariant [8]. With similar aims, the Global Sequence Protocol (gsp) [5] proposes an operational model to reason about applications running on top of replicated stores. Basically, the state of a store is represented as the sequence of updates that have led to it. Clients have their own copy of the state which they operate upon: each read and write operation has immediate effect over the local state and the system propagates changes to make all replicas consistent using a reliable total order broadcast protocol (rtob). The rtob protocol guarantees that all messages are delivered in the same total order to all clients. Replicas rely on the order generated by rtob to converge to the same state. In the very basic model, called core gsp, each client interacts with its local state by performing read and write operations. Albeit simple, this model introduces some subtleties when programming because it does not ensure read stability (i.e., two successive reads may return different values) nor atomicity of several updates (i.e., another client may partially observe the effects of a sequence of updates). To overcome these limitations, three synchronisation primitives, namely pull, push and confirmed, allow programmers to control the propagation of changes. It has been shown that this model can be implemented so to handle communication failures and to represent updates efficiently by using two type of objects: states and deltas. Both models, i.e. the idealised one and its implementation, have been defined in terms of a reference implementation.

In this paper, we propose a formal account for each model: the gsp and igsp calculi (Sects. 2 and 3). We prove that the behaviour of a program running over igsp can be observed over the idealised model. Technically, we show that each igsp system can be simulated by the corresponding gsp system (Sect. 4). Then, we study and prove the consistency guarantees ensured by gsp. We rely on the characterisation of consistency guarantees in terms of abstract histories proposed in [2]. Abstract histories capture the visibility relation between actions and the arbitration order of updates in the system. Then, a wide-spectrum of consistency models can be characterised in terms of these two relations. In Sect. 5, we show how to operationally associate abstract histories to concrete computations and prove that gsp enjoys properties such as Monotonic Read, Causal Visibility and Consistent prefix, among others. Finally, in Sect. 6 we study the extension of gsp with synchronous write operations, which ensures strong consistency.

2.1 Syntax

Clients interact with a store by performing operations in \({\mathcal {U}}\cup {\mathcal {R}}\): an element in \({\mathcal {U}}\) denotes an update operation, while one in \({\mathcal {R}}\) stands for a read operation. No operation can simultaneously read and update a store, therefore we assume \({\mathcal {U}}\cap {\mathcal {R}}= \emptyset \). We write \({{u}}, {{u}}{'}, {{u}}{''},\ldots \) for updates and \({{r}}, {{r}}{'}, {{r}}{''},\ldots \) for reads.

The state of a store is represented by a sequence of updates. For technical convenience (particularly in Sect. 5), we distinguish different executions of the same operation. Formally, stores associate each update with a fresh event identifier. We assume a set \({\mathbb {V}}\) of event identifiers and write for the update \({{u}}\) associated with the event .

We use \({\mathsf {u}}\) to denote sequences of decorated updates and for an atomic block of updates. We write \({\mathsf {b}}\) for a sequence of blocks. We denote the empty sequence with \({\epsilon }\) and use the usual operations on sequences such as \({\mathsf {b}}{[i]}\) to denote the i-th element of \({\mathsf {b}}\), \({\mathsf {b}}{[i..j]}\) for the subsequence of \({\mathsf {b}}\) from position i to j, \(|{\mathsf {b}}|\) for its length and \({\mathsf {b}}\setminus {\mathsf {b}}{'}\) for the relative complement of \({\mathsf {b}}\) in \({\mathsf {b}}{'}\). Additionally, \({\underline{{\mathsf {b}}}}\) stands for the plain sequence of updates in \({\mathsf {b}}\) (i.e., without any separation in blocks).

We rely on the countable sets \({\mathcal {X}}\) of program variables \(x,x',\ldots \) and \({\mathcal {I}}\) of client identifiers \({\mathsf{i}},{\mathsf{i}}',\ldots ,{\mathsf{i}}_1,\ldots \).

Definition 2.1

(GSP Language). The set of gsp terms is given by the grammar in Fig. 1.

Syntax of the gsp calculus

Full size image

A gsp system \({N}\) consists of a store and zero or more clients. The global store \({S}\) is completely defined by its state, which consists of a sequence of blocks. The term \({\langle {P},{\mathsf{u}_\mathsf{T}},{\mathsf{b}_\mathsf{S}},{\mathsf{b}_\mathsf{p}},{k},{j}\rangle }_{\mathsf{i}}\) stands for a client identified by \({\mathsf{i}}\) and engaged on the execution of the program P. The remaining elements are used to describe the state of the local replica: \({\mathsf {u}}_\mathsf{T}\) contains the updates that have been made locally and are part of an unfinished block; \({\mathsf {b}}_{S}\) models the communication buffer, which keeps all blocks completed by the client but not received by the global store; \({{\mathsf {b}}_{P}}\) is the pending buffer, which contains all completed blocks that are unconfirmed by the global store. For simplicity, we do not have an explicit replica of the global store in each client; we use instead a natural number \({k}\) to indicate the portion of the global state that is known to the client. Specifically, the client \({\mathsf{i}}\) knows the sequence \({S}[0..{k}-1]\). Similarly, \({j}\) indicates the number of updates received by the client that have not been added to the local replica, i.e., the client has received the updates contained in the segment \({S}[{k}..{k}+{j}-1]\).

A program P is built as a sequence of operations that interacts with the store: \(\mathtt{read}(r), \mathtt{update}({{u}}), \mathtt{pull}, \mathtt{push}, \mathtt{confirmed}\) (we postpone their description until Sect. 2.2). A program \(\mathtt{let}\ x = \ldots \ \mathtt{in}\ P\) introduces a bound variable whose scope is P. The definition of free variables of a program is standard. We say that a process P is closed when it does not contain free variables. We keep the language for programs simple. We remark that this choice does not affect the results presented in this paper. Actually, we could just have characterised the behaviour of programs as a labelled transition system, but we prefer to have a syntax throughout the presentation.

Definition 2.2

(Well-formedness). A gsp system \({N}= {C}_0|\!|\ldots |\!|{C}_m|\!|{S}\) where \({C}_l = {\langle {P_{l}},{\mathsf{u}_{\mathsf{T}l}},{\mathsf{b}_{\mathsf{S}l}},{\mathsf{b}_{\mathsf{p}l}},{k_{l}},{j_{l}}\rangle }_{{\mathsf{i}}_{l}}\) for all \(l\in \{0,\ldots ,m\}\) is well-formed if the following conditions hold

1. 1.

   \({\mathsf{i}}_{l} \ne {\mathsf{i}}_{l'}\) for all \(l\ne l'\);

2. 2.

   \(k_l+j_l\le |{S}|\) for all l;

3. 3.

   and for all \(\mathsf{1} \le x < y \le \mathsf{p}\) there exists \(x',y'\) s.t. , and \({k}_l\le x' < y'\); and

4. 4.

   \({\mathsf {u}}= {\underline{{S}\cdot {{\mathsf {b}}_{{S}0}}\cdots {{\mathsf {b}}_{{S}m}}\cdot {{\mathsf {u}}_{\mathsf{T}0}}\cdots {{\mathsf {u}}_{\mathsf{T}m}}}}\), if , and \(x \ne y\) then .

We require identifiers to univocally identify clients (1) and every local state to be consistent with the global store, i.e., a client can see at most every message in the store (2), all unconfirmed blocks in \({{\mathsf {b}}_{{P}l}}\) are either in the communication buffer \({{\mathsf {b}}_{{S}l}}\) or in the unseen part of the global store (3). Moreover, an event identifier is associated with a unique update in the system (4). Hereafter, we assume every gsp system to be well-formed.

2.2 Operational Semantics

The operational semantics of gsp is given by a labelled transition system over well-formed terms, quotiented by the structural equivalence \(\equiv \) defined as the least equivalence such that \(|\!|\) is associative, commutative and has 0 as neutral element. The set of actions is given by the following grammar:

As usual, \(\tau \) stands for an internal, unobservable action, while the remaining ones correspond to the interaction of a client with the store. A label \((\lambda ,{\mathsf{i}})\) indicates that the client \({\mathsf{i}}\) performs the action \(\lambda \). We write \(\xrightarrow {\lambda }_{{\mathsf{i}}}\) instead of \(\xrightarrow {(\lambda ,{\mathsf{i}})}\).

Operational semantics for gsp

Full size image

We now comment on the inference rules in Fig. 2. When a client performs an update (rule update), the change has only local effects: the sequence of local updates \({\mathsf {u}}_\mathsf{T}\) is extended with the operation \({{u}}\) decorated with a globally fresh identifier . We remark that decorations are used for technical reasons but they are operationally irrelevant (see Sect. 5).

A client propagates its local changes to the global store by executing \(\mathtt{push}\) (rule push): all local changes in \({\mathsf {u}}_\mathsf{T}\) will be transmitted as a block , i.e., as an atomic unit. Nevertheless, these changes are not made available immediately at the global store because of the asynchronous communication model. In fact, the new block is added to the communication buffer \({\mathsf {b}}_{S}\), which contains all blocks that have not reached the global store. Also, is added to the pending messages \({{\mathsf {b}}_{P}}\). Rule send stands for a block that finally reaches the global store. Conversely, rule receive models the reception of a new update. The received update is not immediately added to the local replica. Actually, each client explicitly refreshes its local view by executing pull (rule pull). At this time, all previously received updates \({j}\) are incorporated to the local copy (i.e., \({k}\) is changed to \({k}+{j}\)). Additionally, all pending updates in the new fragment \({S}[k..k+{j}-1]\) are remove from \({{\mathsf {b}}_{P}}\).

The semantics of operations is defined abstractly by the interpretation function \({\textit{rvalue}}:{\mathcal {R}}\times {\mathcal {U}}^*\rightarrow {\mathcal {V}}\), i.e., a function that takes a read operation and a sequence of updates and returns a value in some domain \({\mathcal {V}}\). A read operation \({{r}}\) is evaluated over the local state of the client (rule read), i.e., the known prefix of the global store \({S}[0..{k}-1]\) and the local updates in \({{\mathsf {b}}_{P}}\) and \({\mathsf {u}}_\mathsf{T}\). The value v is bound to the variable x, and hence all free occurrences of x in the continuation P are substituted by v. A client may perform \(\mathtt{confirmed}\) to check whether its executed updates are already in the global store: this operation returns true only when the local buffers \({{\mathsf {b}}_{P}}\) and \({\mathsf {u}}_\mathsf{T}\) are both empty (rule confirm).

We remark that the operational semantics preserves well-formedness.

Lemma 2.1

If \({N}\) is well-formed and \({N}\xrightarrow {\lambda }_{{\mathsf{i}}}{N}{'}\), then \({N}{'}\) is well-formed.

The gsp model describes an idealised system that abstracts away from several implementation details, such as non-optimised representation of the state and unreliable communication. This section presents a formal model for the implementation proposed in [5].

3.1 Syntax

The implementation of gsp relies on a compact representation for states and updates. Their precise definition highly depends on the datatype of the values handled by the store, but they are characterised in terms of two abstract types: \({State}\) and \({Delta}\), which provides the following operations [5]:

Constants \({\delta _\emptyset }\) and \({\emptyset }\) denote the empty elements in their respective types. An object \({{\delta }}\in {Delta}\) describes the effects of a sequence of updates and is built by either appending an update to an existing delta (\({\textit{append}}\)) or combining together several deltas (\({\textit{reduce}}\)). Operation \({\textit{read}}\) is the interpretation function for operations (i.e., the implementation counterpart of function \({{\textit{rvalue}}(\_\!\_, \_\!\_)}\) used by the idealised model) and \({\textit{apply}}\) corresponds to state transformations.

Clients and the global store exchange \({{\delta }}\) objects to communicate changes. As each single \({{\delta }}\) may correspond to several update operations, clients send each \({{\delta }}\) accompanied by its own identifier and a sequence number \({n}\). Precisely, clients send rounds, i.e. triples \({ r }= {\langle {{\mathsf{i}}},{n},{{{\delta }}}\rangle }\). Differently, the global store sends segments \({ seg }= {{\langle {{{\delta }}},{{\mathtt {f}}}\rangle }}\), in which \({{\delta }}\) is accompanied by a function \({\mathtt {f}}\in {\mathcal {I}}\rightarrow {\mathbbm {N}}\). In this way, the global store confirms all changes from client \({\mathsf{i}}\) until round \({\mathtt {f}}({\mathsf{i}})\). To deal with crashes and recovery, the server may send segments of the form \({{\langle {{\mathtt {s}}},{{\mathtt {f}}}\rangle }}\), which communicates a complete state instead of a delta object.

Definition 3.1

(GSP Language). The set of igsp terms is given by the grammar in Fig. 3.

Syntax of the igsp calculus

Full size image

As for gsp, a system is composed by a global store \({\mathtt {S}}\) and possibly many clients \({\mathtt {C}}\). A global store is modelled by a tuple \(\langle {{\mathtt {s}}}, {{\mathtt {f}}}, {{\mathtt {in}}_{\mathtt{s}}}, {{\mathtt {out}}_{\mathtt{s}}}\rangle \) containing a state \({\mathtt {s}}\), a function \({\mathtt {f}}\) to keep track of processed rounds and the communication buffers \({\mathtt {in}}_{\mathtt{s}}\) and \({\mathtt {out}}_{\mathtt{s}}\). There are two dedicated buffers for each client \({\mathsf{i}}\): \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}})\) contains the rounds received from \({\mathsf{i}}\), and \({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}})\) the segments that have been sent to \({\mathsf{i}}\).

A client is represented by a term \({\langle } P,{\mathtt {s}},{{{\delta }}_\mathsf{T}},{{{\delta }}_\mathsf{P}},{n},{\mathtt {r}},{\mathtt {in}}_\mathtt{c}{\rangle }_{{\mathsf{i}}}\). As for gsp, \({\mathsf{i}}\) is its identity and P is its program. Note that the language for programs remains unaltered. The component \({{{\delta }}_\mathsf{T}}\) is analogous to \({\mathsf {u}}_\mathsf{T}\) in the gsp model, i.e., it keeps all local updates until the client performs \(\mathtt{push}\). Differently, \({{{\delta }}_\mathsf{P}}\) keeps all finished blocks that have not been sent. The number \({n}\) identifies the current round. Buffer \({\mathtt {r}}\) keeps all sent rounds that have not been confirmed by the global store (similar to \({{\mathsf {b}}_{P}}\) in gsp), while \({\mathtt {in}}_\mathtt{c}\) keeps all received segments (analogous to \({j}\)).

We also impose the following well-formedness condition on systems.

Definition 3.2

( igsp well-formedness). A igsp system \({\mathtt {N}}= {\mathtt {C}}_0|\!|\ldots |\!|{\mathtt {C}}_m|\!|{\mathtt {S}}\) with \({\mathtt {S}}=\langle {{\mathtt {s}}}, {{\mathtt {f}}}, {{\mathtt {in}}_{\mathtt{s}}}, {{\mathtt {out}}_{\mathtt{s}}}\rangle \) and \({\mathtt {C}}_l = {{\langle } P_{l},{\mathtt {s}}_{l},{{{\delta }}_{\mathsf{T}l}},{{{\delta }}_{\mathsf{P}l}},{n}_{l},{\mathtt {r}}_{l},{\mathtt {in}}_{\mathtt{c}l}{\rangle }}_{{\mathsf{i}}_{l}}\) for \(l\in \{0,\ldots ,m\}\) is well-formed if the following conditions hold

1. 1.

   \({\mathsf{i}}_l \ne {\mathsf{i}}_{l'}\) for all \(l\ne l'\).

2. 2.

   \(\textit{dom}({\mathtt {in}}_{\mathtt{s}}) = \textit{dom}({\mathtt {out}}_{\mathtt{s}}) \subseteq \{0,\ldots ,m\}\).

3. 3.

   \({\mathsf{i}}_l\not \in \textit{dom}({\mathtt {out}}_{\mathtt{s}})\) implies \({\mathtt {in}}_{\mathtt{c}l} = \epsilon \).

4. 4.

   if \({\mathsf{i}}_l\in \textit{dom}({\mathtt {out}}_{\mathtt{s}})\) and \({\mathtt {in}}_{\mathtt{c}l}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) \ne \epsilon \) then either

   1. (i)

      \({{\mathtt {in}}_{\mathtt{c}l}}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l)= \langle {{{\delta }}_{0}},{{\mathtt {f}}_{0}\rangle }\cdots \langle {{{\delta }}_{h}},{{\mathtt {f}}_{h}\rangle }\); or

   2. (ii)

      \({{\mathtt {in}}_{\mathtt{c}l}}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l)= \langle {{\mathtt {s}}},{{\mathtt {f}}}_{0}\rangle \cdot \langle {{{\delta }}}_{1},{{\mathtt {f}}}_{1}\rangle \cdots \langle {{{\delta }}}_{h},{{\mathtt {f}}}_{h}\rangle \)

   and \({\mathtt {f}}_j({\mathsf{i}}_l) \le \ {\mathtt {f}}_k({\mathsf{i}}_l)\) for all \({ j}<{k} \in \{0 .. h\}\) and \({\mathtt {f}}_h = {\mathtt {f}}\).

5. 5.

   \({\mathtt {r}}_l = {\langle {{\mathsf{i}}}_{0},{n}_{0},{\delta }_{0}\rangle }\cdots {\langle {{\mathsf{i}}}_{r},{n}_{r},{\delta }_{r}\rangle }\), \({n}_j < {n}_k\) for all \({ j}<{k} \in \{0 .. r\}\) and either

   1. (i)

      \({{{\delta }}_\mathsf{P}}_l ={\delta _\emptyset }\), \({n}_r \le {n}_l\) and \({\mathtt {f}}({\mathsf{i}}_l) \le {n}_l\); or

   2. (ii)

      \({{{\delta }}_\mathsf{P}}_l \ne {\delta _\emptyset }\), \({n}_r < {n}_l\) and \({\mathtt {f}}({\mathsf{i}}_l) < {n}_l\).

6. 6.

   either

   1. (i)

      \({\mathtt {r}}_l = \epsilon \), \({\mathtt {f}}({\mathsf{i}}_l) \le {n}_l\) and if \({\mathsf{i}}_l \in \textit{dom}({\mathtt {in}}_{\mathtt{s}})\) then \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}}_l)=\epsilon \);

   2. (ii)

      \({\mathtt {r}}_l = {\mathtt {in}}_{\mathtt{s}}({\mathsf{i}}_l)\) \(= \langle {{\mathsf{i}}_{l}},{n_{ fst}},{\delta }_{ fst}\rangle \cdot {{\mathtt {r}}_{l}}{'}\) and \( {n}_{ fst}> {{\mathtt {f}}} ({\mathsf{i}}_l)\);

   3. (iii)

      \({\mathtt {r}}_l ={{\mathtt {r}}_{l}}{''}\cdot {\langle {{\mathsf{i}}_l},{n_{ lst}},{\delta }_{ lst}\rangle } \cdot {\mathtt {in}}_{\mathtt{s}}({\mathsf{i}}_l)\) and \({\mathtt {in}}_{\mathtt{c}l}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) = \langle {{{\delta }}}_{0},{{\mathtt {f}}}_{0}\rangle \cdots \langle {\delta {'}_{lst}},{{\mathtt {f}}_{lst}}\rangle \) with \({{\mathtt {f}}_{lst}} ({\mathsf{i}}_l) = {n}_{lst}\); or

   4. (iv)

      \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}}_l) = \epsilon \), \({\mathtt {r}}_l ={{{\mathtt {r}}_{l}}{''}}\cdot {\langle }{{\mathsf{i}}_{l}},{n_{lst}},{\delta _{lst}}{\rangle }\) and either \({\mathtt {in}}_{\mathtt{c}l}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) = \langle {{\mathtt {s}}},{{\mathtt {f}}{'}}\rangle \cdot {{\mathtt {seg}}}\)

      with \({{\mathtt {f}}{'}}({\mathsf{i}}_l) \le {n}_{lst}\) or \({\mathtt {in}}_{\mathtt{c}l}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) = \epsilon \) and \({{\mathtt {f}}} ({\mathsf{i}}_l) \le {n}_{lst}\).

We require all clients to have different identifiers (1). Communication channels in the implementation are bidirectional, hence \({\mathsf{i}}_l\in \textit{dom}({\mathtt {in}}_{\mathtt{s}})\) iff \({\mathsf{i}}_l\in \textit{dom}({\mathtt {out}}_{\mathtt{s}})\) (2). Moreover, the input buffer of a disconnected client is empty (3). Condition (4) states that \(\langle \mathtt{s},{{\mathtt {f}}{'}}\rangle \) can appear only as the first message in the flow from the store and that the store confirms processed rounds in a non-decreasing order. Similarly, clients send rounds with increasing round number (5). The last condition (6) states a coherence requirement between pending rounds and the segments sent by the store, which can only confirm rounds that are pending.

Operational semantics of igsp

Full size image

3.2 Operational Semantics

As for the idealised model, the operational semantics is given by a labelled transition system over well-formed terms, up-to structural equivalence. We consider a new label \(\tau \) without any client annotation for transitions associated with changes in the global store and communication failures. The inference rules are in Fig. 4.

Rule (i-update), which is analogous to rule (update), adds the operation \({{u}}\) to the temporary block \({{{\delta }}_\mathsf{T}}\). The decoration is irrelevant in this model, hence we do not impose any freshness requirement. A client terminates a block by executing \(\mathtt{push}\) (i-push). At this time, the block \({{{\delta }}_\mathsf{T}}\) is appended to the already terminated blocks in \({{{\delta }}_\mathsf{P}}\), which will be sent on the next round. Additionally, the block counter \({n}\) is incremented by 1. By rule (i-send), a client sends changes to the global store. This transition takes place whenever the client is connected (i.e., \({\mathsf{i}}\in \textit{dom}({\mathtt {in}}_{\mathtt{s}})\)), there are finished blocks in \({{{\delta }}_\mathsf{P}}\) (i.e., \({{{\delta }}_\mathsf{P}}\ne {\delta _\emptyset }\)) and there is no need for resynchronisation (i.e., \({\mathtt {in}}_\mathtt{c}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}) \ne \langle {{\mathtt {s}}'},{{\mathtt {f}}}\rangle \cdot {\mathtt {seg}}\))^{Footnote 1}. The available blocks are sent within the same round \({ r }= \langle {\mathsf{i}},{n},{\delta _{\mathsf{P}}}\rangle \), which contains the number \({n}\) corresponding to the last finished block. The new round \({ r }\) is added to the corresponding input buffer in the store, i.e., \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}})\) is updated to \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}})\cdot { r }\) (where \(\_\!\_[\_\!\_ \mapsto \_\!\_]\) is the update operator for functions). Additionally, \({ r }\) is added to the sequence of pending rounds \({\mathtt {r}}\) and the buffer \({{{\delta }}_\mathsf{P}}\) is reset to \({\delta _\emptyset }\).

Symmetrically, the client \({\mathsf{i}}\) may receive an available segment at any time (i-receive). The new segment \({ seg }\) is removed from the buffer \({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}})\) of the global store and added to the input buffer of the client. As for the idealised model, all received changes are applied to the local replica when \({\mathsf{i}}\) performs \(\mathtt{pull}\). Rule \((\textsc {i-pull}_1)\) handles the case in which the connection with the global store has not been previously reset. In such case, all received segments are of the form \({{\langle {{{\delta }}},{{\mathtt {f}}}\rangle }}\). Therefore, the changes \({{\delta }}_1\cdots {{\delta }}_k\) are applied to the local state \({\mathtt {s}}\) and all rounds confirmed by the received segments are removed from the pending list \({\mathtt {r}}\). By well-formedness (Definition 3.2, 5), it suffices to consider the confirmation \( {\mathtt {f}}_k\), which has the greatest confirmation. Hence, all rounds up-to \({\mathtt {f}}_k({\mathsf{i}})\) are removed from \({\mathtt {r}}\). This is done by the auxiliary function \(\textit{filter}(\_\!\_,\_\!\_)\), defined as follows

Rules (i-read) and (i-confirm) are analogous the ones in the gsp calculus. We use \({\varDelta (\_\!\_)}\) for the function that projects a sequence of rounds into the sequence that contains the corresponding \({{\delta }}\)s. The global store changes its state as prescribed by rule (i-batch): it collects all received rounds in \({\mathtt {in}}_{\mathtt{s}}\) by using the auxiliary function \(\textit{rnds}(\_\!\_)\), which builds a unique object \({{\delta }}\) by appending all available rounds, and a function \({\mathtt {f}}\) that associates each client with the number of the last received round. Let \({\mathtt {in}}_{\mathtt{s}}\) be such that \(\textit{dom}({\mathtt {in}}_{\mathtt{s}}) = \{{\mathsf{i}}_0,\ldots ,{\mathsf{i}}_m\}\) and \(\forall {\mathsf{i}}_l\in \textit{dom}({\mathtt {in}}_{\mathtt{s}}).{\mathtt {in}}_{\mathtt{s}}({\mathsf{i}}_l) = {\mathtt {r}}_l\cdot \langle {{\mathsf{i}}_l},{{n}^{k_l}_l},{{{\delta }}^{k_l}_l}\rangle \). Then, \(\textit{rnds}(\_\!\_)\) is defined as follows

The obtained \({{\delta }}\) is applied to the current state \({\mathtt {s}}\) and \({\mathtt {f}}\) is updated with \({\mathtt {f}}{'}\). In addition, the new segment \(\langle {\delta ,{{\mathtt {f}}{[{\mathtt {f}}{'}]}}}\rangle \) is sent to every connected client, i.e., it is added at the end of every buffer \({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}})\). The input buffers \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}}_l)\) are emptied because all received rounds have been processed.

The remaining rules deal with connectivity issues: rule (i-drop-cxn) models a disconnection: the buffers \({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}})\) and \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}})\) are removed from the global store and also the input buffer of \({\mathsf{i}}\) is set to \(\epsilon \). When the client \({\mathsf{i}}\) (re-)establishes its connection (i-accept-cxn), the store creates the buffers for \({\mathsf{i}}\) and sends a segment containing the current state of the store. Rule \((\textsc {i-pull}_2)\) is analogous to \((\textsc {i-pull}_1)\), but handles the first \(\mathtt{pull}\) after a reconnection. The first received segment \(\langle {{\mathtt {s}}'''},\mathtt{f}_{\mathtt{0}}\rangle \) contains a state instead of a delta object. The client uses \({\mathtt {s}}'''\) instead of its local state to resynchronise. The application of successive segments is analogous to rule \((\textsc {i-pull}_1)\). Moreover, the client resends a round \({\mathtt {r}}{'}\) containing all pending segments lost by the server during the disconnection.

The proposed implementation allows for a server to crash, i.e., to close all communication buffers, but we do not model explicitly this behaviour because it can be obtained by applying rule (i-drop-cxn) several times.

Lemma 3.1

Let \({\mathtt {N}}\) be a well-formed igsp system. If \({\mathtt {N}}\xrightarrow {\lambda }_{{\mathsf{i}}}{\mathtt {N}}{'}\), then \({\mathtt {N}}{'}\) is well-formed.

We now prove that igsp is a correct implementation of gsp. We recall in Fig. 5 the requirements stated in [5] for the operations provided by the data types State and Delta. Formally, the relation \(\_\!\_\triangleleft \_\!\_\) associates delta and state objects with sequences of updates: \({{\delta }}\triangleleft {\mathsf {u}}\) (similarly, \({\mathtt {s}}\triangleleft {\mathsf {u}}\)) means that \(\delta \) (correspondingly, \({\mathtt {s}}\)) is a compact representation of \({\mathsf {u}}\). Then, it is also assumed that \({\mathtt {s}}\triangleleft {\mathsf {u}}\) implies \({{\textit{read}}({{r}},{\mathtt {s}})}= {{\textit{rvalue}}({{r}}, {\mathsf {u}})}\) for any \({{r}}\). Building on the above relation, we define under which conditions a igsp system is an implementation of a gsp system.

Coherence requirements for \({Delta}\) and \({State}\) operators

Full size image

Definition 4.1

Let \({N}= {C}_0 \ |\!|\ldots |\!|\ {C}_m\ |\!|\ {S}\) be a gsp system such that \({C}_l={\langle {P_{l}},{\mathsf{u}_{\mathsf{T}l}},{\mathsf{b}_{\mathsf{S}l}},{\mathsf{b}_{\mathsf{P}l}},{k_{l}},{j_{l}}\rangle }_{\mathsf{i}_l}\) for all \(l\in \{0,\ldots ,m\}\), and \({\mathtt {N}}= \mathtt{C}_0 \ |\!|\ldots |\!|\ \mathtt{C}_m\ |\!|\ {S}\) a igsp system such that \({\mathtt {S}}= {\langle \mathtt{s}, {\mathtt{f}_{\mathtt{s}}},{\mathtt{in}_{\mathtt{s}}},{\mathtt{out}_{\mathtt{s}}}\rangle }\) and \({\mathtt {C}}_l = {\langle {P_{l}},{\mathtt{s}_{l}},{\delta _{\mathsf{T}l}},{\delta _{\mathsf{P}l}},{n_{l}},\mathtt{r}_{l},\mathsf{in}_{\mathtt{c}l} \rangle }_{\mathsf{i}{l}}\). We say \({\mathtt {N}}\) implements \({N}\) if the following conditions hold:

1. 1.

   \({\mathtt {s}}\triangleleft {\underline{{S}}}\);

2. 2.

   \({\mathtt {s}}_l \triangleleft {\underline{{S}[0 .. k_l - 1]}}\);

3. 3.

   \({\delta }_{\mathsf{T}l}\triangleleft {\mathsf{u}}_{\mathsf{T}l}\);

4. 4.

   \(reduce(\varDelta ({\mathtt{r}_l})\cdot {\delta }_{\mathsf{P}l}) \triangleleft {\underline{\mathsf{b}_{\mathsf{P}{l}}}}\);

5. 5.

   if \({\mathsf{i}}_l \in \textit{dom}({\mathtt {in}}_{\mathtt{s}})\) and \({\mathtt {in}}_\mathtt{c}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) \ne \langle {{\mathtt {s}}'},{{\mathtt {f}}}\rangle \cdot {\mathtt {seg}}\) then

   \(reduce({\varDelta (\mathsf{in}_\mathsf{s}({\mathsf{i}}_l)})\cdot {\delta _{\mathsf{P}l} ) \triangleleft \underline{ \mathsf{b}_{\mathsf{S}l}}}\);

6. 6.

   if \({\mathsf{i}}_l \in \textit{dom}({\mathtt {out}}_{\mathtt{s}})\) then either

   1. i.

      \({{\mathtt {in}}_{\mathtt{c}l}} \cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) = \epsilon \), \({k}_l = |{S}|\);

   2. ii.

      \({{\mathtt {in}}_{\mathtt{c}l}} = \langle {\delta {'}},{\mathtt{f}}\rangle \cdot {\mathtt {seg}}\), \({{\textit{reduce}}({\varDelta ({{\mathtt {in}}_{\mathtt{c}l}})})}\triangleleft {\underline{ {S}[{k}_l..{k}_l+{j}_{l}-1]}}\), and

      \({{\textit{reduce}}({\varDelta ({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l))})}\triangleleft {\underline{{S}[{k}_l+{j}_l..|{S}| - 1]}}\);

   3. iii.

      \({{\mathtt {in}}_{\mathtt{c}l}} = \langle {{\mathtt {s}}{'}},\mathtt{f}_{\mathtt{0}}\rangle \cdot {\mathtt {seg}}\), there exists t s.t. \({k}_l\le t \le {k}_l+{j}_l\) s.t. \({\mathtt {s}}{'} \triangleleft \ {\underline{{S}[0 .. t - 1]}}\),

      \({{\textit{reduce}}({\varDelta ({\mathtt {seg}})})}\triangleleft \ {\underline{ {S}[t..{k}_l+{j}_l-1]}}\) and

      \({{\textit{reduce}}({\varDelta ({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) )})}\triangleleft \ {\underline{{S}[{k}_l+{j}_l..|{S}| - 1]}}\); or

   4. iv.

      \({{\mathtt {in}}_{\mathtt{c}l}} = \epsilon \), \({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) = \langle {{\mathtt {s}}{'}},\mathtt{f}\rangle \cdot {\mathtt {seg}}\) there exists \(t \ge {k}_l+{j}_l \) s.t. \({\mathtt {s}}{'} \triangleleft \ {\underline{{S}[0 .. t - 1]}}\)

      \({{\textit{reduce}}({\varDelta ({\mathtt {seg}})})}\triangleleft \ {\underline{ {S}[t..|{S}| - 1]}}\);

7. 7.

   for all \({\mathtt {f}}\) s.t \({\mathtt {f}}= {\mathtt {f}}_{s}\) or \(\langle {\delta },\mathtt{f}\rangle \in {\mathtt {in}}_{\mathtt{c}l}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l)\), for all \(\langle {\mathsf{i}},{n},{\delta }{'}\rangle \in {\mathtt {r}}_l\) if \({n}\le {\mathtt {f}}({\mathsf{i}}_l)\) then \({{\delta }}\triangleleft {\underline{{S}[x..x']}}\) and \({{\delta }}'\triangleleft {\underline{{S}[y..y']}}\) with \(y'\le x'\).

The first three conditions are self-explanatory. Condition (4) states that the pending blocks in \({\underline{{{\mathsf {b}}_{{P}l}}}}\) correspond either to rounds in the pending list \({\mathtt {r}}_l\) or to blocks ready to be sent, i.e., in \({{{{\delta }}_\mathsf{P}}}_l\). By condition (5), if a client is synchronised with the store (i.e., \({\mathsf{i}}_l \in \textit{dom}({\mathtt {in}}_{\mathtt{s}})\) and \({\mathtt {in}}_\mathtt{c}\cdot {\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l) \ne \langle {{\mathtt {s}}{'}},{\mathtt{f}}\rangle \cdot {\mathtt {seg}}\)) then all blocks in the sending list \({{\mathsf {b}}_{{S}l}}\) are either rounds that have been sent, i.e., in \({\mathtt {in}}_{\mathtt{s}}({\mathsf{i}}_l)\), or ready blocks in \({{{{\delta }}_\mathsf{P}}}_l\). Condition (6) establishes the relation between the received messages in both models. Basically, the local replica is complete when there are no segments for the client (i). When the first received segment is a delta object (ii), the content in the input buffer \({\mathtt {in}}_{\mathtt{c}l}\) corresponds to the received messages in \({S}[{k}_l..{k}_l+{j}_l-1]\) and the output buffer \({\mathtt {out}}_{\mathtt{s}}({\mathsf{i}}_l)\) contains the updates in the sequence \({S}[{k}_l+{j}_l..|{S}| - 1]\). In the remaining two cases, the first segment contains a state. When the segment is in the input buffer of the client (iii), the received state \({\mathtt {s}}{'}\) corresponds to a prefix of the sequence \({S}\) whose length lies in between of the updates already received by the client in the idealised model, i.e., \({S}[0 .. t - 1]\) with \({k}\le t \le {k}_l+{j}_l\), while the remaining conditions are analogous to the previous case. Differently, when the first segment is still on the output buffer of the store (iv), \({\mathtt {s}}{'}\) corresponds to a prefix that contains at least all updates in \({S}\) already known to the client, i.e., \(t \ge {k}_l+{j}_l \) because the store confirmations are monotonic.

Condition (7) states that in any segment \({{\langle {{{\delta }}},{{\mathtt {f}}}\rangle }}\) sent by the store, \({{\delta }}\) corresponds to a contiguous sequence of updates in \({S}\), i.e., \({S}[x..x']\). Moreover, all confirmed rounds are also within the prefix \({S}[0..x']\).

We now show that igsp is a correct implementation of gsp by proving that \({N}\) weakly simulates \({\mathtt {N}}\) when \({\mathtt {N}}\) implements \({N}\). We use standard simulation but technically we take into account the fact that gsp associates a fresh event identifier to each update while igsp does not. Take \(\rightarrow = \xrightarrow {\tau } \bigcup _{{\mathsf{i}}\in {\mathcal {I}}} \xrightarrow {\tau }_{{\mathsf{i}}}\), \(\Rightarrow \) as the reflexive and transitive closure of \(\rightarrow \), i.e.\(\Rightarrow = \rightarrow ^*\), and .

Definition 4.2

(Simulation). \(\mathcal {R}\) is an implementation simulation if for all \(({\mathtt {N}},{N})\in \mathcal {R}\) we have:

1. 1.

   If then s.t. and \(({\mathtt {N}}{'},{N}{'})\in \mathcal {R}\);

2. 2.

   If \({\mathtt {N}}\xrightarrow {\lambda }_{{\mathsf{i}}}{\mathtt {N}}{'}\) and then \(\exists {N}{'}\) s.t. and \(({\mathtt {N}}{'},{N}{'})\in \mathcal {R}\);

3. 3.

   If \({\mathtt {N}}\xrightarrow {}{\mathtt {N}}{'}\) then \(\exists {N}{'}\) s.t. \({N}\Rightarrow {N}{'}\) and \(({\mathtt {N}}{'},{N}{'})\in \mathcal {R}\);

As usual, we write \({\mathtt {N}}\precsim {N}\) if there exists a simulation \(\mathcal {R}\) s.t. \(({\mathtt {N}},{N})\in \mathcal {R}\).

Theorem 4.1

If \({\mathtt {N}}\) implements \({N}\), then \({\mathtt {N}}\precsim {N}\).

Proof

We show that \(\mathcal {R} = \{ ({\mathtt {N}}, {N}) \ |\ {{\mathtt {N}}{}}\ implements \ {{N}} \}\) is a simulation.

We remark that \(\mathcal {R}^{-1}\) is not a simulation because the implementation cannot mimic the behaviour in which a client have completed two consecutive blocks (i.e., two push commands) without sending the first block. In gsp it is still possible to interleave the two blocks with blocks sent by other clients but in igsp they are treated as atomic because they will be sent as a unique \(\delta \) object.

In this section we study the consistency properties offered by gsp. We rely on the characterisation of properties in terms of abstract executions [4], execution histories enriched with information about visibility and arbitration of actions.

Definition 5.1

Let \({N}\) be a well-formed gsp system, an abstract history for \({N}\) is a tuple where:

• maps events to operations;

• associates events with a session (i.e., a client);

• describes the order of operations within a session;

• indicates whether the effects of an update are visible to a read;

• resolves concurrent update conflicts.

We write \(\_\!\_\!\!\downarrow _{\_\!\_}\) for function/relation restriction. For a given abstract history , we write (similarly, ) for the codomain restriction of \({\textsc {OP}}\) to \({\mathcal {U}}\) (correspondingly, \({\mathcal {R}}\)), i.e., ().

Definition 5.2

(Well-formed history). Let \({N}= {C}_0|\!|\ldots |\!|{C}_m|\!|{S}\) be a gsp system where \({C}_l = {\langle {{P}_{l}},{\mathsf{u}}_{\mathsf{T}l},{\mathsf{b}}_{\mathsf{S}l},{\mathsf{b}}_{\mathsf{P}l},{k_l},{j_l}\rangle }_{\mathsf{i}_l}\). A history is well-formed if the following conditions hold:

1. 1.

   for all \({\mathsf{i}}\in \textit{dom}({\textsc {SS}})\), \({\textsc {SS}}({\mathsf{i}}) \subseteq { dom}({\textsc {OP}})\);

2. 2.

   then exist \({\mathsf{i}}\in \textit{dom}({\textsc {SS}})\) s.t. .

3. 3.

   for all \({\mathsf{i}}\in \textit{dom}({\textsc {SS}})\), \({\textsc {SO}}\downarrow _{{\textsc {SS}}({\mathsf{i}})}\) is a total order;

4. 4.

   ;

5. 5.

   is a prefix order.

6. 6.

   iff

   • and and \(i< j\); or

   • and ;

7. 7.

   if and and \(i< j\), then and .

The above conditions ensure that events in \({\textsc {SS}}\) are associated with an operation by \({\textsc {OP}}\) (1). Besides, \({\textsc {SO}}\) only relates events belonging to the same session (2), which are totally ordered within each session (3). Differently from the definition in [2], we restrict visibility to keep track of dependencies between updates and read events(4). We do not require \({\textsc {AR}}\) to be a total order but instead to be a prefix order (5). In this way the updates in different replicas are arbitrated when they reach the global store. The remaining two conditions require the abstract history to be consistent with the state of the system.

Rules in Fig. 6 provides an operational way to associate abstract executions with gsp computations. Rules (a-update) and (a-read) add new events to the history and corresponds to the execution of a read or update operation by a client. In both cases \({\textsc {OP}}\) is extended with a new event (i.e., ), which is associated with the corresponding operation (either \({{r}}\) or \({{u}}\)). The new event is added to the corresponding session \({\mathsf{i}}\), and \({\textsc {SO}}\) is updated to make the maximal event for the session \({\mathsf{i}}\). Rule (a-update) amends \({\textsc {AR}}\) by capturing the fact that all updates that are already in the global state took place before the new event. Rule (a-read) instead augments \({\textsc {VIS}}\) with the pairs associating the new event with all events that are seen by the read action, namely, the local view of the global state \({S}[0..{k}_{{\mathsf{i}}}-1]\) and the local buffers \({{\mathsf {b}}_{{P}{{\mathsf{i}}}}}\) and \({{\mathsf {u}}_{\mathsf{T}{{\mathsf{i}}}}}\). Rule (a-arb) handles the changes in the state of the global store (due to a send transition in one client) and amends \({\textsc {AR}}\) by arbitrating (i) the new events by respecting the relative order in which they are added to the store (i.e., ) and (ii) all updates in the local state of the clients after the new ones (i.e., ). The remaining transitions of the system are considered as internal changes that do not affect the history and are handled by rule (a-int).

Lemma 5.1

Let be a well-formed history. If , then is well-formed.

Computation of abstract executions

Full size image

We use histories to analyse the ordering guarantees offered by the gsp model. (Due to space limitation, we refer the interested reader to see the characterisations provided in [2, Ch.5]).

Theorem 5.1

If \(\langle {N} , \emptyset , \emptyset , \emptyset , \emptyset , \emptyset \rangle \xrightarrow {}_{{\mathsf{i}}}^*\ \langle {N}' , {\textsc {OP}}, {\textsc {SS}}, {\textsc {SO}}, {\textsc {VIS}}, {\textsc {AR}}\rangle \) then

1. (1)

   Read My Writes:

2. (2)

   Monotonic Read: .

3. (3)

   No Circular Causality: \(({\textsc {SO}}\cup {\textsc {VIS}}) ^+\) is acyclic.

4. (4)

   Causal Visibility: .

5. (5)

   Causal Arbitration: .

6. (6)

   Consistent prefix: \({\textsc {AR}};({\textsc {VIS}}\setminus {\textsc {SS}})\ \subseteq \ {\textsc {VIS}}\).

The following example shows that the gsp model exhibits the Dekker anomaly, hence it does not enjoy sequential consistency [2].

Example 5.1

(Dekker anomaly). Consider the following system consisting of two clients and the empty store \({N}= \epsilon \ |\!|\ {C}_1 \ |\!|\ {C}_2\) where

Since the updates are made locally, none of the clients see the update performed by the other and this is the essence of the Dekker anomaly which is ruled out by strong consistency models like sequential consistency or linearizability.

In this section we study the atomic updates proposed in [5]. We extend the language of programs as follows:

The execution of a program \(\mathtt{syncUpd}(u); P\) remains blocked until the update \({{u}}\) is performed over the global store. This is achieved by continuously pulling (i.e., a busy-waiting) until the updates are confirmed by global store. In order to provide the formal semantics of the language, we consider the following runtime syntax for programs.

The operational semantics for the new primitives is given by the rules in Fig. 7. Rule (sync-upd) rewrites each synchronous update as the sequence consisting of an asynchronous update followed by pull and wait. Processes wait continuously checks whether local changes have been confirmed by the global store. As described by rule (wait), it is implemented as a busy-waiting loop that first checks the local buffers by executing confirmed and then performs the conditional jump \({x}\triangleright (\mathtt{pull};{\mathtt{wait}});{P}\). If the condition x is true, then it follows as P otherwise it continues as \(\mathtt{pull};\mathtt{wait}\), as described by rules (guard-true) and (guard-false).

Semantics of gsp with atomic updates

Full size image

Single order is characterised, essentially, by imposing arbitration and visibility to coincide [2]. Since our definition for \({\textsc {AR}}\) and \({\textsc {VIS}}\) makes them disjoint, we use an alternative characterisation of single order guarantee, which disregards the arbitration order of updates that are not observed. Hence, we use the following characterisation for single order:

The following result shows that any well-formed gsp system, whose programs are free from asynchronous updates enjoy the single order guarantee.

Theorem 6.1

(Single Order). Let \({N}\) be a well-formed system s.t. \(\mathtt{update}({{u}})\) does not appear in \({N}\). If \(\langle {N} , \emptyset , \emptyset , \emptyset , \emptyset , \emptyset \rangle \xrightarrow {}_{{\mathsf{i}}} ^*\ \langle {N}' , {\textsc {OP}}, {\textsc {SS}}, {\textsc {SO}}, {\textsc {VIS}}, {\textsc {AR}}\rangle \) then \({\textsc {AR}};{\textsc {VIS}}\subseteq {\textsc {VIS}}\) and \({\textsc {AR}}^{-1};\lnot {\textsc {VIS}}\subseteq \lnot {\textsc {VIS}}\).

We have proposed a formal model for the Global Sequence Protocol and its proposed implementation. We use our formal model to provide a simplified proof (that relies on standard simulation) that the proposed implementation is correct. We remark that our proof does not require to exhibit an auxiliary state for the simulation and that several invariants are trivially ensured by the definition of the model (e.g., the fact that clients have a consistent view of the global sequence) and the well-formed conditions imposed over systems. We have formally studied the consistency guarantees ensured by the model by relying on the operational semantics of the calculus to incrementally compute (a relaxed version of) abstract histories. We have also shown how gsp can be used to formally study programming patterns, like synchronous update operations, that provide stronger consistency guarantees at the expenses of efficiency and availability. We plan to use the gsp calculus as a formal basis for developing programming techniques to enable the fine-tuning of consistency levels in applications.