Skip to content

Instantly share code, notes, and snippets.

@DaveCTurner
Last active Mar 10, 2021
Embed
What would you like to do?
Safety and liveness proof of Dijkstra's distributed termination detection algorithm
theory EWD840
imports "HOL-TLA.TLA"
begin
section Utilities
textA 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)
textThe 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
textAn 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
textThere 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
textThe 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
textWhen 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.
textThe 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))"
textThe 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