lib: two examples of concurrency reasoning.
Two different simple examples which make use of the prefix refinement framework and the rely-guarantee VCG.
This commit is contained in:
Thomas Sewell
parent
64efe07ff7
commit
c4f43fd8dc
|
|
@ -0,0 +1,839 @@
|
|||
(*
|
||||
* Copyright 2017, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_BSD)
|
||||
*)
|
||||
theory Peterson_Atomicity
|
||||
imports
|
||||
"../Atomicity_Lib"
|
||||
begin
|
||||
|
||||
text {*
|
||||
Preliminaries, a type of identities.
|
||||
*}
|
||||
|
||||
datatype ident = A | B
|
||||
|
||||
primrec other_ident
|
||||
where
|
||||
"other_ident A = B"
|
||||
| "other_ident B = A"
|
||||
|
||||
lemma other_ident_split:
|
||||
"P (other_ident x) = ((x = A \<longrightarrow> P B) \<and> (x = B \<longrightarrow> P A))"
|
||||
by (cases x, simp_all)
|
||||
|
||||
lemma neq_A_B[simp]:
|
||||
"(x \<noteq> A) = (x = B)"
|
||||
"(A \<noteq> x) = (x = B)"
|
||||
"(x \<noteq> B) = (x = A)"
|
||||
"(B \<noteq> x) = (x = A)"
|
||||
by (simp | cases x)+
|
||||
|
||||
lemma forall_ident_eq:
|
||||
"(\<forall>ident. P ident) = (P A \<and> P B)"
|
||||
using ident.nchotomy
|
||||
by metis
|
||||
|
||||
lemma other_other_ident_simps[simp]:
|
||||
"other_ident (other_ident x) = x"
|
||||
"(other_ident x = y) = (x \<noteq> y)"
|
||||
"(x = other_ident y) = (x \<noteq> y)"
|
||||
by (simp_all split: other_ident_split add: eq_commute)
|
||||
|
||||
text {*
|
||||
The state of the algorithm. The variables A/B are condensed into
|
||||
an ab_v variable, so we can parametrise by thread A/B. The priority
|
||||
variable is t_v, and the critical section cs has two variable to
|
||||
operate on, cs1_v and cs2_v.
|
||||
|
||||
Labels are needed to track where we're up to for the preconditions,
|
||||
relies and guarantees.
|
||||
*}
|
||||
|
||||
datatype label = Awaiting | Critical | Exited
|
||||
|
||||
record ('a, 'b) p_state =
|
||||
ab_v :: "ident \<Rightarrow> bool"
|
||||
ab_label :: "ident \<Rightarrow> label"
|
||||
t_v :: "ident"
|
||||
cs1_v :: "'a"
|
||||
cs2_v :: "'b"
|
||||
|
||||
locale mx_locale =
|
||||
fixes cs1 :: "'b \<Rightarrow> 'a"
|
||||
and cs2 :: "(('a, 'b) p_state, unit) tmonad"
|
||||
and csI :: "'b \<Rightarrow> bool"
|
||||
begin
|
||||
|
||||
definition
|
||||
set_ab :: "ident \<Rightarrow> bool \<Rightarrow> ('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state"
|
||||
where
|
||||
"set_ab ident trying s = (s \<lparr> ab_v := (ab_v s) (ident := trying) \<rparr>)"
|
||||
|
||||
definition
|
||||
set_label :: "ident \<Rightarrow> label \<Rightarrow> ('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state"
|
||||
where
|
||||
"set_label ident label s = (s \<lparr> ab_label := (ab_label s) (ident := label) \<rparr>)"
|
||||
|
||||
definition
|
||||
locked :: "ident \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"locked ident s = (ab_v s (other_ident ident) \<longrightarrow> t_v s = ident)"
|
||||
|
||||
definition
|
||||
acquire_lock :: "ident \<Rightarrow> (('a, 'b) p_state, unit) tmonad"
|
||||
where
|
||||
"acquire_lock ident = do
|
||||
interference;
|
||||
modify (set_ab ident True);
|
||||
modify (\<lambda>s. s \<lparr> t_v := other_ident ident \<rparr>);
|
||||
modify (set_label ident Awaiting);
|
||||
interference;
|
||||
Await (locked ident);
|
||||
modify (set_label ident Critical)
|
||||
od"
|
||||
|
||||
definition
|
||||
release_lock :: "ident \<Rightarrow> (('a, 'b) p_state, unit) tmonad"
|
||||
where
|
||||
"release_lock ident = do
|
||||
modify (set_ab ident False);
|
||||
modify (set_label ident Exited);
|
||||
interference;
|
||||
return ()
|
||||
od"
|
||||
|
||||
definition
|
||||
abs_critical_section :: "(('a, 'b) p_state, unit) tmonad"
|
||||
where
|
||||
"abs_critical_section = do
|
||||
interferences;
|
||||
modify (\<lambda>s. s \<lparr> cs1_v := cs1 (cs2_v s) \<rparr>);
|
||||
cs2;
|
||||
interference
|
||||
od"
|
||||
|
||||
definition
|
||||
abs_peterson_proc ::
|
||||
"ident \<Rightarrow> (('a, 'b) p_state, unit) tmonad"
|
||||
where
|
||||
"abs_peterson_proc ident = do
|
||||
acquire_lock ident;
|
||||
abs_critical_section;
|
||||
release_lock ident
|
||||
od"
|
||||
|
||||
definition
|
||||
critical_section :: "(('a, 'b) p_state, unit) tmonad"
|
||||
where
|
||||
"critical_section = do
|
||||
interference;
|
||||
modify (\<lambda>s. s \<lparr> cs1_v := cs1 (cs2_v s) \<rparr>);
|
||||
interference;
|
||||
cs2;
|
||||
interference
|
||||
od"
|
||||
|
||||
definition
|
||||
peterson_proc :: "ident \<Rightarrow> (('a, 'b) p_state, unit) tmonad"
|
||||
where
|
||||
"peterson_proc ident = do
|
||||
acquire_lock ident;
|
||||
critical_section;
|
||||
release_lock ident
|
||||
od"
|
||||
|
||||
abbreviation "critical label \<equiv> label = Critical"
|
||||
|
||||
text {* The required invariant. We can't both be in the critical section.
|
||||
Whenever neither of us is in the critical section, its invariant holds. *}
|
||||
definition
|
||||
req_peterson_inv :: "('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"req_peterson_inv s = (\<not> (critical (ab_label s A) \<and> critical (ab_label s B))
|
||||
\<and> (critical (ab_label s A) \<or> critical (ab_label s B) \<or> csI (cs2_v s)))"
|
||||
|
||||
text {* The key invariant. We can't both be enabled, where that means
|
||||
either we're in the critical section or waiting to enter with priority.
|
||||
*}
|
||||
abbreviation(input)
|
||||
enabled :: "ident \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"enabled ident s \<equiv> (critical (ab_label s ident)
|
||||
\<or> (ab_label s ident = Awaiting \<and> t_v s = ident))"
|
||||
|
||||
definition
|
||||
key_peterson_inv :: "('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"key_peterson_inv s = (\<not> (enabled A s \<and> enabled B s))"
|
||||
|
||||
text {* Some trivia about labels and variables. *}
|
||||
definition
|
||||
local_peterson_inv :: "('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"local_peterson_inv s
|
||||
= (\<forall>ident. ab_label s ident \<noteq> Exited \<longrightarrow> ab_v s ident)"
|
||||
|
||||
definition
|
||||
"invs s = (req_peterson_inv s
|
||||
\<and> key_peterson_inv s \<and> local_peterson_inv s)"
|
||||
|
||||
lemmas invs_defs = req_peterson_inv_def key_peterson_inv_def local_peterson_inv_def
|
||||
|
||||
definition
|
||||
peterson_rel :: "ident \<Rightarrow> ('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"peterson_rel ident s_prior s = ((* assume invs *) invs s_prior \<longrightarrow>
|
||||
(* invariants are preserved *)
|
||||
(invs s
|
||||
(* I won't adjust your variables *)
|
||||
\<and> (ab_v s (other_ident ident) = ab_v s_prior (other_ident ident))
|
||||
\<and> (ab_label s (other_ident ident) = ab_label s_prior (other_ident ident))
|
||||
(* I will only ever give you priority *)
|
||||
\<and> (t_v s_prior = other_ident ident \<longrightarrow> t_v s = other_ident ident)
|
||||
(* If you're in the critical section, I won't change cs2_v and cs1_v *)
|
||||
\<and> (critical (ab_label s_prior (other_ident ident))
|
||||
\<longrightarrow> cs2_v s = cs2_v s_prior \<and> cs1_v s = cs1_v s_prior)
|
||||
))"
|
||||
|
||||
lemma peterson_rel_rtranclp[simp]:
|
||||
"rtranclp (peterson_rel ident) = (peterson_rel ident)"
|
||||
apply (rule rtranclp_id2)
|
||||
apply (clarsimp simp: peterson_rel_def)
|
||||
apply (clarsimp simp: peterson_rel_def)
|
||||
done
|
||||
|
||||
lemma reflp_peterson_rel[simp]:
|
||||
"reflp (peterson_rel x)"
|
||||
apply (rule reflpI)
|
||||
apply (clarsimp simp add: peterson_rel_def)
|
||||
done
|
||||
declare reflp_peterson_rel[THEN reflpD, simp]
|
||||
|
||||
lemma peterson_rel_imp_assume_invs:
|
||||
"invs x \<Longrightarrow> (peterson_rel ident x y \<and> invs x \<and> invs y \<longrightarrow> P x y)
|
||||
\<Longrightarrow> (peterson_rel ident x y \<longrightarrow> P x y)"
|
||||
by (simp add: peterson_rel_def)
|
||||
|
||||
end
|
||||
|
||||
text {*
|
||||
We assume validity for the underspecified critical section code represented by
|
||||
@{text cs2}.
|
||||
|
||||
We also assume some basic sanity properties about the structure of @{text cs2}.
|
||||
*}
|
||||
locale mx_locale_wp = mx_locale cs1 cs2 csI for cs1 :: "'b \<Rightarrow> 'a" and cs2 and csI +
|
||||
assumes
|
||||
cs_wp: "\<forall>s c. I s \<and> lockf s \<longrightarrow> I s \<and> lockf (s \<lparr> cs2_v := c \<rparr>)
|
||||
\<Longrightarrow>
|
||||
\<lbrace> \<lambda>s0' s'. csI (cs2_v s') \<and> s0' = s0 \<and> s' = s \<and> I s \<and> lockf s
|
||||
\<and> cs1_v s' = cs1 (cs2_v s') \<rbrace>,
|
||||
\<lbrace> \<lambda>s0 s. I s0 \<and> lockf s0 \<longrightarrow> cs2_v s = cs2_v s0 \<and> I s \<and> lockf s
|
||||
\<and> cs1_v s = cs1_v s0 \<rbrace>
|
||||
cs2
|
||||
\<lbrace> \<lambda>s0 s. I s0 \<longrightarrow> (\<exists>c. s = s0 \<lparr> cs2_v := c \<rparr>) \<and> I s \<and> lockf s \<rbrace>,
|
||||
\<lbrace> \<lambda>_ s0' s'. \<exists>c. csI c \<and> s' = s \<lparr> cs2_v := c \<rparr>
|
||||
\<and> (\<exists>c'. s0' = s0 \<or> s0' = s \<lparr> cs2_v := c' \<rparr>)
|
||||
\<and> I s' \<and> lockf s' \<rbrace>"
|
||||
and cs_closed: "prefix_closed cs2"
|
||||
and cs_not_env_steps_first: "not_env_steps_first cs2"
|
||||
begin
|
||||
|
||||
method_setup rev_drule = {*
|
||||
Attrib.thms >> curry (fn (thms, ctxt)
|
||||
=> SIMPLE_METHOD (dresolve_tac ctxt thms 1 #> Seq.list_of #> rev #> Seq.of_list))
|
||||
*}
|
||||
|
||||
lemma cs2_wp_apply_peterson[wp]:
|
||||
"\<lbrace> (\<lambda>s0 s. csI (cs2_v s)
|
||||
\<and> invs s0 \<and> invs s \<and> critical (ab_label s ident)
|
||||
\<and> cs1_v s = cs1 (cs2_v s)
|
||||
\<and> (\<forall>s0' c' c. csI c \<longrightarrow> (\<exists>c'. s0' = s0 \<or> s0' = s \<lparr> cs2_v := c' \<rparr>)
|
||||
\<longrightarrow> Q () s0' (s \<lparr> cs2_v := c\<rparr>))) \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
cs2
|
||||
\<lbrace> peterson_rel ident \<rbrace>,
|
||||
\<lbrace> Q \<rbrace>"
|
||||
apply (rule validI_name_pre[OF cs_closed], clarsimp simp del: imp_disjL)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply (rule validI_well_behaved[OF cs_closed])
|
||||
apply (rule validI_strengthen_post)
|
||||
apply (rule_tac s=s and ?s0.0=s0
|
||||
and lockf="\<lambda>s. critical (ab_label s ident)"
|
||||
and I="invs" in cs_wp)
|
||||
apply (clarsimp simp: invs_defs invs_def)
|
||||
apply (clarsimp simp del: imp_disjL)
|
||||
apply (simp only: imp_conjL[symmetric])
|
||||
apply (thin_tac "\<forall>x. P x" for P)
|
||||
apply (clarsimp simp: peterson_rel_def)
|
||||
apply (thin_tac "\<forall>x. P x" for P)
|
||||
apply (clarsimp simp: peterson_rel_def)
|
||||
apply (cases ident; fastforce simp: invs_def key_peterson_inv_def)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma release_lock_mutual_excl:
|
||||
"\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
release_lock ident
|
||||
\<lbrace> peterson_rel ident \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>"
|
||||
apply (simp add: release_lock_def)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply wpsimp+
|
||||
apply (strengthen peterson_rel_imp_assume_invs | simp)+
|
||||
apply (cases ident)
|
||||
apply (safe, simp_all)
|
||||
by ((clarsimp simp: peterson_rel_def set_label_def
|
||||
set_ab_def invs_defs
|
||||
| rule invs_def[THEN iffD2] conjI
|
||||
| rev_drule invs_def[THEN iffD1])+)
|
||||
|
||||
lemma abs_critical_section_mutual_excl:
|
||||
"\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> invs s0
|
||||
\<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
abs_critical_section
|
||||
\<lbrace> peterson_rel ident \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>"
|
||||
apply (simp add: abs_critical_section_def)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply wpsimp+
|
||||
apply (strengthen peterson_rel_imp_assume_invs | simp)+
|
||||
apply (cases ident)
|
||||
apply (safe, simp_all)
|
||||
by ((clarsimp simp: peterson_rel_def invs_defs
|
||||
| rule invs_def[THEN iffD2] conjI
|
||||
| rev_drule invs_def[THEN iffD1])+)
|
||||
|
||||
lemma acquire_lock_mutual_excl:
|
||||
"\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
acquire_lock ident
|
||||
\<lbrace> peterson_rel ident \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> invs s0
|
||||
\<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>"
|
||||
apply (simp add: acquire_lock_def)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply (wpsimp wp: Await_sync_twp)+
|
||||
apply (strengthen peterson_rel_imp_assume_invs | simp)+
|
||||
apply (cases ident)
|
||||
apply (safe, simp_all)
|
||||
by ((clarsimp simp: peterson_rel_def set_label_def set_ab_def
|
||||
locked_def invs_defs
|
||||
| rule invs_def[THEN iffD2] conjI
|
||||
| rev_drule invs_def[THEN iffD1])+)
|
||||
|
||||
theorem abs_peterson_proc_mutual_excl:
|
||||
"\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
abs_peterson_proc ident
|
||||
\<lbrace> peterson_rel ident \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>"
|
||||
apply (simp add: abs_peterson_proc_def bind_assoc)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply (wpsimp wp: release_lock_mutual_excl acquire_lock_mutual_excl
|
||||
abs_critical_section_mutual_excl)+
|
||||
done
|
||||
|
||||
definition
|
||||
peterson_sr :: "(('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool)"
|
||||
where
|
||||
"peterson_sr sa sc \<equiv>
|
||||
t_v sa = t_v sc \<and> ab_v sa = ab_v sc
|
||||
\<and> ab_label sa = ab_label sc \<and> cs2_v sa = cs2_v sc"
|
||||
|
||||
definition
|
||||
peterson_sr' :: "(('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool)"
|
||||
where
|
||||
"peterson_sr' sa sc \<equiv> sa = sc \<lparr> cs1_v := cs1_v sa \<rparr>"
|
||||
|
||||
definition
|
||||
peterson_sr_cs1 :: "(('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool)"
|
||||
where
|
||||
"peterson_sr_cs1 sa sc \<equiv> peterson_sr sa sc \<and> cs1_v sa = cs1_v sc"
|
||||
|
||||
end
|
||||
text {*
|
||||
Finally we assume that we can prove refinement for @{text cs2}, although this
|
||||
may depend on being in a state where @{term cs1_v} has been correctly
|
||||
initialised.
|
||||
*}
|
||||
locale mx_locale_refine = mx_locale_wp cs1 cs2 csI for cs1 :: "'b \<Rightarrow> 'a" and cs2 and csI +
|
||||
assumes
|
||||
cs_refine:
|
||||
"prefix_refinement peterson_sr peterson_sr_cs1 peterson_sr \<top>\<top>
|
||||
(\<lambda>_ s. cs1_v s = cs1 (cs2_v s)) \<top>\<top>
|
||||
(peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
|
||||
cs2 cs2"
|
||||
begin
|
||||
|
||||
lemma
|
||||
"peterson_sr = peterson_sr'"
|
||||
by (auto simp: p_state.splits peterson_sr_def peterson_sr'_def intro!: ext)
|
||||
|
||||
lemma peterson_sr_set_ab[simp]:
|
||||
"peterson_sr s t \<Longrightarrow> peterson_sr (set_ab ident v s) (set_ab ident v t)"
|
||||
by (simp add: peterson_sr_def set_ab_def)
|
||||
|
||||
lemma env_stable_peterson_sr:
|
||||
"env_stable AR R peterson_sr peterson_sr \<top>"
|
||||
by (fastforce simp: env_stable_def rely_stable_def env_rely_stable_iosr_def peterson_sr_def)
|
||||
|
||||
lemmas prefix_refinement_interference_peterson =
|
||||
prefix_refinement_interference[OF env_stable_peterson_sr]
|
||||
|
||||
lemma peterson_sr_reflp[simp]:
|
||||
"reflp peterson_sr"
|
||||
by (simp add: peterson_sr_def reflpI)
|
||||
|
||||
lemma peterson_sr_equivp[simp]:
|
||||
"equivp peterson_sr"
|
||||
by (auto simp: peterson_sr_def intro!: sympI equivpI transpI)
|
||||
|
||||
lemma peterson_sr_cs1_invs: "peterson_sr_cs1 s t \<Longrightarrow> invs s = invs t"
|
||||
apply (auto simp: peterson_sr_def peterson_sr_cs1_def invs_def
|
||||
req_peterson_inv_def key_peterson_inv_def
|
||||
local_peterson_inv_def)[1]
|
||||
done
|
||||
|
||||
lemma env_stable_peterson_sr_cs1:
|
||||
"env_stable (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
|
||||
peterson_sr peterson_sr_cs1 (\<lambda>s. invs s \<and> critical (ab_label s ident))"
|
||||
apply (simp add: env_stable_def rely_stable_def env_rely_stable_iosr_def
|
||||
peterson_rel_def)
|
||||
apply (rule conjI)
|
||||
apply (auto simp: peterson_sr_def peterson_sr_cs1_def)[1]
|
||||
apply (rule conjI)
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: peterson_sr_cs1_invs)
|
||||
apply (auto simp: peterson_sr_cs1_def peterson_sr_def)[1]
|
||||
apply (auto simp: peterson_sr_cs1_def peterson_sr_def)[1]
|
||||
done
|
||||
|
||||
lemmas prefix_refinement_interference_peterson_cs1 =
|
||||
prefix_refinement_interference[OF env_stable_peterson_sr_cs1]
|
||||
|
||||
lemmas prefix_refinement_bind_2left_2right
|
||||
= prefix_refinement_bind[where a="bind a a'" and c="bind c c'" for a a' c c', simplified bind_assoc]
|
||||
lemmas rel_tr_refinement_bind_left_general_2left_2right
|
||||
= rel_tr_refinement_bind_left_general[where f="bind f f'" and g="bind g g'" for f f' g g', simplified bind_assoc]
|
||||
|
||||
lemma peterson_rel_imp_invs:
|
||||
"peterson_rel ident x y \<Longrightarrow> invs x \<Longrightarrow> invs y"
|
||||
by (simp add: peterson_rel_def)
|
||||
|
||||
lemma peterson_rel_imp_label:
|
||||
"peterson_rel (other_ident ident) x y \<Longrightarrow> invs x
|
||||
\<Longrightarrow> ab_label x ident = ab_label y ident"
|
||||
by (simp add: peterson_rel_def)
|
||||
|
||||
lemma peterson_rel_set_label:
|
||||
"peterson_rel (other_ident ident) (set_label ident label s) s'
|
||||
\<Longrightarrow> invs (set_label ident label s)
|
||||
\<Longrightarrow> ab_label s' ident = label"
|
||||
by (simp add: peterson_rel_def set_label_def)
|
||||
|
||||
lemma acquire_lock_refinement:
|
||||
"prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
|
||||
\<top>\<top> \<top>\<top>
|
||||
(peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
|
||||
(acquire_lock ident) (acquire_lock ident)"
|
||||
apply (unfold acquire_lock_def)
|
||||
apply (rule prefix_refinement_weaken_pre)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule prefix_refinement_interference_peterson)
|
||||
apply (simp add: modify_modify_bind)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule pfx_refn_modifyT)
|
||||
apply (clarsimp simp add: peterson_sr_def set_label_def set_ab_def forall_ident_eq)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule prefix_refinement_interference_peterson)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule prefix_refinement_Await[OF env_stable_peterson_sr abs_rely_stableT])
|
||||
apply (clarsimp simp add: peterson_sr_def locked_def)
|
||||
apply (clarsimp simp add: peterson_sr_def locked_def)
|
||||
apply (rule pfx_refn_modifyT)
|
||||
apply (clarsimp simp add: peterson_sr_def set_label_def)
|
||||
apply (wpsimp wp: Await_sync_twp)+
|
||||
done
|
||||
|
||||
lemma peterson_sr_invs[simp]:
|
||||
"peterson_sr as cs \<Longrightarrow> invs as \<Longrightarrow> invs cs"
|
||||
by (simp add: peterson_sr_def invs_def invs_defs)
|
||||
|
||||
lemma peterson_sr_invs_sym:
|
||||
"peterson_sr as cs \<Longrightarrow> invs cs \<Longrightarrow> invs as"
|
||||
by (simp add: peterson_sr_def invs_def invs_defs)
|
||||
|
||||
lemma peterson_sr_ab_label:
|
||||
"peterson_sr as cs \<Longrightarrow> ab_label as = ab_label cs"
|
||||
by (simp add: peterson_sr_def)
|
||||
|
||||
lemma critical_section_refinement:
|
||||
"prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
|
||||
(\<lambda>_ s. invs s \<and> ab_label s ident = Critical) \<top>\<top>
|
||||
(peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
|
||||
abs_critical_section critical_section"
|
||||
apply (simp add: abs_critical_section_def critical_section_def)
|
||||
apply (rule prefix_refinement_weaken_pre)
|
||||
apply (rule prefix_refinement_interferences_split)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule prefix_refinement_interference_peterson)
|
||||
|
||||
(* reorder the interference and modify*)
|
||||
apply (rule pfx_refinement_use_rel_tr_refinement_equivp
|
||||
[where Q="\<lambda>s. invs s \<and> ab_label s (ident) = Critical"])
|
||||
apply (rule rel_tr_refinement_bind_left_general_2left_2right)
|
||||
apply simp
|
||||
apply (rule disjI1,
|
||||
clarsimp simp: not_env_steps_first_all
|
||||
cs_not_env_steps_first release_lock_def)
|
||||
apply (rule rshuttle_modify_interference)
|
||||
apply (simp add: peterson_sr_def peterson_rel_def)
|
||||
apply (clarsimp simp: peterson_rel_def)
|
||||
apply (clarsimp simp: p_state.splits)
|
||||
apply (clarsimp simp: peterson_rel_def invs_def invs_defs)
|
||||
apply simp
|
||||
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule prefix_refinement_interference_peterson)
|
||||
apply (rule prefix_refinement_bind[where intsr=peterson_sr_cs1])
|
||||
apply (rule pfx_refn_modifyT)
|
||||
apply (clarsimp simp add: peterson_sr_def peterson_sr_cs1_def)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule cs_refine)
|
||||
apply (rule prefix_refinement_interference_peterson)
|
||||
|
||||
apply (wpsimp wp: validI_triv[OF cs_closed])+
|
||||
apply (subst peterson_rel_imp_label[symmetric], assumption, simp)
|
||||
apply (drule peterson_rel_imp_invs, simp)
|
||||
apply (simp add: peterson_sr_ab_label)
|
||||
done
|
||||
|
||||
lemma release_lock_refinement:
|
||||
"prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
|
||||
\<top>\<top> \<top>\<top>
|
||||
(peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
|
||||
(release_lock ident) (release_lock ident)"
|
||||
apply (unfold release_lock_def)
|
||||
apply (rule prefix_refinement_weaken_pre)
|
||||
apply (simp add: modify_modify_bind)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule pfx_refn_modifyT)
|
||||
apply (clarsimp simp add: peterson_sr_def peterson_sr_cs1_def set_label_def set_ab_def)
|
||||
apply (rule prefix_refinement_interference_peterson)
|
||||
apply wpsimp+
|
||||
done
|
||||
|
||||
lemma critical_section_prefix_closed[simp]:
|
||||
"prefix_closed critical_section"
|
||||
by (auto intro!: prefix_closed_bind
|
||||
simp: cs_closed critical_section_def)
|
||||
|
||||
lemma abs_critical_section_prefix_closed[simp]:
|
||||
"prefix_closed abs_critical_section"
|
||||
by (auto intro!: prefix_closed_bind
|
||||
simp: cs_closed abs_critical_section_def)
|
||||
|
||||
lemma peterson_rel_trans:
|
||||
"peterson_rel ident x y \<Longrightarrow> peterson_rel ident y z \<Longrightarrow>
|
||||
peterson_rel ident x z"
|
||||
by (clarsimp simp: peterson_rel_def)
|
||||
|
||||
lemma invs_set_label_Critical:
|
||||
"invs s \<Longrightarrow> locked ident s \<Longrightarrow> ab_label s ident = Awaiting
|
||||
\<Longrightarrow> invs (set_label ident Critical s)"
|
||||
by (auto simp: invs_def invs_defs set_label_def locked_def)
|
||||
|
||||
lemma acquire_lock_wp:
|
||||
"\<lbrace> \<lambda>s0 s. invs s \<and> ab_label s ident = Exited \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
acquire_lock ident
|
||||
\<lbrace> \<top>\<top> \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. invs s \<and> ab_label s ident = Critical \<rbrace>"
|
||||
apply (simp add: acquire_lock_def)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply (wpsimp wp: Await_sync_twp)+
|
||||
apply (subst (asm) peterson_rel_imp_label, assumption+)
|
||||
apply (drule(1) peterson_rel_imp_invs)
|
||||
apply (drule(1) peterson_rel_trans)
|
||||
apply (thin_tac "peterson_rel (other_ident ident) s'a x")
|
||||
apply (frule peterson_rel_set_label)
|
||||
apply (fastforce simp: set_label_def set_ab_def
|
||||
locked_def invs_def invs_defs)
|
||||
apply (drule peterson_rel_imp_invs)
|
||||
apply (fastforce simp: set_label_def set_ab_def
|
||||
locked_def invs_def invs_defs)
|
||||
apply (clarsimp simp: invs_set_label_Critical)
|
||||
apply (clarsimp simp: set_label_def set_ab_def)
|
||||
done
|
||||
|
||||
lemma acquire_lock_prefix_closed[simp]:
|
||||
"prefix_closed (acquire_lock ident)"
|
||||
by (auto intro!: prefix_closed_bind
|
||||
simp: cs_closed acquire_lock_def)
|
||||
|
||||
theorem peterson_proc_refinement:
|
||||
"prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
|
||||
(\<lambda>_ s. invs s \<and> ab_label s ident = Exited)
|
||||
(\<lambda>_ s. invs s \<and> ab_label s ident = Exited)
|
||||
(peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
|
||||
(abs_peterson_proc ident)
|
||||
(peterson_proc ident)"
|
||||
apply (simp add: abs_peterson_proc_def peterson_proc_def)
|
||||
apply (rule prefix_refinement_weaken_pre)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule acquire_lock_refinement)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule critical_section_refinement)
|
||||
apply (rule release_lock_refinement)
|
||||
apply (wpsimp wp: validI_triv acquire_lock_wp
|
||||
simp: bipred_conj_def)+
|
||||
done
|
||||
|
||||
definition
|
||||
peterson_rel2 :: "ident \<Rightarrow> ('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"peterson_rel2 ident s_prior s = ((* assume invs *) invs s_prior \<longrightarrow>
|
||||
(* If you're in the critical section, I won't change cs1_v *)
|
||||
(critical (ab_label s_prior (other_ident ident))
|
||||
\<longrightarrow> cs1_v s = cs1_v s_prior))"
|
||||
|
||||
definition
|
||||
peterson_rel3 :: "ident \<Rightarrow> ('a, 'b) p_state \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool"
|
||||
where
|
||||
"peterson_rel3 ident s_prior s = ((* assume invs *) invs s_prior \<longrightarrow>
|
||||
(* invariants are preserved *)
|
||||
(invs s
|
||||
(* I won't adjust your variables *)
|
||||
\<and> (ab_v s (other_ident ident) = ab_v s_prior (other_ident ident))
|
||||
\<and> (ab_label s (other_ident ident) = ab_label s_prior (other_ident ident))
|
||||
(* I will only ever give you priority *)
|
||||
\<and> (t_v s_prior = other_ident ident \<longrightarrow> t_v s = other_ident ident)
|
||||
(* If you're in the critical section, I won't change cs2_v *)
|
||||
\<and> (critical (ab_label s_prior (other_ident ident))
|
||||
\<longrightarrow> cs2_v s = cs2_v s_prior)))"
|
||||
|
||||
lemma peterson_rel_helpers:
|
||||
"peterson_rel2 ident s0 s \<and> peterson_rel3 ident s0 s
|
||||
\<longrightarrow> peterson_rel ident s0 s"
|
||||
by (clarsimp simp: peterson_rel_def peterson_rel2_def peterson_rel3_def)
|
||||
|
||||
lemma peterson_rel_peterson_rel2:
|
||||
"peterson_rel ident s0 s \<longrightarrow> peterson_rel2 ident s0 s"
|
||||
by (clarsimp simp: peterson_rel_def peterson_rel2_def)
|
||||
|
||||
lemma peterson_sr_peterson_rel3:
|
||||
"peterson_sr as0 cs0 \<Longrightarrow> peterson_sr as cs
|
||||
\<Longrightarrow> peterson_rel ident as0 as \<Longrightarrow> peterson_rel3 ident cs0 cs"
|
||||
apply (clarsimp simp: peterson_rel_def peterson_rel3_def invs_def
|
||||
invs_defs peterson_sr_ab_label)
|
||||
apply (clarsimp simp: peterson_sr_def)
|
||||
done
|
||||
|
||||
lemma peterson_proc_prefix_closed[simp]:
|
||||
"prefix_closed (peterson_proc ident)"
|
||||
by (auto intro!: prefix_closed_bind
|
||||
simp: cs_closed peterson_proc_def acquire_lock_def release_lock_def)
|
||||
|
||||
lemma peterson_proc_mutual_excl_helper:
|
||||
"\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
peterson_proc ident
|
||||
\<lbrace> peterson_rel3 ident \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. peterson_rel3 ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>"
|
||||
apply (rule prefix_refinement_validI')
|
||||
apply (rule peterson_proc_refinement)
|
||||
apply (rule abs_peterson_proc_mutual_excl)
|
||||
apply (clarsimp simp: peterson_sr_peterson_rel3 peterson_sr_ab_label)
|
||||
apply (clarsimp simp: peterson_sr_peterson_rel3)
|
||||
apply clarsimp
|
||||
apply (rule_tac x=t0 in exI)
|
||||
apply (rule_tac x="t \<lparr>cs1_v := cs1_v t0\<rparr>" in exI)
|
||||
apply (clarsimp simp: peterson_rel_def peterson_sr_def)
|
||||
apply clarsimp
|
||||
apply (rule_tac x="t \<lparr>cs1_v := cs1_v s0\<rparr>" in exI)
|
||||
apply (clarsimp simp: peterson_rel_def peterson_sr_def invs_def invs_defs)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
lemma peterson_proc_mutual_excl_helper':
|
||||
"\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
peterson_proc ident
|
||||
\<lbrace> peterson_rel2 ident \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. peterson_rel2 ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>"
|
||||
apply (simp add: peterson_proc_def acquire_lock_def release_lock_def
|
||||
critical_section_def)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply (wp Await_sync_twp | simp add: split_def
|
||||
| rule validI_strengthen_guar[OF _ allI[OF allI[OF peterson_rel_peterson_rel2]]])+
|
||||
apply (clarsimp simp: imp_conjL)
|
||||
apply (strengthen peterson_rel_imp_assume_invs | simp)+
|
||||
apply (cases ident)
|
||||
apply (safe, simp_all)
|
||||
by ((clarsimp simp: peterson_rel_def peterson_rel2_def forall_ident_eq
|
||||
set_label_def set_ab_def locked_def invs_defs cs_closed
|
||||
| rule invs_def[THEN iffD2] conjI
|
||||
| rev_drule invs_def[THEN iffD1])+)
|
||||
|
||||
lemma peterson_proc_mutual_excl:
|
||||
"\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>,
|
||||
\<lbrace> peterson_rel (other_ident ident) \<rbrace>
|
||||
peterson_proc ident
|
||||
\<lbrace> peterson_rel ident \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
|
||||
\<and> ab_label s ident = Exited \<rbrace>"
|
||||
apply (rule validI_strengthen_guar, rule validI_strengthen_post, rule validI_guar_post_conj_lift)
|
||||
apply (rule peterson_proc_mutual_excl_helper)
|
||||
apply (rule peterson_proc_mutual_excl_helper')
|
||||
apply (clarsimp simp: peterson_rel_helpers)+
|
||||
done
|
||||
|
||||
definition "abs_peterson_proc_system \<equiv>
|
||||
parallel (do repeat (abs_peterson_proc A); interference od)
|
||||
(do repeat (abs_peterson_proc B); interference od)"
|
||||
|
||||
lemma validI_repeat_interference:
|
||||
"\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
|
||||
\<Longrightarrow> \<forall>s0 s. P s0 s \<longrightarrow> (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s
|
||||
\<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> do repeat f; interference od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>"
|
||||
apply (rule bind_twp)
|
||||
apply simp
|
||||
apply (rule interference_twp)
|
||||
apply (rule validI_strengthen_post)
|
||||
apply (rule repeat_validI, assumption)
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma abs_peterson_proc_system_mutual_excl:
|
||||
"\<lbrace> \<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<rbrace>,
|
||||
\<lbrace> \<lambda>s0 s. s0 = s \<rbrace>
|
||||
abs_peterson_proc_system
|
||||
\<lbrace> \<lambda>s0 s. invs s0 \<longrightarrow> invs s \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. invs s \<rbrace>"
|
||||
apply (rule validI_weaken_pre, rule validI_strengthen_post)
|
||||
apply (unfold abs_peterson_proc_system_def)
|
||||
apply (rule rg_validI[where Qf="\<lambda>_ _. invs" and Qg="\<lambda>_ _. invs"])
|
||||
apply (rule validI_repeat_interference[OF abs_peterson_proc_mutual_excl])
|
||||
apply (clarsimp simp: peterson_rel_imp_invs)
|
||||
apply (rule validI_repeat_interference[OF abs_peterson_proc_mutual_excl])
|
||||
apply (clarsimp simp: peterson_rel_imp_invs)
|
||||
apply (simp add: reflp_ge_eq)+
|
||||
apply (clarsimp simp: peterson_rel_def)+
|
||||
done
|
||||
|
||||
definition "peterson_proc_system \<equiv>
|
||||
parallel (do repeat (peterson_proc A); interference od)
|
||||
(do repeat (peterson_proc B); interference od)"
|
||||
|
||||
lemma abs_peterson_proc_prefix_closed[simp]:
|
||||
"prefix_closed (abs_peterson_proc ident)"
|
||||
by (auto intro!: prefix_closed_bind
|
||||
simp: cs_closed abs_peterson_proc_def acquire_lock_def release_lock_def)
|
||||
|
||||
lemma peterson_repeat_refinement:
|
||||
"prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
|
||||
(\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited)
|
||||
(\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited)
|
||||
(peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
|
||||
(do repeat (abs_peterson_proc ident);
|
||||
interference
|
||||
od)
|
||||
(do repeat (peterson_proc ident);
|
||||
interference
|
||||
od)"
|
||||
apply (rule prefix_refinement_weaken_pre)
|
||||
apply (rule prefix_refinement_bind_sr)
|
||||
apply (rule prefix_refinement_repeat[rotated])
|
||||
apply (rule abs_peterson_proc_mutual_excl[THEN validI_strengthen_guar])
|
||||
apply simp
|
||||
apply (rule peterson_proc_mutual_excl[THEN validI_strengthen_guar, THEN validI_weaken_pre])
|
||||
apply simp+
|
||||
apply (rule peterson_proc_refinement[THEN prefix_refinement_weaken_pre])
|
||||
apply simp+
|
||||
apply (rule prefix_refinement_interference_peterson)
|
||||
apply (wpsimp wp: validI_triv)+
|
||||
done
|
||||
|
||||
theorem peterson_proc_system_refinement:
|
||||
"prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
|
||||
(\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited))
|
||||
(\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited))
|
||||
(\<lambda>s0 s. s0 = s) (\<lambda>t0 t. t0 = t)
|
||||
abs_peterson_proc_system peterson_proc_system"
|
||||
apply (unfold abs_peterson_proc_system_def peterson_proc_system_def)
|
||||
apply (rule prefix_refinement_parallel')
|
||||
apply (rule prefix_refinement_weaken_rely, rule prefix_refinement_weaken_pre)
|
||||
apply (rule peterson_repeat_refinement)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (rule eq_refl, rule bipred_disj_op_eq, simp)
|
||||
apply (rule eq_refl, rule bipred_disj_op_eq, simp)
|
||||
apply (rule prefix_refinement_weaken_rely, rule prefix_refinement_weaken_pre)
|
||||
apply (rule peterson_repeat_refinement)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (rule eq_refl, rule bipred_disj_op_eq, simp)
|
||||
apply (rule eq_refl, rule bipred_disj_op_eq, simp)
|
||||
apply (clarsimp intro!: par_tr_fin_bind par_tr_fin_interference)
|
||||
apply (clarsimp intro!: par_tr_fin_bind par_tr_fin_interference)
|
||||
apply (rule validI_weaken_pre, rule validI_weaken_rely)
|
||||
apply (rule validI_repeat_interference; simp)
|
||||
apply (rule peterson_proc_mutual_excl)
|
||||
apply (simp+)[3]
|
||||
apply (rule validI_weaken_pre, rule validI_weaken_rely)
|
||||
apply (rule validI_repeat_interference; simp)
|
||||
apply (rule peterson_proc_mutual_excl)
|
||||
apply (simp+)[3]
|
||||
apply (rule validI_weaken_pre, rule validI_weaken_rely)
|
||||
apply (rule validI_repeat_interference; simp)
|
||||
apply (rule abs_peterson_proc_mutual_excl)
|
||||
apply (simp+)[3]
|
||||
apply (rule validI_weaken_pre, rule validI_weaken_rely)
|
||||
apply (rule validI_repeat_interference; simp)
|
||||
apply (rule abs_peterson_proc_mutual_excl)
|
||||
apply (simp+)[3]
|
||||
done
|
||||
|
||||
lemma peterson_proc_system_prefix_closed[simp]:
|
||||
"prefix_closed (peterson_proc_system)"
|
||||
by (auto intro!: prefix_closed_bind parallel_prefix_closed
|
||||
simp: cs_closed peterson_proc_system_def)
|
||||
|
||||
theorem peterson_proc_system_mutual_excl:
|
||||
"\<lbrace> \<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited) \<rbrace>,
|
||||
\<lbrace> \<lambda>s0 s. s0 = s \<rbrace>
|
||||
peterson_proc_system
|
||||
\<lbrace> \<lambda>s0 s. invs s0 \<longrightarrow> invs s \<rbrace>,
|
||||
\<lbrace> \<lambda>rv s0 s. invs s \<rbrace>"
|
||||
apply (rule prefix_refinement_validI')
|
||||
apply (rule peterson_proc_system_refinement)
|
||||
apply (rule abs_peterson_proc_system_mutual_excl)
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: peterson_sr_invs_sym )
|
||||
apply (fastforce simp: peterson_rel_def peterson_sr_def)
|
||||
apply clarsimp
|
||||
apply (fastforce simp: peterson_sr_def)
|
||||
done
|
||||
|
||||
end
|
||||
end
|
||||
|
|
@ -0,0 +1,256 @@
|
|||
(*
|
||||
* Copyright 2017, Data61, CSIRO
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(DATA61_BSD)
|
||||
*)
|
||||
theory Plus2_Prefix
|
||||
imports
|
||||
"../Prefix_Refinement"
|
||||
begin
|
||||
|
||||
section {* The plus2 example. *}
|
||||
|
||||
text {*
|
||||
This example presents an application of prefix refinement
|
||||
to solve the plus2 verification problem.
|
||||
|
||||
The function below can be proven to do two increments per
|
||||
instance when grouped in parallel. But RG-reasoning doesn't
|
||||
work well for this proof, since the state change (+1) performed
|
||||
by the counterparts must be allowed by the rely, which must be
|
||||
transitively closed, allowing any number of (+1) operations,
|
||||
which is far too general.
|
||||
|
||||
We address the issue with a ghost variable which records the number
|
||||
of increments by each thread. We use prefix refinement to relate the
|
||||
program with ghost variable to the initial program.
|
||||
*}
|
||||
|
||||
definition
|
||||
"plus2 \<equiv> do env_steps; modify (op + (1 :: nat));
|
||||
interference; modify (op + 1); interference od"
|
||||
|
||||
section {* The ghost-extended program. *}
|
||||
|
||||
record
|
||||
plus2_xstate =
|
||||
mainv :: nat
|
||||
threadv :: "nat \<Rightarrow> nat"
|
||||
|
||||
definition
|
||||
point_update :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> (('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b))"
|
||||
where
|
||||
"point_update x fup f = f (x := fup (f x))"
|
||||
|
||||
definition
|
||||
"plus2_x tid \<equiv> do env_steps;
|
||||
modify (mainv_update (op + 1) o threadv_update (point_update tid (op + 1)));
|
||||
interference;
|
||||
modify (mainv_update (op + 1) o threadv_update (point_update tid (op + 1)));
|
||||
interference
|
||||
od"
|
||||
|
||||
section {* Verifying the extended @{term plus2}. *}
|
||||
text {* The RG-reasoning needed to verify the @{term plus2_x} program. *}
|
||||
definition
|
||||
"plus2_inv tids s = (mainv s = sum (threadv s) tids)"
|
||||
|
||||
definition
|
||||
"plus2_rel tids fix_tids s0 s
|
||||
= ((plus2_inv tids s0 \<longrightarrow> plus2_inv tids s) \<and> (\<forall>tid \<in> fix_tids. threadv s tid = threadv s0 tid))"
|
||||
|
||||
lemma plus2_rel_trans[simp]:
|
||||
"rtranclp (plus2_rel tids ftids) = plus2_rel tids ftids"
|
||||
apply (rule rtranclp_id2)
|
||||
apply (simp add: plus2_rel_def)
|
||||
apply (clarsimp simp: plus2_rel_def)
|
||||
done
|
||||
|
||||
lemma plus2_inv_Suc[simp]:
|
||||
"tid \<in> tids \<Longrightarrow> finite tids
|
||||
\<Longrightarrow> plus2_inv tids (mainv_update Suc (threadv_update (point_update tid Suc) s))
|
||||
= plus2_inv tids s"
|
||||
apply (simp add: plus2_inv_def point_update_def)
|
||||
apply (simp add: sum.If_cases[where h=f and g=f and P="op = tid" and A="tids" for f x, simplified])
|
||||
done
|
||||
|
||||
theorem plus2_x_property:
|
||||
"\<lbrace>\<lambda>s0 s. plus2_inv tids s \<and> threadv s tid = 0 \<and> s = s0 \<and> tid \<in> tids \<and> finite tids\<rbrace>,\<lbrace>plus2_rel tids {tid}\<rbrace>
|
||||
plus2_x tid \<lbrace>plus2_rel tids (- {tid})\<rbrace>,\<lbrace>\<lambda>_ _ s. plus2_inv tids s \<and> threadv s tid = 2\<rbrace>"
|
||||
apply (simp add: plus2_x_def)
|
||||
apply (rule validI_weaken_pre)
|
||||
apply wp
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: plus2_rel_def point_update_def)
|
||||
done
|
||||
|
||||
corollary plus2_x_parallel:
|
||||
"\<lbrace>\<lambda>s0 s. mainv s = 0 \<and> (\<forall>tid \<in> {1, 2}. threadv s tid = 0) \<and> s = s0\<rbrace>,\<lbrace>\<lambda>a b. a = b\<rbrace>
|
||||
parallel (plus2_x 1) (plus2_x 2) \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. mainv s = 4\<rbrace>"
|
||||
apply (rule validI_weaken_pre)
|
||||
apply (rule validI_strengthen_post)
|
||||
apply ((rule rg_validI plus2_x_property[where tids="{1, 2}"])+; simp add: plus2_rel_def le_fun_def)
|
||||
apply (clarsimp simp: plus2_inv_def bipred_conj_def)
|
||||
apply (clarsimp simp add: bipred_conj_def plus2_inv_def)
|
||||
done
|
||||
|
||||
section {* Mapping across prefix refinement. *}
|
||||
text {* Proving prefix refinement of @{term plus2} and @{term plus2_x} and
|
||||
deriving the final result. *}
|
||||
|
||||
lemma env_stable:
|
||||
"env_stable AR R (\<lambda>s t. t = mainv s) (\<lambda>s t. t = mainv s) \<top>"
|
||||
apply (simp add: env_stable_def rely_stable_def env_rely_stable_iosr_def)
|
||||
apply (simp add: plus2_xstate.splits)
|
||||
done
|
||||
|
||||
abbreviation(input)
|
||||
"p_refn rvr P Q AR R \<equiv> prefix_refinement (\<lambda>s t. t = mainv s) (\<lambda>s t. t = mainv s)
|
||||
(\<lambda>s t. t = mainv s) rvr P Q AR R"
|
||||
|
||||
theorem pfx_refn_plus2_x:
|
||||
"p_refn (\<top>\<top>) (op =) (\<top>\<top>) AR R (plus2_x tid) plus2"
|
||||
apply (simp add: plus2_x_def plus2_def)
|
||||
apply (rule prefix_refinement_weaken_pre)
|
||||
apply (rule pfx_refn_bind prefix_refinement_interference
|
||||
prefix_refinement_env_steps allI
|
||||
pfx_refn_modifyT env_stable
|
||||
| simp
|
||||
| wp)+
|
||||
done
|
||||
|
||||
lemma par_tr_fin_plus2_x:
|
||||
"par_tr_fin_principle (plus2_x tid)"
|
||||
by (simp add: plus2_x_def par_tr_fin_interference par_tr_fin_bind)
|
||||
|
||||
lemma prefix_closed_plus2:
|
||||
"prefix_closed plus2"
|
||||
apply (simp add: plus2_def)
|
||||
apply (rule validI_prefix_closed_T, rule validI_weaken_pre, wp)
|
||||
apply simp
|
||||
done
|
||||
|
||||
theorem plus2_parallel:
|
||||
"\<lbrace>\<lambda>s0 s. s = 0 \<and> s = s0\<rbrace>,\<lbrace>\<lambda>a b. a = b\<rbrace>
|
||||
parallel plus2 plus2 \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. s = 4\<rbrace>"
|
||||
apply (rule_tac sr="\<lambda>s t. t = mainv s" in prefix_refinement_validI)
|
||||
apply (rule prefix_refinement_parallel_triv;
|
||||
((rule par_tr_fin_plus2_x prefix_closed_plus2)?))
|
||||
apply (rule pfx_refn_plus2_x[where tid=1])
|
||||
apply (rule pfx_refn_plus2_x[where tid=2])
|
||||
apply clarsimp
|
||||
apply (rule validI_strengthen_post)
|
||||
apply (rule plus2_x_parallel[simplified])
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: plus2_xstate.splits)
|
||||
apply (strengthen exI[where x="f(1 := x, 2 := y)" for f x y])
|
||||
apply simp
|
||||
apply clarsimp
|
||||
apply (intro parallel_prefix_closed prefix_closed_plus2)
|
||||
done
|
||||
|
||||
section {* Generalising *}
|
||||
text {* Just for fun, generalise to arbitrarily many
|
||||
copies of the @{term plus2} program. *}
|
||||
|
||||
lemma plus2_x_n_parallel_induct:
|
||||
"n > 0 \<Longrightarrow> n \<le> N \<Longrightarrow>
|
||||
\<lbrace>\<lambda>s0 s. plus2_inv {..< N} s \<and> (\<forall>i < N. threadv s i = 0) \<and> s = s0\<rbrace>,\<lbrace>plus2_rel {..< N} {..< n}\<rbrace>
|
||||
fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) \<lbrace>plus2_rel {..< N} ( - {..< n})\<rbrace>,\<lbrace>\<lambda>_ _ s.
|
||||
plus2_inv {..< N} s \<and> (\<forall>i < n. threadv s i = 2)\<rbrace>"
|
||||
apply (induct n)
|
||||
apply simp
|
||||
apply (case_tac n)
|
||||
apply (simp only: lessThan_Suc)
|
||||
apply simp
|
||||
apply (rule validI_weaken_pre, rule plus2_x_property)
|
||||
apply clarsimp
|
||||
apply (clarsimp split del: if_split)
|
||||
apply (rule validI_weaken_pre, rule validI_strengthen_post,
|
||||
rule rg_validI, rule plus2_x_property[where tids="{..< N}"],
|
||||
assumption, (clarsimp simp: plus2_rel_def)+)
|
||||
apply (auto dest: less_Suc_eq[THEN iffD1])[1]
|
||||
apply (clarsimp simp: bipred_conj_def)
|
||||
done
|
||||
|
||||
theorem plus2_x_n_parallel:
|
||||
"n > 0 \<Longrightarrow>
|
||||
\<lbrace>\<lambda>s0 s. mainv s = 0 \<and> (\<forall>i < n. threadv s i = 0) \<and> s = s0\<rbrace>,\<lbrace>plus2_rel {..< n} {..< n}\<rbrace>
|
||||
fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ _ s. mainv s = (n * 2)\<rbrace>"
|
||||
apply (rule validI_weaken_pre, rule validI_strengthen_post,
|
||||
rule validI_strengthen_guar, erule plus2_x_n_parallel_induct)
|
||||
apply simp
|
||||
apply simp
|
||||
apply (clarsimp simp: plus2_inv_def)
|
||||
apply (clarsimp simp: plus2_inv_def)
|
||||
done
|
||||
|
||||
lemma par_tr_fin_principle_parallel:
|
||||
"par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle g
|
||||
\<Longrightarrow> par_tr_fin_principle (parallel f g)"
|
||||
apply (subst par_tr_fin_principle_def, clarsimp simp: parallel_def3)
|
||||
apply (drule(1) par_tr_fin_principleD)+
|
||||
apply (clarsimp simp: neq_Nil_conv)
|
||||
done
|
||||
|
||||
lemma fold_parallel_par_tr_fin_principle[where xs="rev xs" for xs, simplified]:
|
||||
"\<forall>x \<in> insert x (set xs). par_tr_fin_principle x
|
||||
\<Longrightarrow> par_tr_fin_principle (fold parallel (rev xs) x)"
|
||||
by (induct xs, simp_all add: par_tr_fin_principle_parallel)
|
||||
|
||||
lemma fold_parallel_prefix_closed[where xs="rev xs" for xs, simplified]:
|
||||
"\<forall>x \<in> insert x (set xs). prefix_closed x
|
||||
\<Longrightarrow> prefix_closed (fold parallel (rev xs) x)"
|
||||
by (induct xs, simp_all add: parallel_prefix_closed)
|
||||
|
||||
lemma bipred_disj_top_eq:
|
||||
"(Rel Or (\<lambda>_ _. True)) = (\<lambda>_ _. True)"
|
||||
"((\<lambda>_ _. True) Or Rel) = (\<lambda>_ _. True)"
|
||||
by (auto simp add: bipred_disj_def)
|
||||
|
||||
lemma fold_parallel_pfx_refn_induct:
|
||||
"list_all2 (prefix_refinement sr sr sr (\<lambda>_ _. True) P Q (\<top>\<top>) (\<top>\<top>)) xs ys
|
||||
\<Longrightarrow> prefix_refinement sr sr sr (\<lambda>_ _. True) P Q (\<top>\<top>) (\<top>\<top>) x y
|
||||
\<Longrightarrow> \<forall>x \<in> set (x # xs). par_tr_fin_principle x
|
||||
\<Longrightarrow> \<forall>y \<in> set (y # ys). prefix_closed y
|
||||
\<Longrightarrow> prefix_refinement sr sr sr (\<lambda>_ _. True) P Q (\<top>\<top>) (\<top>\<top>)
|
||||
(fold parallel (rev xs) x) (fold parallel (rev ys) y)"
|
||||
apply (induct rule: list_all2_induct; simp)
|
||||
apply (rule prefix_refinement_parallel_triv[simplified bipred_disj_top_eq]; simp?)
|
||||
apply (clarsimp simp: fold_parallel_par_tr_fin_principle
|
||||
fold_parallel_prefix_closed)+
|
||||
done
|
||||
|
||||
lemmas fold_parallel_pfx_refn
|
||||
= fold_parallel_pfx_refn_induct[where xs="rev xs" and ys="rev ys" for xs ys, simplified]
|
||||
|
||||
theorem plus2_n_parallel:
|
||||
"n > 0
|
||||
\<Longrightarrow> \<lbrace>\<lambda>s0 s. s = 0 \<and> s = s0\<rbrace>,\<lbrace>\<lambda>a b. a = b\<rbrace>
|
||||
fold parallel (replicate (n - 1) plus2) plus2 \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. s = n * 2\<rbrace>"
|
||||
apply (rule_tac sr="\<lambda>s t. t = mainv s" in prefix_refinement_validI)
|
||||
apply (rule prefix_refinement_weaken_rely,
|
||||
rule_tac xs="map plus2_x [1 ..< n]" in fold_parallel_pfx_refn)
|
||||
apply (clarsimp simp: list_all2_conv_all_nth)
|
||||
apply (rule pfx_refn_plus2_x)
|
||||
apply (rule pfx_refn_plus2_x[where tid=0])
|
||||
apply (simp add: par_tr_fin_plus2_x)
|
||||
apply (simp add: prefix_closed_plus2)
|
||||
apply (simp add: le_fun_def)
|
||||
apply (simp add: le_fun_def)
|
||||
apply simp
|
||||
apply (rule validI_strengthen_post, rule plus2_x_n_parallel[simplified], simp)
|
||||
apply clarsimp
|
||||
apply (clarsimp simp: plus2_xstate.splits exI[where x="\<lambda>_. 0"])
|
||||
apply clarsimp
|
||||
apply (rule exI, strengthen refl)
|
||||
apply (clarsimp simp: plus2_rel_def plus2_inv_def)
|
||||
apply (rule fold_parallel_prefix_closed)
|
||||
apply (simp add: prefix_closed_plus2)
|
||||
done
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue