Theory Convergence
section‹Strong Eventual Consistency›
text‹In this section we formalise the notion of strong eventual consistency.
We do not make any assumptions about networks or data structures; instead,
we use an abstract model of operations that may be reordered, and we reason about
the properties that those operations must satisfy.
We then provide concrete implementations of that abstract model in later sections.›
theory
Convergence
imports
Util
begin
text‹The \emph{happens-before} relation, as introduced by \<^cite>‹"Lamport:1978jq"›, captures
causal dependencies between operations. It can be defined in terms of sending and receiving
messages on a network.
However, for now, we keep it abstract, our only restriction on the happens-before relation is
that it must be a \emph{strict partial order},
that is, it must be irreflexive and transitive, which implies that it is also antisymmetric.
We describe the state of a node using an abstract type variable.
To model state changes, we assume the existence of an \emph{interpretation} function \isa{interp}
which lifts an operation into a \emph{state transformer}---a function that either maps
an old state to a new state, or fails.›
locale happens_before = preorder hb_weak hb
for hb_weak :: "'a ⇒ 'a ⇒ bool" (infix "≼" 50)
and hb :: "'a ⇒ 'a ⇒ bool" (infix "≺" 50) +
fixes interp :: "'a ⇒ 'b ⇀ 'b" ("⟨_⟩" [0] 1000)
begin
subsection‹Concurrent operations›
text‹We say that two operations $x$ and $y$ are \emph{concurrent}, written
$\isa{x} \mathbin{\isasymparallel} \isa{y}$, whenever one does not happen before the other:
$\neg (\isa{x} \prec \isa{y})$ and $\neg (\isa{y} \prec \isa{x})$.›
definition concurrent :: "'a ⇒ 'a ⇒ bool" (infix "∥" 50) where
"s1 ∥ s2 ≡ ¬ (s1 ≺ s2) ∧ ¬ (s2 ≺ s1)"
lemma concurrentI [intro!]: "¬ (s1 ≺ s2) ⟹ ¬ (s2 ≺ s1) ⟹ s1 ∥ s2"
by (auto simp: concurrent_def)
lemma concurrentD1 [dest]: "s1 ∥ s2 ⟹ ¬ (s1 ≺ s2)"
by (auto simp: concurrent_def)
lemma concurrentD2 [dest]: "s1 ∥ s2 ⟹ ¬ (s2 ≺ s1)"
by (auto simp: concurrent_def)
lemma concurrent_refl [intro!, simp]: "s ∥ s"
by (auto simp: concurrent_def)
lemma concurrent_comm: "s1 ∥ s2 ⟷ s2 ∥ s1"
by (auto simp: concurrent_def)
definition concurrent_set :: "'a ⇒ 'a list ⇒ bool" where
"concurrent_set x xs ≡ ∀y ∈ set xs. x ∥ y"
lemma concurrent_set_empty [simp, intro!]:
"concurrent_set x []"
by (auto simp: concurrent_set_def)
lemma concurrent_set_ConsE [elim!]:
assumes "concurrent_set a (x#xs)"
and "concurrent_set a xs ⟹ concurrent x a ⟹ G"
shows "G"
using assms by (auto simp: concurrent_set_def)
lemma concurrent_set_ConsI [intro!]:
"concurrent_set a xs ⟹ concurrent a x ⟹ concurrent_set a (x#xs)"
by (auto simp: concurrent_set_def)
lemma concurrent_set_appendI [intro!]:
"concurrent_set a xs ⟹ concurrent_set a ys ⟹ concurrent_set a (xs@ys)"
by (auto simp: concurrent_set_def)
lemma concurrent_set_Cons_Snoc [simp]:
"concurrent_set a (xs@[x]) = concurrent_set a (x#xs)"
by (auto simp: concurrent_set_def)
subsection‹Happens-before consistency›
text‹The purpose of the happens-before relation is to require that some operations must be applied
in a particular order, while allowing concurrent operations to be reordered with respect to each other.
We assume that each node applies operations in some sequential order (a standard assumption
for distributed algorithms), and so we can model the execution history of a node as a list of operations.›
inductive hb_consistent :: "'a list ⇒ bool" where
[intro!]: "hb_consistent []" |
[intro!]: "⟦ hb_consistent xs; ∀x ∈ set xs. ¬ y ≺ x ⟧ ⟹ hb_consistent (xs @ [y])"
text‹As a result, whenever two operations $\isa{x}$ and $\isa{y}$ appear in a hb-consistent list,
and $\isa{x}\prec\isa{y}$, then $\isa{x}$ must appear before $\isa{y}$ in the list.
However, if $\isa{x}\mathbin{\isasymparallel}\isa{y}$, the operations can appear in the list
in either order.›
lemma "(x ≺ y ∨ concurrent x y) = (¬ y ≺ x)"
using less_asym by blast
lemma consistentI [intro!]:
assumes "hb_consistent (xs @ ys)"
and "∀x ∈ set (xs @ ys). ¬ z ≺ x"
shows "hb_consistent (xs @ ys @ [z])"
using assms hb_consistent.intros append_assoc by metis
inductive_cases hb_consistent_elim [elim]:
"hb_consistent []"
"hb_consistent (xs@[y])"
"hb_consistent (xs@ys)"
"hb_consistent (xs@ys@[z])"
inductive_cases hb_consistent_elim_gen:
"hb_consistent zs"
lemma hb_consistent_append_D1 [dest]:
assumes "hb_consistent (xs @ ys)"
shows "hb_consistent xs"
using assms by(induction ys arbitrary: xs rule: List.rev_induct) auto
lemma hb_consistent_append_D2 [dest]:
assumes "hb_consistent (xs @ ys)"
shows "hb_consistent ys"
using assms by(induction ys arbitrary: xs rule: List.rev_induct) fastforce+
lemma hb_consistent_append_elim_ConsD [elim]:
assumes "hb_consistent (y#ys)"
shows "hb_consistent ys"
using assms hb_consistent_append_D2 by(metis append_Cons append_Nil)
lemma hb_consistent_remove1 [intro]:
assumes "hb_consistent xs"
shows "hb_consistent (remove1 x xs)"
using assms by (induction rule: hb_consistent.induct) (auto simp: remove1_append)
lemma hb_consistent_singleton [intro!]:
shows "hb_consistent [x]"
using hb_consistent.intros by fastforce
lemma hb_consistent_prefix_suffix_exists:
assumes "hb_consistent ys"
"hb_consistent (xs @ [x])"
"{x} ∪ set xs = set ys"
"distinct (x#xs)"
"distinct ys"
shows "∃prefix suffix. ys = prefix @ x # suffix ∧ concurrent_set x suffix"
using assms proof (induction arbitrary: xs rule: hb_consistent.induct, simp)
fix xs y ys
assume IH: "(⋀xs. hb_consistent (xs @ [x]) ⟹
{x} ∪ set xs = set ys ⟹
distinct (x # xs) ⟹ distinct ys ⟹
∃prefix suffix. ys = prefix @ x # suffix ∧ concurrent_set x suffix) "
assume assms: "hb_consistent ys" "∀x∈set ys. ¬ hb y x"
"hb_consistent (xs @ [x])"
"{x} ∪ set xs = set (ys @ [y])"
"distinct (x # xs)" "distinct (ys @ [y])"
hence "x = y ∨ y ∈ set xs"
using assms by auto
moreover {
assume "x = y"
hence "∃prefix suffix. ys @ [y] = prefix @ x # suffix ∧ concurrent_set x suffix"
by force
}
moreover {
assume y_in_xs: "y ∈ set xs"
hence "{x} ∪ (set xs - {y}) = set ys"
using assms by (auto intro: set_equality_technical)
hence remove_y_in_xs: "{x} ∪ set (remove1 y xs) = set ys"
using assms by auto
moreover have "hb_consistent ((remove1 y xs) @ [x])"
using assms hb_consistent_remove1 by force
moreover have "distinct (x # (remove1 y xs))"
using assms by simp
moreover have "distinct ys"
using assms by simp
ultimately obtain prefix suffix where ys_split: "ys = prefix @ x # suffix ∧ concurrent_set x suffix"
using IH by force
moreover {
have "concurrent x y"
using assms y_in_xs remove_y_in_xs concurrent_def by blast
hence "concurrent_set x (suffix@[y])"
using ys_split by clarsimp
}
ultimately have "∃prefix suffix. ys @ [y] = prefix @ x # suffix ∧ concurrent_set x suffix"
by force
}
ultimately show "∃prefix suffix. ys @ [y] = prefix @ x # suffix ∧ concurrent_set x suffix"
by auto
qed
lemma hb_consistent_append [intro!]:
assumes "hb_consistent suffix"
"hb_consistent prefix"
"⋀s p. s ∈ set suffix ⟹ p ∈ set prefix ⟹ ¬ s ≺ p"
shows "hb_consistent (prefix @ suffix)"
using assms by (induction rule: hb_consistent.induct) force+
lemma hb_consistent_append_porder:
assumes "hb_consistent (xs @ ys)"
"x ∈ set xs"
"y ∈ set ys"
shows "¬ y ≺ x"
using assms by (induction ys arbitrary: xs rule: rev_induct) force+
subsection‹Apply operations›
text‹We can now define a function \isa{apply-operations} that composes an arbitrary list of operations
into a state transformer. We first map \isa{interp} across the list to obtain a state transformer
for each operation, and then collectively compose them using the Kleisli arrow composition combinator.›
definition apply_operations :: "'a list ⇒ 'b ⇀ 'b" where
"apply_operations es ≡ foldl (⊳) Some (map interp es)"
lemma apply_operations_empty [simp]: "apply_operations [] s = Some s"
by(auto simp: apply_operations_def)
lemma apply_operations_Snoc [simp]:
"apply_operations (xs@[x]) = (apply_operations xs) ⊳ ⟨x⟩"
by(auto simp add: apply_operations_def kleisli_def)
subsection‹Concurrent operations commute›
text‹We say that two operations $\isa{x}$ and $\isa{y}$ \emph{commute} whenever
$\langle\isa{x}\rangle \mathbin{\isasymrhd} \langle\isa{y}\rangle = \langle\isa{y}\rangle \mathbin{\isasymrhd} \langle\isa{x}\rangle$,
i.e. when we can swap the order of the composition of their interpretations without changing
the resulting state transformer. For our purposes, requiring that this property holds for
\emph{all} pairs of operations is too strong. Rather, the commutation property is only required
to hold for operations that are concurrent.›
definition concurrent_ops_commute :: "'a list ⇒ bool" where
"concurrent_ops_commute xs ≡
∀x y. {x, y} ⊆ set xs ⟶ concurrent x y ⟶ ⟨x⟩⊳⟨y⟩ = ⟨y⟩⊳⟨x⟩"
lemma concurrent_ops_commute_empty [intro!]: "concurrent_ops_commute []"
by(auto simp: concurrent_ops_commute_def)
lemma concurrent_ops_commute_singleton [intro!]: "concurrent_ops_commute [x]"
by(auto simp: concurrent_ops_commute_def)
lemma concurrent_ops_commute_appendD [dest]:
assumes "concurrent_ops_commute (xs@ys)"
shows "concurrent_ops_commute xs"
using assms by (auto simp: concurrent_ops_commute_def)
lemma concurrent_ops_commute_rearrange:
"concurrent_ops_commute (xs@x#ys) = concurrent_ops_commute (xs@ys@[x])"
by (clarsimp simp: concurrent_ops_commute_def)
lemma concurrent_ops_commute_concurrent_set:
assumes "concurrent_ops_commute (prefix@suffix@[x])"
"concurrent_set x suffix"
"distinct (prefix @ x # suffix)"
shows "apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)"
using assms proof(induction suffix arbitrary: rule: rev_induct, force)
fix a xs
assume IH: "concurrent_ops_commute (prefix @ xs @ [x]) ⟹
concurrent_set x xs ⟹ distinct (prefix @ x # xs) ⟹
apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs)"
assume assms: "concurrent_ops_commute (prefix @ (xs @ [a]) @ [x])"
"concurrent_set x (xs @ [a])" "distinct (prefix @ x # xs @ [a])"
hence ac_comm: "⟨a⟩ ⊳ ⟨x⟩ = ⟨x⟩ ⊳ ⟨a⟩"
by (clarsimp simp: concurrent_ops_commute_def) blast
have copc: "concurrent_ops_commute (prefix @ xs @ [x])"
using assms by (clarsimp simp: concurrent_ops_commute_def) blast
have "apply_operations ((prefix @ x # xs) @ [a]) = (apply_operations (prefix @ x # xs)) ⊳ ⟨a⟩"
by (simp del: append_assoc)
also have "... = (apply_operations (prefix @ xs @ [x])) ⊳ ⟨a⟩"
using IH assms copc by auto
also have "... = ((apply_operations (prefix @ xs)) ⊳ ⟨x⟩) ⊳ ⟨a⟩"
by (simp add: append_assoc[symmetric] del: append_assoc)
also have "... = (apply_operations (prefix @ xs)) ⊳ (⟨a⟩ ⊳ ⟨x⟩)"
using ac_comm kleisli_comm_cong kleisli_assoc by simp
finally show "apply_operations (prefix @ (xs @ [a]) @ [x]) = apply_operations (prefix @ x # xs @ [a])"
by (metis Cons_eq_appendI append_assoc apply_operations_Snoc kleisli_assoc)
qed
subsection‹Abstract convergence theorem›
text‹We can now state and prove our main theorem, $\isa{convergence}$.
This theorem states that two hb-consistent lists of distinct operations, which are permutations
of each other and in which concurrent operations commute, have the same interpretation.›
theorem convergence:
assumes "set xs = set ys"
"concurrent_ops_commute xs"
"concurrent_ops_commute ys"
"distinct xs"
"distinct ys"
"hb_consistent xs"
"hb_consistent ys"
shows "apply_operations xs = apply_operations ys"
using assms proof(induction xs arbitrary: ys rule: rev_induct, simp)
case assms: (snoc x xs)
then obtain prefix suffix where ys_split: "ys = prefix @ x # suffix ∧ concurrent_set x suffix"
using hb_consistent_prefix_suffix_exists by fastforce
moreover hence *: "distinct (prefix @ suffix)" "hb_consistent xs"
using assms by auto
moreover {
have "hb_consistent prefix" "hb_consistent suffix"
using ys_split assms hb_consistent_append_D2 hb_consistent_append_elim_ConsD by blast+
hence "hb_consistent (prefix @ suffix)"
by (metis assms(8) hb_consistent_append hb_consistent_append_porder list.set_intros(2) ys_split)
}
moreover have **: "concurrent_ops_commute (prefix @ suffix @ [x])"
using assms ys_split by (clarsimp simp: concurrent_ops_commute_def)
moreover hence "concurrent_ops_commute (prefix @ suffix)"
by (force simp del: append_assoc simp add: append_assoc[symmetric])
ultimately have "apply_operations xs = apply_operations (prefix@suffix)"
using assms by simp (metis Diff_insert_absorb Un_iff * concurrent_ops_commute_appendD set_append)
moreover have "apply_operations (prefix@suffix @ [x]) = apply_operations (prefix@x # suffix)"
using ys_split assms ** concurrent_ops_commute_concurrent_set by force
ultimately show ?case
using ys_split by (force simp: append_assoc[symmetric] simp del: append_assoc)
qed
corollary convergence_ext:
assumes "set xs = set ys"
"concurrent_ops_commute xs"
"concurrent_ops_commute ys"
"distinct xs"
"distinct ys"
"hb_consistent xs"
"hb_consistent ys"
shows "apply_operations xs s = apply_operations ys s"
using convergence assms by metis
end
subsection‹Convergence and progress›
text‹Besides convergence, another required property of SEC is \emph{progress}: if a valid operation
was issued on one node, then applying that operation on other nodes must also succeed---that is,
the execution must not become stuck in an error state.
Although the type signature of the interpretation function allows operations to fail, we need to
prove that in all $\isa{hb-consistent}$ network behaviours such failure never actually occurs.
We capture the combined requirements in the $\isa{strong-eventual-consistency}$ locale,
which extends $\isa{happens-before}$.›
locale strong_eventual_consistency = happens_before +
fixes op_history :: "'a list ⇒ bool"
and initial_state :: "'b"
assumes causality: "op_history xs ⟹ hb_consistent xs"
assumes distinctness: "op_history xs ⟹ distinct xs"
assumes commutativity: "op_history xs ⟹ concurrent_ops_commute xs"
assumes no_failure: "op_history(xs@[x]) ⟹ apply_operations xs initial_state = Some state ⟹ ⟨x⟩ state ≠ None"
assumes trunc_history: "op_history(xs@[x]) ⟹ op_history xs"
begin
theorem sec_convergence:
assumes "set xs = set ys"
"op_history xs"
"op_history ys"
shows "apply_operations xs = apply_operations ys"
by (meson assms convergence causality commutativity distinctness)
theorem sec_progress:
assumes "op_history xs"
shows "apply_operations xs initial_state ≠ None"
using assms proof(induction xs rule: rev_induct, simp)
case (snoc x xs)
have "apply_operations xs initial_state ≠ None"
using snoc.IH snoc.prems trunc_history kleisli_def bind_def by blast
moreover have "apply_operations (xs @ [x]) = apply_operations xs ⊳ ⟨x⟩"
by simp
ultimately show ?case
using no_failure snoc.prems by (clarsimp simp add: kleisli_def split: bind_splits)
qed
end
end