Eventual Consistency for CRDTs
Abstract
We address the problem of validity in eventually consistent (EC) systems: In what sense does an EC data structure satisfy the sequential specification of that data structure? Because EC is a very weak criterion, our definition does not describe every EC system; however it is expressive enough to describe any Convergent or Commutative Replicated Data Type (CRDT).
1 Introduction
In a replicated implementation of a data structure, there are two impediments to requiring that all replicas achieve consensus on a global total order of the operations performed on the data structure (Lamport 1978): (a) the associated serialization bottleneck negatively affects performance and scalability (e.g. see (Ellis and Gibbs 1989)), and (b) the cap theorem imposes a tradeoff between consistency and partitiontolerance (Gilbert and Lynch 2002).
In systems based on optimistic replication (Vogels 2009; Saito and Shapiro 2005), a replica may execute an operation without synchronizing with other replicas. If the operation is a mutator, the other replicas are updated asynchronously. Due to the vagaries of the network, the replicas could receive and apply the updates in possibly different orders.
For sequential systems, the correctness problem is typically divided into two tasks: proving termination and proving partial correctness. Termination requires that the program eventually halt on all inputs, whereas partial correctness requires that the program only returns results that are allowed by the specification.
For replicated systems, the analogous goals are convergence and validity. Convergence requires that all replicas eventually agree. Validity requires that they agree on something sensible. In a replicated list, for example, if the only value put into the list is 1, then convergence ensures that all replicas eventually see the same value for the head of the list; validity requires that the value be 1.
Convergence has been wellunderstood since the earliest work on replicated systems. Convergence is typically defined as eventual consistency, which requires that once all messages are delivered, all replicas have the same state. Strong eventual consistency (sec) additionally requires convergence for all subsets of messages: replicas that have seen the same messages must have the same state.
In this paper we give the first definition of validity that is both (1) derived from standard sequential specifications and (2) validates the examples of interest.“It is infinitely easier and more intuitive for us humans to specify how abstract data structures behave in a sequential setting, where there are no interleavings. Thus, the standard approach to arguing the safety properties of a concurrent data structure is to specify the structure’s properties sequentially, and find a way to map its concurrent executions to these ‘correct’ sequential ones.”
We take the “examples of interest” to be Convergent/Commutative Replicated Data Types (crdts). These are replicated structures that obey certain monotonicity or commutativity properties. As an example of a crdt, consider the addwins set, also called an “observed remove” set in Shapiro et al. (2011a). The addwins set behaves like a sequential set if add and remove operations on the same element are ordered. The concurrent execution of an add and remove result in the element being added to the set; thus the remove is ignored and the “add wins.” This concurrent specification is very simple, but as we will see in the next section, it is quite difficult to pin down the relationship between the crdt and the sequential specification used in the crdt’s definition. This paper is the first to successfully capture this relationship.
Many replicated data types are crdts, but not all (Shapiro et al. 2011a). Notably, Amazon’s Dynamo (DeCandia et al. 2007) is not a crdt. Indeed, interest in crdts is motivated by a desire to avoid the wellknow concurrency anomalies suffered by Dynamo and other ad hoc systems (Bieniusa et al. 2012).
Shapiro et al. (2011b) introduced the notion of crdt and proved that every crdt has an sec implementation. Their definition of sec includes convergence, but not validity.
The validity requirement can be broken into two components. We describe these below using the example of a list data type that supports only two operations: the mutator put, which adds an element to the end of the list, and the query q, which returns the state of the list. This structure can be specified as a set of strings such as Open image in new window and Open image in new window .

Linearization requires that a response be consistent with some specification string. A state that received put(1) and put(3), may report q=[1,3] or q=[3,1], but not q=[2,1,3], since 2 has not been put into the list.

Monotonicity requires that states evolve in a sensible way. We might permit the state q=[1,3] to evolve into q=[1,2,3], due to the arrival of action put(2). But we would not expect that q=[1,3] could evolve into q=[3,1], since the data type does not support deletion or reordering.
Burckhardt et al. (2012) provide a formal definition of validity using partial orders over events: linearizations respect the partial order on events; monotonicity is ensured by requiring that evolution extends the partial order. Similar definitions can be found in Jagadeesan and Riely (2015) and Perrin et al. (2015). Replicated data structures that are sound with respect to this definition enjoy many good properties, which we discuss throughout this paper. However, this notion of correctness is not general enough to capture common crdts, such as the addwins set.
This lack of expressivity lead Burckhardt et al. (2014) to abandon notions of validity that appeal directly to a sequential specification. Instead they work directly with concurrent specifications, formalizing the style of specification found informally in Shapiro et al. (2011b). This has been a fruitful line of work, leading to proof rules (Gotsman et al. 2016) and extensions (Bouajjani et al. 2014). See (Burckhardt 2014; Viotti and Vukolic 2016) for a detailed treatment.
Positively, concurrent specifications can be used to validate any replicated structure, including crdts as well as anomalous structures such as Dynamo. Negatively, concurrent specifications have no the clear connection to their sequential counterparts. In this paper, we restore this connection. We arrive at a definition of sec that admits crdts, but rejects Dynamo.
The following “corner cases” are a useful sanitycheck for any proposed notion of validity.

The principle of single threaded semantics (psts) (Haas et al. 2015) states that if an execution uses only a single replica, it should behave according to the sequential semantics.

The principle of single master (psm) (Budhiraja et al. 1993) states that if all mutators in an execution are initiated at a single replica, then the execution should be linearizable (Herlihy and Wing 1990).

The principle of permutation equivalence (ppe) (Bieniusa et al. 2012) states that “if all sequential permutations of updates lead to equivalent states, then it should also hold that concurrent executions of the updates lead to equivalent states.”
In the next section, we describe the validity problem and our solution in detail, using the example of a binary set. The formal definitions follow in Sect. 3. We state some consequences of the definition and prove that the addwins set satisfies our definition. In Sect. 4, we describe a collaborative text editor and prove that it is sec. In Sect. 5 we characterize the programmer’s view of a crdt by defining the most general crdt that satisfies a given sequential specification. We show that any program that is correct using the most general crdt will be correct using a more restricted crdt. We also show that our validity criterion for sec is local in the sense of Herlihy and Wing (1990): independent structures can be verified independently. In Sect. 6, we apply these results to prove the correctness of a graph that is implemented using two sec sets.
Our work is inspired by the study of relaxed memory, such as (Alglave 2012). In particular, we have drawn insight from the rmo model of Higham and Kawash (2000).
2 Understanding Replicated Sets
In this section, we motivate the definition of sec using replicated sets as an example. The final definition is quite simple, but requires a fresh view of both executions and specifications. We develop the definition in stages, each of which requires a subtle shift in perspective. Each subsection begins with an example and ends with a summary.
2.1 Mutators and Nonmutators
lpos with noninteracting replicas can be denoted compactly using sequential and parallel composition. For example, the prefix of (1) that only includes the first three events at each replica can be written Open image in new window .
A specification is a set of strings. Let \({\textsc {set}}\) be the specification of a sequential set with elements 0 and 1. Then we expect that set includes the string “ Open image in new window ”, but not “ Open image in new window ”. Indeed, each specification string can uniquely be extended with either Open image in new window or Open image in new window and either Open image in new window or Open image in new window .
There is an isomorphism between strings and labelled total orders. Thus, specification strings correspond to the restricted class of lpos where the visibility relation provides a total order.
Linearizability (Herlihy and Wing 1990) is the gold standard for concurrent correctness in tightly coupled systems. Under linearizability, an execution is valid if there exists a linearization \(\tau \) of the events in the execution such that for every event e, the prefix of e in \(\tau \) is a valid specification string.
Execution (1) is not linearizable. The failure can already be seen in the sublpo Open image in new window . Any linearization must have either Open image in new window before Open image in new window or Open image in new window before Open image in new window . In either case, the linearization is invalid for set.
It is straightforward to see that execution (1) satisfies this weaker criterion. For both Open image in new window and Open image in new window , the mutator prefix is Open image in new window . This includes Open image in new window but not Open image in new window , and thus their answers are validated. Symmetrically, the mutator prefixes of Open image in new window and Open image in new window only include Open image in new window . The mutator prefixes for the final four events include both Open image in new window and Open image in new window , but none of the prior accessors.
Summary: Convergent states must agree on the final order of mutators, but intermediate states may see incompatible subsequences of this order. By restricting attention to mutator prefixes, the later states need not linearize these incompatible views of the partial past.
This relaxation is analogous to the treatment of nonmutators in update serializability (Hansdah and Patnaik 1986; GarciaMolina and Wiederhold 1982), which requires a global serialization order for mutators, ignoring nonmutators.
2.2 Dependency
This lpo is not valid under the definition of the previous subsection: Since Open image in new window and Open image in new window see the same mutators, they must agree on a linearization of Open image in new window . Any linearization must end in either Open image in new window or Open image in new window ; thus it is not possible for both Open image in new window and Open image in new window to be valid.
Under this definition, execution (2) is validated: Any interleaving of the strings Open image in new window and Open image in new window linearizes the dependent restriction of (2) given in (3).
Summary: crdts allow independent mutators to commute. We formalize this intuition by restricting attention to mutator prefixes of the dependent restriction. The crdt must respect program order between dependent operations, but is free to reorder independent operations.
This relaxation is analogous to the distinction between program order and preserved program order (ppo) in relaxed memory models (Higham and Kawash 2000; Alglave 2012). Informally, ppo is the suborder of program order that removes order between independent memory actions, such as successive reads on different locations without an intervening memory barrier.
2.3 Puns
Indeed, this lpo is not valid under the definition of the previous subsection. First note that all events are mutually dependent. To prove validity we must find a linearization that satisfies the given requirements. Any linearization of the mutators must end in either Open image in new window or Open image in new window . Suppose we choose Open image in new window and look for a mutator prefix to satisfy Open image in new window . (All other choices lead to similar problems.) Since Open image in new window precedes Open image in new window and is the last mutator in our chosen linearization, every possible witness for Open image in new window must end with mutator Open image in new window . Indeed the only possible witness is Open image in new window . However, this is not a valid specification string.
Each of these is a valid specification string. In addition, looking only at mutators, each is a subsequence of Open image in new window .
Summary: While dependent events at a single replica must be linearized in order, concurrent events may slip anywhere into the linearization. A crdt may pun on concurrent events with same label, using them in different positions at different replicas. Thus a crdt may establish a final total over the labels of an execution even when there is no linearization of the events.
2.4 Frontiers
In the introduction, we mentioned that the validity problem can be decomposed into the separate concerns of linearizability and monotonicity. The discussion thus far has centered on the appropriate meaning of linearizability for crdts. In this subsection and the next, we look at the constraints imposed by monotonicity.
Unfortunately, execution (6) is valid by the definition given in the previous section: The witnesses for \(a\)–\(f\) are as before. In particular, the witness for Open image in new window is “ Open image in new window ”. The witness for Open image in new window is “ Open image in new window ”. In each case, the mutator prefix is a subsequence of the global mutator order “ Open image in new window ”.
It is well known that punning can lead to bad jokes. In this case, the problem is that Open image in new window is punning on a concurrent Open image in new window that cannot be matched by a visible Open image in new window in its history: the execution Open image in new window that is visible to Open image in new window must appear between the two Open image in new window operations; the specification Open image in new window that is used by Open image in new window must appear after. The final states of execution (4) have seen both remove operations, therefore the pun is harmless there. But Open image in new window and Open image in new window have seen only one remove. They must agree on how it is used.
Up to now, we have discussed the linearization of each event in isolation. We must also consider the relationship between these linearizations. When working with linearizations of events, it is sufficient to require that the linearization chosen for each event be a subsequence for the linearization chosen for each visible predecessor; since events are unique, there can be no confusion in the linearization about which event is which. Execution (6) shows that when working with linearizations of labels, it is insufficient to consider the relationship between individual events. The linearization “ Open image in new window ” chosen for Open image in new window is a supersequence of those chosen for its predecessors: “ Open image in new window ” for Open image in new window and “ Open image in new window ” for Open image in new window . The linearization “ Open image in new window ” chosen for Open image in new window is also a supersequence for the same predecessors. And yet, Open image in new window and Open image in new window are incompatible states.
Sequential systems have a single state, which evolves over time. In distributed systems, each replica has its own state, and it is this set of states that evolves. Such a set of states is called a (consistent) cut (Chandy and Lamport 1985).
A cut of an lpo is a sublpo that is downclosed with respect to visibility. The frontier of cut is the set of maximal elements. For example, there are 14 frontiers of execution (6): the singletons Open image in new window , Open image in new window , Open image in new window , Open image in new window , Open image in new window , Open image in new window , the pairs Open image in new window , Open image in new window , Open image in new window , Open image in new window , Open image in new window , Open image in new window , Open image in new window , and the triple Open image in new window . As we explain below, we consider nonmutators in isolation. Thus we do not consider the last four cuts, which include a nonmutator with other events. That leaves 10 frontiers. The definition of the previous section only considered the 6 singletons. Singleton frontiers are generated by pointed cuts, with a single maximal element.
When applied to frontiers, the monotonicity requirement invalidates execution (6). Monotonicity requires that the linearization chosen for a frontier be a subsequence of the linearization chosen for any extension of that frontier. If we are to satisfy state Open image in new window in execution (6), the frontier Open image in new window must linearize to “ Open image in new window ”. If we are to satisfy state Open image in new window , the frontier Open image in new window must linearize to “ Open image in new window ”. Since we require a unique linearization for each frontier, the execution is disallowed.
In order to validate nonmutators, we must consider singleton nonmutator frontiers. The example shows that we must not consider frontiers with multiple nonmutators. There is some freedom in the choices otherwise. For set, we can “saturate” an execution with accessors by augmenting the execution with accessors that witness each cut of the mutators. In a saturated execution, it is sufficient to consider only the pointed accessor cuts, which end in a maximal accessor. For nonsaturated executions, we are forced to examine each mutator cut: it is possible that a future accessor extension may witness that cut. The status of “mixed” frontiers, which include mutators with a single maximal nonmutator, is open for debate. We choose to ignore them, but the definition does not change if they are included.
Summary: A crdt must have a strategy for linearizing all mutator labels, even in the face of partitions. In order to ensure strong ec, the definition must consider sets of events across multiple replicas. Because nonmutators are resolved locally, sec must ignore frontiers with multiple nonmutators.
Cuts and frontiers are wellknown concepts in the literature of distributed systems (Chandy and Lamport 1985). It is natural to consider frontiers when discussing the evolving correctness of a crdt.
2.5 Stuttering
Any linearization of Open image in new window must end in Open image in new window , since the addwin set must reply Open image in new window : the only possibility is “ Open image in new window ”. The linearization of Open image in new window must end in Open image in new window . If it must be a supersequence, the only possibility is “ Open image in new window ”. Taking one more step on the left, Open image in new window must linearize to “ Open image in new window ”. Thus the final state Open image in new window must linearize to “ Open image in new window ”. Reasoning symmetrically, the linearization of Open image in new window must be “ Open image in new window ”, and thus the final Open image in new window must linearize to “ Open image in new window ”. The constraints on the final state are incompatible. Each of these states can be verified in isolation; it is the relation between them that is not satisfiable.
Recall that monotonicity requires that the linearization chosen for a frontier be a subsequence of the linearization chosen for any extension of that frontier. The difficulty here is that subsequence relation ignores the similarity between “ Open image in new window ” and “ Open image in new window ”. Neither of these is a subsequence of the other, yet they capture exactly the same sequence of states, each with six alternations between Open image in new window and Open image in new window . The canonical statebased representative for these sequences is “ Open image in new window ”.
Recall that without stuttering, we deduced that Open image in new window must linearize to “ Open image in new window ” and Open image in new window must linearize to “ Open image in new window ”. Under stuttering equivalence, these are the same, with canonical representative “ Open image in new window ”. Thus, monotonicity under stuttering allows both linearizations to be extended to satisfy the final state Open image in new window , which has canonical representative “ Open image in new window ”.
Summary: crdts are described in terms of convergent states, whereas specifications are described as strings of actions. Actions correspond to labels in the lpo of an execution. Many strings of actions may lead to equivalent states. For example, idempotent actions can be applied repeatedly without modifying the state.
The stuttering equivalence of Brookes (1996) addresses this mismatch. In order to capture the validity of crdts, the definition of subsequence must change from a definition over individual specification strings to a definition over equivalence classes of strings up to stuttering.
3 Eventual Consistency for CRDTs
This section formalizes the intuitions developed in Sect. 2. We define executions, specifications and strong eventual consistency (sec). We discuss properties of eventual consistency and prove that the addwins set is sec.
3.1 Executions
An execution realizes causal delivery if, whenever an event is received at a replica, all predecessors of the event are also received. Most of the crdts in Shapiro et al. (2011a) assume causal delivery, and we assumed it throughout the introductory section. There are costs to maintaining causality, however, and not all crdts assume that executions incur these costs. In the formal development, we allow noncausal executions.
This is a noncausal execution: at the bottom replica, Open image in new window is received before Open image in new window , even though Open image in new window precedes Open image in new window at the top replica.
Causal executions are naturally described as Labelled Partial Orders (lpos), which are transitive and antisymmetric. Section 2 presented several examples of lpos. To capture noncausal systems, we move to Labelled Visibility Orders (lvos), which are merely acyclic. Acyclicity ensures that the transitive closure of an lvo is an lpo. The right picture above shows the lvo corresponding to the timeline on the left. The zigzag arrow represents an intransitive communication. When drawing executions, we use straight lines for “transitive” edges, with the intuitive reading that “this and all preceding actions are delivered”.
lvos arise directly due to noncausal implementations. As we will see in Sect. 4, they also arise via projection from an lpo.
lvos are unusual in the literature. To make this paper selfcontained, we define the obvious generalizations of concepts familiar from lpos, including isomorphism, suborder, restriction, maximality, downclosure and cut.
Fix a set \(\mathbf {L}\) of labels. A Labelled Visibility Order (lvo, also known as an execution) is a triple Open image in new window where Open image in new window is a finite set of events, Open image in new window and Open image in new window is reflexive and acyclic.
Let \({u}\), \(v\) range over lvos. Many concepts extend smoothly from lpos to lvos.

