Last active
March 10, 2021 04:37
-
-
Save DaveCTurner/4dbf5c4b43cd0500ff223ef1ed412b21 to your computer and use it in GitHub Desktop.
Safety and liveness proof of Dijkstra's distributed termination detection algorithm
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
theory EWD840 | |
imports "HOL-TLA.TLA" | |
begin | |
section Utilities | |
text ‹A handful of general lemmas that were useful along the way.› | |
lemma temp_impI: | |
assumes "sigma ⊨ P ⟹ sigma ⊨ Q" | |
shows "sigma ⊨ P ⟶ Q" | |
using assms by simp | |
lemma imp_leadsto_reflexive: "⊢ S ⟶ (F ↝ F)" using LatticeReflexivity [where F = F] by auto | |
lemma imp_leadsto_transitive: | |
assumes "⊢ S ⟶ (F ↝ G)" "⊢ S ⟶ (G ↝ H)" | |
shows "⊢ S ⟶ (F ↝ H)" | |
proof (intro tempI temp_impI) | |
fix sigma | |
assume S: "S sigma" | |
with assms have 1: "sigma ⊨ (F ↝ G)" "sigma ⊨ (G ↝ H)" | |
by (auto simp add: Valid_def) | |
from 1 LatticeTransitivity [where F = F and G = G and H = H] | |
show "sigma ⊨ F ↝ H" | |
by (auto simp add: Valid_def) | |
qed | |
lemma imp_leadsto_diamond: | |
assumes "⊢ S ⟶ (A ↝ (B ∨ C))" | |
assumes "⊢ S ⟶ (B ↝ D)" | |
assumes "⊢ S ⟶ (C ↝ D)" | |
shows "⊢ S ⟶ (A ↝ D)" | |
proof (intro tempI temp_impI) | |
fix sigma | |
assume S: "sigma ⊨ S" | |
with assms have | |
ABC: "sigma ⊨ A ↝ (B ∨ C)" and | |
BD: "sigma ⊨ B ↝ D" and | |
CD: "sigma ⊨ C ↝ D" | |
by (auto simp add: Valid_def) | |
with LatticeDiamond [where A = A and B = B and C = C and D = D] | |
show "sigma ⊨ A ↝ D" | |
by (auto simp add: Valid_def) | |
qed | |
lemma temp_conj_eq_imp: | |
assumes "⊢ P ⟶ (Q = R)" | |
shows "⊢ (P ∧ Q) = (P ∧ R)" | |
using assms by (auto simp add: Valid_def) | |
text ‹The following lemma is particularly useful for a system that makes | |
some progress which either reaches the desired state directly or which leaves it in | |
a state that is definitely not the desired state but from which it can reach the desired state via | |
some further progress.› | |
lemma imp_leadsto_triangle_excl: | |
assumes AB: "⊢ S ⟶ (A ↝ B)" | |
assumes BC: "⊢ S ⟶ ((B ∧ ¬C) ↝ C)" | |
shows "⊢ S ⟶ (A ↝ C)" | |
proof - | |
have "⊢ ((B ∧ ¬C) ∨ (B ∧ C)) = B" by auto | |
from inteq_reflection [OF this] AB have ABCBC: "⊢ S ⟶ (A ↝ ((B ∧ ¬C) ∨ (B ∧ C)))" by simp | |
show ?thesis | |
proof (intro imp_leadsto_diamond [OF ABCBC] BC) | |
from ImplLeadsto_simple [where F = "LIFT (B ∧ C)"] | |
show "⊢ S ⟶ (B ∧ C ↝ C)" | |
by (auto simp add: Valid_def) | |
qed | |
qed | |
text ‹An action that updates a single value of a function.› | |
definition updatedFun :: "('a ⇒ 'b) stfun ⇒ 'a ⇒ 'b trfun ⇒ action" where | |
"updatedFun f x v ≡ ACT (∀n. id<f$,#n> = (if #n = #x then v else id<$f,#n>))" | |
section Nodes | |
text ‹There is a fixed, finite, set of nodes, which are numbered. Introduce a distinct type | |
for node identifiers, and an ordering relation, and an induction principle.› | |
axiomatization NodeCount :: nat where NodeCount_positive: "NodeCount > 0" | |
typedef Node = "{0..<NodeCount}" using NodeCount_positive by auto | |
definition FirstNode :: Node where "FirstNode == Abs_Node 0" | |
definition LastNode :: Node where "LastNode == Abs_Node (NodeCount-1)" | |
definition PreviousNode :: "Node ⇒ Node" where "PreviousNode == λn. Abs_Node (Rep_Node n - 1)" | |
instantiation Node :: linorder | |
begin | |
definition less_eq_Node :: "Node ⇒ Node ⇒ bool" where "n ≤ m ≡ Rep_Node n ≤ Rep_Node m" | |
definition less_Node :: "Node ⇒ Node ⇒ bool" where "n < m ≡ Rep_Node n < Rep_Node m" | |
instance proof | |
show "⋀(x::Node) y. (x < y) = (x ≤ y ∧ ¬ y ≤ x)" using less_Node_def less_eq_Node_def by force | |
show "⋀(x::Node). x ≤ x" using less_eq_Node_def by force | |
show "⋀(x::Node) y z. x ≤ y ⟹ y ≤ z ⟹ x ≤ z" using less_eq_Node_def by force | |
show "⋀(x::Node) y. x ≤ y ∨ y ≤ x" using less_eq_Node_def by force | |
show "⋀(x::Node) y. x ≤ y ⟹ y ≤ x ⟹ x = y" using less_Node_def less_eq_Node_def | |
by (simp add: Rep_Node_inject) | |
qed | |
end | |
lemma PreviousNode_fixed_point: | |
assumes "n = PreviousNode n" | |
shows "n = FirstNode" | |
using assms | |
unfolding PreviousNode_def FirstNode_def | |
by (metis Abs_Node_inject One_nat_def Rep_Node Rep_Node_inverse atLeastLessThan_iff cancel_comm_monoid_add_class.diff_cancel diff_Suc_less diff_le_self le_less_trans le_neq_implies_less not_le) | |
lemma Node_gt_PreviousNode: | |
assumes "n ≠ FirstNode" | |
shows "m > (PreviousNode n) = (m > n ∨ m = n)" | |
using assms unfolding PreviousNode_def less_Node_def FirstNode_def | |
by (smt Abs_Node_inverse Rep_Node Rep_Node_inject atLeastLessThan_iff diff_Suc_1 diff_is_0_eq' diff_le_self le_add_diff_inverse less_Suc_eq_le not_le_imp_less not_less_iff_gr_or_eq) | |
lemma Node_gt_ne: "(m::Node) > n ⟹ m ≠ n" unfolding less_Node_def by blast | |
lemma Node_gt_LastNode [simp]: "n > LastNode = False" | |
unfolding LastNode_def less_Node_def | |
using Abs_Node_inverse NodeCount_positive Rep_Node not_less_eq by auto | |
lemma Node_induct [case_names FirstNode PreviousNode]: | |
assumes FirstNode: "P FirstNode" | |
assumes PreviousNode: "⋀n. n ≠ FirstNode ⟹ P (PreviousNode n) ⟹ P n" | |
shows "P n" | |
proof - | |
define n_num where "n_num == Rep_Node n" | |
have n_eq: "n = Abs_Node n_num" | |
by (simp add: Rep_Node_inverse n_num_def) | |
have "n_num < NodeCount" using Rep_Node n_num_def by auto | |
thus ?thesis | |
unfolding n_eq | |
proof (induct n_num) | |
case 0 with FirstNode show ?case by (simp add: FirstNode_def) | |
next | |
case (Suc n_num) | |
hence hyp: "P (Abs_Node n_num)" by auto | |
show ?case | |
proof (rule PreviousNode) | |
show "Abs_Node (Suc n_num) ≠ FirstNode" unfolding FirstNode_def | |
by (simp add: Abs_Node_inject NodeCount_positive Suc.prems) | |
from hyp Suc.prems show " P (PreviousNode (Abs_Node (Suc n_num)))" | |
unfolding PreviousNode_def by (simp add: Abs_Node_inverse) | |
qed | |
qed | |
qed | |
datatype TerminationState = MaybeTerminated | NotTerminated | |
axiomatization | |
isNodeActive :: "(Node ⇒ bool) stfun" and | |
nodeState :: "(Node ⇒ TerminationState) stfun" and | |
tokenPosition :: "Node stfun" and | |
tokenState :: "TerminationState stfun" | |
where | |
ewd_basevars: "basevars (isNodeActive, nodeState, tokenPosition, tokenState)" | |
definition StartState :: stpred where | |
"StartState == PRED tokenPosition = #FirstNode ∧ tokenState = #NotTerminated" | |
definition InitiateProbe :: action where | |
"InitiateProbe == ACT | |
(($tokenPosition = #FirstNode) | |
∧ ($tokenState = #NotTerminated ∨ id<$nodeState,#FirstNode> = #NotTerminated) | |
∧ tokenPosition$ = #LastNode | |
∧ tokenState$ = #MaybeTerminated | |
∧ (unchanged isNodeActive) | |
∧ (updatedFun nodeState FirstNode (const MaybeTerminated)))" | |
definition PassToken :: "Node ⇒ action" where | |
"PassToken i == ACT | |
(($tokenPosition = #i) | |
∧ ($tokenPosition ≠ #FirstNode) | |
∧ (¬ id<$isNodeActive,#i> ∨ id<$nodeState,#i> = #NotTerminated ∨ $tokenState = #NotTerminated) | |
∧ (tokenPosition$ = PreviousNode<$tokenPosition>) | |
∧ (tokenState$ = (if id<$nodeState,#i> = #NotTerminated then #NotTerminated else $tokenState)) | |
∧ (unchanged isNodeActive) | |
∧ (updatedFun nodeState i (const MaybeTerminated)))" | |
definition SendMsg :: "Node ⇒ action" where | |
"SendMsg i == ACT | |
id<$isNodeActive,#i> | |
∧ (∃ j. #j ≠ #i ∧ (updatedFun isNodeActive j (const True)) | |
∧ (updatedFun nodeState i (ACT if #i < #j then #NotTerminated else id<$nodeState,#i>))) | |
∧ unchanged (tokenPosition, tokenState)" | |
definition Deactivate :: "Node ⇒ action" where | |
"Deactivate i == ACT | |
id<$isNodeActive,#i> | |
∧ (updatedFun isNodeActive i (const False)) | |
∧ unchanged (tokenPosition, tokenState, nodeState)" | |
definition Controlled :: action where | |
"Controlled ≡ ACT (InitiateProbe ∨ (∃ n. PassToken n))" | |
definition Environment :: action where | |
"Environment ≡ ACT (∃ n. SendMsg n ∨ Deactivate n)" | |
definition Next :: action where | |
"Next ≡ ACT (Controlled ∨ Environment)" | |
definition Fairness :: temporal where | |
"Fairness ≡ TEMP WF(Controlled)_(isNodeActive,nodeState,tokenPosition,tokenState)" | |
definition Spec :: temporal where | |
"Spec ≡ TEMP (Init StartState ∧ □[Next]_(isNodeActive,nodeState,tokenPosition,tokenState) ∧ Fairness)" | |
definition TerminationDetected :: stpred where | |
"TerminationDetected ≡ PRED | |
(tokenPosition = #FirstNode | |
∧ tokenState = #MaybeTerminated | |
∧ id<nodeState,#FirstNode> = #MaybeTerminated | |
∧ ¬ id<isNodeActive,#FirstNode>)" | |
lemma angle_Controlled_lifted: "⊢ <Controlled>_(isNodeActive, nodeState, tokenPosition, tokenState) = Controlled" | |
unfolding angle_def Controlled_def InitiateProbe_def PassToken_def updatedFun_def | |
using PreviousNode_fixed_point by auto | |
lemmas angle_Controlled = inteq_reflection [OF angle_Controlled_lifted] | |
lemma basevars_arbitrary: | |
assumes "⋀u. ⟦ tokenPosition u = A; tokenState u = B; isNodeActive u = C; nodeState u = D ⟧ ⟹ P" | |
shows P | |
using assms ewd_basevars unfolding basevars_def surj_def apply auto by metis | |
lemma enabled_controlled_lifted: | |
"⊢ Enabled Controlled | |
= (tokenState = #NotTerminated ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ (tokenPosition ≠ #FirstNode ∧ ¬ id<isNodeActive, tokenPosition>))" | |
proof - | |
have 1: "⊢ Enabled Controlled = (Enabled InitiateProbe ∨ Enabled (∃n. PassToken n))" | |
unfolding Controlled_def | |
using enabled_disj by simp | |
have 2: "⊢ Enabled InitiateProbe = (tokenPosition = #FirstNode ∧ (tokenState = #NotTerminated ∨ id<nodeState, #FirstNode> = #NotTerminated))" | |
proof (intro intI) | |
fix w | |
show "w ⊨ Enabled InitiateProbe = (tokenPosition = #FirstNode ∧ (tokenState = #NotTerminated ∨ id<nodeState, #FirstNode> = #NotTerminated))" | |
apply (rule basevars_arbitrary [of LastNode MaybeTerminated "isNodeActive w" "λn. if n = FirstNode then MaybeTerminated else nodeState w n"]) | |
unfolding InitiateProbe_def enabled_def updatedFun_def | |
by auto | |
qed | |
have 3: "⊢ Enabled (∃n. PassToken n) = ((tokenPosition ≠ #FirstNode ∧ (¬ id<isNodeActive, tokenPosition> ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ tokenState = #NotTerminated)))" | |
proof (intro intI) | |
fix w | |
show "w ⊨ Enabled (∃n. PassToken n) = ((tokenPosition ≠ #FirstNode ∧ (¬ id<isNodeActive, tokenPosition> ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ tokenState = #NotTerminated)))" | |
apply (rule basevars_arbitrary [of "PreviousNode (tokenPosition w)" "if nodeState w (tokenPosition w) = NotTerminated then NotTerminated else tokenState w" "isNodeActive w" "λn. if n = tokenPosition w then MaybeTerminated else nodeState w n"]) | |
unfolding PassToken_def enabled_def updatedFun_def | |
by auto | |
qed | |
have 4: | |
"⊢ Enabled Controlled = ((tokenPosition = #FirstNode ∧ (tokenState = #NotTerminated ∨ id<nodeState, #FirstNode> = #NotTerminated)) | |
∨ (tokenPosition ≠ #FirstNode ∧ (¬ id<isNodeActive, tokenPosition> ∨ id<nodeState, tokenPosition> = #NotTerminated ∨ tokenState = #NotTerminated)))" | |
unfolding inteq_reflection [OF 1] | |
inteq_reflection [OF 2] | |
inteq_reflection [OF 3] | |
by auto | |
show ?thesis | |
unfolding inteq_reflection [OF 4] by auto | |
qed | |
lemmas enabled_controlled = inteq_reflection [OF enabled_controlled_lifted] | |
section Safety | |
text ‹The safety property of the algorithm says that termination is detected only if all nodes | |
are inactive. The proof works by showing that the safety invariant is actually an invariant, | |
and that this invariant implies the desired safety property.› | |
definition AllNodesInactive :: stpred where | |
"AllNodesInactive ≡ PRED (∀ n. ¬ id<isNodeActive,#n>)" | |
definition SafetyInvariant where | |
"SafetyInvariant ≡ PRED | |
(∀ n. (tokenPosition < #n) ⟶ ¬ id<isNodeActive,#n>) | |
∨ (∃ n. #n ≤ tokenPosition ∧ id<nodeState,#n> = #NotTerminated) | |
∨ tokenState = #NotTerminated" | |
lemma safety: | |
shows "⊢ Spec ⟶ □(TerminationDetected ⟶ AllNodesInactive)" | |
proof - | |
have "⊢ Spec ⟶ □SafetyInvariant" | |
proof invariant | |
fix sigma | |
assume s: "Spec sigma" | |
thus "sigma ⊨ Init SafetyInvariant" | |
by (auto simp add: Spec_def SafetyInvariant_def StartState_def Init_def) | |
show "sigma ⊨ stable SafetyInvariant" | |
proof (intro Stable) | |
from s show "sigma ⊨ □[Next]_(isNodeActive, nodeState, tokenPosition, tokenState)" | |
by (simp add: Spec_def) | |
show "⊢ $SafetyInvariant ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ SafetyInvariant$" | |
proof clarsimp | |
fix s t | |
assume s: "SafetyInvariant s" | |
and st: "(s, t) ⊨ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState)" | |
from st have | |
"((s, t) ⊨ InitiateProbe) | |
∨ (∃n. (s, t) ⊨ PassToken n) | |
∨ (∃n. (s, t) ⊨ SendMsg n) | |
∨ (∃n. (s, t) ⊨ Deactivate n) | |
∨ ((s, t) ⊨ unchanged (isNodeActive, nodeState, tokenPosition, tokenState))" | |
by (auto simp add: square_def Next_def Controlled_def Environment_def) | |
thus "SafetyInvariant t" | |
proof (elim disjE conjE exE) | |
assume "(s, t) ⊨ unchanged (isNodeActive, nodeState, tokenPosition, tokenState)" | |
with s show "SafetyInvariant t" by (simp add: SafetyInvariant_def) | |
next | |
assume "InitiateProbe (s, t)" | |
hence step: | |
"tokenPosition s = FirstNode" "tokenState s = NotTerminated ∨ nodeState s FirstNode = NotTerminated" | |
"tokenPosition t = LastNode" "tokenState t = MaybeTerminated" "isNodeActive t = isNodeActive s" | |
"⋀n. nodeState t n = (if n = FirstNode then MaybeTerminated else nodeState s n)" | |
unfolding InitiateProbe_def updatedFun_def | |
by auto | |
note step_simps[simp] = `tokenPosition s = FirstNode` `tokenPosition t = LastNode` `tokenState t = MaybeTerminated` `isNodeActive t = isNodeActive s` | |
`⋀n. nodeState t n = (if n = FirstNode then MaybeTerminated else nodeState s n)` | |
show "SafetyInvariant t" | |
unfolding SafetyInvariant_def | |
apply (auto simp add: less_Node_def LastNode_def) | |
by (metis Abs_Node_inverse Rep_Node Suc_pred atLeastLessThan_iff diff_Suc_less less_or_eq_imp_le neq0_conv not_less_eq) | |
next | |
fix n assume "Deactivate n (s, t)" | |
hence step: | |
"tokenPosition t = tokenPosition s" "tokenState t = tokenState s" "nodeState t = nodeState s" "⋀n. isNodeActive t n ⟹ isNodeActive s n" | |
unfolding Deactivate_def updatedFun_def apply auto | |
by (metis id_apply unl_before unl_con unl_lift2) | |
from s show "SafetyInvariant t" by (auto simp add: less_Node_def LastNode_def SafetyInvariant_def step) | |
next | |
fix sender assume step: "SendMsg sender (s, t)" | |
from step have step_simps[simp]: "tokenPosition t = tokenPosition s" "tokenState t = tokenState s" by (auto simp add: SendMsg_def) | |
from step have n_active: "isNodeActive s sender" by (simp add: SendMsg_def) | |
from step obtain receiver where receiver: "receiver ≠ sender" | |
"⋀m. isNodeActive t m = (m = receiver ∨ isNodeActive s m)" | |
"⋀m. nodeState t m = (if m = sender ∧ receiver > sender then NotTerminated else nodeState s m)" | |
unfolding SendMsg_def updatedFun_def by auto | |
show ?thesis | |
proof (cases "receiver < tokenPosition s") | |
case False | |
with s show ?thesis | |
unfolding SafetyInvariant_def less_Node_def | |
apply auto | |
apply (metis le_less_trans less_Node_def n_active not_le receiver(2) receiver(3)) | |
by (metis receiver(3)) | |
next | |
case True | |
with s receiver show ?thesis unfolding SafetyInvariant_def less_Node_def by fastforce | |
qed | |
next | |
fix n assume step: "PassToken n (s,t)" | |
hence step_tokenPosition[simp]: "tokenPosition s = n" "tokenPosition t = PreviousNode n" "n ≠ FirstNode" unfolding PassToken_def by auto | |
from step have step_active[simp]: "isNodeActive t = isNodeActive s" unfolding PassToken_def by auto | |
from step have step_colour: "⋀m. nodeState t m = (if m = n then MaybeTerminated else nodeState s m)" | |
by (simp add: PassToken_def updatedFun_def) | |
from step have step_tokenState: "tokenState t = (if nodeState s n = NotTerminated then NotTerminated else tokenState s)" | |
unfolding PassToken_def by simp | |
show ?thesis | |
proof (cases "nodeState s n = NotTerminated ∨ tokenState s = NotTerminated") | |
case True with step_tokenState show ?thesis by (auto simp add: SafetyInvariant_def) | |
next | |
case False | |
with TerminationState.exhaust have whites: "nodeState s n = MaybeTerminated" "tokenState s = MaybeTerminated" by auto | |
from whites step_colour step_tokenState have step_simps[simp]: | |
"nodeState t = nodeState s" "tokenState t = tokenState s" by auto | |
from step whites have n_inactive: "¬isNodeActive s n" unfolding PassToken_def by auto | |
from step_tokenPosition(3) | |
have gt1: "⋀m. m < n = (m < (PreviousNode n) ∨ m = PreviousNode n)" | |
using Node_gt_PreviousNode not_less_iff_gr_or_eq by blast | |
have gt2: "⋀m. n < m = ((PreviousNode n) < m ∧ m ≠ n)" | |
using Node_gt_PreviousNode step_tokenPosition(3) by blast | |
from s n_inactive show ?thesis | |
unfolding SafetyInvariant_def | |
apply (clarsimp simp add: gt1 gt2) | |
by (metis TerminationState.simps(2) gt2 leD leI whites(1)) | |
qed | |
qed | |
qed | |
qed | |
qed | |
moreover have "⊢ □SafetyInvariant ⟶ □(TerminationDetected ⟶ AllNodesInactive)" | |
unfolding SafetyInvariant_def | |
proof (intro STL4, clarsimp, intro conjI impI) | |
fix w | |
assume inactive_gt: "∀n. (tokenPosition w < n) ⟶ ¬ isNodeActive w n" | |
show "TerminationDetected w ⟹ AllNodesInactive w" | |
unfolding TerminationDetected_def AllNodesInactive_def | |
proof clarsimp | |
fix n assume a: "isNodeActive w n" "tokenPosition w = FirstNode" "¬ isNodeActive w FirstNode" | |
with inactive_gt have "¬ n > FirstNode" by auto | |
hence "n = FirstNode" | |
unfolding less_Node_def FirstNode_def | |
by (metis Abs_Node_inverse NodeCount_positive Rep_Node Rep_Node_inject atLeastLessThan_iff le_numeral_extra(3) nat_less_le) | |
with a show False by simp | |
qed | |
next | |
fix w | |
assume "tokenState w = NotTerminated" | |
thus "TerminationDetected w ⟹ AllNodesInactive w" | |
unfolding TerminationDetected_def | |
by auto | |
next | |
fix w | |
assume "∃n. (n ≤ tokenPosition w) ∧ nodeState w n = NotTerminated" | |
then obtain n where n: "n ≤ tokenPosition w" "nodeState w n = NotTerminated" by auto | |
thus "TerminationDetected w ⟹ AllNodesInactive w" | |
unfolding TerminationDetected_def AllNodesInactive_def | |
proof clarsimp | |
assume "tokenPosition w = FirstNode" "nodeState w FirstNode = MaybeTerminated" | |
with n show False | |
by (metis Abs_Node_inverse TerminationState.distinct(2) FirstNode_def NodeCount_positive Rep_Node_inverse atLeastLessThan_iff le_zero_eq less_eq_Node_def) | |
qed | |
qed | |
ultimately show ?thesis by (simp add: Valid_def) | |
qed | |
section Liveness | |
text ‹When all nodes become inactive the algorithm runs through up to three further distinct | |
phases before detecting termination. The first phase is simply to return the token to the first | |
node, without any constraints on its state or the states of the nodes. The second phase | |
passes the token around the ring once more which sets each node's state to $MaybeTerminated$, | |
although the token itself may be ``contaminated'' by a $NotTerminated$ state. The third phase | |
passes the token around the ring one last time to remove any such contamination.› | |
text ‹The following predicates correspond to each step of each of these phases.› | |
definition AllNodesInactiveAndTokenAt where "AllNodesInactiveAndTokenAt n ≡ PRED | |
(AllNodesInactive ∧ tokenPosition = #n)" | |
definition NodeCleaningRunAt where "NodeCleaningRunAt n ≡ PRED | |
(AllNodesInactiveAndTokenAt n | |
∧ id<nodeState,#FirstNode> = #MaybeTerminated | |
∧ (∀ m. #n < #m ⟶ id<nodeState,#m> = #MaybeTerminated))" | |
definition TokenCleaningRunAt where "TokenCleaningRunAt n ≡ PRED | |
(AllNodesInactiveAndTokenAt n | |
∧ tokenState = #MaybeTerminated | |
∧ (∀ m. id<nodeState,#m> = #MaybeTerminated))" | |
text ‹The liveness proof now shows that each phase completes and either detects termination | |
or leads to the next phase.› | |
lemma step: | |
assumes "⊢ P ⟶ AllNodesInactive" | |
assumes "⊢ P ⟶ ¬ TerminationDetected" | |
assumes "⊢ $P ∧ unchanged (isNodeActive, nodeState, tokenPosition, tokenState) ⟶ P$" | |
assumes "⊢ $P ∧ Controlled ⟶ Q$" | |
shows "⊢ Spec ⟶ (P ↝ Q)" | |
proof - | |
have "⊢ (□[Next]_(isNodeActive, nodeState, tokenPosition, tokenState) | |
∧ WF(Controlled)_(isNodeActive, nodeState, tokenPosition, tokenState)) ⟶ (P ↝ Q)" | |
proof (intro WF1) | |
from assms have no_Environment: "⋀s t. s ⊨ P ⟹ (s, t) ⊨ Environment ⟹ False" | |
by (auto simp add: Environment_def AllNodesInactive_def Valid_def SendMsg_def Deactivate_def) | |
with assms | |
show "⊢ $P ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ P$ ∨ Q$" | |
"⊢ ($P ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState)) ∧ <Controlled>_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ Q$" | |
"⊢ $P ∧ [Next]_(isNodeActive, nodeState, tokenPosition, tokenState) ⟶ $Enabled (<Controlled>_(isNodeActive, nodeState, tokenPosition, tokenState))" | |
unfolding angle_Controlled enabled_controlled Next_def square_def Valid_def AllNodesInactive_def TerminationDetected_def | |
apply simp_all | |
apply (meson TerminationState.exhaust, blast) | |
by (metis (full_types) TerminationState.exhaust) | |
qed | |
thus ?thesis | |
by (auto simp add: Spec_def Fairness_def) | |
qed | |
lemma liveness: "⊢ Spec ⟶ (AllNodesInactive ↝ TerminationDetected)" | |
proof - | |
note [simp] = TokenCleaningRunAt_def NodeCleaningRunAt_def | |
AllNodesInactiveAndTokenAt_def AllNodesInactive_def | |
square_def Controlled_def InitiateProbe_def PassToken_def updatedFun_def | |
TerminationDetected_def | |
have "⊢ Spec ⟶ (AllNodesInactive ↝ AllNodesInactiveAndTokenAt FirstNode)" | |
proof - | |
have "⊢ AllNodesInactive = (∃n. AllNodesInactiveAndTokenAt n)" unfolding AllNodesInactiveAndTokenAt_def by auto | |
hence "⊢ (AllNodesInactive ↝ AllNodesInactiveAndTokenAt FirstNode) | |
= (∀n. (AllNodesInactiveAndTokenAt n ↝ AllNodesInactiveAndTokenAt FirstNode))" | |
by (metis inteq_reflection leadsto_exists) | |
moreover { | |
fix n | |
have "⊢ Spec ⟶ (AllNodesInactiveAndTokenAt n ↝ AllNodesInactiveAndTokenAt FirstNode)" | |
proof (induct n rule: Node_induct) | |
case FirstNode show ?case by (intro imp_leadsto_reflexive) | |
next | |
case (PreviousNode n) | |
hence "⊢ Spec ⟶ (AllNodesInactiveAndTokenAt n ↝ AllNodesInactiveAndTokenAt (PreviousNode n))" | |
by (intro step, auto) | |
with PreviousNode show ?case by (metis imp_leadsto_transitive) | |
qed | |
} | |
ultimately show ?thesis by (auto simp add: Valid_def) | |
qed | |
moreover have "⊢ Spec ⟶ ((AllNodesInactiveAndTokenAt FirstNode ∧ ¬ TerminationDetected) ↝ NodeCleaningRunAt LastNode)" | |
by (intro step, auto) | |
moreover have "⋀n. ⊢ Spec ⟶ (NodeCleaningRunAt n ↝ NodeCleaningRunAt FirstNode)" | |
proof - | |
fix n show "?thesis n" | |
proof (induct n rule: Node_induct) | |
case FirstNode | |
with LatticeReflexivity show ?case by auto | |
next | |
case (PreviousNode n) | |
with Node_gt_PreviousNode Node_gt_ne | |
have "⊢ Spec ⟶ (NodeCleaningRunAt n ↝ NodeCleaningRunAt (PreviousNode n))" | |
by (intro step, auto) | |
with PreviousNode show ?case by (metis imp_leadsto_transitive) | |
qed | |
qed | |
moreover have "⊢ Spec ⟶ (NodeCleaningRunAt FirstNode ∧ ¬ TerminationDetected ↝ TokenCleaningRunAt LastNode)" | |
proof - | |
have firstNode_min: "⋀n. n = FirstNode ∨ FirstNode < n" | |
using Abs_Node_inverse FirstNode_def NodeCount_positive le_less less_eq_Node_def by fastforce | |
hence "⊢ NodeCleaningRunAt FirstNode | |
= (AllNodesInactiveAndTokenAt FirstNode ∧ (∀ m. id<nodeState,#m> = #MaybeTerminated))" | |
by (auto, force) | |
thus ?thesis by (intro step, auto, metis firstNode_min) | |
qed | |
moreover have "⋀n. ⊢ Spec ⟶ (TokenCleaningRunAt n ↝ TerminationDetected)" | |
proof - | |
fix n | |
show "?thesis n" | |
proof (induct n rule: Node_induct) | |
case FirstNode | |
have "⊢ TokenCleaningRunAt FirstNode ⟶ TerminationDetected" by auto | |
hence "⊢ TokenCleaningRunAt FirstNode ↝ TerminationDetected" | |
using ImplLeadsto_simple by auto | |
thus ?case by (auto simp add: ImplLeadsto_simple intI tempD) | |
next | |
case (PreviousNode n) | |
hence "⊢ Spec ⟶ (TokenCleaningRunAt n ↝ TokenCleaningRunAt (PreviousNode n))" | |
by (intro step, auto, blast) | |
with PreviousNode show ?case by (metis imp_leadsto_transitive) | |
qed | |
qed | |
ultimately show ?thesis | |
by (metis imp_leadsto_transitive imp_leadsto_triangle_excl) | |
qed | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment