2582 lines
125 KiB
Plaintext
2582 lines
125 KiB
Plaintext
(*
|
|
* Copyright 2014, NICTA
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
*
|
|
* @TAG(NICTA_GPL)
|
|
*)
|
|
|
|
theory Scheduler_IF
|
|
imports "Syscall_IF" "PasUpdates"
|
|
|
|
begin
|
|
|
|
|
|
crunch cur_thread: activate_thread "\<lambda>s. P (cur_thread s)"
|
|
crunch cur_thread: arch_switch_to_thread "\<lambda>s. P( cur_thread s)"
|
|
|
|
|
|
abbreviation scheduler_affects_globals_frame where
|
|
"scheduler_affects_globals_frame s \<equiv> ptr_range (arm_globals_frame (arch_state s)) 2"
|
|
|
|
definition globals_equiv_scheduler :: "'z::state_ext state \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
|
|
"globals_equiv_scheduler s s' \<equiv> arm_globals_frame (arch_state s) = arm_globals_frame (arch_state s') \<and>
|
|
arm_global_pd (arch_state s) = arm_global_pd (arch_state s') \<and>
|
|
(\<forall>x\<in>range_of_arm_globals_frame s - scheduler_affects_globals_frame s. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x) \<and>
|
|
kheap s (arm_global_pd (arch_state s)) = kheap s' (arm_global_pd (arch_state s))
|
|
\<and> idle_equiv s s'"
|
|
|
|
definition scheduler_globals_frame_equiv :: "'z::state_ext state \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" where
|
|
"scheduler_globals_frame_equiv s s' \<equiv> arm_globals_frame (arch_state s) = arm_globals_frame (arch_state s') \<and> (\<forall>x\<in>scheduler_affects_globals_frame s. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x)"
|
|
|
|
definition domain_fields_equiv :: "det_ext state \<Rightarrow> det_ext state \<Rightarrow> bool"
|
|
where
|
|
"domain_fields_equiv s s' \<equiv> cur_domain s = cur_domain s' \<and>
|
|
domain_time s = domain_time s' \<and>
|
|
domain_index s = domain_index s' \<and>
|
|
domain_list s = domain_list s'"
|
|
|
|
|
|
definition scheduler_equiv :: "'a subject_label PAS \<Rightarrow> det_ext state \<Rightarrow> det_ext state \<Rightarrow> bool"
|
|
where
|
|
"scheduler_equiv aag s s' \<equiv>
|
|
domain_fields_equiv s s' \<and> idle_thread s = idle_thread s' \<and> globals_equiv_scheduler s s' \<and> silc_dom_equiv aag s s' \<and> irq_state_of_state s = irq_state_of_state s'"
|
|
|
|
(* The equivalence relation for what the scheduler can affect.
|
|
Since information can flow from the scheduler to any domain,
|
|
we assert that the result states are equivalent with respect
|
|
to any domain.
|
|
|
|
*)
|
|
|
|
|
|
|
|
definition reads_scheduler where
|
|
"reads_scheduler aag l \<equiv> if (l = SilcLabel) then {} else
|
|
subjectReads (pasPolicy aag) l"
|
|
|
|
definition scheduler_affects_equiv :: "'a subject_label PAS \<Rightarrow> ('a subject_label) \<Rightarrow> det_state \<Rightarrow> det_state \<Rightarrow> bool"
|
|
where
|
|
"scheduler_affects_equiv aag l s s' \<equiv>
|
|
(states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasDomainAbs aag x \<in> reads_scheduler aag l) (\<lambda> x. ptr_range x 12) s s' \<and>
|
|
((pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l \<or>
|
|
pasDomainAbs aag (cur_domain s')\<in> reads_scheduler aag l) \<longrightarrow>
|
|
(cur_thread s = cur_thread s' \<and> scheduler_action s = scheduler_action s' \<and>
|
|
work_units_completed s = work_units_completed s' \<and>
|
|
scheduler_globals_frame_equiv s s' \<and>
|
|
idle_thread s = idle_thread s' \<and>
|
|
(cur_thread s \<noteq> idle_thread s' \<longrightarrow> exclusive_state_equiv s s'))))"
|
|
|
|
lemma ev_modify: "(\<And> s t. \<lbrakk>P s; P t; A s t; I s t\<rbrakk> \<Longrightarrow> (I (f s) (f t)) \<and> (B (f s) (f t))) \<Longrightarrow> equiv_valid I A B P (modify f)"
|
|
apply (clarsimp simp add: equiv_valid_def2 equiv_valid_2_def simpler_modify_def)
|
|
done
|
|
|
|
abbreviation reads_respects_scheduler
|
|
where
|
|
"reads_respects_scheduler aag l P f \<equiv>
|
|
equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) P f"
|
|
|
|
lemma globals_equiv_from_scheduler:
|
|
"\<lbrakk> globals_equiv_scheduler s s'; scheduler_globals_frame_equiv s s'; cur_thread s = cur_thread s'; cur_thread s \<noteq> idle_thread s \<longrightarrow> exclusive_state_equiv s s'\<rbrakk> \<Longrightarrow>
|
|
globals_equiv s s'"
|
|
apply (clarsimp simp add: globals_equiv_scheduler_def scheduler_globals_frame_equiv_def globals_equiv_def)
|
|
apply blast
|
|
done
|
|
|
|
lemma globals_equiv_scheduler_refl:
|
|
"globals_equiv_scheduler s s"
|
|
by (simp add: globals_equiv_scheduler_def idle_equiv_refl)
|
|
|
|
lemma globals_equiv_scheduler_sym:
|
|
"globals_equiv_scheduler s s' \<Longrightarrow> globals_equiv_scheduler s' s"
|
|
by (auto simp add: globals_equiv_scheduler_def idle_equiv_sym)
|
|
|
|
lemma globals_equiv_scheduler_trans:
|
|
"globals_equiv_scheduler s s' \<Longrightarrow> globals_equiv_scheduler s' s'' \<Longrightarrow> globals_equiv_scheduler s s''"
|
|
apply (clarsimp simp add: globals_equiv_scheduler_def)
|
|
apply (rule idle_equiv_trans,assumption,assumption)
|
|
done
|
|
|
|
|
|
lemma scheduler_globals_frame_equiv_refl:
|
|
"scheduler_globals_frame_equiv s s"
|
|
by (simp add: scheduler_globals_frame_equiv_def)
|
|
|
|
lemma scheduler_globals_frame_equiv_sym[elim]:
|
|
"scheduler_globals_frame_equiv s s' \<Longrightarrow> scheduler_globals_frame_equiv s' s"
|
|
by (simp add: scheduler_globals_frame_equiv_def)
|
|
|
|
lemma scheduler_globals_frame_equiv_trans[elim]:
|
|
"scheduler_globals_frame_equiv s s' \<Longrightarrow> scheduler_globals_frame_equiv s' s'' \<Longrightarrow> scheduler_globals_frame_equiv s s''"
|
|
by (simp add: scheduler_globals_frame_equiv_def)
|
|
|
|
lemma preserves_equivalence_2_weak:
|
|
assumes A: "(u,b) \<in> fst (f s)"
|
|
assumes B: "(u',ba) \<in> fst (g t)"
|
|
assumes R_preserved: "\<And>st. \<lbrace>P and (R st)\<rbrace> f \<lbrace>\<lambda>_.(R st)\<rbrace>"
|
|
assumes R_preserved': "\<And>st. \<lbrace>S and (R st)\<rbrace> g \<lbrace>\<lambda>_.(R st)\<rbrace>"
|
|
assumes R_sym: "\<forall>s s'. R s s' \<longrightarrow> R s' s"
|
|
assumes R_trans: "\<forall>s s' s''. R s s' \<longrightarrow> R s' s'' \<longrightarrow> R s s''"
|
|
shows "\<lbrakk> R s t;P s; S t\<rbrakk> \<Longrightarrow> R b ba"
|
|
apply (insert A B)
|
|
apply (drule use_valid[OF _ R_preserved])
|
|
apply simp
|
|
apply (rule R_sym[rule_format])
|
|
apply assumption
|
|
apply (drule use_valid[OF _ R_preserved'])
|
|
apply simp
|
|
apply (metis R_trans R_sym)
|
|
done
|
|
|
|
lemma preserves_equivalence_weak:
|
|
assumes A: "(u,b) \<in> fst (f s)"
|
|
assumes B: "(u',ba) \<in> fst (f t)"
|
|
assumes R_preserved: "\<And>st. \<lbrace>P and (R st)\<rbrace> f \<lbrace>\<lambda>_.(R st)\<rbrace>"
|
|
assumes R_sym: "\<forall>s s'. R s s' \<longrightarrow> R s' s"
|
|
assumes R_trans: "\<forall>s s' s''. R s s' \<longrightarrow> R s' s'' \<longrightarrow> R s s''"
|
|
shows "\<lbrakk> R s t;P s; P t\<rbrakk> \<Longrightarrow> R b ba"
|
|
using assms
|
|
apply (blast intro: preserves_equivalence_2_weak)
|
|
done
|
|
|
|
|
|
|
|
lemma scheduler_equiv_trans[elim]:
|
|
"scheduler_equiv aag s s' \<Longrightarrow> scheduler_equiv aag s' s'' \<Longrightarrow> scheduler_equiv aag s s''"
|
|
apply (simp add: scheduler_equiv_def domain_fields_equiv_def)
|
|
apply clarify
|
|
apply (rule conjI)
|
|
apply (rule globals_equiv_scheduler_trans)
|
|
apply simp+
|
|
apply(blast intro: silc_dom_equiv_trans)
|
|
done
|
|
|
|
|
|
|
|
lemma scheduler_equiv_sym[elim]:
|
|
"scheduler_equiv aag s s' \<Longrightarrow> scheduler_equiv aag s' s"
|
|
by (simp add: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_sym silc_dom_equiv_sym)
|
|
|
|
lemma scheduler_affects_equiv_trans[elim]:
|
|
"\<lbrakk>scheduler_affects_equiv aag l s s'; scheduler_equiv aag s s'; scheduler_affects_equiv aag l s' s''; scheduler_equiv aag s' s''\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l s s''"
|
|
apply (simp add: scheduler_affects_equiv_def scheduler_equiv_trans[where s'=s'])+
|
|
apply clarify
|
|
apply (rule conjI)
|
|
apply (rule states_equiv_for_trans[where t=s'])
|
|
apply simp+
|
|
apply (rule conjI)
|
|
apply clarsimp
|
|
apply (rule conjI)
|
|
apply (clarsimp simp add: scheduler_globals_frame_equiv_trans[where s'=s'] scheduler_equiv_def
|
|
domain_fields_equiv_def)+
|
|
(*apply (blast intro: silc_dom_equiv_trans)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)
|
|
apply (rule conjI)
|
|
apply (rule scheduler_globals_frame_equiv_trans[where s'=s'])
|
|
apply (auto intro: silc_dom_equiv_trans)*)
|
|
done
|
|
|
|
lemma scheduler_affects_equiv_sym[elim]:
|
|
"scheduler_affects_equiv aag l s s' \<Longrightarrow> scheduler_affects_equiv aag l s' s"
|
|
apply (simp add: scheduler_affects_equiv_def)
|
|
apply (auto simp: scheduler_globals_frame_equiv_sym states_equiv_for_sym silc_dom_equiv_sym)
|
|
done
|
|
|
|
declare globals_equiv_scheduler_sym[elim]
|
|
declare globals_equiv_scheduler_trans[elim]
|
|
declare scheduler_affects_equiv_sym[elim]
|
|
declare scheduler_affects_equiv_trans[elim]
|
|
declare silc_dom_equiv_sym[elim]
|
|
declare silc_dom_equiv_trans[elim]
|
|
|
|
lemma scheduler_equiv_lift':
|
|
assumes s: "\<And>st. \<lbrace>P and globals_equiv_scheduler st\<rbrace> f \<lbrace>\<lambda>_.(globals_equiv_scheduler st)\<rbrace>"
|
|
assumes d: "\<And>Q. \<lbrace>P and (\<lambda>s. Q (cur_domain s))\<rbrace> f \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>"
|
|
assumes i: "\<And>P. invariant f (\<lambda>s. P (idle_thread s))"
|
|
assumes e: "\<And>Q. \<lbrace>P and domain_fields Q\<rbrace> f \<lbrace>\<lambda>_. domain_fields Q\<rbrace>"
|
|
assumes g: "\<And>P. invariant f (\<lambda>s. P (irq_state_of_state s))"
|
|
assumes f: "\<And>st. \<lbrace>P and silc_dom_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>"
|
|
shows "\<lbrace>P and scheduler_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>"
|
|
apply (simp add: scheduler_equiv_def[abs_def] domain_fields_equiv_def)
|
|
apply (rule hoare_pre)
|
|
apply (wp d e s i f g)
|
|
apply simp
|
|
done
|
|
|
|
lemmas scheduler_equiv_lift = scheduler_equiv_lift'[where P=\<top>,simplified]
|
|
|
|
lemma equiv_valid_inv_unobservable:
|
|
assumes f: "\<And>st. \<lbrace>P and I st and A st\<rbrace> f \<lbrace>\<lambda>_. I st\<rbrace>"
|
|
assumes g: "\<And>st. \<lbrace>P' and I st and A st\<rbrace> f \<lbrace>\<lambda>_. A st\<rbrace>"
|
|
assumes sym: "\<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s"
|
|
assumes trans: "\<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''"
|
|
assumes s: "\<And>s. Q s \<Longrightarrow> P s \<and> P' s"
|
|
shows "equiv_valid_inv I A Q (f:: 'a \<Rightarrow> (unit \<times> 'a) set \<times> bool)"
|
|
apply (clarsimp simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)
|
|
apply (erule preserves_equivalence_weak,assumption)
|
|
apply (rule hoare_pre)
|
|
apply (rule hoare_vcg_conj_lift)
|
|
apply (rule f)
|
|
apply (rule g)
|
|
apply force
|
|
apply (insert s)
|
|
apply (fastforce intro!: sym trans)+
|
|
done
|
|
|
|
lemma reads_respects_scheduler_unobservable'':
|
|
"\<lbrakk>\<And>st. \<lbrace>P and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> f
|
|
\<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>;
|
|
\<And>st. \<lbrace>P' and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> f
|
|
\<lbrace>\<lambda>(_ :: unit). scheduler_affects_equiv aag l st\<rbrace>;
|
|
\<And>s. Q s \<Longrightarrow> P s \<and> P' s\<rbrakk>
|
|
\<Longrightarrow> reads_respects_scheduler aag l Q f"
|
|
apply (rule equiv_valid_inv_unobservable,fastforce+)
|
|
done
|
|
|
|
lemma reads_respects_scheduler_unobservable':
|
|
assumes f: "\<And>st. \<lbrace>P and scheduler_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>"
|
|
assumes g: "\<And>st. \<lbrace>P and scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
shows "reads_respects_scheduler aag l P (f:: (unit,det_ext) s_monad)"
|
|
apply (rule reads_respects_scheduler_unobservable'')
|
|
apply (wp f g | force)+
|
|
done
|
|
|
|
definition swap_things where
|
|
"swap_things s t \<equiv> t\<lparr> machine_state := underlying_memory_update
|
|
(\<lambda>m a. if a \<in> scheduler_affects_globals_frame t
|
|
then (underlying_memory (machine_state s) a)
|
|
else m a) (machine_state t)
|
|
\<lparr>exclusive_state := exclusive_state (machine_state s)\<rparr>\<rparr>
|
|
\<lparr>cur_thread := cur_thread s\<rparr>"
|
|
|
|
definition swap_things' where
|
|
"swap_things' s t \<equiv> t\<lparr> machine_state := underlying_memory_update
|
|
(\<lambda>m a. if a \<notin> scheduler_affects_globals_frame t
|
|
then (underlying_memory (machine_state s) a)
|
|
else m a) (machine_state t)
|
|
\<lparr> exclusive_state := exclusive_state (machine_state t)\<rparr>\<rparr>
|
|
\<lparr>arch_state := (arm_globals_frame_update (\<lambda>_. arm_globals_frame (arch_state s)) (arch_state t))
|
|
\<lparr> arm_global_pd := arm_global_pd (arch_state s)\<rparr>\<rparr>
|
|
\<lparr>kheap := \<lambda>x. if x = (arm_global_pd (arch_state s)) then kheap s x else kheap t x\<rparr>
|
|
\<lparr>cur_thread := cur_thread s\<rparr>"
|
|
|
|
lemma idle_equiv_machine_state_update[simp]: "idle_equiv st (s\<lparr>machine_state := x\<rparr>) = idle_equiv st s"
|
|
apply (simp add: idle_equiv_def)
|
|
done
|
|
|
|
lemma idle_equiv_machine_state_update'[simp]: "idle_equiv (st\<lparr>machine_state := x\<rparr>) s = idle_equiv st s"
|
|
apply (simp add: idle_equiv_def)
|
|
done
|
|
|
|
lemma idle_equiv_cur_thread_update'[simp]: "idle_equiv (st\<lparr>cur_thread := x\<rparr>) s = idle_equiv st s"
|
|
apply (simp add: idle_equiv_def)
|
|
done
|
|
|
|
lemma globals_equiv_scheduler_inv':
|
|
"(\<And>st. \<lbrace> P and globals_equiv st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv st\<rbrace>) \<Longrightarrow>
|
|
\<lbrace> P and globals_equiv_scheduler s\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler s\<rbrace>"
|
|
apply atomize
|
|
apply (rule use_spec)
|
|
apply (simp add: spec_valid_def)
|
|
apply (erule_tac x="(swap_things sa s)" in allE)
|
|
apply (rule_tac Q="\<lambda>r st. globals_equiv (swap_things sa s) st" in hoare_strengthen_post )
|
|
apply (rule hoare_pre)
|
|
apply assumption
|
|
apply (clarsimp simp add: globals_equiv_def swap_things_def globals_equiv_scheduler_def)+
|
|
apply(fastforce)
|
|
done
|
|
|
|
lemmas globals_equiv_scheduler_inv = globals_equiv_scheduler_inv'[where P="\<top>",simplified]
|
|
|
|
lemmas reads_respects_scheduler_unobservable = reads_respects_scheduler_unobservable'[where P="\<top>",simplified]
|
|
|
|
crunch globals_equiv[wp]: set_scheduler_action "globals_equiv st"
|
|
|
|
lemma silc_dom_equiv_scheduler_action_update[simp]: "silc_dom_equiv aag st (s\<lparr>scheduler_action := x\<rparr>) = silc_dom_equiv aag st s"
|
|
apply (simp add: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
crunch silc_dom_equiv[wp]: set_scheduler_action "silc_dom_equiv aag st"
|
|
|
|
lemma schedule_globals_frame_trans_state_upd[simp]: "scheduler_globals_frame_equiv st (trans_state f s) = scheduler_globals_frame_equiv st s"
|
|
apply (simp add: scheduler_globals_frame_equiv_def)
|
|
done
|
|
|
|
lemma idle_equiv_scheduler_action_update[simp]: "idle_equiv (scheduler_action_update f st) s = idle_equiv st s"
|
|
apply (simp add: idle_equiv_def)
|
|
done
|
|
|
|
lemma idle_equiv_scheduler_action_update'[simp]: "idle_equiv st (scheduler_action_update f s) = idle_equiv st s"
|
|
apply (simp add: idle_equiv_def)
|
|
done
|
|
|
|
lemma set_scheduler_action_rev_scheduler[wp]: "reads_respects_scheduler aag l \<top> (set_scheduler_action a)"
|
|
apply (clarsimp simp add: set_scheduler_action_def)
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def
|
|
scheduler_equiv_def states_equiv_for_def
|
|
equiv_asids_def equiv_asid_def
|
|
domain_fields_equiv_def
|
|
globals_equiv_scheduler_def
|
|
silc_dom_equiv_def
|
|
scheduler_globals_frame_equiv_def
|
|
equiv_for_def)
|
|
done
|
|
|
|
lemma globals_equiv_scheduler_cur_thread_update[simp]: "globals_equiv_scheduler st (s\<lparr>cur_thread := x\<rparr>) = globals_equiv_scheduler st s"
|
|
by (simp add: globals_equiv_scheduler_def idle_equiv_def)
|
|
|
|
lemma globals_equiv_scheduler_trans_state_update[simp]: "globals_equiv_scheduler st (trans_state f s) = globals_equiv_scheduler st s"
|
|
by (simp add: globals_equiv_scheduler_def idle_equiv_def)
|
|
|
|
lemma states_equiv_for_cur_thread_update[simp]: "states_equiv_for P Q R S X s (s'\<lparr>cur_thread := x\<rparr>) = states_equiv_for P Q R S X s s'"
|
|
apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def)
|
|
done
|
|
|
|
lemma scheduler_globals_frame_equiv_cur_thread_update[simp]: "scheduler_globals_frame_equiv st (s\<lparr>cur_thread := x\<rparr>) = scheduler_globals_frame_equiv st s"
|
|
apply (simp add: scheduler_globals_frame_equiv_def)
|
|
done
|
|
|
|
lemma scheduler_globals_frame_equiv_ready_queues_update[simp]: "scheduler_globals_frame_equiv st (s\<lparr>ready_queues := x\<rparr>) = scheduler_globals_frame_equiv st s"
|
|
apply (simp add: scheduler_globals_frame_equiv_def)
|
|
done
|
|
|
|
lemma scheduler_globals_frame_equiv_ready_queues_update'[simp]: "scheduler_globals_frame_equiv (st\<lparr>ready_queues := x\<rparr>) s = scheduler_globals_frame_equiv st s"
|
|
apply (simp add: scheduler_globals_frame_equiv_def)
|
|
done
|
|
|
|
lemma silc_dom_equiv_cur_thread_update[simp]: "silc_dom_equiv aag st (s\<lparr>cur_thread := x\<rparr>) = silc_dom_equiv aag st s"
|
|
apply (simp add: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
lemma silc_dom_equiv_ready_queues_update[simp]: "silc_dom_equiv aag st (s\<lparr>ready_queues := x\<rparr>) = silc_dom_equiv aag st s"
|
|
apply (simp add: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
lemma silc_dom_equiv_ready_queues_update'[simp]: "silc_dom_equiv aag (st\<lparr>ready_queues := x\<rparr>) s = silc_dom_equiv aag st s"
|
|
apply (simp add: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
lemma silc_dom_equiv_cur_thread_update'[simp]: "silc_dom_equiv aag (st\<lparr>cur_thread := x\<rparr>) s = silc_dom_equiv aag st s"
|
|
apply (simp add: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
|
|
lemma scheduler_equiv_ready_queues_update[simp]: "scheduler_equiv aag (st\<lparr>ready_queues := x\<rparr>) s = scheduler_equiv aag st s"
|
|
apply (simp add: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def
|
|
idle_equiv_def)
|
|
done
|
|
|
|
lemma scheduler_equiv_ready_queues_update'[simp]: "scheduler_equiv aag st (s\<lparr>ready_queues := x\<rparr>) = scheduler_equiv aag st s"
|
|
apply (simp add: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def
|
|
idle_equiv_def)
|
|
done
|
|
|
|
|
|
lemma get_tcb_queue_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l (K(pasDomainAbs aag rv \<in> reads_scheduler aag l)) (get_tcb_queue rv rva)"
|
|
apply (rule gen_asm_ev)
|
|
apply (simp add: get_tcb_queue_def)
|
|
apply (subst gets_apply)
|
|
apply (wp gets_apply_ev)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def)
|
|
done
|
|
|
|
lemma ethread_get_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l (K(pasObjectAbs aag t \<in> reads_scheduler aag l)) (ethread_get f t)"
|
|
apply (rule gen_asm_ev)
|
|
apply (simp add: ethread_get_def)
|
|
apply wp
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def get_etcb_def)
|
|
done
|
|
|
|
|
|
lemma (in is_extended') globals_equiv[wp]: "I (globals_equiv st)" by (rule lift_inv,simp)
|
|
|
|
lemma (in is_extended') globals_equiv_scheduler[wp]: "I (globals_equiv_scheduler st)" by (rule lift_inv,simp)
|
|
|
|
|
|
lemma tcb_domain_wellformed: "pas_refined aag s \<Longrightarrow> ekheap s t = Some a \<Longrightarrow> pasObjectAbs aag t = pasDomainAbs aag (tcb_domain a)"
|
|
apply (clarsimp simp add: pas_refined_def tcb_domain_map_wellformed_aux_def)
|
|
apply (drule_tac x="(t,tcb_domain a)" in bspec)
|
|
apply (rule domtcbs)
|
|
apply force+
|
|
done
|
|
|
|
lemma reads_respects_scheduler_cases:
|
|
assumes b: "pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> reads_respects_scheduler aag l P' (f t)"
|
|
assumes b': "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> P' s"
|
|
assumes c: "pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> reads_respects_scheduler aag l P'' (f t)"
|
|
assumes c': "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> P'' s"
|
|
shows "reads_respects_scheduler aag l Q (f t)"
|
|
apply (insert b b' c c')
|
|
apply (case_tac "pasObjectAbs aag t \<in> reads_scheduler aag l")
|
|
apply (fastforce intro: equiv_valid_guard_imp)+
|
|
done
|
|
|
|
|
|
lemma silc_dom_equiv_trans_state[simp]: "silc_dom_equiv aag st (trans_state f s) = silc_dom_equiv aag st s"
|
|
apply (simp add: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
lemma (in is_extended') silc_dom_equiv[wp]: "I (silc_dom_equiv aag st)" by (rule lift_inv,simp)
|
|
|
|
|
|
lemma tcb_action_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l (pas_refined aag) (tcb_sched_action f t)"
|
|
apply (rule reads_respects_scheduler_cases)
|
|
apply (simp add: tcb_sched_action_def set_tcb_queue_def)
|
|
apply wp
|
|
apply (rule ev_modify[where P=\<top>])
|
|
apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def)
|
|
apply (clarsimp simp: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def idle_equiv_def
|
|
)
|
|
apply (rule ext)
|
|
apply clarsimp
|
|
apply wp
|
|
apply (clarsimp simp add: etcb_at_def split: option.splits)
|
|
apply (frule(1) tcb_domain_wellformed)
|
|
apply simp
|
|
apply (simp add: tcb_sched_action_def set_tcb_queue_def)
|
|
apply (rule reads_respects_scheduler_unobservable'[where P="pas_refined aag"])
|
|
apply wp
|
|
apply (clarsimp simp add: etcb_at_def split: option.splits)
|
|
apply wp
|
|
apply (clarsimp simp: etcb_at_def split: option.splits)
|
|
apply (clarsimp simp: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def)
|
|
apply (frule(1) tcb_domain_wellformed)
|
|
apply (rule ext)
|
|
apply clarsimp+
|
|
done
|
|
|
|
|
|
lemma arm_globals_frame_aligned:
|
|
"valid_arch_state s \<Longrightarrow> pspace_aligned s \<Longrightarrow> is_aligned (arm_globals_frame (arch_state s)) 12"
|
|
apply (clarsimp simp add: valid_arch_state_def pspace_aligned_def obj_at_def)
|
|
apply (erule_tac x="arm_globals_frame (arch_state s)" in ballE)
|
|
apply clarsimp+
|
|
done
|
|
|
|
|
|
lemma plus_in_scheduler_affects_globals_frame': "\<lbrakk>valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>a. a \<le> 3 \<longrightarrow> (arm_globals_frame (arch_state s) + a) \<in> scheduler_affects_globals_frame s"
|
|
apply clarsimp
|
|
apply (rule ptr_range_add_memI)
|
|
apply (frule (1) arm_globals_frame_aligned)
|
|
apply (clarsimp simp: is_aligned_def)
|
|
apply (clarsimp simp: dvd_def)
|
|
apply clarsimp
|
|
apply uint_arith
|
|
done
|
|
|
|
lemma range_is_globals_frame: "\<lbrakk>valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow>
|
|
{(arm_globals_frame (arch_state s)) .. (arm_globals_frame (arch_state s)) + 3}
|
|
= scheduler_affects_globals_frame s"
|
|
apply (frule(1) arm_globals_frame_aligned)
|
|
apply (rule equalityI)
|
|
apply clarsimp
|
|
apply (clarsimp simp add: is_aligned_def dvd_def ptr_range_def)
|
|
apply uint_arith
|
|
apply (clarsimp simp add: is_aligned_def dvd_def ptr_range_def)
|
|
apply uint_arith
|
|
done
|
|
|
|
|
|
lemmas plus_in_scheduler_affects_globals_frame = plus_in_scheduler_affects_globals_frame'[rule_format]
|
|
|
|
|
|
|
|
lemma globals_equiv_scheduler_update:
|
|
|
|
"pspace_aligned s \<Longrightarrow> valid_arch_state s \<Longrightarrow> globals_equiv_scheduler sta s \<Longrightarrow>
|
|
globals_equiv_scheduler sta
|
|
(s\<lparr>machine_state :=
|
|
underlying_memory_update
|
|
(\<lambda>m a. if a = arm_globals_frame (arch_state s) + 3
|
|
then x1
|
|
else if a = arm_globals_frame (arch_state s) + 2
|
|
then x2
|
|
else if a = arm_globals_frame (arch_state s) + 1
|
|
then x3
|
|
else if a = arm_globals_frame (arch_state s)
|
|
then x4
|
|
else m a)
|
|
(machine_state s)\<rparr>)"
|
|
apply (frule (1) plus_in_scheduler_affects_globals_frame[where a=0 and s=s,simplified])
|
|
apply (frule (1) plus_in_scheduler_affects_globals_frame[where a=1 and s=s,simplified])
|
|
apply (frule (1) plus_in_scheduler_affects_globals_frame[where a=2 and s=s,simplified])
|
|
apply (frule (1) plus_in_scheduler_affects_globals_frame[where a=3 and s=s,simplified])
|
|
apply (auto simp: globals_equiv_scheduler_def)
|
|
done
|
|
|
|
lemma dmo_no_mem_globals_equiv_scheduler:
|
|
"(\<And>P. invariant f (\<lambda>ms. P (underlying_memory ms))) \<Longrightarrow>
|
|
invariant (do_machine_op f) (globals_equiv_scheduler s)"
|
|
unfolding do_machine_op_def
|
|
apply(wp | simp add: split_def)+
|
|
apply(fastforce simp: valid_def globals_equiv_scheduler_def idle_equiv_def)
|
|
done
|
|
|
|
lemma clearExMonitor_globals_equiv_scheduler[wp]: "\<lbrace> globals_equiv_scheduler sta \<rbrace> do_machine_op clearExMonitor \<lbrace> \<lambda>_. globals_equiv_scheduler sta \<rbrace>"
|
|
unfolding clearExMonitor_def
|
|
apply (wp dmo_no_mem_globals_equiv_scheduler)
|
|
apply simp
|
|
done
|
|
|
|
lemma arch_switch_to_thread_globals_equiv_scheduler:
|
|
"\<lbrace>invs and globals_equiv_scheduler sta\<rbrace> arch_switch_to_thread thread
|
|
\<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>"
|
|
unfolding arch_switch_to_thread_def storeWord_def
|
|
apply (wp clearExMonitor_globals_equiv_scheduler dmo_wp modify_wp thread_get_wp')
|
|
apply (rule_tac Q="\<lambda>r s. invs s \<and> globals_equiv_scheduler sta s" in hoare_strengthen_post)
|
|
apply wp
|
|
apply (rule globals_equiv_scheduler_inv')
|
|
apply (wp set_vm_root_globals_equiv)
|
|
apply clarsimp+
|
|
apply (rule globals_equiv_scheduler_update)
|
|
apply clarsimp+
|
|
done
|
|
|
|
lemma dmo_storeWord_reads_respects_scheduler[wp]:
|
|
"reads_respects_scheduler aag l \<top> (do_machine_op (storeWord rva rvb))"
|
|
apply (clarsimp simp add: do_machine_op_def bind_def gets_def get_def
|
|
return_def select_f_def storeWord_def
|
|
assert_def simpler_modify_def fail_def)
|
|
apply (fold simpler_modify_def)
|
|
apply (intro impI conjI)
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def silc_dom_equiv_def
|
|
)
|
|
apply (simp add: equiv_valid_def2 equiv_valid_2_def)
|
|
done
|
|
|
|
definition weak_scheduler_affects_equiv :: "'a subject_label PAS \<Rightarrow> ('a subject_label) \<Rightarrow> det_state \<Rightarrow> det_state \<Rightarrow> bool"
|
|
where
|
|
"weak_scheduler_affects_equiv aag l s s' \<equiv>
|
|
(states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasDomainAbs aag x \<in> reads_scheduler aag l) (\<lambda> x. ptr_range x 12) s s')"
|
|
|
|
definition midstrength_scheduler_affects_equiv :: "'a subject_label PAS \<Rightarrow> ('a subject_label) \<Rightarrow> det_state \<Rightarrow> det_state \<Rightarrow> bool"
|
|
where
|
|
"midstrength_scheduler_affects_equiv aag l s s' \<equiv>
|
|
(states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasDomainAbs aag x \<in> reads_scheduler aag l) (\<lambda> x. ptr_range x 12) s s') \<and>
|
|
((pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l \<or>
|
|
pasDomainAbs aag (cur_domain s')\<in> reads_scheduler aag l) \<longrightarrow>
|
|
work_units_completed s = work_units_completed s')"
|
|
|
|
abbreviation strong_reads_respects_scheduler
|
|
where
|
|
"strong_reads_respects_scheduler aag l P f \<equiv>
|
|
equiv_valid (scheduler_equiv aag) (weak_scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) P f"
|
|
|
|
abbreviation midstrength_reads_respects_scheduler
|
|
where
|
|
"midstrength_reads_respects_scheduler aag l P f \<equiv>
|
|
equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) P f"
|
|
|
|
abbreviation weak_reads_respects_scheduler
|
|
where
|
|
"weak_reads_respects_scheduler aag l P f \<equiv>
|
|
equiv_valid (scheduler_equiv aag) (weak_scheduler_affects_equiv aag l) (weak_scheduler_affects_equiv aag l) P f"
|
|
|
|
lemma range_is_globals_frame': "\<lbrakk>valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow>
|
|
x \<in> scheduler_affects_globals_frame s \<Longrightarrow>
|
|
x = (arm_globals_frame (arch_state s)) \<or>
|
|
x = (arm_globals_frame (arch_state s)) + 1 \<or>
|
|
x = (arm_globals_frame (arch_state s)) + 2 \<or>
|
|
x = (arm_globals_frame (arch_state s)) + 3"
|
|
apply (frule(1) range_is_globals_frame[symmetric])
|
|
apply clarsimp
|
|
apply (rule ccontr)
|
|
apply uint_arith
|
|
done
|
|
|
|
lemma store_cur_thread_midstrength_reads_respects: "equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
|
|
(scheduler_affects_equiv aag l) (invs and (\<lambda>s. rva = arm_globals_frame (arch_state s)) and (\<lambda>s. t = idle_thread s))
|
|
(do y \<leftarrow> do_machine_op (storeWord rva rvb);
|
|
x \<leftarrow> modify (cur_thread_update (\<lambda>_. t));
|
|
set_scheduler_action resume_cur_thread
|
|
od)"
|
|
apply (clarsimp simp add: do_machine_op_def bind_def gets_def get_def
|
|
return_def select_f_def storeWord_def bind_def
|
|
set_scheduler_action_def
|
|
assert_def simpler_modify_def fail_def)
|
|
apply (fold simpler_modify_def)
|
|
apply (intro impI conjI)
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def silc_dom_equiv_def
|
|
weak_scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def
|
|
idle_equiv_def)
|
|
apply (drule range_is_globals_frame'[rotated -1], clarsimp+)
|
|
apply (simp add: equiv_valid_def2 equiv_valid_2_def)
|
|
done
|
|
|
|
lemma globals_frame_equiv_as_states_equiv: "scheduler_globals_frame_equiv st s =
|
|
(states_equiv_for (\<lambda>x. x \<in> scheduler_affects_globals_frame s) \<bottom> \<bottom> \<bottom> (\<lambda>_. {})
|
|
(s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s)"
|
|
apply (clarsimp simp add: states_equiv_for_def equiv_for_def
|
|
scheduler_globals_frame_equiv_def
|
|
equiv_asids_def)
|
|
apply force
|
|
done
|
|
|
|
lemma silc_dom_equiv_as_states_equiv: "silc_dom_equiv aag st s =
|
|
(states_equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) \<bottom> \<bottom> \<bottom> (\<lambda>_. {})
|
|
(s\<lparr>kheap := kheap st\<rparr>) s)"
|
|
apply (clarsimp simp add: states_equiv_for_def equiv_for_def
|
|
silc_dom_equiv_def
|
|
equiv_asids_def)
|
|
done
|
|
|
|
lemma silc_dom_equiv_states_equiv_lift:
|
|
assumes a: "\<And>P Q R S X st. \<lbrace>states_equiv_for P Q R S X st\<rbrace> f \<lbrace>\<lambda>_. states_equiv_for P Q R S X st\<rbrace>"
|
|
shows "\<lbrace>silc_dom_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>"
|
|
apply (simp add: silc_dom_equiv_as_states_equiv[abs_def])
|
|
apply (clarsimp simp add: valid_def)
|
|
apply (frule use_valid[OF _ a])
|
|
apply assumption
|
|
apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def)
|
|
done
|
|
|
|
lemma scheduler_affects_equiv_unobservable:
|
|
assumes a: "\<And>P Q R S X st. \<lbrace>states_equiv_for P Q R S X st\<rbrace> f \<lbrace>\<lambda>_. states_equiv_for P Q R S X st\<rbrace>"
|
|
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>"
|
|
assumes e: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>"
|
|
assumes s: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>r s. P (scheduler_action s)\<rbrace>"
|
|
assumes w: "\<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> f \<lbrace>\<lambda>r s. P (work_units_completed s)\<rbrace>"
|
|
assumes i: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>"
|
|
assumes x: "\<And>P. \<lbrace>\<lambda>s. P (exclusive_state (machine_state s))\<rbrace> f \<lbrace>\<lambda>r s. P (exclusive_state (machine_state s))\<rbrace>"
|
|
shows "\<lbrace>scheduler_affects_equiv aag l st\<rbrace> f
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
proof -
|
|
have d: "\<lbrace>scheduler_globals_frame_equiv st\<rbrace> f \<lbrace>\<lambda>_. scheduler_globals_frame_equiv st\<rbrace>"
|
|
apply (simp add: globals_frame_equiv_as_states_equiv[abs_def])
|
|
apply (clarsimp simp add: valid_def)
|
|
apply (frule use_valid[OF _ a])
|
|
apply assumption
|
|
apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def)
|
|
done
|
|
show ?thesis
|
|
apply (simp add: scheduler_affects_equiv_def[abs_def])
|
|
apply (rule hoare_pre)
|
|
apply (wps c)
|
|
apply (wp static_imp_wp a silc_dom_equiv_states_equiv_lift d e s w i x hoare_vcg_imp_lift)
|
|
apply fastforce
|
|
done
|
|
qed
|
|
|
|
lemma midstrength_scheduler_affects_equiv_unobservable:
|
|
assumes a: "\<And>P Q R S X st. \<lbrace>states_equiv_for P Q R S X st\<rbrace> f \<lbrace>\<lambda>_. states_equiv_for P Q R S X st\<rbrace>"
|
|
assumes w: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s) (work_units_completed s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s) (work_units_completed s)\<rbrace>"
|
|
shows "\<lbrace>midstrength_scheduler_affects_equiv aag l st\<rbrace> f
|
|
\<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: midstrength_scheduler_affects_equiv_def[abs_def])
|
|
apply (rule hoare_pre)
|
|
apply (wp a w silc_dom_equiv_states_equiv_lift)
|
|
apply clarsimp
|
|
done
|
|
|
|
lemma dmo_mol_exclusive_state[wp]:
|
|
"invariant (do_machine_op (machine_op_lift mop)) (\<lambda>s. P (exclusive_state (machine_state s)))"
|
|
by(wp mol_exclusive_state dmo_wp | simp add: split_def dmo_bind_valid writeTTBR0_def isb_def dsb_def )+
|
|
|
|
crunch exclusive_state[wp]: set_vm_root "\<lambda>s. P (exclusive_state (machine_state s))"
|
|
(ignore: do_machine_op simp: invalidateTLB_ASID_def setHardwareASID_def setCurrentPD_def dsb_def isb_def writeTTBR0_def dmo_bind_valid crunch_simps)
|
|
|
|
lemmas set_vm_root_scheduler_affects_equiv[wp] = scheduler_affects_equiv_unobservable[OF set_vm_root_states_equiv_for set_vm_root_cur_domain _ _ _ set_vm_root_idle_thread set_vm_root_exclusive_state]
|
|
|
|
|
|
lemma set_vm_root_reads_respects_scheduler[wp]:
|
|
"reads_respects_scheduler aag l \<top> (set_vm_root thread)"
|
|
apply (rule reads_respects_scheduler_unobservable'[OF scheduler_equiv_lift'[OF globals_equiv_scheduler_inv']])
|
|
apply (wp silc_dom_equiv_states_equiv_lift set_vm_root_states_equiv_for | simp)+
|
|
done
|
|
|
|
lemma thread_get_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l (K(pasObjectAbs aag t \<in> reads_scheduler aag l)) (thread_get f t)"
|
|
apply (rule gen_asm_ev)
|
|
apply (simp add: thread_get_def)
|
|
apply wp
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def get_tcb_def)
|
|
done
|
|
|
|
|
|
lemma plus_in_arm_globals_frame': "\<lbrakk>valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>a. a \<le> 3 \<longrightarrow> (arm_globals_frame (arch_state s) + a) \<in> range_of_arm_globals_frame s"
|
|
apply clarsimp
|
|
apply (rule ptr_range_add_memI)
|
|
apply (frule (1) arm_globals_frame_aligned)
|
|
apply (clarsimp simp: is_aligned_def)
|
|
apply (clarsimp simp: dvd_def)
|
|
apply uint_arith
|
|
done
|
|
|
|
lemma dmo_storeWord_other_domain: "\<lbrace>scheduler_affects_equiv aag l st and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l)
|
|
and (\<lambda>s. globals = arm_globals_frame (arch_state s))
|
|
and (\<lambda>s. cur_domain s = cur_domain st)
|
|
and valid_arch_state and pspace_aligned\<rbrace>
|
|
do_machine_op (storeWord globals buffer_ptr)
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (rule hoare_pre)
|
|
apply (rule dmo_wp)
|
|
apply (simp add: storeWord_def)
|
|
apply wp
|
|
apply (clarsimp simp add: states_equiv_for_def
|
|
scheduler_affects_equiv_def equiv_for_def
|
|
equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def
|
|
silc_dom_equiv_def)
|
|
apply (frule(1) plus_in_arm_globals_frame')
|
|
apply (frule(1) plus_in_arm_globals_frame'[rule_format,where a=0,simplified])
|
|
apply (intro impI conjI)
|
|
apply clarsimp+
|
|
done
|
|
|
|
crunch idle_thread[wp]: guarded_switch_to,schedule "\<lambda>(s :: det_state). P (idle_thread s)" (wp: crunch_wps simp: crunch_simps)
|
|
|
|
lemma silc_dom_lift:
|
|
assumes a: "\<And>P. \<lbrace>\<lambda>s. P (kheap s)\<rbrace> f \<lbrace>\<lambda>r s. P (kheap s)\<rbrace>"
|
|
shows "\<lbrace>silc_dom_equiv aag st\<rbrace> f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>"
|
|
apply (simp add: silc_dom_equiv_def equiv_for_def[abs_def])
|
|
apply (wp a)
|
|
done
|
|
|
|
lemma dmo_silc_dom[wp]: "\<lbrace>silc_dom_equiv aag st\<rbrace> do_machine_op mop \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>"
|
|
apply (wp silc_dom_lift)
|
|
done
|
|
|
|
crunch kheap[wp]: guarded_switch_to, schedule "\<lambda>s :: det_state. P (kheap s)" (wp: dxo_wp_weak crunch_wps simp: crunch_simps)
|
|
|
|
lemma [wp]: "\<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>"
|
|
apply (simp add: storeWord_def)
|
|
apply (wp dmo_wp modify_wp)
|
|
apply simp
|
|
done
|
|
|
|
lemma [wp]: "\<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>"
|
|
apply (rule hoare_pre)
|
|
apply (wp dmo_wp irq_state_clearExMonitor | simp)+
|
|
done
|
|
|
|
lemma [wp]: "\<lbrace> scheduler_equiv aag st \<rbrace> do_machine_op clearExMonitor \<lbrace> \<lambda>_. scheduler_equiv aag st \<rbrace>"
|
|
apply (rule scheduler_equiv_lift)
|
|
apply wp
|
|
done
|
|
|
|
lemma dmo_ev:
|
|
"(\<And>s s'. equiv_valid (\<lambda>ms ms'. I (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>))
|
|
(\<lambda>ms ms'. A (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>))
|
|
(\<lambda>ms ms'. B (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>))
|
|
(K (P s \<and> P s')) f)
|
|
\<Longrightarrow> equiv_valid I A B P (do_machine_op f)"
|
|
apply (clarsimp simp: do_machine_op_def bind_def equiv_valid_def2 equiv_valid_2_def gets_def get_def select_f_def modify_def put_def return_def split_def)
|
|
apply atomize
|
|
apply (erule_tac x=s in allE)
|
|
apply (erule_tac x=t in allE)
|
|
apply simp
|
|
apply (erule_tac x="machine_state s" in allE)
|
|
apply (erule_tac x="machine_state t" in allE)
|
|
apply fastforce
|
|
done
|
|
|
|
lemma [wp]: "reads_respects_scheduler aag l (\<lambda>_. True) (do_machine_op clearExMonitor)"
|
|
apply (simp add: clearExMonitor_def)
|
|
apply (wp dmo_ev)
|
|
apply (rule ev_modify)
|
|
apply clarsimp
|
|
apply (rule conjI)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def silc_dom_equiv_def equiv_for_def)
|
|
apply (clarsimp simp: scheduler_affects_equiv_def states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def scheduler_globals_frame_equiv_def simp del: split_paired_All)
|
|
done
|
|
|
|
definition "asahi_scheduler_affects_equiv aag l s s' \<equiv>
|
|
states_equiv_for
|
|
(\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. pasDomainAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. ptr_range x 12) s s' \<and>
|
|
(pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l \<or>
|
|
pasDomainAbs aag (cur_domain s') \<in> reads_scheduler aag l \<longrightarrow>
|
|
work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s')"
|
|
|
|
lemma asahi_scheduler_affects_equiv_unobservable:
|
|
assumes a: "\<And>P Q R S X st. \<lbrace>states_equiv_for P Q R S X st\<rbrace> f \<lbrace>\<lambda>_. states_equiv_for P Q R S X st\<rbrace>"
|
|
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>"
|
|
assumes w: "\<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> f \<lbrace>\<lambda>r s. P (work_units_completed s)\<rbrace>"
|
|
shows "\<lbrace>asahi_scheduler_affects_equiv aag l st\<rbrace> f
|
|
\<lbrace>\<lambda>_. asahi_scheduler_affects_equiv aag l st\<rbrace>"
|
|
proof -
|
|
have d: "\<lbrace>scheduler_globals_frame_equiv st\<rbrace> f \<lbrace>\<lambda>_. scheduler_globals_frame_equiv st\<rbrace>"
|
|
apply (simp add: globals_frame_equiv_as_states_equiv[abs_def])
|
|
apply (clarsimp simp add: valid_def)
|
|
apply (frule use_valid[OF _ a])
|
|
apply assumption
|
|
apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def)
|
|
done
|
|
show ?thesis
|
|
apply (simp add: asahi_scheduler_affects_equiv_def[abs_def])
|
|
apply (rule hoare_pre)
|
|
apply (wps c)
|
|
apply (wp static_imp_wp a silc_dom_equiv_states_equiv_lift d w)
|
|
apply clarsimp
|
|
done
|
|
qed
|
|
|
|
lemma asahi_scheduler_affects_equiv_sym[elim]:
|
|
"asahi_scheduler_affects_equiv aag l s s' \<Longrightarrow> asahi_scheduler_affects_equiv aag l s' s"
|
|
apply (simp add: asahi_scheduler_affects_equiv_def)
|
|
apply (auto simp: scheduler_globals_frame_equiv_sym states_equiv_for_sym silc_dom_equiv_sym)
|
|
done
|
|
|
|
lemma asahi_scheduler_affects_equiv_trans[elim]:
|
|
"\<lbrakk>asahi_scheduler_affects_equiv aag l s s'; scheduler_equiv aag s s'; asahi_scheduler_affects_equiv aag l s' s''; scheduler_equiv aag s' s''\<rbrakk> \<Longrightarrow> asahi_scheduler_affects_equiv aag l s s''"
|
|
apply (simp add: asahi_scheduler_affects_equiv_def scheduler_equiv_trans[where s'=s'])+
|
|
apply clarify
|
|
apply (rule conjI)
|
|
apply (rule states_equiv_for_trans[where t=s'])
|
|
apply simp+
|
|
apply (rule conjI)
|
|
apply clarsimp
|
|
apply (rule conjI)
|
|
apply (clarsimp simp add: scheduler_globals_frame_equiv_trans[where s'=s'] scheduler_equiv_def
|
|
domain_fields_equiv_def)+
|
|
done
|
|
|
|
definition "asahi_ex_scheduler_affects_equiv aag l s s' \<equiv>
|
|
states_equiv_for
|
|
(\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. pasDomainAbs aag x \<in> reads_scheduler aag l)
|
|
(\<lambda>x. ptr_range x 12) s s' \<and>
|
|
(pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l \<or>
|
|
pasDomainAbs aag (cur_domain s') \<in> reads_scheduler aag l \<longrightarrow>
|
|
work_units_completed s = work_units_completed s' \<and> scheduler_globals_frame_equiv s s' \<and>
|
|
exclusive_state_equiv s s')"
|
|
|
|
lemma asahi_ex_scheduler_affects_equiv_unobservable:
|
|
assumes a: "\<And>P Q R S X st. \<lbrace>states_equiv_for P Q R S X st\<rbrace> f \<lbrace>\<lambda>_. states_equiv_for P Q R S X st\<rbrace>"
|
|
assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>"
|
|
assumes w: "\<And>P. \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace> f \<lbrace>\<lambda>r s. P (work_units_completed s)\<rbrace>"
|
|
assumes x: "\<And>P. \<lbrace>\<lambda>s. P (exclusive_state (machine_state s))\<rbrace> f \<lbrace>\<lambda>r s. P (exclusive_state (machine_state s))\<rbrace>"
|
|
shows "\<lbrace>asahi_ex_scheduler_affects_equiv aag l st\<rbrace> f
|
|
\<lbrace>\<lambda>_. asahi_ex_scheduler_affects_equiv aag l st\<rbrace>"
|
|
proof -
|
|
have d: "\<lbrace>scheduler_globals_frame_equiv st\<rbrace> f \<lbrace>\<lambda>_. scheduler_globals_frame_equiv st\<rbrace>"
|
|
apply (simp add: globals_frame_equiv_as_states_equiv[abs_def])
|
|
apply (clarsimp simp add: valid_def)
|
|
apply (frule use_valid[OF _ a])
|
|
apply assumption
|
|
apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def)
|
|
done
|
|
show ?thesis
|
|
apply (simp add: asahi_ex_scheduler_affects_equiv_def[abs_def])
|
|
apply (rule hoare_pre)
|
|
apply (wps c)
|
|
apply (wp static_imp_wp a silc_dom_equiv_states_equiv_lift d w x)
|
|
apply clarsimp
|
|
done
|
|
qed
|
|
|
|
lemma asahi_ex_scheduler_affects_equiv_sym[elim]:
|
|
"asahi_ex_scheduler_affects_equiv aag l s s' \<Longrightarrow> asahi_ex_scheduler_affects_equiv aag l s' s"
|
|
apply (simp add: asahi_ex_scheduler_affects_equiv_def)
|
|
apply (auto simp: scheduler_globals_frame_equiv_sym states_equiv_for_sym silc_dom_equiv_sym)
|
|
done
|
|
|
|
lemma asahi_ex_scheduler_affects_equiv_trans[elim]:
|
|
"\<lbrakk>asahi_ex_scheduler_affects_equiv aag l s s'; scheduler_equiv aag s s'; asahi_ex_scheduler_affects_equiv aag l s' s''; scheduler_equiv aag s' s''\<rbrakk> \<Longrightarrow> asahi_ex_scheduler_affects_equiv aag l s s''"
|
|
apply (simp add: asahi_ex_scheduler_affects_equiv_def scheduler_equiv_trans[where s'=s'])+
|
|
apply clarify
|
|
apply (rule conjI)
|
|
apply (rule states_equiv_for_trans[where t=s'])
|
|
apply simp+
|
|
apply (rule conjI)
|
|
apply clarsimp
|
|
apply (rule conjI)
|
|
apply (clarsimp simp add: scheduler_globals_frame_equiv_trans[where s'=s'] scheduler_equiv_def
|
|
domain_fields_equiv_def)+
|
|
done
|
|
|
|
lemma ev_midstrength_to_asahi_dmo_storeWord: "equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
|
|
(asahi_scheduler_affects_equiv aag l) (invs and (\<lambda>s. rva = arm_globals_frame (arch_state s)))
|
|
(do_machine_op (storeWord rva rvb))"
|
|
apply (clarsimp simp add: do_machine_op_def bind_def gets_def get_def
|
|
return_def select_f_def storeWord_def bind_def
|
|
set_scheduler_action_def
|
|
assert_def simpler_modify_def fail_def)
|
|
apply (fold simpler_modify_def)
|
|
apply (intro impI conjI)
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def silc_dom_equiv_def
|
|
weak_scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def
|
|
asahi_scheduler_affects_equiv_def idle_equiv_def)
|
|
apply (subgoal_tac "pspace_aligned t" "valid_arch_state t")
|
|
apply (frule(2) range_is_globals_frame')
|
|
apply simp
|
|
apply ((simp add: invs_def valid_state_def valid_pspace_def)+)[2]
|
|
apply (simp add: equiv_valid_def2 equiv_valid_2_def)
|
|
done
|
|
|
|
lemma ev_asahi_to_asahi_ex_dmo_clearExMonitor:
|
|
"equiv_valid (scheduler_equiv aag) (asahi_scheduler_affects_equiv aag l) (asahi_ex_scheduler_affects_equiv aag l)
|
|
\<top> (do_machine_op clearExMonitor)"
|
|
apply (simp add: clearExMonitor_def)
|
|
apply (wp dmo_ev)
|
|
apply (rule ev_modify)
|
|
apply clarsimp
|
|
apply (rule conjI)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def silc_dom_equiv_def equiv_for_def)
|
|
apply (clarsimp simp: asahi_scheduler_affects_equiv_def asahi_ex_scheduler_affects_equiv_def states_equiv_for_def equiv_for_def equiv_asids_def equiv_asid_def scheduler_globals_frame_equiv_def simp del: split_paired_All)
|
|
done
|
|
|
|
lemma ev_asahi_ex_to_full_fragement:
|
|
"equiv_valid (scheduler_equiv aag) (asahi_ex_scheduler_affects_equiv aag l) (scheduler_affects_equiv aag l) \<top>
|
|
(do x \<leftarrow> modify (cur_thread_update (\<lambda>_. t));
|
|
set_scheduler_action resume_cur_thread
|
|
od)"
|
|
apply (clarsimp simp add: bind_def gets_def get_def return_def select_f_def bind_def set_scheduler_action_def assert_def simpler_modify_def fail_def)
|
|
apply (fold simpler_modify_def)
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def silc_dom_equiv_def
|
|
weak_scheduler_affects_equiv_def
|
|
asahi_ex_scheduler_affects_equiv_def idle_equiv_def)
|
|
done
|
|
|
|
lemma store_cur_thread_fragment_midstrength_reads_respects:
|
|
"equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
|
|
(scheduler_affects_equiv aag l) (invs and (\<lambda>s. rva = arm_globals_frame (arch_state s)))
|
|
(do z \<leftarrow> do_machine_op (storeWord rva rvb);
|
|
y \<leftarrow> do_machine_op clearExMonitor;
|
|
x \<leftarrow> modify (cur_thread_update (\<lambda>_. t));
|
|
set_scheduler_action resume_cur_thread
|
|
od)"
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule bind_ev_general)
|
|
apply (rule bind_ev_general)
|
|
apply (rule ev_asahi_ex_to_full_fragement)
|
|
apply (rule ev_asahi_to_asahi_ex_dmo_clearExMonitor)
|
|
apply (wp)
|
|
apply (rule ev_midstrength_to_asahi_dmo_storeWord)
|
|
apply (wp)
|
|
apply (simp)
|
|
done
|
|
(*******************************)
|
|
|
|
lemma arch_switch_to_thread_globals_equiv_scheduler':
|
|
"\<lbrace>invs and globals_equiv_scheduler sta\<rbrace>
|
|
do x \<leftarrow> set_vm_root t;
|
|
globals \<leftarrow> gets (arm_globals_frame \<circ> arch_state);
|
|
buffer_ptr \<leftarrow> thread_get tcb_ipc_buffer t;
|
|
do_machine_op (storeWord globals buffer_ptr)
|
|
od
|
|
\<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>"
|
|
unfolding arch_switch_to_thread_def storeWord_def
|
|
apply (wp clearExMonitor_globals_equiv_scheduler dmo_wp modify_wp thread_get_wp')
|
|
apply (rule_tac Q="\<lambda>r s. invs s \<and> globals_equiv_scheduler sta s" in hoare_strengthen_post)
|
|
apply wp
|
|
apply (rule globals_equiv_scheduler_inv')
|
|
apply (wp set_vm_root_globals_equiv)
|
|
apply clarsimp+
|
|
apply (rule globals_equiv_scheduler_update)
|
|
apply clarsimp+
|
|
done
|
|
|
|
lemma arch_switch_to_thread_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l ((\<lambda>s. pasObjectAbs aag t = pasDomainAbs aag (cur_domain s)) and invs) (arch_switch_to_thread t)"
|
|
apply (rule reads_respects_scheduler_cases)
|
|
apply (simp add: arch_switch_to_thread_def)
|
|
apply wp
|
|
apply (clarsimp simp: scheduler_equiv_def globals_equiv_scheduler_def)
|
|
apply (simp add: arch_switch_to_thread_def)
|
|
apply (simp add:bind_assoc[symmetric])
|
|
apply wp_once
|
|
apply wp_once
|
|
apply (simp add: bind_assoc)
|
|
apply (rule reads_respects_scheduler_unobservable''[where P'="invs and (\<lambda>s. pasObjectAbs aag t = pasDomainAbs aag (cur_domain s))"])
|
|
apply (rule hoare_pre)
|
|
apply (rule scheduler_equiv_lift')
|
|
apply (rule arch_switch_to_thread_globals_equiv_scheduler')
|
|
apply (wp silc_dom_lift | simp)+
|
|
apply force
|
|
apply (rule hoare_pre)
|
|
apply (wp dmo_storeWord_other_domain | simp)+
|
|
apply (simp add: scheduler_equiv_def invs_def valid_state_def valid_pspace_def
|
|
domain_fields_equiv_def)
|
|
apply clarsimp
|
|
apply assumption
|
|
apply wp
|
|
apply (fastforce simp: reads_lrefl)
|
|
done
|
|
|
|
lemma arch_switch_to_thread_pas_refined[wp]:
|
|
"\<lbrace>pas_refined aag\<rbrace>
|
|
arch_switch_to_thread t
|
|
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
|
|
unfolding arch_switch_to_thread_def
|
|
by (wp do_machine_op_pas_refined | simp)+
|
|
|
|
|
|
lemma cur_thread_update_idle_reads_respects_scheduler: "reads_respects_scheduler aag l (\<lambda>s. t = idle_thread s)
|
|
(modify (cur_thread_update (\<lambda>_. t)))"
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def
|
|
scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def idle_equiv_def)
|
|
done
|
|
|
|
|
|
|
|
|
|
|
|
|
|
lemma strong_cur_domain_unobservable: "reads_respects_scheduler aag l (P and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l)) f \<Longrightarrow> strong_reads_respects_scheduler aag l (P and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l))
|
|
f"
|
|
apply (clarsimp simp add: equiv_valid_def2 equiv_valid_2_def
|
|
scheduler_equiv_def domain_fields_equiv_def
|
|
scheduler_affects_equiv_def weak_scheduler_affects_equiv_def)
|
|
apply (drule_tac x=s in spec)
|
|
apply (drule_tac x=t in spec)
|
|
apply clarsimp
|
|
apply (drule_tac x="(a,b)" in bspec,clarsimp+)
|
|
apply (drule_tac x="(aa,ba)" in bspec,clarsimp+)
|
|
done
|
|
|
|
lemma midstrength_cur_domain_unobservable: "reads_respects_scheduler aag l (P and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l)) f \<Longrightarrow> midstrength_reads_respects_scheduler aag l (P and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l))
|
|
f"
|
|
apply (clarsimp simp add: equiv_valid_def2 equiv_valid_2_def
|
|
scheduler_equiv_def domain_fields_equiv_def
|
|
scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def)
|
|
apply (drule_tac x=s in spec)
|
|
apply (drule_tac x=t in spec)
|
|
apply clarsimp
|
|
apply (drule_tac x="(a,b)" in bspec,clarsimp+)
|
|
apply (drule_tac x="(aa,ba)" in bspec,clarsimp+)
|
|
done
|
|
|
|
|
|
lemma equiv_valid_get_assert:
|
|
"equiv_valid I A B P f \<Longrightarrow>
|
|
equiv_valid I A B P (get >>= (\<lambda> s. assert (g s) >>= (\<lambda> y. f)))"
|
|
apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def bind_def get_def
|
|
assert_def return_def fail_def)
|
|
apply fastforce
|
|
done
|
|
|
|
|
|
|
|
lemma midstrength_reads_respects_scheduler_cases:
|
|
assumes b: "pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l P' (f t)"
|
|
assumes b': "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> P' s"
|
|
|
|
assumes c: "pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> reads_respects_scheduler aag l P'' (f t)"
|
|
assumes c': "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> P'' s"
|
|
assumes d: "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t = pasDomainAbs aag (cur_domain s)"
|
|
shows "midstrength_reads_respects_scheduler aag l Q (f t)"
|
|
apply (case_tac "pasObjectAbs aag t \<in> reads_scheduler aag l")
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule b)
|
|
apply simp+
|
|
apply (rule b')
|
|
apply simp+
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule midstrength_cur_domain_unobservable)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule c)
|
|
apply simp+
|
|
apply fastforce
|
|
apply clarsimp
|
|
apply (rule conjI)
|
|
apply (rule c')
|
|
apply simp+
|
|
apply (metis reads_lrefl d)
|
|
done
|
|
|
|
lemma thread_get_weak_reads_respects_scheduler[wp]: "weak_reads_respects_scheduler aag l
|
|
(K (pasObjectAbs aag t \<in> reads_scheduler aag l))
|
|
(thread_get f t)"
|
|
apply (rule gen_asm_ev)
|
|
apply (simp add: thread_get_def)
|
|
apply wp
|
|
apply (clarsimp simp add: weak_scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def get_tcb_def)
|
|
done
|
|
|
|
|
|
|
|
lemma gets_globals_frame_weak_reads_respects_scheduler[wp]: "weak_reads_respects_scheduler aag l
|
|
\<top>
|
|
(gets (arm_globals_frame o arch_state))"
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply wp
|
|
apply (clarsimp simp: scheduler_equiv_def globals_equiv_scheduler_def)
|
|
done
|
|
|
|
|
|
lemma midstrength_weak[intro]:
|
|
"midstrength_scheduler_affects_equiv aag l s s' \<Longrightarrow> weak_scheduler_affects_equiv aag l s s'"
|
|
apply(auto simp: midstrength_scheduler_affects_equiv_def weak_scheduler_affects_equiv_def)
|
|
done
|
|
|
|
lemma weak_reads_respects_scheduler_to_midstrength:
|
|
assumes w: "weak_reads_respects_scheduler aag l P f"
|
|
assumes i: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
|
|
shows "equiv_valid_inv (scheduler_equiv aag)
|
|
(midstrength_scheduler_affects_equiv aag l) P f"
|
|
apply(clarsimp simp: equiv_valid_def2 equiv_valid_2_def)
|
|
apply(rule conjI)
|
|
apply(insert w)[1]
|
|
apply(fastforce simp: equiv_valid_def2 equiv_valid_2_def)
|
|
apply(blast dest: state_unchanged[OF i])
|
|
done
|
|
|
|
lemma gets_globals_frame_lowermidstrength_equiv_scheduler[wp]: "equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
|
|
\<top>
|
|
(gets (arm_globals_frame o arch_state))"
|
|
apply (rule weak_reads_respects_scheduler_to_midstrength)
|
|
apply wp
|
|
done
|
|
|
|
lemma weak_scheduler_affects_equiv_trans[elim]:
|
|
"\<lbrakk>weak_scheduler_affects_equiv aag l s s'; weak_scheduler_affects_equiv aag l s' s''\<rbrakk> \<Longrightarrow> weak_scheduler_affects_equiv aag l s s''"
|
|
apply (simp add: weak_scheduler_affects_equiv_def)
|
|
apply (fastforce intro: states_equiv_for_trans)
|
|
done
|
|
|
|
lemma midstrength_scheduler_affects_equiv_trans[elim]:
|
|
"\<lbrakk>scheduler_equiv aag s s'; midstrength_scheduler_affects_equiv aag l s s'; scheduler_equiv aag s' s''; midstrength_scheduler_affects_equiv aag l s' s''\<rbrakk> \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s s''"
|
|
apply (simp add: midstrength_scheduler_affects_equiv_def scheduler_equiv_def domain_fields_equiv_def)
|
|
apply (fastforce intro: states_equiv_for_trans)
|
|
done
|
|
|
|
|
|
lemma weak_scheduler_affects_equiv_sym[elim]:
|
|
"weak_scheduler_affects_equiv aag l s s' \<Longrightarrow> weak_scheduler_affects_equiv aag l s' s"
|
|
apply (simp add: weak_scheduler_affects_equiv_def)
|
|
apply (fastforce intro: states_equiv_for_sym)
|
|
done
|
|
|
|
lemma midstrength_scheduler_affects_equiv_sym[elim]:
|
|
"midstrength_scheduler_affects_equiv aag l s s' \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s' s"
|
|
apply (simp add: midstrength_scheduler_affects_equiv_def)
|
|
apply (fastforce intro: states_equiv_for_sym)
|
|
done
|
|
|
|
lemma ethread_get_oblivious_cur_thread: "oblivious (cur_thread_update f) (ethread_get a b)"
|
|
apply (simp add: ethread_get_def gets_the_def)
|
|
apply (wp oblivious_bind | simp add: oblivious_gets get_etcb_def)+
|
|
done
|
|
|
|
lemma ethread_get_oblivious_schact: "oblivious (scheduler_action_update f) (ethread_get a b)"
|
|
apply (simp add: ethread_get_def gets_the_def)
|
|
apply (wp oblivious_bind | simp add: oblivious_gets get_etcb_def)+
|
|
done
|
|
|
|
lemma tcb_action_oblivious_cur_thread: "oblivious (cur_thread_update a) (tcb_sched_action f t)"
|
|
apply (simp add: tcb_sched_action_def)
|
|
apply (wp oblivious_bind ethread_get_oblivious_cur_thread | clarsimp simp add: get_tcb_queue_def set_tcb_queue_def)+
|
|
apply (fastforce intro: state.equality det_ext.equality)
|
|
done
|
|
|
|
lemma tcb_action_oblivious_schact: "oblivious (scheduler_action_update a) (tcb_sched_action f t)"
|
|
apply (simp add: tcb_sched_action_def)
|
|
apply (wp oblivious_bind ethread_get_oblivious_schact | clarsimp simp add: get_tcb_queue_def set_tcb_queue_def)+
|
|
apply (fastforce intro: state.equality det_ext.equality)
|
|
done
|
|
|
|
lemma cur_thread_update_not_subject_reads_respects_scheduler: "reads_respects_scheduler aag l (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l \<and> pasObjectAbs aag t = pasDomainAbs aag (cur_domain s))
|
|
(modify (cur_thread_update (\<lambda>_. t)))"
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def
|
|
scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def idle_equiv_def)
|
|
done
|
|
|
|
lemma switch_to_thread_midstrength_reads_respects_scheduler[wp]: "midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t = pasDomainAbs aag (cur_domain s))) (switch_to_thread t >>= (\<lambda>_. set_scheduler_action resume_cur_thread))"
|
|
apply (simp add: switch_to_thread_def)
|
|
apply (subst oblivious_modify_swap[symmetric, OF tcb_action_oblivious_cur_thread])
|
|
apply (simp add: bind_assoc)
|
|
apply (simp add: set_scheduler_action_def)
|
|
apply (subst oblivious_modify_swap[symmetric, OF tcb_action_oblivious_schact])
|
|
apply (rule equiv_valid_get_assert)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (simp add: bind_assoc[symmetric])
|
|
apply (rule bind_ev_general)
|
|
apply (rule tcb_action_reads_respects_scheduler)
|
|
apply (simp add: bind_assoc)
|
|
apply (rule midstrength_reads_respects_scheduler_cases[where Q="(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t = pasDomainAbs aag (cur_domain s)))"])
|
|
apply (simp add: arch_switch_to_thread_def bind_assoc)
|
|
apply (rule bind_ev_general)
|
|
apply (rule bind_ev_general)
|
|
apply (rule bind_ev_general)
|
|
apply (fold set_scheduler_action_def)
|
|
apply (rule store_cur_thread_fragment_midstrength_reads_respects)
|
|
apply (wp weak_reads_respects_scheduler_to_midstrength[OF thread_get_weak_reads_respects_scheduler])
|
|
apply (rule_tac P="\<top>" and P'="\<top>" in equiv_valid_inv_unobservable)
|
|
apply (rule hoare_pre)
|
|
apply (rule scheduler_equiv_lift'[where P=\<top>])
|
|
apply (wp globals_equiv_scheduler_inv silc_dom_lift | simp)+
|
|
apply (wp midstrength_scheduler_affects_equiv_unobservable set_vm_root_states_equiv_for | simp)+
|
|
apply (wp cur_thread_update_not_subject_reads_respects_scheduler | simp | fastforce)+
|
|
done
|
|
|
|
lemma switch_to_thread_globals_equiv_scheduler[wp]:
|
|
"\<lbrace>invs and globals_equiv_scheduler sta\<rbrace> switch_to_thread thread
|
|
\<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>"
|
|
apply (simp add: switch_to_thread_def)
|
|
apply (wp dxo_wp_weak arch_switch_to_thread_globals_equiv_scheduler | simp)+
|
|
done
|
|
|
|
|
|
lemma ev_irrelevant_bind:
|
|
assumes inv: "\<And> P. \<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. P \<rbrace>"
|
|
assumes ev: "equiv_valid I A B P g"
|
|
shows "equiv_valid I A B P (do y \<leftarrow> f; g od)"
|
|
proof -
|
|
have a: "\<And>a b s. (a,b) \<in> fst (f s) \<Longrightarrow> b = s"
|
|
apply (erule use_valid[OF _ inv])
|
|
apply simp
|
|
done
|
|
show ?thesis
|
|
apply (insert ev)
|
|
apply (clarsimp simp add: equiv_valid_def2 equiv_valid_2_def
|
|
bind_def)
|
|
apply (drule a)+
|
|
apply clarsimp
|
|
apply fastforce
|
|
done
|
|
qed
|
|
|
|
lemma guarded_switch_to_thread_midstrength_reads_respects_scheduler[wp]: "midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t = pasDomainAbs aag (cur_domain s))) (guarded_switch_to t >>= (\<lambda>_. set_scheduler_action resume_cur_thread))"
|
|
apply (simp add: guarded_switch_to_def bind_assoc)
|
|
apply (subst bind_assoc[symmetric])
|
|
apply (rule ev_irrelevant_bind)
|
|
apply (wp gts_wp | simp)+
|
|
done
|
|
|
|
lemma arch_switch_to_idle_thread_globals_equiv_scheduler[wp]:
|
|
"\<lbrace>invs and globals_equiv_scheduler sta\<rbrace> arch_switch_to_idle_thread
|
|
\<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>"
|
|
unfolding arch_switch_to_idle_thread_def storeWord_def
|
|
apply (wp dmo_wp modify_wp thread_get_wp')
|
|
apply clarsimp
|
|
apply (rule globals_equiv_scheduler_update)
|
|
apply clarsimp+
|
|
done
|
|
|
|
lemma switch_to_idle_thread_globals_equiv_scheduler[wp]:
|
|
"\<lbrace>invs and globals_equiv_scheduler sta\<rbrace> switch_to_idle_thread
|
|
\<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>"
|
|
apply (simp add: switch_to_idle_thread_def)
|
|
apply (wp | simp)+
|
|
done
|
|
|
|
crunch cur_domain[wp]: guarded_switch_to,arch_switch_to_idle_thread,choose_thread "\<lambda>s. P (cur_domain s)" (wp: crunch_wps simp: crunch_simps)
|
|
|
|
crunch domain_fields[wp]: guarded_switch_to,arch_switch_to_idle_thread, choose_thread "domain_fields P" (wp: crunch_wps simp: crunch_simps)
|
|
|
|
|
|
|
|
lemma switch_to_idle_thread_midstrength_reads_respects_scheduler[wp]: "midstrength_reads_respects_scheduler aag l (invs and pas_refined aag) (switch_to_idle_thread >>= (\<lambda>_. set_scheduler_action resume_cur_thread))"
|
|
apply (simp add: switch_to_idle_thread_def)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (simp add: arch_switch_to_idle_thread_def bind_assoc)
|
|
apply (rule bind_ev_general)
|
|
apply (rule bind_ev_general)
|
|
apply (rule store_cur_thread_midstrength_reads_respects)
|
|
apply wp
|
|
apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def)
|
|
done
|
|
|
|
lemma gets_read_queue_reads_respects_scheduler[wp]: "weak_reads_respects_scheduler aag l (\<lambda>s. pasDomainAbs aag d \<in> reads_scheduler aag l) (gets (\<lambda>s. ready_queues s d))"
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply wp
|
|
apply (clarsimp simp add: weak_scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def)
|
|
done
|
|
|
|
lemma gets_ready_queue_midstrength_equiv_scheduler[wp]: "equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
|
|
(\<lambda>s. pasDomainAbs aag d \<in> reads_scheduler aag l)
|
|
(gets (\<lambda>s. ready_queues s d))"
|
|
apply (rule weak_reads_respects_scheduler_to_midstrength)
|
|
apply wp
|
|
done
|
|
|
|
lemma gets_cur_domain_reads_respects_scheduler[wp]: "equiv_valid (scheduler_equiv aag) A A \<top> (gets cur_domain)"
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply wp
|
|
apply (clarsimp simp add: scheduler_equiv_def states_equiv_for_def
|
|
equiv_for_def domain_fields_equiv_def)
|
|
done
|
|
|
|
|
|
lemma any_valid_thread: "queues p \<noteq> [] \<Longrightarrow> (\<And>x prio. x \<in> set (queues prio) \<Longrightarrow> P x) \<Longrightarrow>
|
|
P (hd (max_non_empty_queue queues))"
|
|
apply (simp add: max_non_empty_queue_def)
|
|
apply (rule Max_prop)
|
|
prefer 2
|
|
apply simp
|
|
apply blast
|
|
apply (drule_tac x="hd (queues (Max {prio. queues prio \<noteq> []}))" in meta_spec)
|
|
apply (drule_tac x="Max {prio. queues prio \<noteq> []}" in meta_spec)
|
|
apply simp
|
|
done
|
|
|
|
lemma tcb_with_domain_at: "valid_queues s \<Longrightarrow> x \<in> set (ready_queues s d p) \<Longrightarrow>
|
|
\<exists>t. ekheap s x = Some t \<and> (tcb_domain t) = d"
|
|
apply (fastforce simp add: valid_queues_def is_etcb_at_def etcb_at_def
|
|
split: option.splits)
|
|
done
|
|
|
|
lemma if_ev_bind: "\<lbrakk>b \<Longrightarrow> equiv_valid I A B P (f >>= s); \<not> b \<Longrightarrow> equiv_valid I A B Q (g >>= s)\<rbrakk>
|
|
\<Longrightarrow> equiv_valid I A B (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ((if b then f else g) >>= s)"
|
|
apply simp
|
|
done
|
|
|
|
lemma choose_thread_reads_respects_scheduler_cur_domain: "midstrength_reads_respects_scheduler aag l ( invs and pas_refined aag and valid_queues and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l)) (choose_thread >>= (\<lambda>_. set_scheduler_action resume_cur_thread))"
|
|
apply (simp add: choose_thread_def bind_assoc)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule bind_ev_general)
|
|
apply (rule bind_ev_general)
|
|
apply (rule if_ev_bind)
|
|
apply (rule switch_to_idle_thread_midstrength_reads_respects_scheduler)
|
|
apply (rule guarded_switch_to_thread_midstrength_reads_respects_scheduler)
|
|
apply wp
|
|
apply clarsimp
|
|
apply (erule any_valid_thread)
|
|
apply (frule(1) tcb_with_domain_at)
|
|
apply clarsimp
|
|
apply (frule(1) tcb_domain_wellformed)
|
|
apply simp
|
|
done
|
|
|
|
|
|
lemma cur_thread_update_unobservable: "\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain s = cur_domain st)\<rbrace> modify (cur_thread_update (\<lambda>_. thread))
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply wp
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def scheduler_equiv_def
|
|
domain_fields_equiv_def)
|
|
done
|
|
|
|
|
|
lemma arch_switch_to_idle_thread_unobservable:
|
|
"\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s) and invs\<rbrace> arch_switch_to_idle_thread
|
|
\<lbrace>\<lambda>rv s. scheduler_affects_equiv aag l st s\<rbrace>"
|
|
apply (simp add: arch_switch_to_idle_thread_def)
|
|
apply (wp dmo_storeWord_other_domain)
|
|
apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def
|
|
invs_def valid_state_def)
|
|
done
|
|
|
|
|
|
lemma switch_to_idle_thread_unobservable:
|
|
"\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain s = cur_domain st) and invs\<rbrace> switch_to_idle_thread
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: switch_to_idle_thread_def)
|
|
apply (wp cur_thread_update_unobservable arch_switch_to_idle_thread_unobservable)
|
|
apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
lemma clearExMonitor_unobservable: "\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain s = cur_domain st)\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: clearExMonitor_def)
|
|
apply (rule hoare_pre)
|
|
apply (wp dmo_wp modify_wp)
|
|
apply (clarsimp simp add: states_equiv_for_def
|
|
scheduler_affects_equiv_def equiv_for_def
|
|
equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def
|
|
silc_dom_equiv_def)
|
|
done
|
|
|
|
lemma arch_switch_to_thread_unobservable:
|
|
"\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s) and invs\<rbrace> arch_switch_to_thread t
|
|
\<lbrace>\<lambda>rv s. scheduler_affects_equiv aag l st s\<rbrace>"
|
|
apply (simp add: arch_switch_to_thread_def)
|
|
apply (wp dmo_storeWord_other_domain set_vm_root_scheduler_affects_equiv clearExMonitor_unobservable | simp)+
|
|
apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def
|
|
invs_def valid_state_def)+
|
|
done
|
|
|
|
lemma tcb_sched_action_unobservable: "\<lbrace>pas_refined aag and scheduler_affects_equiv aag l st and
|
|
(\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l)\<rbrace> tcb_sched_action f t
|
|
\<lbrace>\<lambda>rv. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: tcb_sched_action_def)
|
|
apply wp
|
|
apply (clarsimp simp add: etcb_at_def split: option.splits)
|
|
apply (clarsimp simp: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def)
|
|
apply (rule ext)
|
|
apply clarsimp
|
|
apply (frule(1) tcb_domain_wellformed)
|
|
apply simp
|
|
done
|
|
|
|
|
|
lemma switch_to_thread_unobservable:
|
|
"\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and
|
|
(\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and
|
|
scheduler_affects_equiv aag l st and scheduler_equiv aag st and invs and pas_refined aag\<rbrace> switch_to_thread t
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: switch_to_thread_def)
|
|
apply (wp cur_thread_update_unobservable arch_switch_to_idle_thread_unobservable
|
|
tcb_sched_action_unobservable arch_switch_to_thread_unobservable)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
|
|
|
|
|
|
lemma choose_thread_reads_respects_scheduler_other_domain: "reads_respects_scheduler aag l ( invs and pas_refined aag and valid_queues and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l)) choose_thread"
|
|
apply (rule reads_respects_scheduler_unobservable''[where P'="\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l \<and> invs s \<and> pas_refined aag s \<and> valid_queues s"])
|
|
apply (rule hoare_pre)
|
|
apply (rule scheduler_equiv_lift'[where P="invs"])
|
|
apply (simp add: choose_thread_def)
|
|
apply (wp guarded_switch_to_lift silc_dom_lift | simp)+
|
|
apply force
|
|
|
|
apply (simp add: choose_thread_def)
|
|
apply (wp guarded_switch_to_lift switch_to_idle_thread_unobservable
|
|
switch_to_thread_unobservable | simp)+
|
|
apply clarsimp
|
|
apply (intro impI conjI)
|
|
apply (simp add: scheduler_equiv_def domain_fields_equiv_def)
|
|
apply (elim exE)
|
|
apply (erule any_valid_thread)
|
|
apply (frule(1) tcb_with_domain_at)
|
|
apply clarsimp
|
|
apply (frule(1) tcb_domain_wellformed)
|
|
apply simp+
|
|
done
|
|
|
|
lemma equiv_valid_cases': "(\<And>s t. A s t \<Longrightarrow> I s t \<Longrightarrow> P s = P t) \<Longrightarrow> equiv_valid I A B (R and P) f \<Longrightarrow> equiv_valid I A B ((\<lambda>s. \<not>P s) and R) f \<Longrightarrow> equiv_valid I A B R f"
|
|
apply (simp add: equiv_valid_def2 equiv_valid_2_def)
|
|
apply fastforce
|
|
done
|
|
|
|
lemmas equiv_valid_cases = equiv_valid_cases'[rotated]
|
|
|
|
|
|
lemma choose_thread_reads_respects_scheduler: "midstrength_reads_respects_scheduler aag l ( invs and pas_refined aag and valid_queues) (choose_thread >>= (\<lambda>_. set_scheduler_action resume_cur_thread))"
|
|
apply (rule equiv_valid_cases[where P="\<lambda>s. pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l"])
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule choose_thread_reads_respects_scheduler_cur_domain)
|
|
apply simp
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule midstrength_cur_domain_unobservable)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (wp choose_thread_reads_respects_scheduler_other_domain | simp)+
|
|
apply force
|
|
apply (clarsimp simp: reads_lrefl)
|
|
apply (simp add: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
|
|
lemma next_domain_midstrength_equiv_scheduler: "equiv_valid (scheduler_equiv aag) (weak_scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) \<top> next_domain"
|
|
apply (simp add: next_domain_def)
|
|
apply (rule ev_modify)
|
|
apply (clarsimp simp add: scheduler_equiv_def Let_def
|
|
domain_fields_equiv_def globals_equiv_scheduler_def
|
|
silc_dom_equiv_def equiv_for_def
|
|
weak_scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def
|
|
states_equiv_for_def equiv_asids_def
|
|
equiv_asid_def idle_equiv_def)
|
|
done
|
|
|
|
|
|
lemma ev_weaken_pre_relation: "equiv_valid I A B P f \<Longrightarrow> (\<And>s t. A' s t \<Longrightarrow> A s t) \<Longrightarrow> equiv_valid I A' B P f"
|
|
apply (clarsimp simp add: equiv_valid_def2 equiv_valid_2_def)
|
|
apply fastforce
|
|
done
|
|
|
|
|
|
lemma weak_scheduler_affects_equiv[intro]: "scheduler_affects_equiv aag l st s \<Longrightarrow> weak_scheduler_affects_equiv aag l st s"
|
|
apply (simp add: scheduler_affects_equiv_def weak_scheduler_affects_equiv_def)
|
|
done
|
|
|
|
lemma midstrength_scheduler_affects_equiv[intro]: "scheduler_affects_equiv aag l st s \<Longrightarrow> midstrength_scheduler_affects_equiv aag l st s"
|
|
apply (simp add: scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def)
|
|
done
|
|
|
|
lemma next_domain_snippit: "reads_respects_scheduler aag l (invs and pas_refined aag and valid_queues) (do
|
|
dom_time \<leftarrow> gets domain_time;
|
|
y \<leftarrow> when (dom_time = 0) next_domain;
|
|
y\<leftarrow> choose_thread;
|
|
set_scheduler_action resume_cur_thread
|
|
od)"
|
|
apply (simp add: when_def)
|
|
apply (rule bind_ev_pre)
|
|
apply (rule bind_ev_general)
|
|
apply (simp add: when_def)
|
|
apply (rule choose_thread_reads_respects_scheduler)
|
|
apply (wp next_domain_midstrength_equiv_scheduler)
|
|
apply (rule ev_weaken_pre_relation)
|
|
apply (rule next_domain_midstrength_equiv_scheduler)
|
|
apply fastforce
|
|
apply (rule ev_weaken_pre_relation)
|
|
apply wp
|
|
apply fastforce
|
|
apply (wp next_domain_valid_queues)
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
lemma get_thread_state_reads_respects_scheduler: "reads_respects_scheduler aag l
|
|
((\<lambda>s. st_tcb_at \<top> rv s \<longrightarrow> pasObjectAbs aag rv \<in> reads_scheduler aag l \<or>
|
|
rv = idle_thread s)
|
|
and valid_idle) (get_thread_state rv)"
|
|
apply (clarsimp simp add: get_thread_state_def thread_get_def gets_the_def
|
|
gets_def get_def assert_opt_def get_tcb_def
|
|
bind_def return_def fail_def
|
|
valid_idle_def pred_tcb_at_def
|
|
obj_at_def
|
|
equiv_valid_def2 equiv_valid_2_def
|
|
split: option.splits kernel_object.splits
|
|
)
|
|
apply (clarsimp simp add: scheduler_equiv_def)
|
|
apply (elim disjE,simp_all)
|
|
apply (clarsimp simp: scheduler_affects_equiv_def
|
|
states_equiv_for_def equiv_for_def)
|
|
done
|
|
|
|
lemma get_cur_thread_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l)) (gets cur_thread)"
|
|
apply (clarsimp simp add: scheduler_equiv_def
|
|
scheduler_affects_equiv_def
|
|
domain_fields_equiv_def gets_def
|
|
get_def bind_def return_def
|
|
equiv_valid_def2 equiv_valid_2_def)
|
|
done
|
|
|
|
lemma get_scheduler_action_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l ( (\<lambda>s. pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l)) (gets scheduler_action)"
|
|
apply (clarsimp simp add: scheduler_equiv_def
|
|
scheduler_affects_equiv_def
|
|
domain_fields_equiv_def gets_def
|
|
get_def bind_def return_def
|
|
equiv_valid_def2 equiv_valid_2_def)
|
|
done
|
|
|
|
lemma switch_to_cur_domain: "valid_sched s \<Longrightarrow> scheduler_action s = switch_thread x \<Longrightarrow>
|
|
pas_refined aag s \<Longrightarrow> pasObjectAbs aag x = pasDomainAbs aag (cur_domain s)"
|
|
apply (clarsimp simp add: valid_sched_def
|
|
valid_sched_action_def
|
|
switch_in_cur_domain_def
|
|
in_cur_domain_def etcb_at_def
|
|
weak_valid_sched_action_def
|
|
is_etcb_at_def st_tcb_at_def
|
|
obj_at_def
|
|
valid_etcbs_def)
|
|
apply (drule_tac x=x in spec)
|
|
apply clarsimp
|
|
apply (drule(1) tcb_domain_wellformed)
|
|
apply simp
|
|
done
|
|
|
|
lemma equiv_valid_dc:
|
|
assumes a:"(\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>)"
|
|
assumes b:"(\<And>P. \<lbrace>P\<rbrace> f' \<lbrace>\<lambda>_. P\<rbrace>)"
|
|
shows "equiv_valid_2 I A A dc P P' f f'"
|
|
apply (clarsimp simp add: equiv_valid_2_def)
|
|
apply (erule use_valid[OF _ a])
|
|
apply (erule use_valid[OF _ b])
|
|
apply simp
|
|
done
|
|
|
|
|
|
|
|
lemma equiv_valid_2_unobservable:
|
|
assumes fI: "\<And>st. \<lbrace>P and I st and A st\<rbrace> f \<lbrace>\<lambda>_. I st\<rbrace>"
|
|
assumes fA: "\<And>st. \<lbrace>P' and I st and A st\<rbrace> f \<lbrace>\<lambda>_. A st\<rbrace>"
|
|
assumes gI: "\<And>st. \<lbrace>S and I st and A st\<rbrace> g \<lbrace>\<lambda>_. I st\<rbrace>"
|
|
assumes gA: "\<And>st. \<lbrace>S' and I st and A st\<rbrace> g \<lbrace>\<lambda>_. A st\<rbrace>"
|
|
assumes sym: "\<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s"
|
|
assumes trans: "\<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''"
|
|
shows "equiv_valid_2 I A A dc (P and P') (S and S') (f:: 'a \<Rightarrow> (unit \<times> 'a) set \<times> bool) g"
|
|
apply (clarsimp simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)
|
|
apply (erule preserves_equivalence_2_weak,assumption)
|
|
apply (rule hoare_pre)
|
|
apply (rule hoare_vcg_conj_lift)
|
|
apply (rule fI)
|
|
apply (rule fA)
|
|
apply force
|
|
apply (rule hoare_pre)
|
|
apply (rule hoare_vcg_conj_lift)
|
|
apply (rule gI)
|
|
apply (rule gA)
|
|
apply force
|
|
apply (fastforce intro!: sym trans)+
|
|
done
|
|
|
|
|
|
lemma equiv_valid_2: "equiv_valid I A B P f \<Longrightarrow> equiv_valid_rv I A B (op =) P f"
|
|
apply (simp add: equiv_valid_def2)
|
|
done
|
|
|
|
lemma ev_gets_const: "equiv_valid_inv I A (\<lambda>s. f s = x) (gets f)"
|
|
apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def
|
|
gets_def get_def bind_def return_def)
|
|
done
|
|
|
|
|
|
lemma reads_respects_scheduler_invisible_domain_switch: "reads_respects_scheduler aag l (\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_queues s \<and> guarded_pas_domain aag s \<and> domain_time s = 0 \<and> scheduler_action s = choose_new_thread \<and> ((pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l))) schedule"
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (simp add: schedule_def)
|
|
apply (simp add: equiv_valid_def2)
|
|
apply (rule equiv_valid_rv_bind[where W=dc])
|
|
apply (rule equiv_valid_dc)
|
|
apply wp[2]
|
|
apply (rule equiv_valid_2_bind_pre[where R'=dc])
|
|
apply (rule equiv_valid_2_bind_pre[where R'="op ="])
|
|
apply simp
|
|
apply (rule_tac P="rv'b = choose_new_thread" in EquivValid.gen_asm_ev2_l)
|
|
apply simp
|
|
apply (rule equiv_valid_2_bind_pre)
|
|
apply (rule equiv_valid_2)
|
|
apply (rule next_domain_snippit)
|
|
apply (rule_tac P="\<top>" and
|
|
P'="pas_refined aag and
|
|
(\<lambda>s. (runnable rva \<longrightarrow> (pasObjectAbs aag rv \<notin> reads_scheduler aag l)))" and
|
|
S="\<top>" and
|
|
S'="pas_refined aag and
|
|
(\<lambda>s. (runnable rv'a \<longrightarrow> pasObjectAbs aag rv' \<notin> reads_scheduler aag l))"
|
|
in equiv_valid_2_unobservable)
|
|
apply wp
|
|
apply (rule scheduler_equiv_lift)
|
|
apply wp
|
|
apply simp
|
|
apply clarsimp
|
|
apply wp
|
|
apply (wp tcb_sched_action_unobservable)
|
|
apply clarsimp
|
|
apply (wp scheduler_equiv_lift)
|
|
apply (wp | simp)+
|
|
apply (wp tcb_sched_action_unobservable)
|
|
apply simp
|
|
apply (fastforce+)[2]
|
|
apply wp
|
|
apply (force+)[2]
|
|
apply (rule equiv_valid_2)
|
|
apply (rule ev_gets_const)
|
|
apply wp
|
|
apply (force+)[2]
|
|
apply (rule equiv_valid_dc)
|
|
apply wp[2]
|
|
apply (wp gts_wp)
|
|
apply (force+)[2]
|
|
apply wp
|
|
apply clarsimp
|
|
apply (intro impI conjI allI)
|
|
apply force
|
|
apply force
|
|
apply (simp add: guarded_pas_domain_def)
|
|
apply (subgoal_tac "cur_thread s \<noteq> idle_thread s")
|
|
apply simp
|
|
apply (clarsimp simp add: pred_tcb_at_def obj_at_def valid_state_def
|
|
valid_idle_def invs_def)+
|
|
done
|
|
|
|
crunch globals_equiv_scheduler[wp]: choose_thread,schedule "(\<lambda>s:: det_state. globals_equiv_scheduler st s)" (wp: guarded_switch_to_lift crunch_wps ignore: guarded_switch_to simp: crunch_simps)
|
|
|
|
|
|
lemma schedule_no_domain_switch: "\<lbrace>(\<lambda>s. domain_time s \<noteq> 0) and (\<lambda>s. Q (cur_domain s))\<rbrace> schedule \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>"
|
|
apply (simp add: schedule_def)
|
|
apply (wp | wpc)+
|
|
apply (rule hoare_pre_cont)
|
|
apply wp
|
|
apply simp
|
|
apply wps
|
|
apply (wp gts_wp)
|
|
apply clarsimp
|
|
done
|
|
|
|
lemma schedule_no_domain_fields: "\<lbrace>(\<lambda>s. domain_time s \<noteq> 0) and domain_fields Q\<rbrace> schedule \<lbrace>\<lambda>_. domain_fields Q\<rbrace>"
|
|
apply (simp add: schedule_def)
|
|
apply (wp | wpc)+
|
|
apply (rule hoare_pre_cont)
|
|
apply wp
|
|
apply simp
|
|
apply wps
|
|
apply (wp gts_wp)
|
|
apply clarsimp
|
|
done
|
|
|
|
lemma set_scheduler_action_unobservable: "\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s)\<rbrace> set_scheduler_action a
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: set_scheduler_action_def)
|
|
apply wp
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def
|
|
scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
lemma choose_thread_unobservable: "\<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and invs and valid_queues and pas_refined aag and scheduler_equiv aag st\<rbrace> choose_thread
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: choose_thread_def)
|
|
apply (wp switch_to_idle_thread_unobservable guarded_switch_to_lift
|
|
switch_to_thread_unobservable)
|
|
apply (simp add: scheduler_affects_equiv_def
|
|
scheduler_equiv_def domain_fields_equiv_def)
|
|
apply (intro impI conjI)
|
|
apply (elim conjE exE)
|
|
apply (erule any_valid_thread)
|
|
apply (frule(1) tcb_with_domain_at)
|
|
apply clarsimp
|
|
apply (frule(1) tcb_domain_wellformed)
|
|
apply simp
|
|
done
|
|
|
|
lemma tcb_sched_action_scheduler_equiv[wp]: "\<lbrace>scheduler_equiv aag st\<rbrace> tcb_sched_action f a\<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>"
|
|
apply (rule scheduler_equiv_lift)
|
|
apply wp
|
|
done
|
|
|
|
lemma cur_thread_cur_domain: "st_tcb_at (op = st) (cur_thread s) s \<Longrightarrow> \<not> idle st \<Longrightarrow> invs s \<Longrightarrow>
|
|
guarded_pas_domain aag s \<Longrightarrow> pasObjectAbs aag (cur_thread s) = pasDomainAbs aag (cur_domain s)"
|
|
apply (clarsimp simp add: pred_tcb_at_def invs_def valid_idle_def
|
|
valid_state_def
|
|
obj_at_def guarded_pas_domain_def)
|
|
apply fastforce
|
|
done
|
|
|
|
lemma sched_equiv_cur_domain[intro]: "scheduler_equiv aag st s \<Longrightarrow> cur_domain st = cur_domain s"
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
lemma valid_sched_valid_queues[intro]: "valid_sched s \<Longrightarrow> valid_queues s"
|
|
apply (simp add: valid_sched_def)
|
|
done
|
|
|
|
|
|
|
|
lemma reads_respects_scheduler_invisible_no_domain_switch: "reads_respects_scheduler aag l (\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) schedule"
|
|
apply (rule reads_respects_scheduler_unobservable''[where P=Q and P'=Q and Q=Q for Q])
|
|
apply (rule hoare_pre)
|
|
apply (rule scheduler_equiv_lift'[where P="invs and (\<lambda>s. domain_time s \<noteq> 0)"])
|
|
apply (wp schedule_no_domain_switch schedule_no_domain_fields
|
|
silc_dom_lift | simp)+
|
|
apply (simp add: schedule_def)
|
|
apply (wp guarded_switch_to_lift
|
|
scheduler_equiv_lift
|
|
choose_thread_unobservable
|
|
set_scheduler_action_unobservable
|
|
tcb_sched_action_unobservable
|
|
switch_to_thread_unobservable silc_dom_lift | wpc | simp)+
|
|
apply (rule hoare_pre_cont)
|
|
apply (wp tcb_sched_action_unobservable | simp)+
|
|
apply (wp_once hoare_drop_imps)
|
|
apply (wp tcb_sched_action_unobservable gts_wp | simp)+
|
|
apply clarsimp
|
|
apply (intro impI conjI allI)
|
|
apply ((fastforce intro!: valid_sched_valid_queues dest!: switch_to_cur_domain cur_thread_cur_domain)+)[5]
|
|
apply (fastforce simp: st_tcb_at_def obj_at_def)
|
|
apply ((fastforce intro!: valid_sched_valid_queues dest!: switch_to_cur_domain cur_thread_cur_domain)+)
|
|
done
|
|
|
|
lemma schedule_reads_respects_scheduler_cur_domain: "reads_respects_scheduler aag l
|
|
(invs and pas_refined aag and valid_sched and
|
|
guarded_pas_domain aag and
|
|
(\<lambda>s. pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l)) schedule"
|
|
apply (simp add: schedule_def)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule bind_ev)
|
|
apply (rule bind_ev)
|
|
apply (rule bind_ev)
|
|
apply wpc
|
|
apply wp[1]
|
|
apply (rule bind_ev)
|
|
apply simp
|
|
apply (rule ev_weaken_pre_relation)
|
|
apply (rule guarded_switch_to_thread_midstrength_reads_respects_scheduler)
|
|
apply fastforce
|
|
apply (wp when_ev)[2]
|
|
apply (rule bind_ev)
|
|
apply simp
|
|
apply (rule next_domain_snippit)
|
|
apply (wp_trace when_ev gts_wp get_thread_state_reads_respects_scheduler)
|
|
apply (clarsimp simp: reads_lrefl)
|
|
apply (intro impI conjI allI)
|
|
apply (simp add: guarded_pas_domain_def)
|
|
apply (fastforce simp: reads_lrefl)
|
|
apply (simp add: invs_def valid_state_def)
|
|
apply (clarsimp simp add: scheduler_equiv_def)
|
|
apply (rule switch_to_cur_domain,simp+)
|
|
apply (simp add: valid_sched_def)
|
|
apply (clarsimp simp add: st_tcb_at_def obj_at_def)
|
|
apply (simp add: scheduler_equiv_def)
|
|
apply (rule switch_to_cur_domain,simp+)
|
|
apply (simp add: valid_sched_def)
|
|
done
|
|
|
|
definition tick_done where
|
|
"tick_done s \<equiv> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread"
|
|
|
|
lemma schedule_reads_respects_scheduler: "reads_respects_scheduler aag l
|
|
(invs and pas_refined aag and valid_sched and
|
|
guarded_pas_domain aag and tick_done) schedule"
|
|
apply (rule_tac P="\<lambda>s. pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l" in equiv_valid_cases)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule schedule_reads_respects_scheduler_cur_domain)
|
|
apply simp
|
|
apply (rule_tac P="\<lambda>s. domain_time s = 0" in equiv_valid_cases)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule reads_respects_scheduler_invisible_domain_switch)
|
|
apply (clarsimp simp: tick_done_def valid_sched_def)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule reads_respects_scheduler_invisible_no_domain_switch)
|
|
apply simp
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)+
|
|
done
|
|
|
|
lemma reschedule_required_scheduler_equiv[wp]: "\<lbrace>scheduler_equiv aag st\<rbrace> reschedule_required \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>"
|
|
apply (simp add: reschedule_required_def)
|
|
apply (wp scheduler_equiv_lift | wpc | simp)+
|
|
done
|
|
|
|
lemma switch_to_cur_domain': "valid_etcbs s \<Longrightarrow> valid_sched_action s \<Longrightarrow> scheduler_action s = switch_thread x \<Longrightarrow>
|
|
pas_refined aag s \<Longrightarrow> pasObjectAbs aag x = pasDomainAbs aag (cur_domain s)"
|
|
apply (clarsimp simp add: valid_sched_def
|
|
valid_sched_action_def
|
|
switch_in_cur_domain_def
|
|
in_cur_domain_def etcb_at_def
|
|
weak_valid_sched_action_def
|
|
is_etcb_at_def st_tcb_at_def
|
|
obj_at_def
|
|
valid_etcbs_def)
|
|
apply (drule_tac x=x in spec)
|
|
apply clarsimp
|
|
apply (drule(1) tcb_domain_wellformed)
|
|
apply simp
|
|
done
|
|
|
|
lemma reschedule_required_scheduler_affects_equiv_unobservable[wp]:
|
|
"\<lbrace>pas_refined aag and
|
|
(\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l) and
|
|
valid_queues and
|
|
valid_etcbs and
|
|
valid_sched_action and
|
|
scheduler_equiv aag st and
|
|
scheduler_affects_equiv aag l st\<rbrace>
|
|
reschedule_required \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: reschedule_required_def)
|
|
apply (wp set_scheduler_action_unobservable
|
|
tcb_sched_action_unobservable
|
|
| wpc | simp)+
|
|
apply ((fastforce intro!: valid_sched_valid_queues dest!: switch_to_cur_domain' cur_thread_cur_domain)+)
|
|
done
|
|
|
|
|
|
abbreviation is_domain where
|
|
"is_domain aag l s \<equiv> pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l"
|
|
|
|
lemma reads_respects_scheduler_cases':
|
|
assumes b: "reads_respects_scheduler aag l P' (f t)"
|
|
assumes b': "\<And>s. Q s \<Longrightarrow> pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l \<Longrightarrow> P' s"
|
|
assumes c: "reads_respects_scheduler aag l P'' (f t)"
|
|
assumes c': "\<And>s. Q s \<Longrightarrow> pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l \<Longrightarrow> P'' s"
|
|
shows "reads_respects_scheduler aag l Q (f t)"
|
|
apply (rule_tac P="\<lambda>s. pasDomainAbs aag (cur_domain s) \<in> reads_scheduler aag l" in equiv_valid_cases)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule b)
|
|
apply (simp add: b')
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule c)
|
|
apply (simp add: c')
|
|
apply (simp add: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
lemma reschedule_required_reads_respects_scheduler: "reads_respects_scheduler aag l (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action) reschedule_required"
|
|
apply (rule reads_respects_scheduler_cases')
|
|
apply (simp add: reschedule_required_def)
|
|
apply (wp | wpc)+
|
|
apply clarsimp
|
|
apply (rule reads_respects_scheduler_unobservable'')
|
|
apply (wp | simp | force)+
|
|
done
|
|
|
|
|
|
|
|
lemma dec_domain_time_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l \<top> dec_domain_time"
|
|
apply (simp add: dec_domain_time_def)
|
|
apply (wp ev_modify)
|
|
apply (fastforce simp add: scheduler_equiv_def
|
|
domain_fields_equiv_def
|
|
globals_equiv_scheduler_def
|
|
scheduler_globals_frame_equiv_def
|
|
silc_dom_equiv_def
|
|
equiv_for_def
|
|
scheduler_affects_equiv_def
|
|
states_equiv_for_def equiv_for_def
|
|
equiv_asids_def equiv_asid_def idle_equiv_def)
|
|
done
|
|
|
|
lemma ethread_set_reads_respects_scheduler: "reads_respects_scheduler aag l (\<lambda>s. pasObjectAbs aag t \<in> reads_scheduler aag l)
|
|
(ethread_set f t)"
|
|
apply (clarsimp simp add: thread_set_time_slice_def
|
|
ethread_set_def gets_the_def
|
|
gets_def get_def bind_def put_def get_etcb_def
|
|
return_def assert_opt_def set_eobject_def
|
|
fail_def equiv_valid_def2 equiv_valid_2_def
|
|
split: option.splits)
|
|
apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def idle_equiv_def
|
|
)
|
|
apply (rule conjI)
|
|
apply (clarsimp simp: silc_dom_equiv_def reads_scheduler_def
|
|
equiv_for_def
|
|
split: split_if_asm)
|
|
apply (simp add: scheduler_affects_equiv_def)
|
|
apply clarsimp
|
|
apply (rule conjI)
|
|
apply (rule states_equiv_for_identical_ekheap_updates,assumption)
|
|
apply (elim states_equiv_forE equiv_forE)
|
|
apply (clarsimp simp: identical_ekheap_updates_def)
|
|
apply (clarsimp simp: scheduler_globals_frame_equiv_def)
|
|
done
|
|
|
|
lemma ethread_set_time_slice_valid_queues[wp]: "\<lbrace>valid_queues\<rbrace> ethread_set (tcb_time_slice_update f) t \<lbrace>\<lambda>_. valid_queues\<rbrace>"
|
|
apply (simp add: ethread_set_def set_eobject_def)
|
|
apply (wp)
|
|
apply (clarsimp simp: get_etcb_def valid_sched_def
|
|
valid_etcbs_def is_etcb_at_def
|
|
valid_queues_def etcb_at'_def
|
|
valid_sched_action_def
|
|
weak_valid_sched_action_def
|
|
switch_in_cur_domain_def
|
|
ct_in_cur_domain_def
|
|
in_cur_domain_def)
|
|
apply (intro impI conjI allI ballI)
|
|
apply fastforce+
|
|
done
|
|
|
|
lemma ethread_set_time_slice_valid_sched_action[wp]: "\<lbrace>valid_sched_action\<rbrace> ethread_set (tcb_time_slice_update f) t \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
|
|
apply (simp add: ethread_set_def set_eobject_def)
|
|
apply (wp)
|
|
apply (clarsimp simp: get_etcb_def valid_sched_def
|
|
valid_etcbs_def is_etcb_at_def
|
|
valid_queues_def etcb_at'_def
|
|
valid_sched_action_def
|
|
weak_valid_sched_action_def
|
|
switch_in_cur_domain_def
|
|
ct_in_cur_domain_def
|
|
in_cur_domain_def)
|
|
done
|
|
|
|
lemma dec_domain_time_valid_queues[wp]: "\<lbrace>valid_queues\<rbrace> dec_domain_time \<lbrace>\<lambda>_. valid_queues\<rbrace>"
|
|
apply (simp add: dec_domain_time_def)
|
|
apply (wp | simp)+
|
|
done
|
|
|
|
lemma dec_domain_time_valid_etcbs[wp]: "\<lbrace>valid_etcbs\<rbrace> dec_domain_time \<lbrace>\<lambda>_. valid_etcbs\<rbrace>"
|
|
apply (simp add: dec_domain_time_def)
|
|
apply (wp | simp)+
|
|
done
|
|
|
|
lemma dec_domain_time_valid_sched_action[wp]: "\<lbrace>valid_sched_action\<rbrace> dec_domain_time \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
|
|
apply (simp add: dec_domain_time_def)
|
|
apply (wp | simp)+
|
|
done
|
|
|
|
|
|
lemma timer_tick_snippit:
|
|
"reads_respects_scheduler aag l (pas_refined aag and valid_queues and valid_etcbs and valid_sched_action)
|
|
(when (Suc 0 < num_domains)
|
|
(do x \<leftarrow> dec_domain_time;
|
|
dom_time \<leftarrow> gets domain_time;
|
|
when (dom_time = 0) reschedule_required
|
|
od))"
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (wp when_ev | wp_once hoare_drop_imps)+
|
|
apply (clarsimp simp: scheduler_equiv_def)
|
|
apply (wp reschedule_required_reads_respects_scheduler | wp_once hoare_drop_imps)+
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
|
|
|
|
lemma timer_tick_reads_respects_scheduler_cur_domain: "reads_respects_scheduler aag l (is_domain aag l and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) (timer_tick)"
|
|
apply (simp add: timer_tick_def)
|
|
apply (subst Let_def)
|
|
apply (subst thread_set_time_slice_def)+
|
|
apply (wp when_ev reschedule_required_reads_respects_scheduler
|
|
ethread_set_reads_respects_scheduler
|
|
get_thread_state_reads_respects_scheduler gts_wp
|
|
| wpc | wp_once hoare_drop_imps)+
|
|
apply (fastforce simp add: invs_def valid_state_def valid_idle_def
|
|
pred_tcb_at_def obj_at_def guarded_pas_domain_def
|
|
scheduler_equiv_def domain_fields_equiv_def
|
|
valid_sched_def valid_sched_action_def
|
|
split: split: option.splits)+
|
|
done
|
|
|
|
lemma ethread_set_unobservable[wp]:
|
|
"\<lbrace>(\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> ethread_set f t \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: ethread_set_def set_eobject_def)
|
|
apply wp
|
|
apply (clarsimp simp: get_etcb_def
|
|
scheduler_affects_equiv_def)
|
|
apply (elim states_equiv_forE equiv_forE)
|
|
apply (clarsimp simp: equiv_for_def states_equiv_for_def
|
|
equiv_asids_def equiv_asid_def)+
|
|
done
|
|
|
|
|
|
lemma timer_tick_reads_respects_scheduler_unobservable: "reads_respects_scheduler aag l ((\<lambda>s. \<not>is_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) (timer_tick)"
|
|
apply (simp add: timer_tick_def)
|
|
apply (subst Let_def)
|
|
apply (subst thread_set_time_slice_def)+
|
|
apply (simp add: bind_assoc[symmetric])
|
|
apply (rule bind_ev_pre)
|
|
apply (simp add: bind_assoc)
|
|
apply (rule timer_tick_snippit)
|
|
apply (rule_tac P=\<top> and P'="(\<lambda>s. \<not> is_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched" in reads_respects_scheduler_unobservable'')
|
|
apply (rule hoare_pre)
|
|
apply (rule scheduler_equiv_lift)
|
|
apply (wp gts_wp tcb_sched_action_unobservable
|
|
scheduler_equiv_lift| wpc | simp)+
|
|
apply (clarsimp simp: etcb_at_def split: option.splits)
|
|
apply (intro impI conjI allI)
|
|
apply (fastforce dest!: cur_thread_cur_domain)+
|
|
apply ((clarsimp simp add: st_tcb_at_def obj_at_def valid_sched_def)+)[3]
|
|
apply (fastforce dest!: cur_thread_cur_domain)
|
|
apply force
|
|
apply (wp gts_wp| wpc)+
|
|
apply (clarsimp simp: etcb_at_def valid_sched_def st_tcb_at_def
|
|
obj_at_def valid_sched_action_def split: option.splits)
|
|
done
|
|
|
|
lemma timer_tick_reads_respects_scheduler: "reads_respects_scheduler aag l (invs and guarded_pas_domain aag and pas_refined aag and valid_sched) (timer_tick)"
|
|
apply (rule reads_respects_scheduler_cases')
|
|
apply (rule timer_tick_reads_respects_scheduler_cur_domain)
|
|
apply simp
|
|
apply (rule timer_tick_reads_respects_scheduler_unobservable)
|
|
apply simp
|
|
done
|
|
|
|
|
|
lemma gets_ev': "equiv_valid_inv I A (P and K(\<forall>s t. P s \<longrightarrow> P t \<longrightarrow> I s t \<and> A s t \<longrightarrow> f s = f t)) (gets f)"
|
|
apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def
|
|
gets_def get_def bind_def
|
|
return_def)
|
|
done
|
|
|
|
lemma get_irq_state_reads_respects_scheduler_trivial: "reads_respects_scheduler aag l (domain_sep_inv False st) (get_irq_state irq)"
|
|
apply (simp add: get_irq_state_def)
|
|
apply (rule equiv_valid_guard_imp)
|
|
apply (rule_tac P="domain_sep_inv False st" in gets_ev')
|
|
apply clarsimp
|
|
apply (clarsimp simp: domain_sep_inv_def)
|
|
done
|
|
|
|
lemma dmo_ack_noop: "do_machine_op (ackInterrupt irq) = return ()"
|
|
apply (simp add: do_machine_op_def ackInterrupt_def
|
|
select_f_def return_def bind_def
|
|
gets_def get_def simpler_modify_def)
|
|
done
|
|
|
|
lemma resetTimer_underlying_memory[wp]: "\<lbrace>\<lambda>s. P(underlying_memory s)\<rbrace> resetTimer \<lbrace>\<lambda>r s. P (underlying_memory s)\<rbrace>"
|
|
apply (simp add: resetTimer_def machine_op_lift_def machine_rest_lift_def)
|
|
apply (wp | wpc| simp)+
|
|
done
|
|
|
|
lemma resetTimer_irq_state[wp]: "\<lbrace>\<lambda>s. P(irq_state s)\<rbrace> resetTimer \<lbrace>\<lambda>r s. P (irq_state s)\<rbrace>"
|
|
apply (simp add: resetTimer_def machine_op_lift_def machine_rest_lift_def)
|
|
apply (wp | wpc| simp)+
|
|
done
|
|
|
|
|
|
lemma dmo_resetTimer_underlying_memory[wp]: "\<lbrace>\<lambda>s. P(underlying_memory (machine_state s))\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r s. P (underlying_memory (machine_state s))\<rbrace>"
|
|
apply (wp dmo_wp | simp)+
|
|
done
|
|
|
|
lemma dmo_resetTimer_arch_state[wp]: "\<lbrace>\<lambda>s. P(arch_state s)\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
|
|
apply (wp dmo_wp | simp)+
|
|
done
|
|
|
|
lemma dmo_resetTimer_exclusive_state[wp]: "\<lbrace>\<lambda>s. P (exclusive_state (machine_state s))\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>r s. P (exclusive_state (machine_state s))\<rbrace>"
|
|
apply (wp dmo_mol_exclusive_state | simp add: resetTimer_def)+
|
|
done
|
|
|
|
lemma dmo_resetTimer_reads_respects_scheduler:
|
|
"reads_respects_scheduler aag l \<top> (do_machine_op resetTimer)"
|
|
apply (rule reads_respects_scheduler_unobservable)
|
|
apply (rule scheduler_equiv_lift)
|
|
apply (simp add: globals_equiv_scheduler_def[abs_def] idle_equiv_def)
|
|
apply (rule hoare_pre)
|
|
apply wps
|
|
apply wp
|
|
apply clarsimp
|
|
apply ((wp silc_dom_lift dmo_wp | simp)+)[5]
|
|
apply (rule scheduler_affects_equiv_unobservable)
|
|
apply (simp add: states_equiv_for_def[abs_def] equiv_for_def equiv_asids_def
|
|
equiv_asid_def)
|
|
apply (rule hoare_pre)
|
|
apply wps
|
|
apply (wp | simp)+
|
|
done
|
|
|
|
lemma irq_inactive_or_timer: "\<lbrace>domain_sep_inv False st and Q IRQTimer and Q IRQInactive\<rbrace> get_irq_state irq \<lbrace>Q\<rbrace>"
|
|
apply (simp add:get_irq_state_def)
|
|
apply wp
|
|
apply (clarsimp simp add: domain_sep_inv_def)
|
|
apply (drule_tac x=irq in spec)
|
|
apply (drule_tac x=a in spec) (*makes yellow variables*)
|
|
apply (drule_tac x=b in spec)
|
|
apply (drule_tac x=aa in spec, drule_tac x=ba in spec)
|
|
apply clarsimp
|
|
apply (case_tac "interrupt_states st irq")
|
|
apply clarsimp+
|
|
done
|
|
|
|
|
|
lemma handle_interrupt_reads_respects_scheduler:
|
|
"reads_respects_scheduler aag l (invs and guarded_pas_domain aag and pas_refined aag and valid_sched and domain_sep_inv False st) (handle_interrupt irq)"
|
|
apply (simp add: handle_interrupt_def dmo_ack_noop)
|
|
apply (wp)
|
|
apply (rule_tac Q="rv = IRQTimer \<or> rv = IRQInactive" in gen_asm_ev(2))
|
|
apply (elim disjE)
|
|
apply simp
|
|
apply (wp timer_tick_reads_respects_scheduler dmo_resetTimer_reads_respects_scheduler get_irq_state_reads_respects_scheduler_trivial fail_ev irq_inactive_or_timer | simp)+
|
|
apply force
|
|
done
|
|
|
|
|
|
(*FIXME: MOVE corres-like statement for out of step equiv_valid. Move to scheduler_IF?*)
|
|
lemma equiv_valid_2_bind_right:
|
|
"\<lbrakk>\<And>rv. equiv_valid_2 D A A R T' (Q rv) g' (g rv);
|
|
\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>; \<And>st. \<lbrace>D st and A st and S'\<rbrace> f \<lbrace>\<lambda>r. D st\<rbrace>; \<And>st. \<lbrace>A st and D st and S''\<rbrace> f \<lbrace>\<lambda>r. A st\<rbrace>;
|
|
\<And>s. T s \<Longrightarrow> P s \<and> S s \<and> S' s \<and> S'' s; \<And>s. T' s \<Longrightarrow> P s\<rbrakk>
|
|
\<Longrightarrow> equiv_valid_2 D A A R T' T g' (f >>= g) "
|
|
apply atomize
|
|
apply (clarsimp simp: equiv_valid_2_def equiv_valid_def2 valid_def bind_def)
|
|
apply fastforce
|
|
done
|
|
|
|
(*FIXME: Move to scheduler_IF*)
|
|
lemma reads_respects_only_scheduler: "reads_respects_scheduler aag SilcLabel P f \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) \<top>\<top> P f"
|
|
apply (simp add: equiv_valid_def2 equiv_valid_2_def scheduler_affects_equiv_def reads_scheduler_def
|
|
states_equiv_for_def equiv_for_def scheduler_equiv_def equiv_asids_def
|
|
equiv_asid_def globals_equiv_scheduler_def)
|
|
apply clarsimp
|
|
apply (drule_tac x=s in spec)
|
|
apply (drule_tac x=t in spec)
|
|
apply fastforce
|
|
done
|
|
|
|
(*FIXME: MOVE do_machine_op distributing over binds/basic operations*)
|
|
lemma dmo_distr: "do_machine_op (f >>= g) = ((do_machine_op f) >>= (\<lambda>x. (do_machine_op (g x))))"
|
|
apply (clarsimp simp: do_machine_op_def bind_assoc)
|
|
apply (clarsimp simp: gets_def simpler_modify_def select_f_def
|
|
bind_def get_def return_def)
|
|
apply (rule ext)
|
|
apply safe
|
|
apply clarsimp
|
|
apply force
|
|
apply clarsimp
|
|
apply force
|
|
apply clarsimp
|
|
apply force
|
|
apply clarsimp
|
|
apply force
|
|
apply (simp add: image_def)
|
|
done
|
|
|
|
lemma dmo_if_distr: "do_machine_op (if A then f else g) = (if A then (do_machine_op f) else (do_machine_op g))"
|
|
apply simp
|
|
done
|
|
|
|
lemma dmo_gets_distr: "do_machine_op (gets f) = (gets (\<lambda>s. f (machine_state s)))"
|
|
apply (clarsimp simp: do_machine_op_def bind_assoc)
|
|
apply (clarsimp simp: gets_def simpler_modify_def select_f_def
|
|
bind_def get_def return_def)
|
|
done
|
|
|
|
lemma dmo_modify_distr: "do_machine_op (modify f) = modify (machine_state_update f)"
|
|
apply (clarsimp simp: do_machine_op_def bind_assoc)
|
|
apply (clarsimp simp: gets_def simpler_modify_def select_f_def
|
|
bind_def get_def return_def)
|
|
apply (rule ext)
|
|
apply clarsimp
|
|
done
|
|
|
|
lemma dmo_return_distr: "do_machine_op (return x) = return x"
|
|
apply (clarsimp simp: do_machine_op_def bind_assoc)
|
|
apply (clarsimp simp: gets_def simpler_modify_def select_f_def
|
|
bind_def get_def return_def)
|
|
done
|
|
|
|
(*FIXME: Move to scheduler_if*)
|
|
lemma dmo_getActive_IRQ_reads_respect_scheduler: "reads_respects_scheduler aag l (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)
|
|
(do_machine_op getActiveIRQ)"
|
|
apply (simp add: getActiveIRQ_def)
|
|
apply (simp add: dmo_distr dmo_if_distr dmo_gets_distr dmo_modify_distr dmo_return_distr cong: if_cong)
|
|
apply wp
|
|
apply (rule ev_modify[where P=\<top>])
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def)
|
|
apply (clarsimp simp add: scheduler_affects_equiv_def states_equiv_for_def
|
|
equiv_for_def equiv_asids_def equiv_asid_def
|
|
scheduler_globals_frame_equiv_def silc_dom_equiv_def
|
|
idle_equiv_def
|
|
)
|
|
apply wp_once
|
|
apply (rule_tac P="\<lambda>s. irq_masks_of_state st = irq_masks_of_state s" in gets_ev')
|
|
apply wp
|
|
apply clarsimp
|
|
apply (simp add: scheduler_equiv_def)
|
|
done
|
|
|
|
definition idle_context where "idle_context s = tcb_context (the (get_tcb (idle_thread s) s))"
|
|
|
|
lemma thread_set_context_globals_equiv: "\<lbrace>(\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and invs and globals_equiv st\<rbrace> thread_set (tcb_context_update (\<lambda>_. tc)) t \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>"
|
|
apply (clarsimp simp: thread_set_def set_object_def)
|
|
apply wp
|
|
apply clarsimp
|
|
apply (subgoal_tac "t \<noteq> arm_global_pd (arch_state s)")
|
|
apply (clarsimp simp: idle_equiv_def globals_equiv_def tcb_at_def2 get_tcb_def idle_context_def)
|
|
apply (clarsimp split: option.splits kernel_object.splits)
|
|
apply (drule arm_global_pd_not_tcb[OF invs_valid_ko_at_arm])
|
|
apply clarsimp
|
|
done
|
|
|
|
lemma thread_set_scheduler_equiv[wp]: "\<lbrace>(invs and K(pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s)) and scheduler_equiv aag st\<rbrace>
|
|
thread_set (tcb_context_update (\<lambda>_. tc)) t
|
|
\<lbrace>\<lambda>r. scheduler_equiv aag st\<rbrace>"
|
|
apply (rule scheduler_equiv_lift')
|
|
apply (rule globals_equiv_scheduler_inv')
|
|
apply (wp thread_set_context_globals_equiv | clarsimp intro!: invs_valid_ko_at_arm)+
|
|
apply (simp add: silc_dom_equiv_def thread_set_def)
|
|
apply (wp set_object_wp)
|
|
apply (clarsimp simp: get_tcb_def equiv_for_def split: kernel_object.splits option.splits)
|
|
done
|
|
|
|
lemma thread_set_scheduler_affects_equiv[wp]: "\<lbrace>(\<lambda>s. x \<noteq> idle_thread s \<longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l) and (\<lambda>s. x = idle_thread s \<longrightarrow> tc = idle_context s) and scheduler_affects_equiv aag l st\<rbrace> thread_set (tcb_context_update (\<lambda>_. tc)) x
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: thread_set_def)
|
|
apply (wp set_object_wp)
|
|
apply (intro impI conjI)
|
|
apply (case_tac "x \<noteq> idle_thread s",simp_all)
|
|
apply (clarsimp simp: scheduler_affects_equiv_def get_tcb_def
|
|
scheduler_globals_frame_equiv_def split: option.splits kernel_object.splits)
|
|
apply (elim states_equiv_forE equiv_forE)
|
|
apply (rule states_equiv_forI,simp_all add: equiv_for_def equiv_asids_def equiv_asid_def)
|
|
apply (clarsimp simp: obj_at_def)
|
|
apply (clarsimp simp: idle_context_def get_tcb_def
|
|
split: option.splits kernel_object.splits)
|
|
apply (subgoal_tac "s = (s\<lparr>kheap := kheap s(idle_thread s \<mapsto> TCB y)\<rparr>)",simp)
|
|
apply (rule state.equality)
|
|
apply (rule ext)
|
|
apply simp+
|
|
done
|
|
|
|
|
|
lemma silc_inv_not_cur_thread: "silc_inv aag st s \<Longrightarrow> invs s \<Longrightarrow> pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel"
|
|
apply (clarsimp simp: silc_inv_def)
|
|
apply (drule_tac x="(cur_thread s)" in spec)
|
|
apply clarsimp
|
|
apply (clarsimp simp add: obj_at_def invs_def cur_tcb_def
|
|
is_cap_table_def is_tcb_def)
|
|
apply (case_tac ko,simp_all)
|
|
done
|
|
|
|
lemma get_tcb_scheduler_equiv: "\<lbrakk>pasObjectAbs aag rv \<in> reads_scheduler aag l;
|
|
scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow>
|
|
get_tcb rv s = get_tcb rv t"
|
|
apply (clarsimp simp: get_tcb_def scheduler_affects_equiv_def
|
|
states_equiv_for_def equiv_for_def
|
|
split: option.splits kernel_object.splits)
|
|
done
|
|
|
|
|
|
lemma idle_equiv_identical_kheap_updates: "identical_kheap_updates s t kh kh' \<Longrightarrow> idle_equiv s t \<Longrightarrow> idle_equiv (s\<lparr>kheap := kh\<rparr>) (t\<lparr>kheap := kh'\<rparr>)"
|
|
apply (clarsimp simp add: identical_kheap_updates_def idle_equiv_def
|
|
tcb_at_def2)
|
|
apply (drule_tac x="idle_thread t" in spec)
|
|
apply fastforce
|
|
done
|
|
|
|
lemma set_object_reads_respects_scheduler[wp]:
|
|
"reads_respects_scheduler aag l \<top> (set_object ptr obj)"
|
|
unfolding equiv_valid_def2 equiv_valid_2_def
|
|
apply(clarsimp simp: set_object_def bind_def get_def put_def return_def
|
|
scheduler_equiv_def domain_fields_equiv_def
|
|
globals_equiv_scheduler_def silc_dom_equiv_def)
|
|
apply (clarsimp simp: equiv_for_def scheduler_affects_equiv_def
|
|
scheduler_globals_frame_equiv_def identical_kheap_updates_def
|
|
intro!: states_equiv_for_identical_kheap_updates idle_equiv_identical_kheap_updates)
|
|
apply (intro conjI impI)
|
|
apply (clarsimp simp: equiv_for_def scheduler_affects_equiv_def
|
|
scheduler_globals_frame_equiv_def identical_kheap_updates_def
|
|
| rule states_equiv_for_identical_kheap_updates idle_equiv_identical_kheap_updates)+
|
|
done
|
|
|
|
lemma sts_reads_respects_scheduler: "reads_respects_scheduler aag l (K(pasObjectAbs aag rv \<in> reads_scheduler aag l) and is_domain aag l and valid_idle and (\<lambda>s. rv \<noteq> idle_thread s))
|
|
(set_thread_state rv st)"
|
|
apply (simp add: set_thread_state_def)
|
|
apply (simp add: set_thread_state_ext_def)
|
|
apply (wp when_ev get_thread_state_reads_respects_scheduler
|
|
gts_wp set_object_wp)
|
|
apply (clarsimp simp: get_tcb_scheduler_equiv)
|
|
apply (clarsimp simp: valid_idle_def pred_tcb_at_def
|
|
obj_at_def)
|
|
done
|
|
|
|
|
|
lemma as_user_reads_respects_scheduler: "reads_respects_scheduler aag l (K(pasObjectAbs aag rv \<in> reads_scheduler aag l) and (\<lambda>s. rv \<noteq> idle_thread s) and K(det f))
|
|
(as_user rv f)"
|
|
apply (rule gen_asm_ev)
|
|
apply (simp add: as_user_def)
|
|
apply (wp select_f_ev | wpc | simp)+
|
|
apply (clarsimp simp: get_tcb_scheduler_equiv)
|
|
done
|
|
|
|
lemma restart_not_idle: "valid_idle s \<Longrightarrow> st_tcb_at (op = Restart) t s \<Longrightarrow> t \<noteq> idle_thread s"
|
|
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
|
|
done
|
|
|
|
lemma sts_silc_dom_equiv[wp]: "\<lbrace>K(pasObjectAbs aag x \<noteq> SilcLabel) and silc_dom_equiv aag st\<rbrace> set_thread_state x f
|
|
\<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>"
|
|
apply (simp add: set_thread_state_def)
|
|
apply (wp dxo_wp_weak set_object_wp | simp)+
|
|
apply (clarsimp simp: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
lemma as_user_silc_dom_equiv[wp]: "\<lbrace>K(pasObjectAbs aag x \<noteq> SilcLabel) and silc_dom_equiv aag st\<rbrace> as_user x f
|
|
\<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>"
|
|
apply (simp add: as_user_def)
|
|
apply (wp dxo_wp_weak set_object_wp | wpc | simp)+
|
|
apply (clarsimp simp: silc_dom_equiv_def equiv_for_def)
|
|
done
|
|
|
|
lemma scheduler_affects_equiv_update: "\<lbrakk>get_tcb x s = Some y;
|
|
pasObjectAbs aag x \<notin> reads_scheduler aag l;
|
|
scheduler_affects_equiv aag l st s\<rbrakk>
|
|
\<Longrightarrow> scheduler_affects_equiv aag l st
|
|
(s\<lparr>kheap := kheap s(x \<mapsto> TCB y')\<rparr>)"
|
|
apply (clarsimp simp: scheduler_affects_equiv_def
|
|
states_equiv_for_def equiv_for_def
|
|
equiv_asids_def equiv_asid_def)
|
|
apply (clarsimp simp: scheduler_globals_frame_equiv_def)
|
|
apply (clarsimp simp: obj_at_def st_tcb_at_def get_tcb_def)
|
|
done
|
|
|
|
lemma set_scheduler_action_wp[wp]:
|
|
"\<lbrace>\<lambda>s. P () (s\<lparr>scheduler_action := a\<rparr>)\<rbrace> set_scheduler_action a \<lbrace>P\<rbrace>"
|
|
apply(simp add: set_scheduler_action_def | wp)+
|
|
done
|
|
|
|
lemma sts_scheduler_affects_equiv[wp]: "\<lbrace>K(pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> set_thread_state x Running
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: set_thread_state_def)
|
|
apply (simp add: set_thread_state_ext_def)
|
|
|
|
apply (wp gts_wp set_object_wp)
|
|
apply (intro impI conjI allI)
|
|
apply (clarsimp simp: st_tcb_at_def obj_at_def)
|
|
apply (fastforce intro!: scheduler_affects_equiv_update)
|
|
done
|
|
|
|
|
|
lemma as_user_scheduler_affects_equiv[wp]: "\<lbrace>K(pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> as_user x f
|
|
\<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>"
|
|
apply (simp add: as_user_def)
|
|
|
|
apply (wp gts_wp set_object_wp | wpc)+
|
|
apply (intro impI conjI allI)
|
|
apply (fastforce intro!: scheduler_affects_equiv_update)
|
|
done
|
|
|
|
lemma activate_thread_reads_respects_scheduler[wp]: "reads_respects_scheduler aag l (invs and silc_inv aag st and guarded_pas_domain aag) activate_thread"
|
|
apply (simp add: activate_thread_def)
|
|
apply (rule reads_respects_scheduler_cases')
|
|
apply ((wp sts_reads_respects_scheduler get_thread_state_reads_respects_scheduler gts_wp
|
|
as_user_reads_respects_scheduler | wpc
|
|
| simp add: setNextPC_det arch_activate_idle_thread_def)+)[1]
|
|
apply (intro impI conjI allI)
|
|
apply (clarsimp simp: getRestartPC_det guarded_pas_domain_def
|
|
restart_not_idle invs_valid_idle)+
|
|
apply (rule reads_respects_scheduler_unobservable''[where P'="\<lambda>s. pasDomainAbs aag (cur_domain s) \<notin> reads_scheduler aag l \<and> guarded_pas_domain aag s \<and> invs s"])
|
|
apply ((wp scheduler_equiv_lift'[where P="invs and silc_inv aag st"] globals_equiv_scheduler_inv'[where P="valid_ko_at_arm and valid_idle"] set_thread_state_globals_equiv gts_wp | wpc | clarsimp simp add: arch_activate_idle_thread_def restart_not_idle invs_valid_ko_at_arm silc_inv_not_cur_thread | force)+)[1]
|
|
apply (wp gts_wp| wpc | simp add: arch_activate_idle_thread_def)+
|
|
apply (clarsimp simp add: guarded_pas_domain_def restart_not_idle
|
|
invs_valid_idle)
|
|
apply force+
|
|
done
|
|
|
|
|
|
(*A function that is agnostic of its parameter with respect
|
|
to the state space (as is the case with thread context updates)
|
|
can be lifted to equiv_valid_2 over that parameter*)
|
|
lemma agnostic_to_ev2:
|
|
assumes param_agnostic: "\<forall>P Q u u'. \<lbrace>P\<rbrace> (f u) \<lbrace>\<lambda>_. Q\<rbrace> \<longrightarrow> \<lbrace>P\<rbrace> (f u') \<lbrace>\<lambda>_. Q\<rbrace>"
|
|
assumes ret_agnostic: "\<And>u. \<lbrace>\<top>\<rbrace> (f u) \<lbrace>\<lambda>r s. r = g u\<rbrace>"
|
|
assumes ev: "\<And>u. equiv_valid I A B P (f u)"
|
|
shows "equiv_valid_2 I A B (\<lambda>r r'. r = (g u) \<and> r' = (g u')) P P (f u) (f u')"
|
|
proof -
|
|
have b: "\<And>a b s u. (a,b) \<in> fst (f u s) \<Longrightarrow> a = g u"
|
|
|
|
apply (erule use_valid[OF _ ret_agnostic])
|
|
apply simp
|
|
done
|
|
have a: "\<And>a b u u' s. (a,b) \<in> fst (f u s) \<Longrightarrow> \<exists>a'. (a',b) \<in> fst (f u' s)"
|
|
apply (cut_tac P="\<lambda>sa. sa = s" and Q="\<lambda>s'. \<exists>a'. (a',s') \<in> fst (f u' s)" and u=u' and u'=u in param_agnostic[rule_format])
|
|
apply (clarsimp simp: valid_def)
|
|
apply force
|
|
apply (clarsimp simp: valid_def)
|
|
apply (drule_tac x="(a,b)" in bspec)
|
|
apply simp
|
|
apply clarsimp
|
|
done
|
|
show ?thesis
|
|
apply (cut_tac u=u in ev)
|
|
apply (cut_tac u=u' in ev)
|
|
apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def)
|
|
apply (frule a[where u=u and u'=u'])
|
|
apply clarsimp
|
|
apply (frule b[where u=u])
|
|
apply (frule b[where u=u'])
|
|
apply fastforce
|
|
done
|
|
qed
|
|
|
|
lemma bind_return_ign: "\<lbrace>P\<rbrace> (f >>= (\<lambda>_. return x)) \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> (f >>= (\<lambda>_. return y)) \<lbrace>\<lambda>_. Q\<rbrace>"
|
|
apply (fastforce simp: valid_def bind_def return_def)
|
|
done
|
|
|
|
|
|
lemma thread_set_reads_respect_scheduler[wp]: "reads_respects_scheduler aag l (invs and K(pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) (thread_set (tcb_context_update (\<lambda>_. tc)) t)"
|
|
apply (rule reads_respects_scheduler_cases[where P'=\<top>])
|
|
prefer 3
|
|
apply (rule reads_respects_scheduler_unobservable'')
|
|
apply (wp | simp | elim conjE)+
|
|
apply (simp add: thread_set_def)
|
|
apply (wp)
|
|
apply (fastforce simp: scheduler_affects_equiv_def get_tcb_def
|
|
states_equiv_for_def equiv_for_def scheduler_equiv_def
|
|
domain_fields_equiv_def
|
|
equiv_asids_def equiv_asid_def split: option.splits
|
|
kernel_object.splits)+
|
|
done
|
|
|
|
lemma op_eq_unit_dc: "((op = ) :: unit \<Rightarrow> unit \<Rightarrow> bool) = (dc)"
|
|
apply (rule ext)+
|
|
apply simp
|
|
done
|
|
|
|
lemma cur_thread_idle': "valid_idle s \<Longrightarrow> only_idle s \<Longrightarrow> ct_idle s = (cur_thread s = idle_thread s)"
|
|
apply (rule iffI)
|
|
apply (clarsimp simp: only_idle_def ct_in_state_def )
|
|
apply (clarsimp simp: valid_idle_def ct_in_state_def pred_tcb_at_def obj_at_def)
|
|
done
|
|
|
|
lemma cur_thread_idle: "invs s \<Longrightarrow> ct_idle s = (cur_thread s = idle_thread s)"
|
|
apply (rule cur_thread_idle')
|
|
apply (simp add: invs_def valid_state_def)+
|
|
done
|
|
|
|
lemma context_update_cur_thread_snippit_unobservable: "equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l)
|
|
(scheduler_affects_equiv aag l) op = (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> is_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. \<not> is_domain aag l s) and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s))
|
|
(gets cur_thread >>= thread_set (tcb_context_update (\<lambda>_. uc)))
|
|
(gets cur_thread >>= thread_set (tcb_context_update (\<lambda>_. uc')))"
|
|
apply (rule equiv_valid_2_guard_imp)
|
|
apply (simp add: op_eq_unit_dc)
|
|
apply (rule equiv_valid_2_unobservable)
|
|
apply (wp | elim conjE | simp add: dc_def)+
|
|
apply fastforce
|
|
apply fastforce
|
|
apply (clarsimp simp: guarded_pas_domain_def
|
|
silc_inv_not_cur_thread cur_thread_idle)+
|
|
done
|
|
|
|
lemma context_update_cur_thread_snippit_cur_domain: "reads_respects_scheduler aag l (\<lambda>s. is_domain aag l s \<and> invs s \<and>
|
|
silc_inv aag st s \<and>
|
|
(ct_idle s \<longrightarrow> uc = idle_context s) \<and>
|
|
guarded_pas_domain aag s)
|
|
(gets cur_thread >>= thread_set (tcb_context_update (\<lambda>_. uc)))"
|
|
apply wp
|
|
apply (clarsimp simp: cur_thread_idle silc_inv_not_cur_thread del: notI)
|
|
done
|
|
|
|
(*If we have to do this again we might consider an equiv_valid_2
|
|
case splitting rule*)
|
|
lemma context_update_cur_thread_snippit: "equiv_valid_2 (scheduler_equiv aag) (scheduler_affects_equiv aag l)
|
|
(scheduler_affects_equiv aag l) op = (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. is_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc = idle_context s)) (invs and silc_inv aag st and guarded_pas_domain aag and (\<lambda>s. is_domain aag l s \<longrightarrow> uc = uc') and (\<lambda>s. ct_idle s \<longrightarrow> uc' = idle_context s))
|
|
(gets cur_thread >>= thread_set (tcb_context_update (\<lambda>_. uc)))
|
|
(gets cur_thread >>= thread_set (tcb_context_update (\<lambda>_. uc')))"
|
|
apply (insert context_update_cur_thread_snippit_cur_domain[where aag=aag and l=l and uc=uc and st=st])
|
|
apply (insert context_update_cur_thread_snippit_unobservable[where aag=aag and l=l and uc=uc and uc'=uc' and st=st])
|
|
apply (clarsimp simp: equiv_valid_2_def equiv_valid_def2)
|
|
apply (drule_tac x=s in spec)
|
|
apply (drule_tac x=s in spec)
|
|
apply (drule_tac x=t in spec)
|
|
apply (drule_tac x=t in spec)
|
|
apply clarsimp
|
|
apply (subgoal_tac "is_domain aag l t = is_domain aag l s")
|
|
apply clarsimp
|
|
apply (case_tac "is_domain aag l s")
|
|
apply ((fastforce)+)[2]
|
|
apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def)
|
|
done
|
|
|
|
|
|
|
|
|
|
lemma equiv_valid_2E:
|
|
assumes ev: "equiv_valid_2 I A B R P P' f g"
|
|
assumes f: "(a,s') \<in> fst (f s)"
|
|
assumes g: "(b,t') \<in> fst (g t)"
|
|
assumes I: "I s t \<and> A s t"
|
|
assumes P: "P s"
|
|
assumes P': "P' t"
|
|
assumes Q: "I s' t' \<Longrightarrow> B s' t' \<Longrightarrow> R a b \<Longrightarrow> S"
|
|
shows S
|
|
apply (insert ev)
|
|
apply (clarsimp simp: equiv_valid_2_def)
|
|
apply (drule_tac x=s in spec)
|
|
apply (drule_tac x=t in spec)
|
|
apply (simp add: I P P')
|
|
apply (drule bspec[OF _ f],simp)
|
|
apply (drule bspec[OF _ g],simp)
|
|
apply (rule Q,simp+)
|
|
done
|
|
|
|
lemma ev2_sym:
|
|
assumes
|
|
symI: "\<And> x y. I x y \<Longrightarrow> I y x"
|
|
assumes
|
|
symA: "\<And> x y. A x y \<Longrightarrow> A y x"
|
|
assumes
|
|
symB: "\<And> x y. B x y \<Longrightarrow> B y x"
|
|
assumes
|
|
symR: "\<And> x y. R x y \<Longrightarrow> R' y x"
|
|
shows
|
|
"equiv_valid_2 I A B R P' P f' f \<Longrightarrow>
|
|
equiv_valid_2 I A B R' P P' f f'"
|
|
apply(clarsimp simp: equiv_valid_2_def)
|
|
apply(blast intro: symA symB symI symR)
|
|
done
|
|
|
|
lemma SilcLabel_affects_scheduler_equiv:
|
|
"scheduler_equiv aag s t \<Longrightarrow> scheduler_affects_equiv aag SilcLabel s t"
|
|
apply (simp add: scheduler_affects_equiv_def reads_scheduler_def
|
|
states_equiv_for_def equiv_for_def scheduler_equiv_def equiv_asids_def
|
|
equiv_asid_def globals_equiv_scheduler_def)
|
|
done
|
|
|
|
end
|