Isomorphism: Write Open image in new window when \({u}\) and \(v\) differ only in the carrier set. We are often interested in the isomorphism class of an lvo.

Pomset: We refer to the isomorphism class of an lvo as a pomset. Pomset abbreviates Partially Ordered Multiset (Plotkin and Pratt 1997). We stick with the name “pomset” here, since “vomset” is not particularly catchy.

Suborder: Write Open image in new window when Open image in new window , Open image in new window , Open image in new window , and Open image in new window .

Restriction:^{1} When Open image in new window , define Open image in new window . Restriction lifts subsets to suborders: Open image in new window denotes the sublvo derived from a subset Open image in new window of events. See Sect. 2.2 for an example of restriction.

Maximal elements: Open image in new window .
We say that \(d\) is maximal for \(v\) when if Open image in new window .

Nonmaximal suborder: Open image in new window .
Open image in new window is the suborder with the maximal elements removed.

Downclosure: \(D\) is downclosed for \(v\) if Open image in new window .

Cut: \({u}\) is a cut of \(v\) if \({u}\subseteq v\) and Open image in new window is downclosed for \(v\).
Let Open image in new window be the set of all cuts of \(v\). A cut is the sublvo corresponding to a downclosed set. Cuts are also known as prefixes. See Sect. 2.4 for an example. A cut is determined by its maximal elements: if Open image in new window then Open image in new window .

Linearization: For Open image in new window , we say that Open image in new window is a linearization of Open image in new window if there exists a bijection Open image in new window such that Open image in new window and Open image in new window .
Executions can be generated operationally as follows: Replicas receive mutator and accessor events from the local client; they also receive mutator events that are forwarded from other replicas. Each replica maintains a set of seen events: an event that is received is added to this set. When an event is received from the local client, the event is additionally added to the execution, with the predecessors in the visibility relation corresponding to the current seen set. If we wish to restrict attention to causal executions, then we require that replicas forward all the mutators in their seen sets, rather than individual events, and, thus, the visibility relation is transitive over mutators.
All executions that are operationally generated satisfy the additional property that Open image in new window is perreplica total: Open image in new window . We do not demand perreplica totality because our results do not rely on replicaspecific information.
3.2 Specifications and Stuttering Equivalence
Specifications are sets of strings, equipped with a distinguished set of mutators and a dependency relation between labels. Specifications are subject to some constraints to ensure that the mutator set and dependency relations are sensible; these are inspired by the conditions on Mazurkiewicz executions (Diekert and Rozenberg 1995). Every specification set yields a derived notion of stuttering equivalence. This leads to the definition of observational subsequence ( Open image in new window ).
We use standard notation for strings: Let \(\sigma \) and \(\tau \) range over strings. Then Open image in new window denotes concatenation, \(\sigma ^*\) denotes Kleene star, \(\sigma \tau \) denotes the set of interleavings, \(\varepsilon \) denotes the empty string and \(\sigma ^{i}\) denotes the \(i^{\text {th}}\) element of \(\sigma \). These notations lift to sets of strings via set union.

\(\mathbf {L}\) is a set of actions (also known as labels),

\(\mathbf {M}\subseteq \mathbf {L}\) is a distinguished set of mutator actions,

Open image in new window is a symmetric and reflexive dependency relation, and

\({\varSigma }\subseteq \mathbf {L}^*\) is a set of valid strings.
Let Open image in new window be the sets of nonmutators.
 (a)
prefix closed: Open image in new window
 (b)
nonmutators are closed under stuttering, and commutation:
 (c)
independent actions commute:
Property (b) ensures that nonmutators do not affect the state of the data structure. Property (c) ensures that commuting of independent actions does not affect the state of the data structure.
Recall that the set specification takes Open image in new window , representing addition and removal of bits 0 and 1, and Open image in new window , representing membership tests returning false or true. The dependency relation is Open image in new window , where \(D^2=D\times D\).
The dependency relation for set is an equivalence, but this need not hold generally. We will see an example in Sect. 4.
The definitions in the rest of the paper assume that we have fixed a specification Open image in new window . In the examples of this section, we use set.
From specification property (b), we know that nonmutators do not affect the state. Thus we have that Open image in new window whenever Open image in new window and Open image in new window . From specification property (c), we know that independent actions commute. Thus we have that Open image in new window whenever Open image in new window and Open image in new window .
Consider specification strings for a unary set over value 0. Since stuttering equivalence allows us to remove both accessors and adjacent mutators with the same label we deduce that the canonical representatives of the equivalence classes induced by \(\sim \) are generated by the regular expression Open image in new window .
Open image in new window can be understood in isolation, whereas Open image in new window can only be understood with respect to a given specification. In the remainder of the paper, the implied specification will be clear from context. Open image in new window is a partial order, whereas Open image in new window is only a preorder, since it is not antisymmetric.
Let \(\sigma \) and \(\tau \) be strings over the unary set with canonical representatives Open image in new window and Open image in new window . Then we have that Open image in new window exactly when either Open image in new window and Open image in new window or Open image in new window and Open image in new window . Thus, observational subsequence order is determined by the number of alternations between the mutators.
Specification strings for the binary set, then, are stuttering equivalent exactly when they yield the same canonical representatives when restricted to 0 and to 1. Thus, observational subsequence order is determined by the number of alternations between the mutators, when restricted to each dependent subsequence. (The final rule in the definition of stuttering, which allows stuttering across independent labels, is crucial to establishing this canonical form.)
3.3 Eventual Consistency
Eventual consistency is defined using the cuts of an execution and the observational subsequence order of the specification. As noted in Sects. 2.2 and 2.4, it is important that we not consider all cuts. Thus, before we define sec, we must define dependent cuts.
The dependent restriction of an execution is defined: Open image in new window where Open image in new window when Open image in new window . See Sect. 2.2 for an example of dependent restriction.
 Linearization:
 Monotonicity:
In Sect. 2, we gave several examples that are sec. See Sects. 2.4 and 2.5 for examples where Open image in new window is given explicitly. Section 2.4 also includes an example that is not sec.
The concerns raised in Sect. 2 are reflected in the definition.

Nonmutators are ignored by the dependent restriction of other nonmutators. As discussed in Sect. 2.1, this relaxation is similar that of updateserializability (Hansdah and Patnaik 1986; GarciaMolina and Wiederhold 1982).

Independent events are ignored by the dependent restriction of an event. As discussed in Sect. 2.2, this relaxation is similar to preserved program order in relaxed memory models (Higham and Kawash 2000; Alglave 2012).

As discussed in Sect. 2.3, punning is allowed: each cut \(p\) is linearized separately to a specification string Open image in new window .

As discussed in Sect. 2.4, we constrain the power puns by considering cuts of the distributed system (Chandy and Lamport 1985).

Monotonicity ensures that the system evolves in a sensible way: new order may be introduced, but old order cannot be forgotten. As discussed in Sect. 2.5, the preserved order is captured in the observational subsequence relation, which allows stuttering (Brookes 1996).
3.4 Properties of Eventual Consistency
We discuss some basic properties of sec. For further analysis, see Sect. 5.
An important property of crdts is prefix closure: If an execution is valid, then every prefix of the execution should also be valid. Prefix closure follows immediately from the definition, since whenever \({u}\) is a prefix of \(v\) we have that Open image in new window .
Prefix closure looks back in time. It is also possible to look forward: A system satisfies eventual delivery if every valid execution can be extended to a valid execution with a maximal element that sees every mutator. If one assumes that every specification string can be extended to a longer specification string by adding nonmutators, then eventual delivery is immediate.
The properties psts, psm and ppe are discussed in the introduction. An sec implementation must satisfies ppe since every dependent set of mutators is linearized: sec enforces the stronger property that there are no new intermediate states, even when executing all mutators in parallel. For causal systems, where Open image in new window is transitive, psts and psm follow by observing that if there is a total order on the mutators of \({u}\) then any linearization of \({u}\) is a specification string.
Burckhardt (2014, Sect. 5) provides a taxonomy of correctness criteria for replicated data types. Our definition implies NoCircularCausality and CausalArbitration, but does not imply either ConsistentPrefix or CausalVisibility. For lpos, which model causal systems, our definition implies CausalVisibility. ReadMyWrites and MonotonicReads require a distinction between local and remote events. If one assumes the replicaspecific constraints given in Sect. 3.1, then our definition satisfies these properties; without them, our definition is too abstract.
3.5 Correctness of the AddWins Set
It answers Open image in new window otherwise. The addwins set is called the “observedremove” set.
We show that any lpo that meets this specification is sec with respect to set. We restrict attention to lpos since causal delivery is assumed for the addwins set in (Shapiro et al. 2011a).
Using the forthcoming composition result (Theorem 2), it suffices for us to address the case when \({u}\) only involves operations on a single element, say 0. For any such lvo \({u}\), we choose a linearization Open image in new window that has a maximum number of alternations between Open image in new window and Open image in new window . If there is a linearization that begins with Open image in new window , then we choose one of these. Below, we summarize some of the key properties of such a linearization.

Open image in new window ends with Open image in new window iff there is an Open image in new window that is not followed by any Open image in new window in \({u}\).

For any lpo \(v\subseteq {u}\), Open image in new window has at most as many alternations as Open image in new window .
The first property above ensures that the accessors are validated correctly, i.e., 0 is deemed to be present iff there is an Open image in new window that is not followed by any Open image in new window .
We are left with proving monotonicity, i.e., if \({u}\subseteq v\), then Open image in new window . Consider Open image in new window and Open image in new window .

If Open image in new window , the second property above ensures that Open image in new window .

In the case that Open image in new window , we deduce by construction that Open image in new window and Open image in new window . In this case, \(\rho \) starts with Open image in new window and has at least as many alternations as Open image in new window . So, we deduce that Open image in new window . The required result follows since Open image in new window .
4 A Collaborative Text Editing Protocol
In this section we consider a variant of the collaborative text editing protocol defined by Attiya et al. (2016). After stating the sequential specification, text, we sketch a correctness proof with respect to our definition of eventual consistency. This example is interesting formally: the dependency relation is not an equivalence, and therefore the dependent projection does not preserve transitivity. The generality of intransitive lvos is necessary to understand text, even assuming a causal implementation.

Mutator Open image in new window initializes the text to node \(a\).

Mutator Open image in new window adds node \(a\) immediately before node \(b\).

Mutator Open image in new window adds node \(a\) immediately after node \(b\).

Mutator Open image in new window removes node \(b\).

Nonmutator query Open image in new window returns the current state of the document.
We demonstrate the correct answers to queries by example. Initially, the document is empty, whereas after initialization, the document contains a single node; thus the specification contains strings such as Open image in new window , where \(\varepsilon \) represents the empty document. Nodes can be added either before or after other nodes; thus Open image in new window results in the document Open image in new window . Nodes are always added adjacent to the target; thus, order matters in Open image in new window which results in Open image in new window rather than Open image in new window . Removal does what one expects; thus Open image in new window results in Open image in new window .
Attiya et al. (2016) define the interface for text using integer indices as targets, rather than nodes. Using the unique correspondence between the nodes and it indices (since node are unique), one can easily adapt an implementation that satisfies our specification to their interface.

Initialization may occur at most once,

each node may be added at most once,

a node may be removed only after it is added, and

a node may be used as a target only if it has been added and not removed.
These constraints forbid adding to a target that has been removed; thus Open image in new window is a valid string, but Open image in new window is not. It also follows that initialization must precede any other mutators.
Implementation. We consider executions that satisfy the same four conditions above imposed on specifications. We refer the reader to the algorithm of Attiya et al. (2016) that provides timestamps for insertions that are monotone with respect to causality.
Correctness. Given an execution, we can find a specification string \(s_1 s_2\) that linearizes the mutators in the dependent restriction of the execution such that \(s_1\) contains only adds and \(s_2\) contains only removes. Such a specification string exists because by the conditions on executions, deletes do not have any outgoing edges to other mutators in the dependent restriction; so, they can be moved to the end in the matching specification string. In order to find \(s_1\) that linearizes the add events, any linearization that respects causality and timestamps (yielded by the algorithm of Attiya et al. (2016)) suffices for our purposes. The conditions required by sec follow immediately.
5 Compositional Reasoning
The aim of this section is to establish compositional methods to reason about replicated data structures. We do so using Labelled Transition Systems (ltss), where the transitions are labelled by dependent cuts. We show how to derive an lts from an execution, Open image in new window . We also define an lts for the most general crdt that validates a specification, Open image in new window . We show that \({u}\) is sec for \({\varSigma }\) exactly when Open image in new window is a refinement of Open image in new window . We use this alternative characterization to establish composition and abstraction results.
LTSs. An lts is a triple consisting of a set a states, an initial state and a labelled transition function between states. We first define the ltss for executions and specifications, then provide examples and discussion.
For both executions and specifications, the labels of the lts are dependent cuts: for executions, these are dependent cuts of the execution itself; for specifications, they are drawn from the set Open image in new window of all possible dependent cuts. We compare lts labels up to isomorphism, rather than identity. Thus it is safe to think of lts labels as (potentially intransitive) pomsets (Plotkin and Pratt 1997).
The states of the lts are different for the execution and specification. For executions, the states are cuts of the execution \({u}\) itself, Open image in new window ; these are general cuts, not just dependent cuts. For specifications, the states are the stuttering equivalence classes of strings allowed by the specification, Open image in new window .
There is an isomorphism between strings and total orders. We make use of this in the definition, treating strings as totallyordered lvos.
The states of the lts are cuts of the execution. The labels on transitions are dependent cuts. The requirements for execution transitions relate the source \(p\), target \(q\) and label \(v\). The leftmost requirements state that the target state must extend both the source and the label; thus the target state must be a combination of events and order from source and label. The middle requirements state that the maximal elements of the label must be new in the target; only the maximal elements of the label are added when moving from source to target. The upper right requirement states that the nonmaximal order of the label must be respected by the source; thus the causal history reported by the label cannot contradict the causal history of the source. The lower right requirement ensures that maximal elements of the label are also maximal in the target. The restriction to dependent cuts explains the labels on transitions Open image in new window and Open image in new window . By definition, there is a selftransition labelled with the empty lvo at every state; we elide these transitions in drawings.
The requirements for specification transitions are similar to those for implementations, but the states are equivalence classes over specification strings: with source \({[}\sigma {]}\) and target \({[}\tau {]}\). There is a transition between the states if there are members of the equivalence classes, \(\sigma \) and \(\tau \), that satisfy the requirements. Since these are total orders, the leftmost requirements state that there must be linearizations of the source and label that are subsequences of the target. Similarly, the upper right requirement states that the nonmaximal order of the label must be respected by the source; thus we have Open image in new window but not Open image in new window for any \(\sigma \). The use of suborder rather than subsequence allows Open image in new window but prevents nonsense transitions such as Open image in new window . Because the states are total orders, we drop the implementation lts requirement that maximal events of the label must be maximal in the target. If we were to impose this restriction, we would disallow Open image in new window .
It is worth noting that the specification of the addwins set removes exactly three edges from the right lts: Open image in new window Open image in new window and Open image in new window .
Refinement. Refinement is a functional form of simulation (Hoare 1972; Lamport 1983; Lynch and Vaandrager 1995). Let Open image in new window and Open image in new window be ltss. A function Open image in new window is a (strong) refinement if Open image in new window imply that there exist Open image in new window and Open image in new window such that Open image in new window . Then \({P}\) refines \({Q}\) (notation Open image in new window ) if there exists a refinement Open image in new window such that the initial states are related, i.e., \(f(p_{0}) =q_{0}\).
We now prove that sec can be characterized as a refinement. We write Open image in new window when \(p_n\) is reachable from \(p_0\) via a finite sequence of steps Open image in new window .
Theorem 1
Open image in new window is EC for the specification \({\varSigma }\) iff Open image in new window .
Proof
For the forward direction, assume \({u}\) is EC and therefore there exists a function Open image in new window such that Open image in new window . For each cut Open image in new window , we start with the dependent restriction, Open image in new window . We further restriction attention to mutators, Open image in new window . The required refinement maps \(p\) to the equivalence class of the linearization of Open image in new window chosen by Open image in new window : Open image in new window . We abuse notation below by identifying each equivalence class with a canonical element of the class.
We show that Open image in new window implies Open image in new window . Since \(p\subseteq q\), we deduce that Open image in new window and by monotonicity, Open image in new window .
We show that Open image in new window implies Open image in new window . Suppose \(v\) only contains mutators. Since \(v\subseteq q\), we deduce that Open image in new window and by monotonicity, Open image in new window . On the other hand, suppose \(v\) contains the nonmutator \(a\). Let \(A= \mathbf {M}\cup \{a\}\). Since \(v\subseteq q\), we deduce that Open image in new window . By monotonicity, Open image in new window . Since Open image in new window we have Open image in new window as required.
Thus Open image in new window , completing this direction of the proof.
For the reverse direction, we are given a refinement Open image in new window . For any Open image in new window , define Open image in new window to be a string in the equivalence class Open image in new window that includes any nonmutator found in \(p\).
We first prove that Open image in new window is a linearization of \(p\). A simple inductive proof demonstrates that for any Open image in new window , there is a transition sequence of the form Open image in new window . Thus, we deduce from the label on the final transition into \(p\) that the Open image in new window related to \(p\) is a linearization of \(p\).
We now establish monotonicity. A simple inductive proof shows that for any Open image in new window , Open image in new window . Thus Open image in new window , by the properties of Open image in new window and the definition of Open image in new window .
Composition. Given two noninteracting data structures whose replicated implementations satisfy their sequential specifications, the implementation that combines them satisfies the interleaving of their specifications. We formalize this as a composition theorem in the style of Herlihy and Wing (1990).
Given an execution \({u}\) and \(L\subseteq \mathbf {L}\), write Open image in new window for the execution that results by restricting \({u}\) to events with labels in L: Open image in new window . This notation lifts to sets in the standard way: Open image in new window . Write Open image in new window to indicate that \({u}\) is sec for \({\varSigma }\).
Theorem 2 (Composition)
Let \(L_1\) and \(L_2\) be mutually independent subsets of \(\mathbf {L}\). For \(i\in \{1,2\}\), let \({\varSigma }_i\) be a specification with labels chosen from \(L_i\), such that \({\varSigma }_1{\varSigma }_2\) is also a specification. If Open image in new window and Open image in new window then Open image in new window (equivalently Open image in new window ).
The proof is immediate. Since \(L_1\) and \(L_2\) are mutually independent, any interleaving of the labels will satisfy the definition.
Abstraction. We describe a process algebra with parallel composition and restriction and establish congruence results. We ignore syntactic details and work directly with ltss. Replica identities do not play a role in the definition; thus, we permit implicit mobility of the client amongst replicas with the only constraint being that the replica has at least as much history on the current item of interaction as the client. This constraint is enforced by the synchronization of the labels, defined below. While the definition includes the case where the client itself is replicated, it does not provide for outofband interaction between the clients at different replicas: All interaction is assumed to happen through the data structure.
The Open image in new window operator is asymmetric between the client and data structure in two ways. First, note that every action of the client must be matched by the data structure. The condition of client quiescence in the definition of \(S_{\times }\), that all of the actions of the client \({P}\) must be matched by \({Q}\); otherwise Open image in new window . However, the first rule for Open image in new window explicitly permits actions of the data structure that may not be matched by the client. This asymmetry permits the composition of the data structure with multiple clients to be described incrementally, one client at a time. Thus, we expect that Open image in new window .
Second, note that right rule for Open image in new window interaction permits the data structure \({Q}\) to introduce order not found in the clients. This is clearly necessary to ensure that that the composition of client Open image in new window with the set data structure is nonempty. In this case, the client has no order between Open image in new window and Open image in new window whereas the data structure orders Open image in new window after Open image in new window . In this paper, we do not permit the client to introduce order that is not seen in the data structure. For a discussion of this issue, see (Jagadeesan and Riely 2015).
We can also define restriction for some set Open image in new window of labels, a lá CCS. Open image in new window . The definitions lift to sets: Open image in new window and Open image in new window .
Lemma 3
If Open image in new window and Open image in new window then Open image in new window and Open image in new window . \(\square \)
It suffices to show that: Open image in new window . The proof proceeds in the traditional style of such proofs in process algebra. We illustrate by sketching the case for client parallel composition. Let \(f\) be the witness for Open image in new window . The proof proceeds by constructing a “product” refinement \(\mathrel {\mathcal {S}}\) relation of the identity on the states of \({P}\) with \(f\), i.e.: Open image in new window .
Thus, an sec implementation can be replaced by the specification.
Theorem 4 (Abstraction)
If \({u}\) is sec for \({\varSigma }\), then Open image in new window .
6 A Replicated Graph Algorithm
We describe a graph implemented with sets for vertices and edges, as specified by Shapiro et al. (2011a). The graph maintains the invariant that the vertices of an edge are also part of the graph. Thus, an edge may be added only if the corresponding vertices exist; conversely, a vertex may be removed only if it supports no edge. In the case of a concurrent addition of an edge with the deletion of either of its vertices, the deletion takes precedence.

Vertices and edges added at most once: Each add label is unique.

Removal of a vertex or edge is preceded by a corresponding add.

Vertices are added before they are mentioned in any edges: If Open image in new window , or Open image in new window there exists \(i,i' <j\) such that: Open image in new window , Open image in new window .

Vertices are removed only after they are mentioned in edges: If Open image in new window , or Open image in new window , then for all \(i<j\): Open image in new window and Open image in new window .
Correctness Using the Set Specification. We first show the correctness of the graph algorithm, using the set specification for the vertex and edge sets. We then apply the abstraction and composition theorems to show the correctness of the algorithm using a set implementation.
 (a)
For any \(v\), Open image in new window is never ordered after Open image in new window , and likewise for \(e\).
 (b)
Open image in new window or Open image in new window is never ordered after Open image in new window or w.
 (c)
Open image in new window or Open image in new window is always ordered after some Open image in new window and Open image in new window .
Define \(\sigma _1\), \(\sigma _2\) and \(\sigma _3\) as follows.

All elements of \(\sigma _1\) are of the form Open image in new window . \(\sigma _1\) exists by (c) above.

All elements of \(\sigma _3\) are of the form Open image in new window . \(\sigma _3\) exists by (b) above.

For each edge Open image in new window that is accessed in \({u}\), let Open image in new window be any interleaving of the events involving Open image in new window in \({u}\) such that no Open image in new window occurs after any Open image in new window in Open image in new window . Open image in new window exists by (a) above. \(\sigma _2\) is any interleaving of all the Open image in new window .
Then \({u}\) is sec with witness Open image in new window .
Full Correctness of the Implementation. We now turn to proving the correctness of the algorithm when the two sets are replaced by their implementations.
7 Conclusions
We have provided a definition of strong eventual consistency that captures validity with respect to a sequential specification. Our definition reflects an attempt to resolve the tension between expressivity (cover the extant examples in the literature) and facilitating reasoning (by retaining a direct relationship with the sequential specification). The notion of concurrent specification developed by Burckhardt et al. (2014) has been used to prove the validity of several replicated data structure implementations. In future work, we would like to discover sufficient conditions relating concurrent and sequential specifications such that any implementation that is correct under the concurrent specification (as defined by Burckhardt et al. (2014)) will also be correct under the sequential counterpart (as defined here).
Footnotes
 1.
We use the standard definitions for restriction on functions and relations. Given a function Open image in new window and \(D\subseteq E\), define Open image in new window and Open image in new window .
 2.
To extend the definition to nonspecification strings, we allow Open image in new window when Open image in new window .
 3.
Readers of Brookes (1996) should note that mumbling is not relevant here, since all mutators are visible.
Notes
Acknowledgements
This paper has been greatly improved by the comments of the anonymous reviewers.
This material is based upon work supported by the National Science Foundation under Grant No. 1617175. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.
References
 Alglave, J.: A formal hierarchy of weak memory models. Formal Methods Syst. Des. 41(2), 178–210 (2012)CrossRefGoogle Scholar
 Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1–7:74 (2014)CrossRefGoogle Scholar
 Attiya, H., Burckhardt, S., Gotsman, A., Morrison, A., Yang, H., Zawirski, M.: Specification and complexity of collaborative text editing. In: Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing, PODC 2016, Chicago, IL, USA, pp. 259–268, 25–28 July 2016Google Scholar
 Bieniusa, A., Zawirski, M., Preguiça, N., Shapiro, M., Baquero, C., Balegas, V., Duarte, S.: Brief announcement: semantics of eventually consistent replicated sets. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 441–442. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642336515_48CrossRefGoogle Scholar
 Bouajjani, A., Enea, C., Hamza, J.: Verifying eventual consistency of optimistic replication systems. In: POPL 2014, pp. 285–296 (2014)Google Scholar
 Brookes, S.D.: Full abstraction for a sharedvariable parallel language. Inf. Comput. 127(2), 145–163 (1996)MathSciNetCrossRefGoogle Scholar
 Budhiraja, N., Marzullo, K., Schneider, F.B., Toueg, S.: The primarybackup approach. In: Mullender, S. (ed.) Distributed Systems, 2nd edn., pp. 199–216 (1993)Google Scholar
 Burckhardt, S.: Principles of eventual consistency. Found. Trends Program. Lang. 1(1–2), 1–150 (2014). ISSN 23251107Google Scholar
 Burckhardt, S., Leijen, D., Fähndrich, M., Sagiv, M.: Eventually consistent transactions. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 67–86. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642288692_4CrossRefGoogle Scholar
 Burckhardt, S., Gotsman, A., Yang, H., Zawirski, M.: Replicated data types: specification, verification, optimality. In: POPL 2014, pp. 271–284 (2014)Google Scholar
 Chandy, K.M., Lamport, L.: Distributed snapshots: determining global states of distributed systems. ACM Trans. Comput. Syst. 3(1), 63–75 (1985)CrossRefGoogle Scholar
 DeCandia, G., Hastorun, D., Jampani, M., Kakulapati, G., Lakshman, A., Pilchin, A., Sivasubramanian, S., Vosshall, P., Vogels, W.: Dynamo: Amazon’s highly available keyvalue store. SIGOPS Oper. Syst. Rev. 41(6), 205–220 (2007)CrossRefGoogle Scholar
 Diekert, V., Rozenberg, G. (eds.): The Book of Traces. World Scientific Publishing Co., Inc., River Edge (1995). ISBN 9810220588Google Scholar
 Ellis, C.A., Gibbs, S.J.: Concurrency control in groupware systems. ACM SIGMOD Rec. 18(2), 399–407 (1989)CrossRefGoogle Scholar
 GarciaMolina, H., Wiederhold, G.: Readonly transactions in a distributed database. ACM Trans. Database Syst. 7(2), 209–234 (1982)CrossRefGoogle Scholar
 Gilbert, S., Lynch, N.: Brewer’s conjecture and the feasibility of consistent, available, partitiontolerant web services. SIGACT News 33(2), 51–59 (2002)CrossRefGoogle Scholar
 Gotsman, A., Yang, H., Ferreira, C., Najafzadeh, M., Shapiro, M.: ‘Cause i’m strong enough: reasoning about consistency choices in distributed systems. In: Proceedings of the 43rd Annual ACM SIGPLANSIGACT POPL, pp. 371–384 (2016)Google Scholar
 Haas, A., Henzinger, T.A., Holzer, A., Kirsch, C.M., Lippautz, M., Payer, H., Sezgin, A., Sokolova, A., Veith, H.: Local linearizability. CoRR, abs/1502.07118 (2015)Google Scholar
 Hansdah, R.C., Patnaik, L.M.: Update serializability in locking. In: Ausiello, G., Atzeni, P. (eds.) ICDT 1986. LNCS, vol. 243, pp. 171–185. Springer, Heidelberg (1986). https://doi.org/10.1007/3540171878_36CrossRefGoogle Scholar
 Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS 12(3), 463–492 (1990)CrossRefGoogle Scholar
 Higham, L., Kawash, J.: Memory consistency and process coordination for SPARC multiprocessors. In: Valero, M., Prasanna, V.K., Vajapeyam, S. (eds.) HiPC 2000. LNCS, vol. 1970, pp. 355–366. Springer, Heidelberg (2000). https://doi.org/10.1007/354044467X_32CrossRefGoogle Scholar
 Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271–281 (1972)CrossRefGoogle Scholar
 Jagadeesan, R., Riely, J.: From sequential specifications to eventual consistency. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015, Part II. LNCS, vol. 9135, pp. 247–259. Springer, Heidelberg (2015). https://doi.org/10.1007/9783662476666_20CrossRefGoogle Scholar
 Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefGoogle Scholar
 Lamport, L.: Specifying concurrent program modules. ACM Trans. Program. Lang. Syst. 5(2), 190–222 (1983)CrossRefGoogle Scholar
 Lynch, N., Vaandrager, F.: Forward and backward simulations. Inf. Comput. 121(2), 214–233 (1995)MathSciNetCrossRefGoogle Scholar
 Perrin, M., Mostéfaoui, A., Jard, C.: Update consistency for waitfree concurrent objects. In: 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, Hyderabad, India, pp. 219–228, 25–29 May 2015Google Scholar
 Plotkin, G., Pratt, V.: Teams can see pomsets. In: Workshop on Partial Order Methods in Verification. DIMACS Series, vol. 29, pp. 117–128. AMS (1997)CrossRefGoogle Scholar
 Saito, Y., Shapiro, M.: Optimistic replication. ACM Comput. Surv. 37(1), 42–81 (2005)CrossRefGoogle Scholar
 Shapiro, M., Preguiça, N., Baquero, C., Zawirski, M.: A comprehensive study of Convergent and Commutative Replicated Data Types. TR 7506, Inria (2011a)Google Scholar
 Shapiro, M. , Preguiça, N.M., Baquero, C., Zawirski, M.: Conflictfree replicated data types. In: Proceedings of the 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems, pp. 386–400 (2011b)Google Scholar
 Shavit, N.: Data structures in the multicore age. Commun. ACM 54(3), 76–84 (2011)CrossRefGoogle Scholar
 Tanenbaum, A., Steen, M.V.: Distributed systems. Pearson Prentice Hall, Upper Saddle River, NJ (2007)MATHGoogle Scholar
 Viotti, P., Vukolic, M.: Consistency in nontransactional distributed storage systems. ACM Comput. Surv. 49(1), 19 (2016)CrossRefGoogle Scholar
 Vogels, W.: Eventually consistent. Commun. ACM 52(1), 40–44 (2009)CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.