adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Revert SELFOUR-242: invert bitfield scheduler and optimise fast path 

This reverts:
- a67b443ca5
    "SELFOUR-242: update goal number based indentation in Fastpath_C"
- f704cf0404
    "SELFOUR-242: invert bitfield scheduler and optimise fast path"

Verification confirmed functional correctness and refinement of the
system in this case. However, guarantees on thread scheduling and
fairness are not modeled in the current verification. Once this issue is
addressed, SELFOUR-242 will be re-examined.
This commit is contained in:
Rafal Kolanski 2016-11-16 14:02:03 +11:00
parent 4262cc231a
commit 72349f81fd
30 changed files with 1982 additions and 2500 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
lib/LemmaBucket.thy
View File

@ -440,9 +440,4 @@ lemma list_ran_prop:"map_of (map (\<lambda>x. (f x, g x)) xs) i = Some t \<Longr
lemma in_set_enumerate_eq2:"(a, b) \<in> set (enumerate n xs) \<Longrightarrow> (b = xs ! (a - n))"
by (simp add: in_set_enumerate_eq)
lemma nat_divide_less_eq:
fixes b :: nat
shows "0 < c \<Longrightarrow> (b div c < a) = (b < a * c)"
using td_gal_lt by blast
end

6
lib/Monad_WP/NonDetMonadLemmas.thy
View File

@ -126,15 +126,9 @@ lemma when_False [simp]: "when False X = return ()"
lemma unless_False [simp]: "unless False X = X"
by (clarsimp simp: unless_def)
lemma unlessE_False [simp]: "unlessE False f = f"
unfolding unlessE_def by fastforce
lemma unless_True [simp]: "unless True X = return ()"
by (clarsimp simp: unless_def)
lemma unlessE_True [simp]: "unlessE True f = returnOk ()"
unfolding unlessE_def by fastforce
lemma unlessE_whenE:
"unlessE P = whenE (~P)"
by (rule ext)+ (simp add: unlessE_def whenE_def)

95
lib/Word_Lib/Word_Lemmas.thy
View File

@ -5377,99 +5377,4 @@ lemma ucast_le_ucast:
apply simp
done
lemma word_le_not_less:
"((b::'a::len word) \<le> a) = (\<not>(a < b))"
by fastforce
lemma nat_add_less_by_max:
"\<lbrakk> (x::nat) \<le> xmax ; y < k - xmax \<rbrakk> \<Longrightarrow> x + y < k"
by simp
lemma ucast_or_distrib:
fixes x :: "'a::len word"
fixes y :: "'a::len word"
shows "(ucast (x || y) :: ('b::len) word) = ucast x || ucast y"
unfolding ucast_def Word.bitOR_word.abs_eq uint_or
by blast
lemma shiftr_less:
"(w::'a::len word) < k \<Longrightarrow> w >> n < k"
apply (simp add: word_less_nat_alt shiftr_div_2n')
apply (blast intro: div_le_dividend le_less_trans)
done
lemma word_and_notzeroD:
"w && w' \<noteq> 0 \<Longrightarrow> w \<noteq> 0 \<and> w' \<noteq> 0"
by auto
lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
apply (cut_tac m = q and n = c in mod_less_divisor)
apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
apply (simp add: add_mult_distrib2)
done
lemma nat_Suc_less_le_imp:
"(k::nat) < Suc n \<Longrightarrow> k \<le> n"
by auto
lemma word_clz_max:
"word_clz w \<le> size (w::'a::len word)"
unfolding word_clz_def
apply (simp add: word_size)
apply (rule_tac y="length (to_bl w)" in order_trans)
apply (rule List.length_takeWhile_le)
apply simp
done
lemma word_clz_nonzero_max:
fixes w :: "'a::len word"
assumes nz: "w \<noteq> 0"
shows "word_clz w < size (w::'a::len word)"
proof -
{
assume a: "word_clz w = size (w::'a::len word)"
hence "length (takeWhile Not (to_bl w)) = length (to_bl w)"
by (simp add: word_clz_def word_size)
hence allj: "\<forall>j\<in>set(to_bl w). \<not> j"
using takeWhile_take_has_property[where n="length (to_bl w)" and xs="to_bl w" and P=Not]
by simp
hence "to_bl w = replicate (length (to_bl w)) False"
by - (blast intro: list_of_false)
hence "w = 0"
apply simp
apply (subst (asm) to_bl_0[symmetric])
apply (drule Word.word_bl.Rep_eqD, assumption)
done
with nz have False by simp
}
thus ?thesis using word_clz_max
by (fastforce intro: le_neq_trans)
qed
lemma unat_add_lem':
"(unat x + unat y < 2 ^ len_of TYPE('a)) \<Longrightarrow>
(unat (x + y :: 'a :: len word) = unat x + unat y)"
by (subst unat_add_lem[symmetric], assumption)
lemma from_bool_eq_if':
"((if P then 1 else 0) = from_bool Q) = (P = Q)"
by (simp add: case_bool_If from_bool_def split: split_if)
lemma word_exists_nth:
"(w::'a::len word) \<noteq> 0 \<Longrightarrow> \<exists>i. w !! i"
using word_log2_nth_same by blast
lemma shiftr_le_0:
"unat (w::'a::len word) < 2 ^ n \<Longrightarrow> w >> n = (0::'a::len word)"
by (rule word_unat.Rep_eqD) (simp add: shiftr_div_2n')
lemma of_nat_shiftl:
"(of_nat x << n) = (of_nat (x * 2 ^ n) :: ('a::len) word)"
proof -
have "(of_nat x::'a word) << n = of_nat (2 ^ n) * of_nat x"
using shiftl_t2n by (metis word_unat_power)
thus ?thesis by simp
qed
end

7
lib/clib/Corres_UL_C.thy
View File

@ -1646,11 +1646,4 @@ lemma ccorres_name_pre:
apply simp
done
(* using subst bind_assoc[symmetric] works, but causes flex-flex pairs in ccorres proofs
using simp won't create flex-flex pairs, but will rearrange everything *)
lemma ccorres_lhs_assoc:
assumes cc: "ccorres_underlying sr E r xf arrel axf G G' hs (m >>= f >>= g) c"
shows "ccorres_underlying sr E r xf arrel axf G G' hs (do x \<leftarrow> m; f x >>= g od) c"
using cc by (simp add: bind_assoc)
end

7
lib/clib/Ctac.thy
View File

@ -1985,13 +1985,6 @@ lemma finish_ceqv_Seq_Skip_cases:
"(y = Skip \<and> (x ;; y) = z \<or> (x ;; y) = (x ;; y))"
by simp_all
lemma semantic_equiv_IF_True:
"semantic_equiv G s s' (IF True THEN c ELSE c' FI) c"
apply (simp add: semantic_equiv_seq_assoc_eq[symmetric])
by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros)
lemmas ccorres_IF_True = ccorres_semantic_equiv[OF semantic_equiv_IF_True]
ML {*
fun tac ctxt =
resolve_tac ctxt [@{thm ccorres_abstract[where xf'="\<lambda>s. ()"]}] 1

4
proof/crefine/ADT_C.thy
View File

@ -1418,10 +1418,10 @@ where
"cbitmap_L1_to_H l1 \<equiv> \<lambda>d. if d \<le> maxDomain then l1.[unat d] else 0"
definition
cbitmap_L2_to_H :: "32 word[8][16] \<Rightarrow> (8 word \<times> nat \<Rightarrow> 32 word)"
cbitmap_L2_to_H :: "32 word[9][16] \<Rightarrow> (8 word \<times> nat \<Rightarrow> 32 word)"
where
"cbitmap_L2_to_H l2 \<equiv> \<lambda>(d, i).
if d \<le> maxDomain \<and> i < l2BitmapSize
if d \<le> maxDomain \<and> i \<le> numPriorities div wordBits
then l2.[unat d].[i] else 0"
lemma cbitmap_L1_to_H_correct:

2246
proof/crefine/Fastpath_C.thy
View File

File diff suppressed because it is too large Load Diff

2
proof/crefine/Finalise_C.thy
View File

@ -16,7 +16,7 @@ context kernel_m
begin
lemma switchIfRequiredTo_ccorres [corres]:
"ccorres dc xfdc (valid_queues and valid_objs' and tcb_at' thread and (\<lambda>s. ksCurDomain s \<le> maxDomain)
"ccorres dc xfdc (valid_queues and valid_objs' and tcb_at' thread
and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' thread)
(UNIV \<inter> \<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
(switchIfRequiredTo thread)

653
proof/crefine/IpcCancel_C.thy
View File

@ -12,21 +12,29 @@ theory IpcCancel_C
imports SyscallArgs_C
begin
lemma unat_of_nat_shiftl_or_8_32: (* FIXME generalise *)
"\<lbrakk> x * 2 ^ n < 256 ; y < 256 \<rbrakk>
\<Longrightarrow> unat (((of_nat x << n) :: 8 word) || of_nat y :: 8 word) = unat (((of_nat x << n):: machine_word) || of_nat y :: machine_word)"
apply (subst unat_ucast_upcast[where 'b=8 and 'a=32,symmetric])
apply (simp add: is_up)
apply (subst ucast_or_distrib)
apply (subst of_nat_shiftl)
apply (subst ucast_of_nat_small, simp)
apply (subst ucast_of_nat_small, simp)
apply (simp add: of_nat_shiftl)
(* FIXME MOVE *)
lemma shiftr_less:
"(w::'a::len word) < k \<Longrightarrow> w >> n < k"
apply (simp add: word_less_nat_alt shiftr_div_2n')
apply (blast intro: div_le_dividend le_less_trans)
done
(* FIXME move *)
lemma word_and_notzeroD:
"w && w' \<noteq> 0 \<Longrightarrow> w \<noteq> 0 \<and> w' \<noteq> 0"
by auto
context kernel_m
begin
(* TODO: move *)
lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
apply (cut_tac m = q and n = c in mod_less_divisor)
apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
apply (simp add: add_mult_distrib2)
done
lemma cready_queues_index_to_C_in_range':
assumes prems: "qdom \<le> ucast maxDom" "prio \<le> ucast maxPrio"
shows "cready_queues_index_to_C qdom prio < numDomains * numPriorities"
@ -873,13 +881,6 @@ lemma prio_to_l1index_spec:
\<lbrace>\<acute>ret__unsigned_long = prio_' s >> wordRadix \<rbrace>"
by vcg (simp add: word_sle_def wordRadix_def')
lemma invert_l1index_spec:
"\<forall>s. \<Gamma> \<turnstile> {s} Call invert_l1index_'proc
\<lbrace>\<acute>ret__unsigned_long = of_nat l2BitmapSize - 1 - l1index_' s \<rbrace>"
unfolding l2BitmapSize_def'
by vcg
(simp add: word_sle_def sdiv_int_def sdiv_word_def smod_word_def smod_int_def)
lemma cbitmap_L1_relation_update:
"\<lbrakk> (\<sigma>, s) \<in> rf_sr ; cbitmap_L1_relation cupd aupd \<rbrakk>
\<Longrightarrow> (\<sigma>\<lparr>ksReadyQueuesL1Bitmap := aupd \<rparr>,
@ -914,7 +915,7 @@ lemma machine_word_and_1F_less_20:
by (rule word_and_less', simp)
lemma prio_ucast_shiftr_wordRadix_helper: (* FIXME generalise *)
"(ucast (p::priority) >> wordRadix :: machine_word) < 8"
"(ucast (p::priority) >> wordRadix :: machine_word) < 9"
unfolding maxPriority_def numPriorities_def wordRadix_def
using unat_lt2p[where x=p]
apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt)
@ -922,7 +923,7 @@ lemma prio_ucast_shiftr_wordRadix_helper: (* FIXME generalise *)
done
lemma prio_ucast_shiftr_wordRadix_helper': (* FIXME generalise *)
"(ucast (p::priority) >> wordRadix :: machine_word) \<le> 7"
"(ucast (p::priority) >> wordRadix :: machine_word) \<le> 8"
unfolding maxPriority_def numPriorities_def wordRadix_def
using unat_lt2p[where x=p]
apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt)
@ -930,7 +931,7 @@ lemma prio_ucast_shiftr_wordRadix_helper': (* FIXME generalise *)
done
lemma prio_unat_shiftr_wordRadix_helper': (* FIXME generalise *)
"unat ((p::priority) >> wordRadix) \<le> 7"
"unat ((p::priority) >> wordRadix) \<le> 8"
unfolding maxPriority_def numPriorities_def wordRadix_def
using unat_lt2p[where x=p]
apply (clarsimp simp add: word_less_nat_alt shiftr_div_2n' unat_ucast_upcast is_up word_le_nat_alt)
@ -992,21 +993,19 @@ lemma cbitmap_L2_relation_bit_set:
fixes p :: priority
fixes d :: domain
shows "\<lbrakk> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>) ;
d \<le> maxDomain ; b = b' \<rbrakk>
d \<le> maxDomain ; prioToL1Index p \<le> numPriorities div wordBits \<rbrakk>
\<Longrightarrow>
cbitmap_L2_relation
(Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d)
(Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d])
(invertL1Index (prioToL1Index p))
(ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] ||
2 ^ unat (p && b))))
(unat (p >> wordRadix))
(ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[unat (p >> wordRadix)] ||
2 ^ unat (p && 0x1F))))
((ksReadyQueuesL2Bitmap \<sigma>)
((d, invertL1Index (prioToL1Index p)) :=
ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) ||
2 ^ unat (p && b')))"
unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def'
((d, prioToL1Index p) :=
ksReadyQueuesL2Bitmap \<sigma> (d, prioToL1Index p) || 2 ^ unat (p && mask wordRadix)))"
unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size
apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def
invertL1Index_def l2BitmapSize_def'
maxDomain_def numDomains_def word_le_nat_alt)
apply (case_tac "da = d" ; clarsimp)
done
@ -1049,6 +1048,11 @@ lemma t_hrs_ksReadyQueues_upd_absorb:
t_hrs_'_update f (g s \<lparr>ksReadyQueues_' := rqupd\<rparr>)"
by simp
lemma prioToL1Index_le_numPriorities_div_wordBits[simp]:
"prioToL1Index (tcbPriority tcb) \<le> numPriorities div wordBits"
unfolding prioToL1Index_def numPriorities_def wordBits_def
by (clarsimp simp: word_size intro!: prio_unat_shiftr_wordRadix_helper')
lemma rf_sr_drop_bitmaps_enqueue_helper:
"\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ;
cbitmap_L1_relation ksqL1upd' ksqL1upd ; cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk>
@ -1085,20 +1089,6 @@ lemma tcb_queue_relation'_empty_ksReadyQueues:
apply (clarsimp simp: tcb_at_not_NULL)
done
lemma invert_prioToL1Index_c_simp:
"p \<le> maxPriority
\<Longrightarrow>
unat ((of_nat l2BitmapSize :: machine_word) - 1 - (ucast p >> wordRadix))
= invertL1Index (prioToL1Index p)"
unfolding maxPriority_def l2BitmapSize_def' invertL1Index_def prioToL1Index_def
numPriorities_def
by (simp add: unat_sub prio_and_dom_limit_helpers)
lemma c_invert_assist: "7 - (ucast (p :: priority) >> 5 :: machine_word) < 8"
using prio_ucast_shiftr_wordRadix_helper'[simplified wordRadix_def]
by - (rule word_less_imp_diff_less, simp_all)
lemma tcbSchedEnqueue_ccorres:
"ccorres dc xfdc
(valid_queues and tcb_at' t and valid_objs')
@ -1108,7 +1098,6 @@ lemma tcbSchedEnqueue_ccorres:
(Call tcbSchedEnqueue_'proc)"
proof -
note prio_and_dom_limit_helpers[simp] word_sle_def[simp] maxDom_to_H[simp] maxPrio_to_H[simp]
note invert_prioToL1Index_c_simp[simp]
show ?thesis
apply (cinit lift: tcb_')
@ -1187,13 +1176,8 @@ proof -
apply (clarsimp simp: cready_queues_index_to_C_def numPriorities_def)
apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
apply (simp add: t_hrs_ksReadyQueues_upd_absorb)
apply (rule conjI)
apply (clarsimp simp: l2BitmapSize_def' wordRadix_def c_invert_assist)
apply (subst rf_sr_drop_bitmaps_enqueue_helper, assumption)
apply (fastforce intro: cbitmap_L1_relation_bit_set)
apply (fastforce intro: cbitmap_L2_relation_bit_set simp: wordRadix_def mask_def)
apply (fastforce intro: cbitmap_L1_relation_bit_set cbitmap_L2_relation_bit_set)+
apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb"
in rf_sr_sched_queue_relation)
apply clarsimp
@ -1201,7 +1185,6 @@ proof -
apply (drule_tac qhead'="tcb_ptr_to_ctcb_ptr t" and s=\<sigma> in tcbSchedEnqueue_update,
simp_all add: valid_queues_valid_q)[1]
apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
apply (erule(1) state_relation_queue_update_helper[where S="{t}"],
(simp | rule globals.equality)+,
simp_all add: cready_queues_index_to_C_def2 numPriorities_def
@ -1413,9 +1396,9 @@ lemma cready_queues_relation_empty_queue_helper:
done
lemma cbitmap_L2_relationD:
"\<lbrakk> cbitmap_L2_relation cbitmap2 abitmap2 ; d \<le> maxDomain ; i < l2BitmapSize \<rbrakk> \<Longrightarrow>
"\<lbrakk> cbitmap_L2_relation cbitmap2 abitmap2 ; d \<le> maxDomain ; i \<le> numPriorities div wordBits \<rbrakk> \<Longrightarrow>
cbitmap2.[unat d].[i] = abitmap2 (d, i)"
unfolding cbitmap_L2_relation_def l2BitmapSize_def'
unfolding cbitmap_L2_relation_def
by clarsimp
(* FIXME move *)
@ -1432,21 +1415,19 @@ lemma cbitmap_L2_relation_bit_clear:
fixes p :: priority
fixes d :: domain
shows "\<lbrakk> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (ksReadyQueuesL2Bitmap \<sigma>) ;
d \<le> maxDomain \<rbrakk>
d \<le> maxDomain ; prioToL1Index p \<le> numPriorities div wordBits \<rbrakk>
\<Longrightarrow>
cbitmap_L2_relation
(Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>')) (unat d)
(Arrays.update (ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d])
(invertL1Index (prioToL1Index p))
(ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[invertL1Index (prioToL1Index p)] &&
(unat (p >> wordRadix))
(ksReadyQueuesL2Bitmap_' (globals \<sigma>').[unat d].[unat (p >> wordRadix)] &&
~~ 2 ^ unat (p && 0x1F))))
((ksReadyQueuesL2Bitmap \<sigma>)
((d, invertL1Index (prioToL1Index p)) :=
ksReadyQueuesL2Bitmap \<sigma> (d, invertL1Index (prioToL1Index p)) &&
~~ 2 ^ unat (p && mask wordRadix)))"
unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size l2BitmapSize_def'
((d, prioToL1Index p) :=
ksReadyQueuesL2Bitmap \<sigma> (d, prioToL1Index p) && ~~ 2 ^ unat (p && mask wordRadix)))"
unfolding cbitmap_L2_relation_def numPriorities_def wordBits_def word_size
apply (clarsimp simp: word_size prioToL1Index_def wordRadix_def mask_def
invertL1Index_def l2BitmapSize_def'
maxDomain_def numDomains_def word_le_nat_alt)
apply (case_tac "da = d" ; clarsimp)
done
@ -1470,10 +1451,6 @@ proof -
\<forall>t\<in>set (ksReadyQueues s (d, p)). tcb_at' t s"
by (fastforce dest: spec elim: obj_at'_weakenE)
have invert_l1_index_limit: "\<And>p. invertL1Index (prioToL1Index p) < 8"
unfolding invertL1Index_def l2BitmapSize_def' prioToL1Index_def
by simp
show ?thesis
apply (cinit lift: tcb_')
apply (rule_tac r'="\<lambda>rv rv'. rv = to_bool rv'"
@ -1546,18 +1523,14 @@ proof -
h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)+
apply (drule(2) filter_empty_unfiltered_contr, simp)+
apply (rule conjI; clarsimp)
apply (rule conjI)
apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
apply (rule conjI; clarsimp)
apply (subst rf_sr_drop_bitmaps_dequeue_helper, assumption)
apply (fastforce intro: cbitmap_L1_relation_bit_clear)
apply (simp add: invert_prioToL1Index_c_simp)
apply (frule rf_sr_cbitmap_L2_relation)
apply (clarsimp simp: cbitmap_L2_relation_def
word_size prioToL1Index_def wordRadix_def mask_def
maxDomain_def numDomains_def word_le_nat_alt
numPriorities_def wordBits_def l2BitmapSize_def'
invertL1Index_def)
numPriorities_def wordBits_def)
apply (case_tac "d = tcbDomain ko" ; fastforce)
apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def)
@ -1578,17 +1551,14 @@ proof -
cmachine_state_relation_def)
apply (erule (2) cready_queues_relation_empty_queue_helper)
(* impossible case, C L2 update disagrees with Haskell update *)
apply (simp add: invert_prioToL1Index_c_simp)
apply (subst (asm) Arrays.index_update)
subgoal by (simp add: maxDomain_def numDomains_def word_le_nat_alt)
apply (subst (asm) Arrays.index_update)
apply (simp add: invert_l1_index_limit)
apply (simp add: less_eq_Suc_le)
apply (frule rf_sr_cbitmap_L2_relation)
apply (drule_tac i="invertL1Index (prioToL1Index (tcbPriority ko))"
in cbitmap_L2_relationD, assumption)
apply (fastforce simp: l2BitmapSize_def' invert_l1_index_limit)
apply (fastforce simp: prioToL1Index_def invertL1Index_def mask_def wordRadix_def)
apply (drule_tac i="prioToL1Index (tcbPriority ko)" in cbitmap_L2_relationD, assumption)
subgoal by (fastforce simp: numPriorities_def wordBits_def word_size prioToL1Index_def)
apply (fastforce simp: prioToL1Index_def mask_def wordRadix_def)
(* impossible case *)
apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
apply (drule(2) filter_empty_unfiltered_contr, fastforce)
@ -1638,8 +1608,6 @@ proof -
apply clarsimp
apply (rule conjI; clarsimp)
apply (rule conjI)
apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
apply (rule conjI; clarsimp)
(* invalid, missing bitmap updates on haskell side *)
apply (fold_subgoals (prefix))[2]
@ -1681,26 +1649,19 @@ proof -
apply (clarsimp simp: typ_heap_simps)
apply (rule conjI; clarsimp simp: typ_heap_simps)
apply (drule(2) filter_empty_unfiltered_contr[simplified filter_noteq_op], simp)
apply (rule conjI)
apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
apply (rule conjI; clarsimp)
(* impossible case, C L2 update disagrees with Haskell update *)
apply (subst (asm) Arrays.index_update)
apply (simp add: maxDomain_def numDomains_def word_le_nat_alt)
apply (subst (asm) Arrays.index_update)
subgoal using invert_l1_index_limit
by (fastforce simp add: invert_prioToL1Index_c_simp intro: nat_Suc_less_le_imp)
apply (simp add: less_eq_Suc_le)
apply (frule rf_sr_cbitmap_L2_relation)
apply (simp add: invert_prioToL1Index_c_simp)
apply (drule_tac i="invertL1Index (prioToL1Index (tcbPriority ko))"
in cbitmap_L2_relationD, assumption)
subgoal by (simp add: invert_l1_index_limit l2BitmapSize_def')
apply (fastforce simp: prioToL1Index_def invertL1Index_def mask_def wordRadix_def)
apply (drule_tac i="prioToL1Index (tcbPriority ko)" in cbitmap_L2_relationD, assumption)
apply (simp add: numPriorities_def wordBits_def word_size prioToL1Index_def)
apply (simp add: prioToL1Index_def mask_def wordRadix_def)
apply (simp add: invert_prioToL1Index_c_simp)
apply (subst rf_sr_drop_bitmaps_dequeue_helper_L2, assumption)
subgoal by (fastforce dest: rf_sr_cbitmap_L2_relation elim!: cbitmap_L2_relation_bit_clear)
(* trivial case, setting queue to empty *)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
cmachine_state_relation_def)
@ -1714,12 +1675,11 @@ proof -
subgoal premises prems using prems by (fastforce simp: maxDom_to_H maxPrio_to_H)+
apply (clarsimp simp: h_val_field_clift'
h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
apply (simp add: invert_prioToL1Index_c_simp)
apply (frule_tac s=\<sigma> in tcb_queue_relation_prev_next')
apply (fastforce simp add: ksQ_tcb_at')+
apply (drule_tac s=\<sigma> in tcbSchedDequeue_update, assumption,
simp_all add: remove1_filter ksQ_tcb_at')[1]
apply (clarsimp simp: filter_noteq_op upd_unless_null_def)
apply (clarsimp simp: filter_noteq_op upd_unless_null_def)
apply (rule conjI, clarsimp)
apply (clarsimp simp: h_val_field_clift'
h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift)
@ -1745,8 +1705,6 @@ proof -
by (fastforce simp: typ_heap_simps tcb_null_sched_ptrs_def)+
apply (clarsimp)
apply (rule conjI; clarsimp simp: typ_heap_simps)
apply (rule conjI)
apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
apply (rule conjI; clarsimp)
(* invalid, missing bitmap updates on haskell side *)
apply (drule tcb_queue_relation'_empty_ksReadyQueues)
@ -1927,14 +1885,10 @@ proof -
simp_all add: valid_queues_valid_q)[1]
apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp)
apply (clarsimp simp: h_val_field_clift' h_t_valid_clift)
apply (simp add: invert_prioToL1Index_c_simp)
apply (rule conjI; clarsimp)
apply (rule conjI)
apply (fastforce simp: c_invert_assist l2BitmapSize_def' wordRadix_def)
apply (simp add: t_hrs_ksReadyQueues_upd_absorb)
apply (subst rf_sr_drop_bitmaps_enqueue_helper, assumption)
apply (fastforce intro: cbitmap_L1_relation_bit_set)
subgoal by (fastforce intro: cbitmap_L2_relation_bit_set simp: wordRadix_def mask_def)
apply (fastforce intro: cbitmap_L1_relation_bit_set cbitmap_L2_relation_bit_set)+
apply (erule(1) state_relation_queue_update_helper[where S="{t}"],
(simp | rule globals.equality)+,
simp_all add: cready_queues_index_to_C_def2 numPriorities_def
@ -2104,466 +2058,85 @@ lemma getCurDomain_ccorres:
rf_sr_ksCurDomain)
done
lemma getReadyQueuesL1Bitmap_sp:
"\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<rbrace>
getReadyQueuesL1Bitmap d
\<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d = rv \<and> d \<le> maxDomain \<and> P s\<rbrace>"
unfolding bitmap_fun_defs
by wp simp
(* this doesn't actually carry over d \<le> maxDomain to the rest of the ccorres,
use ccorres_cross_over_guard to do that *)
lemma ccorres_pre_getReadyQueuesL1Bitmap:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> P rv s))
{s. \<forall>rv. (ksReadyQueuesL1Bitmap_' (globals s)).[unat d] = ucast rv
\<longrightarrow> s \<in> P' rv }
hs (getReadyQueuesL1Bitmap d >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l2)
defer
defer
apply (rule getReadyQueuesL1Bitmap_sp)
apply blast
apply clarsimp
prefer 3
apply (clarsimp simp: bitmap_fun_defs gets_exs_valid)
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply blast
apply assumption
apply (drule rf_sr_cbitmap_L1_relation)
apply (clarsimp simp: cbitmap_L1_relation_def)
done
lemma getReadyQueuesL2Bitmap_sp:
"\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<rbrace>
getReadyQueuesL2Bitmap d i
\<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i < l2BitmapSize \<and> P s\<rbrace>"
unfolding bitmap_fun_defs
by wp simp
lemma ccorres_pre_getReadyQueuesL2Bitmap:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. d \<le> maxDomain \<and> i < l2BitmapSize
\<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d,i) = rv \<longrightarrow> P rv s))
{s. \<forall>rv. (ksReadyQueuesL2Bitmap_' (globals s)).[unat d].[i] = ucast rv
\<longrightarrow> s \<in> P' rv }
hs (getReadyQueuesL2Bitmap d i >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l2)
defer
defer
apply (rule getReadyQueuesL2Bitmap_sp)
apply blast
apply clarsimp
prefer 3
apply (clarsimp simp: bitmap_fun_defs gets_exs_valid)
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply blast
apply assumption
apply (drule rf_sr_cbitmap_L2_relation)
apply (clarsimp simp: cbitmap_L2_relation_def)
done
lemma rf_sr_ksReadyQueuesL1Bitmap_simp:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain \<rbrakk>
\<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap \<sigma> d"
apply (drule rf_sr_cbitmap_L1_relation)
apply (simp add: cbitmap_L1_relation_def)
done
lemma cguard_UNIV:
"P s \<Longrightarrow> s \<in> (if P s then UNIV else {})"
by fastforce
lemma lookupBitmapPriority_le_maxPriority:
"\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; valid_queues s \<rbrakk>
\<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority"
unfolding valid_queues_def valid_queues_no_bitmap_def
by (fastforce dest!: bitmapQ_from_bitmap_lookup bitmapQ_ksReadyQueuesI intro: ccontr)
lemma rf_sr_ksReadyQueuesL1Bitmap_not_zero:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0"
apply (drule rf_sr_cbitmap_L1_relation)
apply (simp add: cbitmap_L1_relation_def)
done
lemma ksReadyQueuesL1Bitmap_word_log2_max:
"\<lbrakk>valid_queues s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk>
\<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < l2BitmapSize"
unfolding valid_queues_def
by (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD)
lemma word_log2_max_word32[simp]:
"word_log2 (w :: 32 word) < 32"
using word_log2_max[where w=w]
by (simp add: word_size)
lemma word_log2_max_word8[simp]:
"word_log2 (w :: 8 word) < 8"
using word_log2_max[where w=w]
by (simp add: word_size)
lemma rf_sr_ksReadyQueuesL2Bitmap_simp:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; valid_queues \<sigma> ; ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[word_log2 (ksReadyQueuesL1Bitmap \<sigma> d)] =
ksReadyQueuesL2Bitmap \<sigma> (d, word_log2 (ksReadyQueuesL1Bitmap \<sigma> d))"
apply (frule rf_sr_cbitmap_L2_relation)
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
apply (drule (3) cbitmap_L2_relationD)
done
lemma ksReadyQueuesL2Bitmap_nonzeroI:
"\<lbrakk> d \<le> maxDomain ; valid_queues s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) \<noteq> 0"
unfolding valid_queues_def
apply clarsimp
apply (frule bitmapQ_no_L1_orphansD)
apply (erule word_log2_nth_same)
apply clarsimp
done
lemma clzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (rule_tac x="ret__long_'_update f x" for f in exI)
apply (simp add: mex_def meq_def)
done
lemma l1index_to_prio_spec:
"\<forall>s. \<Gamma> \<turnstile> {s} Call l1index_to_prio_'proc
\<lbrace>\<acute>ret__unsigned_long = l1index_' s << wordRadix \<rbrace>"
by vcg (simp add: word_sle_def wordRadix_def')
lemma getHighestPrio_ccorres:
"ccorres (\<lambda>rv rv'. rv' = ucast rv) ret__unsigned_long_'
(\<lambda>s. d \<le> maxDomain \<and> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<and> bitmapQ_no_L1_orphans s)
(UNIV \<inter> {s. dom_' s = ucast d}) hs
(getHighestPrio d) (Call getHighestPrio_'proc)"
proof -
note prio_and_dom_limit_helpers [simp]
note Collect_const_mem [simp]
have signed_word_log2:
"\<And>w. w \<noteq> 0 \<Longrightarrow> (0x1F::32 signed word) - of_nat (word_clz (w::machine_word)) = (of_nat (word_log2 w))"
unfolding word_log2_def
by (clarsimp dest!: word_clz_nonzero_max simp: word_size)
have word_log2_def32:
"\<And>w. word_log2 (w::machine_word) = 31 - word_clz w"
unfolding word_log2_def by (simp add: word_size)
(* FIXME generalise *)
have word_clz_sint_upper[simp]:
"\<And>(w::machine_word). sint (of_nat (word_clz w) :: 32 signed word) \<le> 2147483679"
apply (subst sint_eq_uint)
apply (rule not_msb_from_less)
apply simp
apply (rule word_of_nat_less)
apply simp
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (subst uint_nat)
apply (simp add: unat_of_nat)
apply (subst mod_less)
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (rule iffD2 [OF le_nat_iff[symmetric]])
apply simp
apply (rule order_trans[OF word_clz_max])
apply (simp add: word_size)
done
have word_clz_sint_lower[simp]:
"\<And>(w::machine_word). - sint (of_nat (word_clz w) :: 32 signed word) \<le> 2147483616"
apply (subst sint_eq_uint)
apply (rule not_msb_from_less)
apply simp
apply (rule word_of_nat_less)
apply simp
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (subst uint_nat)
apply (simp add: unat_of_nat)
done
have invertL1Index_unat_fold:
"\<And>(w::32 word). \<lbrakk> w \<noteq> 0 ; word_log2 w < l2BitmapSize \<rbrakk> \<Longrightarrow>
unat (of_nat l2BitmapSize - (1::32 word) - of_nat (word_log2 w))
= invertL1Index (word_log2 w)"
apply (subst unat_sub)
apply (clarsimp simp: l2BitmapSize_def')
apply (rule word_of_nat_le)
apply (drule word_log2_nth_same)
apply (clarsimp simp: l2BitmapSize_def')
apply (clarsimp simp: invertL1Index_def l2BitmapSize_def')
apply (simp add: unat_of_nat_eq)
done
show ?thesis
apply (cinit lift: dom_')
apply (clarsimp split del: split_if)
apply (rule ccorres_pre_getReadyQueuesL1Bitmap)
apply (rule ccorres_pre_getReadyQueuesL2Bitmap)
apply (rename_tac l2)
apply (rule ccorres_Guard_Seq|csymbr)+
apply (rule ccorres_abstract_cleanup)
apply (rule ccorres_Guard_Seq|csymbr)+
apply (rule ccorres_abstract_cleanup)
apply (rule ccorres_Guard_Seq|csymbr)+
apply (clarsimp simp: word_log2_def word_size)
apply (rename_tac clz_l1index clz_l2index)
apply (rule_tac P="\<lambda>s. l1 \<noteq> 0 \<and> l2 \<noteq> 0 \<and> word_log2 l1 < l2BitmapSize"
and P'="{s. clz_l1index = of_nat (word_clz l1) \<and>
clz_l2index = of_nat (word_clz l2) }"
in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
subgoal
apply (clarsimp simp: return_def l1IndexToPrio_def)
apply (simp add: signed_word_log2 word_log2_def32[symmetric] ucast_or_distrib)
apply (rule_tac f="op ||" in arg_cong2)
apply (subst of_nat_shiftl)+
apply (subst ucast_of_nat_small, simp add: wordRadix_def l2BitmapSize_def')
apply (rule refl)
apply (subst ucast_of_nat_small, simp add: wordRadix_def)
apply (rule word_log2_max_word32[THEN order_less_le_trans], simp)
apply (rule refl)
done
apply (clarsimp simp: word_sle_def)
apply (frule rf_sr_cbitmap_L1_relation)
apply (subgoal_tac "ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0")
prefer 2
subgoal by (fastforce simp: cbitmap_L1_relation_def)
apply (clarsimp simp: signed_word_log2 cbitmap_L1_relation_def)
apply (frule bitmapQ_no_L1_orphansD, erule word_log2_nth_same)
apply (rule conjI, fastforce simp: invertL1Index_def l2BitmapSize_def')
apply (rule conjI, fastforce)
apply (rule conjI, fastforce)
apply (rule conjI, fastforce simp: invertL1Index_unat_fold)
apply (rule conjI, fastforce simp: sign_simps)
apply (rule conjI)
apply (subst invertL1Index_unat_fold, assumption, fastforce)
apply (frule rf_sr_cbitmap_L2_relation)
apply (fastforce simp: cbitmap_L2_relation_def)
apply (clarsimp simp: l2BitmapSize_def')
apply (rule conjI)
apply (fastforce simp: word_less_nat_alt word_le_nat_alt unat_sub unat_of_nat)
apply (fastforce simp: le_diff_eq)
done
qed
lemma ccorres_abstract_ksCurThread:
assumes ceqv: "\<And>rv' t t'. ceqv \<Gamma> (\<lambda>s. ksCurThread_' (globals s)) rv' t t' d (d' rv')"
and cc: "\<And>ct. ccorres_underlying rf_sr \<Gamma> r xf arrel axf (G ct) (G' ct) hs a (d' (tcb_ptr_to_ctcb_ptr ct))"
shows "ccorres_underlying rf_sr \<Gamma> r xf arrel axf (\<lambda>s. G (ksCurThread s) s)
{s. s \<in> G' (ctcb_ptr_to_tcb_ptr (ksCurThread_' (globals s)))} hs a d"
apply (rule ccorres_guard_imp)
prefer 2
apply assumption
apply (rule ccorres_abstract[OF ceqv, where G'="\<lambda>ct. \<lbrace>ct = \<acute>ksCurThread\<rbrace> \<inter> G' (ctcb_ptr_to_tcb_ptr ct)"])
apply (subgoal_tac "\<exists>t. rv' = tcb_ptr_to_ctcb_ptr t")
apply clarsimp
apply (rule ccorres_guard_imp2)
apply (rule cc)
apply (clarsimp simp: rf_sr_ksCurThread)
apply (metis tcb_ptr_to_tcb_ptr)
apply simp
done
lemma ctcb_relation_unat_tcbPriority_C:
"ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority_C tcb') = unat (tcbPriority tcb)"
apply (clarsimp simp: ctcb_relation_def)
apply (rule trans, rule arg_cong[where f=unat], erule sym)
apply (simp(no_asm))
done
lemma ctcb_relation_unat_tcbDomain_C:
"ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbDomain_C tcb') = unat (tcbDomain tcb)"
apply (clarsimp simp: ctcb_relation_def)
apply (rule trans, rule arg_cong[where f=unat], erule sym)
apply (simp(no_asm))
done
lemma possibleSwitchTo_ccorres:
defines
"skipSched b curPrio targetPrio l1 hiPrio \<equiv>
((curPrio::priority) < targetPrio
\<or> b \<and> (targetPrio = curPrio \<or> (l1::machine_word) = 0
\<or> hiPrio \<le> targetPrio))"
shows
"ccorres dc xfdc
(valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain)
and valid_objs')
(valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t
and valid_objs')
({s. target_' s = tcb_ptr_to_ctcb_ptr t}
\<inter> {s. curThreadWillBlock_' s = from_bool b} \<inter> UNIV) []
\<inter> {s. onSamePriority_' s = from_bool b} \<inter> UNIV) []
(possibleSwitchTo t b)
(Call possibleSwitchTo_'proc)"
proof -
show ?thesis
supply split_if [split del]
supply Collect_const [simp del]
supply dc_simp [simp del]
supply prio_and_dom_limit_helpers[simp]
(* FIXME: these should likely be in simpset for CRefine, or even in general *)
supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] if_1_0_0[simp]
ccorres_IF_True[simp]
apply (cinit lift: target_' curThreadWillBlock_')
apply (fold skipSched_def)
apply (cinit lift: target_' onSamePriority_')
apply (rule ccorres_pre_getCurThread)
apply (rename_tac curThread)
apply (ctac add: getCurDomain_ccorres)
apply (rename_tac curDom curDom')
apply (rule_tac P="curDom \<le> maxDomain" in ccorres_gen_asm)
apply clarsimp
apply (rule ccorres_symb_exec_l3[OF _ threadGet_inv _ empty_fail_threadGet])
apply (rule ccorres_symb_exec_l3[OF _ threadGet_inv _ empty_fail_threadGet])
apply (rule ccorres_symb_exec_l3[OF _ threadGet_inv _ empty_fail_threadGet])
apply (rename_tac curPrio targetDom targetPrio)
apply (rule_tac xf'=curPrio_'
and val="ucast curPrio"
and R="obj_at' (op = curPrio \<circ> tcbPriority) curThread
and (\<lambda>s. ksCurThread s = curThread)"
and R'="UNIV" in ccorres_symb_exec_r_known_rv)
apply vcg
apply clarsimp
apply (drule(1) obj_at_cslift_tcb)+
(* note: if this loops, it's likely unat_arith_simps *)
apply (fastforce simp: typ_heap_simps' rf_sr_ksCurThread
ctcb_relation_unat_tcbPriority_C unat_arith_simps)
apply (ctac(no_vcg) add: getCurDomain_ccorres)
apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'=curPrio_'
in ccorres_split_nothrow_novcg)
apply (rule_tac P="\<lambda>s. ksCurThread s = rv" in threadGet_vcg_corres_P)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: rf_sr_ksCurThread obj_at'_def projectKOs
typ_heap_simps' ctcb_relation_def)
apply ceqv
apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'=targetDom_'
in ccorres_split_nothrow_novcg)
apply (rule threadGet_vcg_corres)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: rf_sr_ksCurThread obj_at'_def projectKOs
typ_heap_simps' ctcb_relation_def)
apply ceqv
apply (rule_tac xf'=targetDom_'
and val="ucast targetDom"
and R="obj_at' (op = targetDom \<circ> tcbDomain) t"
and R'="UNIV" in ccorres_symb_exec_r_known_rv)
apply vcg
apply clarsimp
apply (drule(1) obj_at_cslift_tcb)+
apply (fastforce simp: typ_heap_simps' unat_arith_simps ctcb_relation_unat_tcbDomain_C)
apply ceqv
apply (rule_tac xf'=targetPrio_'
and val="ucast targetPrio"
and R="obj_at' (op = targetPrio \<circ> tcbPriority) t"
and R'="UNIV" in ccorres_symb_exec_r_known_rv)
apply vcg
apply clarsimp
apply (drule(1) obj_at_cslift_tcb)+
apply (fastforce simp: typ_heap_simps' unat_arith_simps
ctcb_relation_unat_tcbPriority_C)
apply (rule_tac r'="\<lambda>rv rv'. rv' = ucast rv" and xf'=targetPrio_'
in ccorres_split_nothrow_novcg)
apply (rule threadGet_vcg_corres)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: rf_sr_ksCurThread obj_at'_def projectKOs
typ_heap_simps' ctcb_relation_def)
apply ceqv
apply (rule_tac r'="cscheduler_action_relation"
and xf'="action___ptr_to_struct_tcb_C_'"
in ccorres_split_nothrow)
and xf'="action___ptr_to_struct_tcb_C_'"
in ccorres_split_nothrow_novcg)
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: getSchedulerAction_def simpler_gets_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
apply ceqv
apply (rename_tac action action')
apply (rule ccorres_cond[where R=\<top>], fastforce simp: up_ucast_inj_eq)
apply (rule_tac R=\<top> in ccorres_cond)
apply clarsimp
apply (ctac add: tcbSchedEnqueue_ccorres)
apply (rule ccorres_pre_getReadyQueuesL1Bitmap)
apply (rename_tac l1)
apply (rule ccorres_rhs_assoc)
apply (rule_tac xf'=ret__int_'
and r'="\<lambda>highestPrio rv'.
rv' = from_bool (skipSched b curPrio targetPrio l1 highestPrio)"
in ccorres_split_nothrow)
apply (rule_tac P="valid_queues and (\<lambda>s. l1 = ksReadyQueuesL1Bitmap s curDom)"
and P'=UNIV in ccorres_inst)
apply (rule ccorres_guard_imp)
apply csymbr
apply ccorres_rewrite
apply (rule ccorres_Cond_rhs)
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l3[OF ccorres_return_Skip'])
apply wp
apply csymbr
apply simp
apply (rule ccorres_Cond_rhs)
apply (rule ccorres_cond_seq2[THEN iffD1])
apply csymbr
apply simp
apply (rule ccorres_Cond_rhs, simp)
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l3[OF ccorres_return_Skip'])
apply wp
apply (rule_tac xf'=ret__int_'
and val="from_bool (l1 = 0)"
and R="\<lambda>s. l1 = ksReadyQueuesL1Bitmap s curDom"
and R'="UNIV"
in ccorres_symb_exec_r_known_rv)
apply (rule conseqPre, vcg, fastforce simp: rf_sr_ksReadyQueuesL1Bitmap_simp)
apply ceqv
apply simp
apply (rule ccorres_Cond_rhs)
apply simp
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l3)
apply (rule ccorres_return_Skip')
apply wp
apply (rule ccorres_add_return2)
apply (ctac add: getHighestPrio_ccorres[simplified getHighestPrio_def'])
apply (rename_tac highestPrio highestPrio')
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg)
apply (rule allI, rule conseqPre, vcg)
apply (fastforce simp: return_def skipSched_def word_le_nat_alt word_less_nat_alt up_ucast_inj_eq)
apply wp
apply (vcg exspec=getHighestPrio_modifies)
apply vcg
apply (rule ccorres_add_return2)
apply (rule ccorres_symb_exec_l3[OF ccorres_return_Skip'])
apply wp
subgoal by (clarsimp simp: valid_queues_def)
apply (clarsimp simp: skipSched_def true_def)
apply (fastforce simp: word_le_nat_alt word_less_nat_alt up_ucast_inj_eq)
apply ceqv
(*concludes condition calculation*)
apply simp
apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow)
apply (rule_tac R="\<lambda>s. weak_sch_act_wf action s" in ccorres_cond)
subgoal by (clarsimp simp: cscheduler_action_relation_def max_word_def
weak_sch_act_wf_def tcb_at_not_NULL
split: scheduler_action.split_asm dest!: pred_tcb_at')
apply (fastforce simp: cscheduler_action_relation_def
intro: ccorres_setSchedulerAction)
apply (ctac add: tcbSchedEnqueue_ccorres)
apply ceqv
apply (simp only: scheduler_action_case_switch_to_if)
apply (rule_tac R="weak_sch_act_wf action" in ccorres_cond)
apply (clarsimp simp: cscheduler_action_relation_def
weak_sch_act_wf_def
tcb_at_not_NULL tcb_at_max_word
split: scheduler_action.split_asm dest!: pred_tcb_at' )
apply (ctac add: rescheduleRequired_ccorres)
apply (rule ccorres_return_Skip)
apply wp
apply (simp add: weak_sch_act_wf_def)
apply (wp weak_sch_act_wf_lift_linear static_imp_wp)
apply (wp threadGet_wp
| vcg exspec=getHighestPrio_modifies exspec=tcbSchedEnqueue_modifies)+
apply (fastforce simp: weak_sch_act_wf_def obj_at'_weakenE[OF _ TrueI]
valid_objs'_maxDomain valid_objs'_maxPriority obj_at'_def)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac R="weak_sch_act_wf rve" in ccorres_cond)
apply (clarsimp simp: from_bool_0)
apply (simp add: word_less_nat_alt unat_ucast_8_32 up_ucast_inj_eq)
apply (simp add: cscheduler_action_relation_def)
apply (clarsimp simp: max_word_def weak_sch_act_wf_def tcb_at_not_NULL
split: scheduler_action.split_asm dest!: pred_tcb_at')
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: setSchedulerAction_def simpler_modify_def)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cscheduler_action_relation_def
carch_state_relation_def cmachine_state_relation_def)
apply (ctac add: tcbSchedEnqueue_ccorres)
apply (simp only: scheduler_action_case_switch_to_if)
apply (rule_tac R="weak_sch_act_wf rve" in ccorres_cond)
apply (clarsimp simp del: Collect_const)
apply (clarsimp simp: cscheduler_action_relation_def
weak_sch_act_wf_def
tcb_at_not_NULL tcb_at_max_word
split: scheduler_action.split_asm dest!: pred_tcb_at' )
apply (ctac add: rescheduleRequired_ccorres)
apply (rule ccorres_return_Skip)
apply (simp split del: split_if)
apply wp
apply (simp add: weak_sch_act_wf_def)
apply (wp weak_sch_act_wf_lift_linear)
apply (simp add: guard_is_UNIV_def)
apply (wp static_imp_wp threadGet_wp | clarsimp simp: guard_is_UNIV_def)+
apply (clarsimp simp: weak_sch_act_wf_def obj_at'_weakenE[OF _ TrueI]
valid_objs'_maxDomain valid_objs'_maxPriority)
done
qed
lemma attemptSwitchTo_ccorres [corres]:
"ccorres dc xfdc (valid_queues and st_tcb_at' runnable' thread and valid_objs'
and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
and (\<lambda>s. ksCurDomain s \<le> maxDomain))
and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s))
(UNIV \<inter> \<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
(attemptSwitchTo thread)
(Call attemptSwitchTo_'proc)"

13
proof/crefine/Ipc_C.thy
View File

@ -3903,12 +3903,10 @@ lemma doIPCTransfer_reply_or_replyslot:
apply simp
done
crunch ksCurDomain[wp]: handleFaultReply "\<lambda>s. P (ksCurDomain s)"
lemma doReplyTransfer_ccorres [corres]:
"ccorres dc xfdc
(invs' and st_tcb_at' (Not \<circ> isReply) sender
and tcb_at' receiver and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain)
and tcb_at' receiver and sch_act_simple
and ((Not o real_cte_at' slot) or cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot)
and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap \<or> isReplyCap (cteCap cte))
slot)
@ -4010,7 +4008,7 @@ proof -
apply (clarsimp simp: guard_is_UNIV_def ThreadState_Restart_def
ThreadState_Inactive_def mask_def to_bool_def)
apply (rule_tac Q="\<lambda>rv. valid_queues and tcb_at' receiver and valid_queues' and
valid_objs' and sch_act_simple and (\<lambda>s. ksCurDomain s \<le> maxDomain) and
valid_objs' and sch_act_simple and
(\<lambda>s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp)
apply (clarsimp simp: inQ_def weak_sch_act_wf_def)
apply (wp threadSet_valid_queues threadSet_sch_act handleFaultReply_sch_act_wf)
@ -4800,7 +4798,6 @@ lemma sendIPC_ccorres [corres]:
and valid_mdb' and tcb_at' dest and cur_tcb'
and tcb_at' thread and K (dest \<noteq> thread)
and sch_act_not thread and K (epptr \<noteq> 0)
and (\<lambda>s. ksCurDomain s \<le> maxDomain)
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and>
(\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))"
in hoare_post_imp)
@ -5592,7 +5589,6 @@ lemma receiveIPC_ccorres [corres]:
apply (rule_tac Q="\<lambda>rv. valid_queues and valid_pspace' and valid_objs'
and st_tcb_at' (op = sendState) sender
and tcb_at' thread and sch_act_not sender
and (\<lambda>s. ksCurDomain s \<le> maxDomain)
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and>
(\<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))))"
in hoare_post_imp)
@ -5606,9 +5602,8 @@ lemma receiveIPC_ccorres [corres]:
and cur_tcb' and tcb_at' sender and tcb_at' thread
and sch_act_not sender and K (thread \<noteq> sender)
and ep_at' (capEPPtr cap)
and (\<lambda>s. ksCurDomain s \<le> maxDomain)
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and>
(\<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))))"
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and>
(\<forall>d p. sender \<notin> set (ksReadyQueues s (d, p))))"
in hoare_post_imp)
subgoal by (auto, auto simp: st_tcb_at'_def obj_at'_def)
apply (wp hoare_vcg_all_lift set_ep_valid_objs')

191
proof/crefine/Recycle_C.thy
View File

@ -1018,106 +1018,111 @@ lemma arch_recycleCap_ccorres:
apply (subgoal_tac "isASIDPoolCap cp") prefer 2
apply (case_tac cp; fastforce simp add: isCap_simps)
apply (simp add: ccorres_cond_iffs Collect_True Collect_False
Let_def
del: Collect_const)
apply (rule ccorres_rhs_assoc)+
apply (csymbr, csymbr, csymbr)
apply (rule ccorres_Guard_Seq)+
apply (rule ccorres_symb_exec_l[OF _ gets_inv gets_wp empty_fail_gets])
apply (rule ccorres_split_nothrow_novcg_dc)
apply (simp add: when_def del: Collect_const)
apply (rule_tac R="\<lambda>s. rv = armKSASIDTable (ksArchState s)
\<and> capASIDPool cp \<noteq> 0"
in ccorres_cond2)
apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_to_H_def cap_lift_asid_pool_cap
cap_asid_pool_cap_lift_def
apply (rule ccorres_rhs_assoc)+
apply (csymbr, csymbr, csymbr)
apply (rule ccorres_Guard_Seq)+
apply (rule ccorres_symb_exec_l
[OF _ gets_inv gets_wp empty_fail_gets])
apply (rule ccorres_split_nothrow_novcg_dc)
apply (simp add: when_def del: Collect_const)
apply (rule_tac R="\<lambda>s. rv = armKSASIDTable (ksArchState s)
\<and> capASIDPool cp \<noteq> 0"
in ccorres_cond2)
apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_to_H_def cap_lift_asid_pool_cap
cap_asid_pool_cap_lift_def
elim!: ccap_relationE)
apply (subst ucast_asid_high_bits_is_shift)
apply (simp add: mask_def asid_bits_def)
apply (rule word_and_le1)
apply (subst rf_sr_armKSASIDTable, assumption)
apply (simp add: asid_high_bits_word_bits)
apply (rule shiftr_less_t2n)
apply (rule order_le_less_trans [OF _ and_mask_less_size])
apply (simp add: asid_low_bits_def asid_high_bits_def mask_def)
apply (rule order_refl)
apply (simp add: asid_low_bits_def asid_high_bits_def word_size)
apply (simp add: option_to_ptr_def option_to_0_def
split: option.split)
apply (rule ccorres_rhs_assoc)+
apply (ctac(no_vcg) add: deleteASIDPool_ccorres)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac P="valid_cap' (ArchObjectCap cp)
and (\<lambda>s. 2 ^ acapBits cp \<le> gsMaxObjectSize s)
and no_0_obj'"
in ccorres_from_vcg[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric]
asidLowBits_handy_convs word_sle_def
word_sless_def)
apply (clarsimp simp: ccap_relation_def cap_asid_pool_cap_lift
cap_to_H_def valid_cap'_def capAligned_def
typ_at_to_obj_at_arches)
apply (subst ghost_assertion_size_logic[unfolded o_def, rotated], assumption)
apply (erule order_trans[rotated])
apply (simp add: asid_low_bits_def)
apply (drule obj_at_ko_at', clarsimp)
apply (rule cmap_relationE1[OF rf_sr_cpspace_asidpool_relation], assumption)
apply (erule ko_at_projectKO_opt)
apply (frule h_t_valid_clift)
apply (subst h_t_valid_dom_s, assumption, simp)
apply (simp add: asid_low_bits_def)
apply simp
apply (rule conjI, clarsimp)
apply (rule conjI, erule is_aligned_no_wrap')
apply (clarsimp simp: asid_low_bits_def)
apply (rule conjI)
apply (erule is_aligned_weaken)
apply (clarsimp simp: asid_low_bits_def)
apply (rule conjI)
apply (clarsimp simp: is_aligned_def asid_low_bits_def)
apply (clarsimp simp: typ_at_to_obj_at_arches)
apply (rule rev_bexI, rule setObject_eq[where P=\<top>],
(simp add: objBits_simps archObjSize_def pageBits_def)+)
apply (simp add: obj_at'_weakenE[OF _ TrueI])
apply (simp only: replicateHider_def[symmetric])
apply (clarsimp simp: asid_low_bits_def)
apply (subst coerce_memset_to_heap_update_asidpool)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def typ_heap_simps
update_asidpool_map_tos
update_asidpool_map_to_asidpools)
apply (rule conjI)
apply (erule cmap_relation_updI, simp_all)[1]
apply (simp add: makeObject_asidpool casid_pool_relation_def)
apply (clarsimp simp: array_relation_def option_to_ptr_def option_to_0_def)
apply (subst fcp_beta)
apply (simp add: asid_low_bits_def, unat_arith)
apply (subst ucast_asid_high_bits_is_shift)
apply (simp add: mask_def asid_bits_def)
apply (rule word_and_le1)
apply (subst rf_sr_armKSASIDTable, assumption)
apply (simp add: asid_high_bits_word_bits)
apply (rule shiftr_less_t2n)
apply (rule order_le_less_trans [OF _ and_mask_less_size])
apply (simp add: asid_low_bits_def asid_high_bits_def mask_def)
apply (rule order_refl)
apply (simp add: asid_low_bits_def asid_high_bits_def word_size)
apply (simp add: option_to_ptr_def option_to_0_def
split: option.split)
apply (rule ccorres_rhs_assoc)+
apply (ctac(no_vcg) add: deleteASIDPool_ccorres)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule_tac P="valid_cap' (ArchObjectCap cp) and (\<lambda>s. 2 ^ acapBits cp \<le> gsMaxObjectSize s)
and no_0_obj'"
in ccorres_from_vcg[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric]
asidLowBits_handy_convs word_sle_def
word_sless_def)
apply (clarsimp simp: ccap_relation_def cap_asid_pool_cap_lift
cap_to_H_def valid_cap'_def capAligned_def
typ_at_to_obj_at_arches)
apply (subst ghost_assertion_size_logic[unfolded o_def, rotated],
assumption)
apply (erule order_trans[rotated])
apply (simp add: asid_low_bits_def)
apply (drule obj_at_ko_at', clarsimp)
apply (rule cmap_relationE1[OF rf_sr_cpspace_asidpool_relation],
assumption)
apply (erule ko_at_projectKO_opt)
apply (frule h_t_valid_clift)
apply (subst h_t_valid_dom_s, assumption, simp)
apply (simp add: asid_low_bits_def)
apply simp
subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps)
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: word_sle_def word_sless_def
asidLowBits_handy_convs
exec_gets simpler_modify_def
simp del: rf_sr_upd_safe)
apply (simp add: cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_lift_asid_pool_cap cap_to_H_def
cap_asid_pool_cap_lift_def
elim!: ccap_relationE
simp del: rf_sr_upd_safe)
apply (clarsimp simp: rf_sr_def cstate_relation_def
apply (rule conjI, clarsimp)
apply (rule conjI, erule is_aligned_no_wrap')
apply (clarsimp simp: asid_low_bits_def)
apply (rule conjI)
apply (erule is_aligned_weaken)
apply (clarsimp simp: asid_low_bits_def)
apply (rule conjI)
apply (clarsimp simp: is_aligned_def asid_low_bits_def)
apply (clarsimp simp: typ_at_to_obj_at_arches)
apply (rule rev_bexI, rule setObject_eq[where P=\<top>],
(simp add: objBits_simps archObjSize_def pageBits_def)+)
apply (simp add: obj_at'_weakenE[OF _ TrueI])
apply (simp only: replicateHider_def[symmetric])
apply (clarsimp simp: asid_low_bits_def)
apply (subst coerce_memset_to_heap_update_asidpool)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cpspace_relation_def typ_heap_simps
update_asidpool_map_tos
update_asidpool_map_to_asidpools)
apply (rule conjI)
apply (erule cmap_relation_updI, simp_all)[1]
apply (simp add: makeObject_asidpool casid_pool_relation_def)
apply (clarsimp simp: array_relation_def
option_to_ptr_def option_to_0_def)
apply (subst fcp_beta)
apply (simp add: asid_low_bits_def, unat_arith)
apply simp
subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def
typ_heap_simps)
apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: word_sle_def word_sless_def
asidLowBits_handy_convs
exec_gets simpler_modify_def
simp del: rf_sr_upd_safe)
apply (simp add: cap_get_tag_isCap_ArchObject[symmetric])
apply (clarsimp simp: cap_lift_asid_pool_cap cap_to_H_def
cap_asid_pool_cap_lift_def
elim!: ccap_relationE
simp del: rf_sr_upd_safe)
apply (clarsimp simp: rf_sr_def cstate_relation_def
Let_def carch_state_relation_def carch_globals_def
cmachine_state_relation_def
h_t_valid_clift_Some_iff
asid_shiftr_low_bits_less[unfolded mask_def asid_bits_def]
word_and_le1)
apply (subst ucast_asid_high_bits_is_shift)
apply (simp add: mask_def asid_bits_def word_and_le1)
apply (subst ucast_asid_high_bits_is_shift)
apply (simp add: mask_def asid_bits_def
word_and_le1)
apply (erule array_relation_update[unfolded fun_upd_def])
subgoal by simp
subgoal by (simp add: option_to_ptr_def option_to_0_def)
@ -1181,7 +1186,6 @@ lemma arch_recycleCap_ccorres:
elim!: ccap_relationE cong: conj_cong)
apply (simp add: page_table_at'_def, drule spec[where x=0], clarsimp)
apply (frule cap_get_tag_isCap_unfolded_H_cap)
apply clarsimp
apply (frule invs_arch_state')
apply (clarsimp simp: capAligned_def pdBits_def pageBits_def)
apply (frule is_aligned_addrFromPPtr_n, simp)
@ -1367,6 +1371,13 @@ lemma tcbSchedEnqueue_ep_at:
apply (clarsimp split: split_if, wp)
done
lemma ctcb_relation_unat_tcbPriority_C:
"ctcb_relation tcb tcb' \<Longrightarrow> unat (tcbPriority_C tcb') = unat (tcbPriority tcb)"
apply (clarsimp simp: ctcb_relation_def)
apply (rule trans, rule arg_cong[where f=unat], erule sym)
apply (simp(no_asm))
done
lemma ccorres_duplicate_guard:
"ccorres r xf (P and P) Q hs f f' \<Longrightarrow> ccorres r xf P Q hs f f'"
by (erule ccorres_guard_imp, auto)

460
proof/crefine/Schedule_C.thy
View File

@ -14,6 +14,89 @@ begin
context begin interpretation Arch . (*FIXME: arch_split*)
lemma nat_add_less_by_max:
"\<lbrakk> (x::nat) \<le> xmax ; y < k - xmax \<rbrakk> \<Longrightarrow> x + y < k"
by simp
lemma ucast_or_distrib:
fixes x :: "'a::len word"
fixes y :: "'a::len word"
shows
"(ucast (x || y) :: ('b::len) word) = ucast x || ucast y"
unfolding ucast_def Word.bitOR_word.abs_eq uint_or
by blast
(* FIXME move *)
lemma of_nat_shiftl:
"(of_nat x << n) = (of_nat (x * 2 ^ n) :: ('a::len) word)"
proof -
have "(of_nat x::'a word) << n = of_nat (2 ^ n) * of_nat x"
using shiftl_t2n by auto
thus ?thesis by simp
qed
lemma unat_of_nat_shiftl_or_8_32: (* FIXME generalise *)
"\<lbrakk> x * 2 ^ n < 256 ; y < 256 \<rbrakk>
\<Longrightarrow> unat (((of_nat x << n) :: 8 word) || of_nat y :: 8 word) = unat (((of_nat x << n):: machine_word) || of_nat y :: machine_word)"
apply (subst unat_ucast_upcast[where 'b=8 and 'a=32,symmetric])
apply (simp add: is_up)
apply (subst ucast_or_distrib)
apply (subst of_nat_shiftl)
apply (subst ucast_of_nat_small, simp)
apply (subst ucast_of_nat_small, simp)
apply (simp add: of_nat_shiftl)
done
(* FIXME move *)
lemma word_clz_max:
"word_clz w \<le> size (w::'a::len word)"
unfolding word_clz_def
apply (simp add: word_size)
apply (rule_tac y="length (to_bl w)" in order_trans)
apply (rule List.length_takeWhile_le)
apply simp
done
(* FIXME move *)
lemma word_clz_nonzero_max:
fixes w :: "'a::len word"
assumes nz: "w \<noteq> 0"
shows "word_clz w < size (w::'a::len word)"
proof -
{
assume a: "word_clz w = size (w::'a::len word)"
hence "length (takeWhile Not (to_bl w)) = length (to_bl w)"
by (simp add: word_clz_def word_size)
hence allj: "\<forall>j\<in>set(to_bl w). \<not> j"
using takeWhile_take_has_property[where n="length (to_bl w)" and xs="to_bl w" and P=Not]
by simp
hence "to_bl w = replicate (length (to_bl w)) False"
by - (blast intro: list_of_false)
hence "w = 0"
apply simp
apply (subst (asm) to_bl_0[symmetric])
apply (drule Word.word_bl.Rep_eqD, assumption)
done
with nz have False by simp
}
thus ?thesis using word_clz_max
by (fastforce intro: le_neq_trans)
qed
(* FIXME: Move to an appropriate place in lib/ somewhere*)
lemma ucast_sub_ucast:
fixes x :: "'a::len word"
assumes "y \<le> x"
assumes T: "len_of TYPE('a) \<le> len_of TYPE('b)"
shows "ucast (x - y) = (ucast x - ucast y :: 'b::len word)"
proof -
from T
have P: "unat x < 2 ^ len_of TYPE('b)" "unat y < 2 ^ len_of TYPE('b)"
by (fastforce intro!: less_le_trans[OF unat_lt2p])+
thus ?thesis
by (simp add: unat_arith_simps unat_ucast split assms[simplified unat_arith_simps])
qed
(* FIXME move *)
lemma setVMRoot_valid_queues':
"\<lbrace> valid_queues' \<rbrace> setVMRoot a \<lbrace> \<lambda>_. valid_queues' \<rbrace>"
@ -361,6 +444,20 @@ lemma queue_in_range_pre:
lemmas queue_in_range' = queue_in_range_pre[unfolded numDomains_def numPriorities_def, simplified]
lemma clzl_spec:
"\<forall>s. \<Gamma> \<turnstile> {\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0} Call clzl_'proc
\<lbrace>\<acute>ret__long = of_nat (word_clz (x_' s)) \<rbrace>"
apply (rule allI, rule conseqPre, vcg)
apply clarsimp
apply (rule_tac x="ret__long_'_update f x" for f in exI)
apply (simp add: mex_def meq_def)
done
lemma l1index_to_prio_spec:
"\<forall>s. \<Gamma> \<turnstile> {s} Call l1index_to_prio_'proc
\<lbrace>\<acute>ret__unsigned_long = l1index_' s << wordRadix \<rbrace>"
by vcg (simp add: word_sle_def wordRadix_def')
lemma getCurDomain_ccorres_dom_':
"ccorres (\<lambda>rv rv'. rv' = ucast rv) dom_'
\<top> UNIV hs curDomain (\<acute>dom :== \<acute>ksCurDomain)"
@ -370,6 +467,73 @@ lemma getCurDomain_ccorres_dom_':
rf_sr_ksCurDomain)
done
lemma getReadyQueuesL1Bitmap_sp:
"\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<rbrace>
getReadyQueuesL1Bitmap d
\<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d = rv \<and> d \<le> maxDomain \<and> P s\<rbrace>"
unfolding bitmap_fun_defs
by wp simp
(* this doesn't actually carry over d \<le> maxDomain to the rest of the ccorres,
use ccorres_cross_over_guard to do that *)
lemma ccorres_pre_getReadyQueuesL1Bitmap:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. d \<le> maxDomain \<and> (\<forall>rv. ksReadyQueuesL1Bitmap s d = rv \<longrightarrow> P rv s))
{s. \<forall>rv. (ksReadyQueuesL1Bitmap_' (globals s)).[unat d] = ucast rv
\<longrightarrow> s \<in> P' rv }
hs (getReadyQueuesL1Bitmap d >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l2)
defer
defer
apply (rule getReadyQueuesL1Bitmap_sp)
apply blast
apply clarsimp
prefer 3
apply (clarsimp simp: bitmap_fun_defs gets_exs_valid)
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply blast
apply assumption
apply (drule rf_sr_cbitmap_L1_relation)
apply (clarsimp simp: cbitmap_L1_relation_def)
done
lemma getReadyQueuesL2Bitmap_sp:
"\<lbrace>\<lambda>s. P s \<and> d \<le> maxDomain \<and> i \<le> numPriorities div wordBits \<rbrace>
getReadyQueuesL2Bitmap d i
\<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, i) = rv \<and> d \<le> maxDomain \<and> i \<le> numPriorities div wordBits \<and> P s\<rbrace>"
unfolding bitmap_fun_defs
by wp simp
lemma ccorres_pre_getReadyQueuesL2Bitmap:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
shows "ccorres r xf
(\<lambda>s. d \<le> maxDomain \<and> i \<le> numPriorities div wordBits
\<and> (\<forall>rv. ksReadyQueuesL2Bitmap s (d,i) = rv \<longrightarrow> P rv s))
{s. \<forall>rv. (ksReadyQueuesL2Bitmap_' (globals s)).[unat d].[i] = ucast rv
\<longrightarrow> s \<in> P' rv }
hs (getReadyQueuesL2Bitmap d i >>= (\<lambda>rv. f rv)) c"
apply (rule ccorres_guard_imp)
apply (rule ccorres_symb_exec_l2)
defer
defer
apply (rule getReadyQueuesL2Bitmap_sp)
apply blast
apply clarsimp
prefer 3
apply (clarsimp simp: bitmap_fun_defs gets_exs_valid)
defer
apply (rule ccorres_guard_imp)
apply (rule cc)
apply blast
apply assumption
apply (drule rf_sr_cbitmap_L2_relation)
apply (clarsimp simp: cbitmap_L2_relation_def)
done
lemma switchToThread_ccorres':
"ccorres (\<lambda>_ _. True) xfdc
(all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t)
@ -382,6 +546,89 @@ lemma switchToThread_ccorres':
apply auto
done
lemma cguard_UNIV:
"P s \<Longrightarrow> s \<in> (if P s then UNIV else {})"
by fastforce
lemma lookupBitmapPriority_le_maxPriority:
"\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; valid_queues s \<rbrakk>
\<Longrightarrow> lookupBitmapPriority d s \<le> maxPriority"
unfolding valid_queues_def valid_queues_no_bitmap_def
by (fastforce dest!: bitmapQ_from_bitmap_lookup bitmapQ_ksReadyQueuesI intro: ccontr)
lemma unat_lookupBitmapPriority_32:
"word_log2 (ksReadyQueuesL1Bitmap s d) < numPriorities div wordBits
\<Longrightarrow> unat (lookupBitmapPriority d s) =
unat (
((of_nat (word_log2 (ksReadyQueuesL1Bitmap s d)) << wordRadix) :: machine_word) ||
of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d, word_log2 (ksReadyQueuesL1Bitmap s d)))))"
unfolding lookupBitmapPriority_def l1IndexToPrio_def numPriorities_def wordBits_def
apply (simp add: word_size)
apply (subst unat_of_nat_shiftl_or_8_32)
apply (clarsimp simp: wordRadix_def)
apply (rule order_less_le_trans[OF word_log2_max])
apply (simp add: word_size)
apply simp
done
lemma rf_sr_ksReadyQueuesL1Bitmap_simp:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain \<rbrakk>
\<Longrightarrow> ksReadyQueuesL1Bitmap_' (globals s').[unat d] = ksReadyQueuesL1Bitmap \<sigma> d"
apply (drule rf_sr_cbitmap_L1_relation)
apply (simp add: cbitmap_L1_relation_def)
done
lemma rf_sr_ksReadyQueuesL1Bitmap_not_zero:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; ksReadyQueuesL1Bitmap_' (globals s').[unat d] \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0"
apply (drule rf_sr_cbitmap_L1_relation)
apply (simp add: cbitmap_L1_relation_def)
done
lemma ksReadyQueuesL1Bitmap_word_log2_max:
"\<lbrakk>valid_queues s; ksReadyQueuesL1Bitmap s d \<noteq> 0\<rbrakk>
\<Longrightarrow> word_log2 (ksReadyQueuesL1Bitmap s d) < numPriorities div wordBits"
unfolding valid_queues_def
by (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD)
lemma word_log2_max_word32[simp]:
"word_log2 (w :: 32 word) < 32"
using word_log2_max[where w=w]
by (simp add: word_size)
lemma word_log2_max_word8[simp]:
"word_log2 (w :: 8 word) < 8"
using word_log2_max[where w=w]
by (simp add: word_size)
lemma rf_sr_ksReadyQueuesL2Bitmap_simp:
"\<lbrakk> (\<sigma>, s') \<in> rf_sr ; d \<le> maxDomain ; valid_queues \<sigma> ; ksReadyQueuesL1Bitmap \<sigma> d \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap_' (globals s').[unat d].[word_log2 (ksReadyQueuesL1Bitmap \<sigma> d)] =
ksReadyQueuesL2Bitmap \<sigma> (d, word_log2 (ksReadyQueuesL1Bitmap \<sigma> d))"
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
apply (frule rf_sr_cbitmap_L2_relation)
apply (drule (1) cbitmap_L2_relationD)
apply (drule less_imp_le)
apply assumption
apply simp
done
lemma ksReadyQueuesL2Bitmap_nonzeroI:
"\<lbrakk> d \<le> maxDomain ; valid_queues s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, word_log2 (ksReadyQueuesL1Bitmap s d)) \<noteq> 0"
unfolding valid_queues_def
apply clarsimp
apply (frule bitmapQ_no_L1_orphansD)
apply (erule word_log2_nth_same)
apply clarsimp
done
(* FIXME move *)
lemma unat_add_lem':
"(unat x + unat y < 2 ^ len_of TYPE('a)) \<Longrightarrow>
(unat (x + y :: 'a :: len word) = unat x + unat y)"
by (subst unat_add_lem[symmetric], assumption)
lemma chooseThread_ccorres:
"ccorres dc xfdc all_invs_but_ct_idle_or_in_cur_domain' UNIV [] chooseThread (Call chooseThread_'proc)"
proof -
@ -390,13 +637,61 @@ proof -
note ksReadyQueuesL2Bitmap_nonzeroI [simp]
note Collect_const_mem [simp]
have signed_word_log2:
"\<And>w. w \<noteq> 0 \<Longrightarrow> (0x1F::32 signed word) - of_nat (word_clz (w::machine_word)) = (of_nat (word_log2 w))"
unfolding word_log2_def
by (clarsimp dest!: word_clz_nonzero_max simp: word_size)
have b[simp]:
"\<And>w. unat (of_nat (word_log2 (w :: machine_word)) :: machine_word) = word_log2 w"
by (fastforce simp add: unat_of_nat
intro: mod_less order_less_le_trans[OF word_log2_max_word32])
have unat_ucast_d[simp]:
"\<And>d. d \<le> maxDomain \<Longrightarrow> unat (ucast d * 0x100 :: machine_word) = unat d * 256"
by (subst unat_mult_simple)
(simp add: word_bits_def maxDomain_def numDomains_def word_le_nat_alt)+
(* FIXME word automation anyone? *)
have word_clz_sint_upper[simp]:
"\<And>(w::machine_word). sint (of_nat (word_clz w) :: 32 signed word) \<le> 2147483679"
apply (subst sint_eq_uint)
apply (rule not_msb_from_less)
apply simp
apply (rule word_of_nat_less)
apply simp
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (subst uint_nat)
apply (simp add: unat_of_nat)
apply (subst mod_less)
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (rule iffD2 [OF le_nat_iff[symmetric]])
apply simp
apply (rule order_trans[OF word_clz_max])
apply (simp add: word_size)
done
have word_clz_sint_lower[simp]:
"\<And>(w::machine_word). - sint (of_nat (word_clz w) :: 32 signed word) \<le> 2147483616"
apply (subst sint_eq_uint)
apply (rule not_msb_from_less)
apply simp
apply (rule word_of_nat_less)
apply simp
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (subst uint_nat)
apply (simp add: unat_of_nat)
done
have invs_no_cicd'_max_CurDomain[intro]:
"\<And>s. invs_no_cicd' s \<Longrightarrow> ksCurDomain s \<le> maxDomain"
by (simp add: invs_no_cicd'_def)
show ?thesis
apply (cinit)
apply ccorres_rewrite
apply (simp add: numDomains_def word_sless_alt word_sle_def)
apply (ctac (no_vcg) add: getCurDomain_ccorres_dom_')
apply clarsimp
@ -407,54 +702,127 @@ proof -
apply (rename_tac l1)
apply (rule_tac R="\<lambda>s. l1 = ksReadyQueuesL1Bitmap s curdom \<and> curdom \<le> maxDomain"
in ccorres_cond)
subgoal by (fastforce dest!: rf_sr_cbitmap_L1_relation simp: cbitmap_L1_relation_def)
prefer 2 -- "switchToIdleThread"
apply (fastforce dest!: rf_sr_cbitmap_L1_relation simp: cbitmap_L1_relation_def)
prefer 2
apply (ctac(no_vcg) add: switchToIdleThread_ccorres)
apply clarsimp
apply (rule ccorres_rhs_assoc)+
apply (rule ccorres_split_nothrow_novcg)
apply (rule_tac xf'=prio_' in ccorres_call)
apply (rule getHighestPrio_ccorres[simplified getHighestPrio_def'])
apply simp+
apply ceqv
apply clarsimp
apply (rename_tac prio)
apply (rule_tac P="curdom \<le> maxDomain" in ccorres_cross_over_guard_no_st)
apply (rule_tac P="prio \<le> maxPriority" in ccorres_cross_over_guard_no_st)
apply (rule ccorres_pre_getQueue)
apply (rule_tac P="queue \<noteq> []" in ccorres_cross_over_guard_no_st)
apply (rule ccorres_symb_exec_l)
apply (rule ccorres_assert)
apply csymbr
apply (rule ccorres_Guard_Seq)+
apply (rule ccorres_symb_exec_r)
apply (simp only: ccorres_seq_skip)
apply (rule ccorres_call[OF switchToThread_ccorres']; simp)
apply vcg
apply (rule conseqPre, vcg)
apply clarsimp
apply wp
apply (simp add: isRunnable_def)
apply wp
apply (clarsimp simp: Let_def guard_is_UNIV_def)
apply (drule invs_no_cicd'_queues)
apply (case_tac queue, simp)
apply (clarsimp simp: tcb_queue_relation'_def cready_queues_index_to_C_def
numPriorities_def )
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (rule_tac x="unat curdom * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
subgoal by (simp add: word_le_nat_alt[symmetric])
subgoal by (simp add: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
apply wp
apply clarsimp
apply (frule invs_no_cicd'_queues)
apply (frule invs_no_cicd'_max_CurDomain)
apply (frule invs_no_cicd'_queues)
apply (clarsimp simp: valid_queues_def lookupBitmapPriority_le_maxPriority)
apply (intro conjI impI)
apply (fastforce dest: bitmapQ_from_bitmap_lookup simp: valid_bitmapQ_bitmapQ_simp)
apply (fastforce dest: lookupBitmapPriority_obj_at'
simp: pred_conj_def comp_def obj_at'_def st_tcb_at'_def)
apply (rule ccorres_Guard_Seq)
apply (rule ccorres_pre_getReadyQueuesL2Bitmap)
apply (rename_tac l2)
apply (rule ccorres_pre_getQueue)
apply (rule_tac P="queue \<noteq> []" in ccorres_cross_over_guard_no_st)
apply (rule ccorres_symb_exec_l)
apply (rule ccorres_assert)
apply csymbr
apply (rule ccorres_abstract_cleanup)
apply (rule ccorres_Guard_Seq)+
apply csymbr
apply (rule ccorres_Guard_Seq)+
apply csymbr
apply (rule ccorres_abstract_cleanup)
apply (rule ccorres_Guard_Seq)+
apply csymbr
apply csymbr
apply csymbr
apply csymbr
apply (rule ccorres_Guard_Seq)+
apply (rule ccorres_symb_exec_r)
apply (simp only: ccorres_seq_skip)
apply (rule ccorres_call)
apply (rule switchToThread_ccorres')
apply simp
apply simp
apply simp
apply vcg
apply clarsimp
apply vcg_step (* vcg creates a state that's not printable in a sane amount of time *)
apply clarsimp
apply wp
apply (simp add: isRunnable_def)
apply wp
apply (rename_tac s' d)
apply (clarsimp simp: Let_def)
apply (safe, simp_all add: invs_no_cicd'_max_CurDomain)
(*12 subgoals *)
apply (drule invs_no_cicd'_queues)
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp signed_word_log2)
apply (simp add: rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
apply (case_tac queue, simp)
apply (clarsimp simp: tcb_queue_relation'_def cready_queues_index_to_C_def
numPriorities_def l1IndexToPrio_def)
apply (erule trans[rotated])
apply (subst unat_of_nat_shiftl_or_8_32)
apply (clarsimp simp: wordRadix_def)
apply (fastforce dest: ksReadyQueuesL1Bitmap_word_log2_max
simp: numPriorities_def wordBits_def word_size)
apply (drule_tac s=s in ksReadyQueuesL1Bitmap_word_log2_max, assumption)
apply (rule order_less_le_trans[OF word_log2_max_word32] ; simp)
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
apply (frule (1) lookupBitmapPriority_le_maxPriority)
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (simp add: unat_lookupBitmapPriority_32)
apply (subst unat_add_lem')
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
apply (simp add: word_le_nat_alt)
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (rename_tac \<sigma>)
apply (drule invs_no_cicd'_queues)
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
apply (frule (1) ksReadyQueuesL1Bitmap_word_log2_max)
apply (frule (1) lookupBitmapPriority_le_maxPriority)
apply (simp add: word_less_nat_alt word_le_nat_alt unat_lookupBitmapPriority_32)
apply (subst unat_add_lem')
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
apply (simp add: word_le_nat_alt)
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (rule_tac x="unat d * 256" and xmax="unat maxDomain * 256" in nat_add_less_by_max)
apply (simp add: word_le_nat_alt)
apply (rule order_le_less_trans)
apply (simp add: word_le_nat_alt)
apply (clarsimp simp: maxDomain_def numDomains_def maxPriority_def numPriorities_def)
apply (simp add: field_simps)
apply (fastforce dest!: invs_no_cicd'_queues
simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp
signed_word_log2)
apply (rename_tac \<sigma>)
apply (drule invs_no_cicd'_queues)
apply (clarsimp simp: rf_sr_ksReadyQueuesL1Bitmap_simp rf_sr_ksReadyQueuesL2Bitmap_simp signed_word_log2)
apply (drule word_log2_nth_same)
apply (drule bitmapQ_no_L1_orphansD[rotated])
apply (simp add: valid_queues_def)
apply (fastforce intro!: cguard_UNIV word_of_nat_less
simp: numPriorities_def wordBits_def word_size)
apply (fastforce simp: field_simps)
apply (fastforce dest: word_log2_nth_same bitmapQ_no_L1_orphansD[rotated] invs_no_cicd'_queues
simp: valid_queues_def)
apply (clarsimp dest!: invs_no_cicd'_queues simp add: valid_queues_def)
apply (drule (2) bitmapQ_from_bitmap_lookup)
apply (simp only: valid_bitmapQ_bitmapQ_simp lookupBitmapPriority_def)
apply (frule invs_no_cicd'_queues)
apply (clarsimp simp add: valid_queues_def)
apply (drule (2) bitmapQ_from_bitmap_lookup)
apply (simp only: valid_bitmapQ_bitmapQ_simp)
apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)", simp)
apply (rename_tac t ts)
apply (frule_tac t=t in valid_queues_no_bitmap_objD)
apply (blast intro: cons_set_intro)
apply (simp add: lookupBitmapPriority_def)
apply (clarsimp simp: obj_at'_def st_tcb_at'_def)
apply (fold lookupBitmapPriority_def)
apply (drule invs_no_cicd'_queues)
apply (erule (1) lookupBitmapPriority_le_maxPriority)
apply (simp add: invs_no_cicd'_def)+
done
qed

4
proof/crefine/StateRelation_C.thy
View File

@ -665,9 +665,9 @@ definition
\<Rightarrow> ((domain \<times> nat) \<Rightarrow> machine_word) \<Rightarrow> bool"
where
"cbitmap_L2_relation cbitmap2 abitmap2 \<equiv>
\<forall>d i. ((d \<le> maxDomain \<and> i < l2BitmapSize)
\<forall>d i. ((d \<le> maxDomain \<and> i \<le> numPriorities div wordBits)
\<longrightarrow> cbitmap2.[unat d].[i] = abitmap2 (d, i)) \<and>
((\<not> (d \<le> maxDomain \<and> i < l2BitmapSize))
((\<not> (d \<le> maxDomain \<and> i \<le> numPriorities div wordBits))
\<longrightarrow> abitmap2 (d, i) = 0)"
end

2
proof/crefine/Syscall_C.thy
View File

@ -1169,7 +1169,7 @@ lemma handleReply_ccorres:
apply clarsimp
apply (intro allI conjI impI,
simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs invs_ksCurDomain_maxDomain')
simp_all add: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs)
apply (rule tcb_aligned', rule tcb_at_invs', simp)
apply (auto simp: cte_wp_at_ctes_of valid_cap'_def
dest!: ctes_of_valid')[1]

127
proof/invariant-abstract/DetSchedSchedule_AI.thy
View File

@ -1579,7 +1579,7 @@ lemma set_scheduler_action_swt_weak_valid_sched:
done
lemma possible_switch_to_valid_sched:
"\<lbrace>valid_sched and st_tcb_at runnable target and not_cur_thread target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
"\<lbrace>valid_sched and st_tcb_at runnable target and (\<lambda>s. \<not> on_same_prio \<longrightarrow> not_cur_thread target s) and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
possible_switch_to target on_same_prio \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
apply (simp add: possible_switch_to_def | wp static_imp_conj_wp static_imp_wp
tcb_sched_action_enqueue_valid_blocked
@ -1589,15 +1589,12 @@ lemma possible_switch_to_valid_sched:
done
lemma switch_if_required_to_valid_sched:
"\<lbrace>valid_sched and not_cur_thread target and st_tcb_at runnable target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
switch_if_required_to target\<lbrace>\<lambda>rv. valid_sched\<rbrace>"
"\<lbrace>valid_sched and not_cur_thread target and st_tcb_at runnable target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace> switch_if_required_to target\<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (simp add: switch_if_required_to_def | wp possible_switch_to_valid_sched)+
lemma attempt_switch_to_valid_sched:
"\<lbrace>valid_sched and st_tcb_at runnable target and not_cur_thread target
and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
attempt_switch_to target \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (simp add: attempt_switch_to_def not_cur_thread_def | wp possible_switch_to_valid_sched)+
"\<lbrace>valid_sched and st_tcb_at runnable target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace> attempt_switch_to target \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (simp add: attempt_switch_to_def | wp possible_switch_to_valid_sched)+
lemma set_sched_action_cnt_not_cur_thread[wp]:
"\<lbrace>\<top>\<rbrace> set_scheduler_action choose_new_thread \<lbrace>\<lambda>rv. not_cur_thread t\<rbrace>"
@ -1740,8 +1737,7 @@ lemma reschedule_required_switch_valid_sched:
by (simp add: valid_sched_def | wp reschedule_required_switch_valid_blocked | force)+
lemma set_scheduler_action_swt_weak_valid_sched':
"\<lbrace>valid_sched_except_blocked and valid_blocked_except t and st_tcb_at runnable t
and in_cur_domain t and simple_sched_action\<rbrace>
"\<lbrace>valid_sched_except_blocked and valid_blocked_except t and st_tcb_at runnable t and in_cur_domain t and simple_sched_action\<rbrace>
set_scheduler_action (switch_thread t)
\<lbrace>\<lambda>_.valid_sched\<rbrace>"
apply (simp add: set_scheduler_action_def)
@ -1750,28 +1746,18 @@ lemma set_scheduler_action_swt_weak_valid_sched':
done
lemma possible_switch_to_valid_sched':
"\<lbrace>valid_sched_except_blocked and valid_blocked_except target and st_tcb_at runnable target
and not_cur_thread target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
possible_switch_to target cur_thread_will_block
\<lbrace>\<lambda>rv. valid_sched\<rbrace>"
"\<lbrace>valid_sched_except_blocked and valid_blocked_except target and st_tcb_at runnable target and (\<lambda>s. \<not> on_same_prio \<longrightarrow> not_cur_thread target s) and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
possible_switch_to target on_same_prio \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
apply (simp add: possible_switch_to_def)
apply (wp static_imp_conj_wp reschedule_required_switch_valid_sched
apply (simp | wp static_imp_conj_wp reschedule_required_switch_valid_sched
tcb_sched_action_enqueue_valid_blocked
| wpc | wp_once hoare_vcg_all_lift | simp)+
apply (wp_once set_scheduler_action_swt_weak_valid_sched')
apply (wp tcb_sched_action_enqueue_valid_blocked)
(* 10 subgoals *)
apply (simp | wp static_imp_conj_wp reschedule_required_switch_valid_sched
tcb_sched_action_enqueue_valid_blocked
| wpc
| wp_once hoare_vcg_all_lift)+
apply (simp add: tcb_sched_action_def)
apply (wp static_imp_wp)
(* 1 subgoal *)
set_scheduler_action_swt_weak_valid_sched' | wpc
| wp_once hoare_vcg_all_lift)+
apply (simp add: tcb_sched_action_def)
apply (wp static_imp_wp)
apply (clarsimp simp: etcb_at'_def not_cur_thread_2_def valid_sched_def valid_sched_action_def in_cur_domain_def ct_in_cur_domain_2_def valid_blocked_def valid_blocked_except_def split: option.splits)
apply (rename_tac cur_tcb target_tcb)
apply (intro conjI impI)
apply (force+)[8]
apply (force+)[8]
apply (clarsimp simp: valid_blocked_except_def)
apply (case_tac "t=target")
apply (force simp: not_queued_def tcb_sched_enqueue_def split: split_if_asm)
@ -1787,8 +1773,7 @@ lemma possible_switch_to_valid_sched':
done
lemma attempt_switch_to_valid_sched':
"\<lbrace>valid_sched_except_blocked and valid_blocked_except target and st_tcb_at runnable target
and not_cur_thread target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
"\<lbrace>valid_sched_except_blocked and valid_blocked_except target and st_tcb_at runnable target and (\<lambda>s. target \<noteq> idle_thread s)\<rbrace>
attempt_switch_to target \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
by (simp add: attempt_switch_to_def | wp possible_switch_to_valid_sched')+
@ -2170,13 +2155,8 @@ crunch valid_sched[wp]: do_ipc_transfer, handle_fault_reply valid_sched
(wp: crunch_wps)
end
lemma thread_set_ct_active_wp:
"\<lbrace> ct_active \<rbrace> thread_set (tcb_fault_update u) t \<lbrace>\<lambda>rv. ct_active \<rbrace>"
by (wp ct_in_state_thread_state_lift thread_set_no_change_tcb_state, simp)
lemma do_reply_transfer_valid_sched[wp]:
"\<lbrace>valid_sched and valid_objs and ct_active and cte_wp_at (op = (ReplyCap t' False)) slot
and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
"\<lbrace>valid_sched and valid_objs and cte_wp_at (op = (ReplyCap t' False)) slot and (\<lambda>s. receiver \<noteq> idle_thread s)\<rbrace>
do_reply_transfer sender receiver slot
\<lbrace>\<lambda>rv. valid_sched\<rbrace>"
apply (simp add: do_reply_transfer_def)
@ -2185,31 +2165,26 @@ lemma do_reply_transfer_valid_sched[wp]:
apply (wp set_thread_state_runnable_valid_queues
set_thread_state_runnable_valid_sched_action
set_thread_state_valid_blocked_except sts_st_tcb_at')[1]
apply (rule_tac Q="\<lambda>_. valid_sched and not_cur_thread receiver
and (\<lambda>s. receiver \<noteq> idle_thread s)"
in hoare_strengthen_post)
apply (rule_tac Q="\<lambda>_. valid_sched and (\<lambda>s. receiver \<noteq> idle_thread s)" in hoare_strengthen_post)
apply wp
apply (simp add: valid_sched_def)
apply (wp attempt_switch_to_valid_sched')
apply simp
apply (rule conjI)
apply clarsimp
apply (rule_tac P="valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver
and ct_active and (\<lambda>s. receiver \<noteq> idle_thread s)" in hoare_weaken_pre)
apply (rule_tac P="valid_sched and st_tcb_at (\<lambda>ts. \<not> runnable ts) receiver and (\<lambda>s. receiver \<noteq> idle_thread s)" in hoare_weaken_pre)
apply (wp set_thread_state_runnable_valid_queues
set_thread_state_runnable_valid_sched_action
set_thread_state_valid_blocked_except sts_st_tcb_at')[1]
apply (fastforce simp: valid_sched_def ct_in_state_def st_tcb_at_def not_cur_thread_def
obj_at_def)
apply (simp add: valid_sched_def)
apply clarsimp
apply (wp set_thread_state_not_runnable_valid_sched)
apply simp
apply (wp thread_set_not_state_valid_sched thread_set_no_change_tcb_state
cap_delete_one_reply_st_tcb_at thread_set_ct_active_wp | simp add: ct_in_state_def | wps)+
cap_delete_one_reply_st_tcb_at | simp)+
apply (wp hoare_drop_imps hoare_vcg_all_lift)[1]
apply (simp add: get_thread_state_def thread_get_def | wp)+
apply (clarsimp simp: ct_in_state_def cte_wp_at_caps_of_state not_cur_thread_def)
apply (fastforce simp: st_tcb_def2)
apply (fastforce simp: st_tcb_at_get_lift)
done
lemma set_thread_state_not_queued_valid_queues:
@ -2323,11 +2298,11 @@ crunch sched_act_not[wp]: set_thread_state, set_endpoint "scheduler_act_not t"
(wp: hoare_drop_imps)
lemma send_ipc_valid_sched:
"\<lbrace>valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread
and (ct_active or ct_idle) and invs\<rbrace>
"\<lbrace>valid_sched and st_tcb_at active thread and scheduler_act_not thread and not_queued thread and invs\<rbrace>
send_ipc block call badge can_grant thread epptr \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
apply (simp add: send_ipc_def)
apply (wp set_thread_state_sched_act_not_valid_sched | wpc)+
apply (wp set_thread_state_sched_act_not_valid_sched | wpc )+
apply ((wp set_thread_state_sched_act_not_valid_sched
setup_caller_cap_sched_act_not_valid_sched
attempt_switch_to_valid_sched'
@ -2335,34 +2310,29 @@ lemma send_ipc_valid_sched:
apply (wp set_thread_state_runnable_valid_queues
set_thread_state_runnable_valid_sched_action
set_thread_state_valid_blocked_except sts_st_tcb_at')[1]
apply (clarsimp simp: conj_ac eq_commute)
apply (rename_tac recvr q recv_state)
apply (rule_tac Q="\<lambda>_. valid_sched and scheduler_act_not thread and not_queued thread
and (\<lambda>s. recvr \<noteq> cur_thread s)
and (\<lambda>s. recvr \<noteq> idle_thread s \<and> recvr \<noteq> thread)"
in hoare_strengthen_post)
apply ((wp thread_set_ct_active_wp|wpc)+)[1]
apply simp
apply (rule_tac Q="\<lambda>_. valid_sched and scheduler_act_not thread and not_queued thread and (\<lambda>s. x21 \<noteq> idle_thread s \<and> x21 \<noteq> thread)" in hoare_strengthen_post)
apply ((wp|wpc)+)[1]
apply (clarsimp simp: valid_sched_def)
apply (clarsimp simp: ct_in_state_def cte_wp_at_caps_of_state not_cur_thread_def)
apply (simp | wp gts_wp hoare_vcg_all_lift)+
apply (rename_tac recvr q recv_state)
apply (wp hoare_vcg_imp_lift)
apply ((simp add: set_endpoint_def set_object_def | wp hoare_drop_imps | wpc)+)[1]
apply (wp hoare_vcg_imp_lift get_object_wp | simp add: get_endpoint_def | wpc |
wp_once hoare_vcg_all_lift)+
apply (subst st_tcb_at_kh_simp[symmetric])
apply (clarsimp simp: st_tcb_at_kh_split_if pred_tcb_at_def2
apply (subst st_tcb_at_kh_simp[symmetric])
apply (clarsimp simp: st_tcb_at_kh_split_if pred_tcb_at_def2 obj_at_def
valid_sched_def valid_sched_action_def
weak_valid_sched_action_def)+
apply (clarsimp simp: scheduler_act_not_def)
apply (subgoal_tac "xb \<noteq> idle_thread s")
apply fastforce
apply clarsimp
apply (frule invs_valid_idle)
apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)
apply (force simp: scheduler_act_not_def)
apply (clarsimp simp: st_tcb_at_kh_split_if pred_tcb_at_def2 obj_at_def
valid_sched_def valid_sched_action_def
weak_valid_sched_action_def scheduler_act_not_def)+
apply (rename_tac tcb recvr q rtcb ep)
apply (case_tac "recvr = idle_thread s")
subgoal by (fastforce dest: invs_valid_idle simp: valid_idle_def pred_tcb_at_def obj_at_def)
apply (case_tac "recvr = cur_thread s")
subgoal by (fastforce simp: ct_in_state_def st_tcb_at_def2 obj_at_def)
apply (clarsimp simp: is_activatable_def)
subgoal by (fastforce simp: valid_sched_def ct_in_state_def st_tcb_at_def not_cur_thread_def
obj_at_def)
apply fastforce+
weak_valid_sched_action_def)+
done
crunch not_queued[wp]: thread_set "not_queued t"
@ -2379,15 +2349,9 @@ lemma thread_set_tcb_fault_set_invs:
lemma send_fault_ipc_valid_sched[wp]:
"\<lbrace>valid_sched and st_tcb_at active tptr and scheduler_act_not tptr and
not_queued tptr and (ct_active or ct_idle) and invs and (\<lambda>_. valid_fault fault)\<rbrace>
send_fault_ipc tptr fault
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
not_queued tptr and invs and (\<lambda>_. valid_fault fault)\<rbrace> send_fault_ipc tptr fault \<lbrace>\<lambda>_. valid_sched\<rbrace>"
apply (simp add: send_fault_ipc_def Let_def)
apply (wp send_ipc_valid_sched thread_set_not_state_valid_sched thread_set_no_change_tcb_state
hoare_gen_asm'[OF thread_set_tcb_fault_set_invs] hoare_drop_imps hoare_vcg_all_lift_R
ct_in_state_thread_state_lift thread_set_no_change_tcb_state
hoare_vcg_disj_lift
| wpc | simp | wps)+
apply (wp send_ipc_valid_sched thread_set_not_state_valid_sched thread_set_no_change_tcb_state hoare_gen_asm'[OF thread_set_tcb_fault_set_invs] hoare_drop_imps hoare_vcg_all_lift_R | wpc | simp)+
done
crunch valid_sched[wp]: delete_caller_cap valid_sched
@ -2437,15 +2401,11 @@ lemma send_fault_ipc_error_not_queued[wp]:
wp hoare_drop_imps hoare_vcg_all_lift_R | wpc)+
lemma handle_fault_valid_sched:
"\<lbrace>valid_sched and st_tcb_at active thread and not_queued thread and (ct_active or ct_idle)
and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ex)\<rbrace>
"\<lbrace>valid_sched and st_tcb_at active thread and not_queued thread and scheduler_act_not thread and invs and (\<lambda>_. valid_fault ex)\<rbrace>
handle_fault thread ex \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
unfolding handle_fault_def
by (simp add: handle_fault_def |
wp handle_double_fault_valid_sched send_fault_ipc_valid_sched)+
by (simp add: handle_fault_def | wp handle_double_fault_valid_sched send_fault_ipc_valid_sched)+
context begin interpretation Arch . (*FIXME: arch_split*)
lemma activate_thread_valid_sched:
"\<lbrace>valid_sched\<rbrace> activate_thread \<lbrace>\<lambda>_. valid_sched\<rbrace>"
apply (simp add: activate_thread_def)
@ -3140,5 +3100,4 @@ lemma call_kernel_valid_sched:
apply (force intro: active_from_running)+
done
end

11
proof/refine/Invariants_H.thy
View File

@ -858,12 +858,10 @@ where
definition
(* for given domain and priority, the scheduler bitmap indicates a thread is in the queue *)
(* second level of the bitmap is stored in reverse for better cache locality in common case *)
bitmapQ :: "domain \<Rightarrow> priority \<Rightarrow> kernel_state \<Rightarrow> bool"
where
"bitmapQ d p s \<equiv> ksReadyQueuesL1Bitmap s d !! prioToL1Index p
\<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p))
!! unat (p && mask wordRadix)"
\<and> ksReadyQueuesL2Bitmap s (d, prioToL1Index p) !! unat (p && mask wordRadix)"
definition
valid_queues_no_bitmap :: "kernel_state \<Rightarrow> bool"
@ -880,8 +878,7 @@ definition
bitmapQ_no_L2_orphans :: "kernel_state \<Rightarrow> bool"
where
"bitmapQ_no_L2_orphans \<equiv> \<lambda>s.
\<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize
\<longrightarrow> (ksReadyQueuesL1Bitmap s d !! i)"
\<forall>d i j. ksReadyQueuesL2Bitmap s (d, i) !! j \<longrightarrow> (ksReadyQueuesL1Bitmap s d !! i)"
definition
(* If the scheduler finds a set bit in L1 of the bitmap, it must find some bit set in L2
@ -893,8 +890,8 @@ definition
bitmapQ_no_L1_orphans :: "kernel_state \<Rightarrow> bool"
where
"bitmapQ_no_L1_orphans \<equiv> \<lambda>s.
\<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and>
i < l2BitmapSize"
\<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, i) \<noteq> 0 \<and>
i < numPriorities div wordBits"
definition
valid_bitmapQ :: "kernel_state \<Rightarrow> bool"

4
proof/refine/IpcCancel_R.thy
View File

@ -1339,8 +1339,8 @@ definition
lemma removeFromBitmap_conceal_valid_inQ_queues[wp]:
"\<lbrace> valid_inQ_queues \<rbrace> removeFromBitmap_conceal d p q t \<lbrace> \<lambda>_. valid_inQ_queues \<rbrace>"
unfolding valid_inQ_queues_def removeFromBitmap_conceal_def
by (wp|clarsimp simp: bitmap_fun_defs)+
unfolding bitmap_fun_defs valid_inQ_queues_def removeFromBitmap_conceal_def
by wp clarsimp
lemma tcbSchedDequeue_valid_inQ_queues[wp]:
"\<lbrace>valid_inQ_queues\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>"

21
proof/refine/Ipc_R.thy
View File

@ -2059,7 +2059,7 @@ lemma possibleSwitchTo_invs'[wp]:
"\<lbrace>invs' and st_tcb_at' runnable' t
and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
possibleSwitchTo t b \<lbrace>\<lambda>rv. invs'\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp static_imp_wp ssa_invs' threadGet_wp | wpc | simp)+
apply (auto simp: obj_at'_def tcb_in_cur_domain'_def)
done
@ -2568,8 +2568,7 @@ lemma attemptSwitchTo_weak_sch_act_wf[wp]:
"\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace>
attemptSwitchTo t \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: attemptSwitchTo_def possibleSwitchTo_def
setSchedulerAction_def threadGet_def curDomain_def
bitmap_fun_defs)
setSchedulerAction_def threadGet_def curDomain_def)
apply (wp rescheduleRequired_weak_sch_act_wf
weak_sch_act_wf_lift_linear[where f="tcbSchedEnqueue t"]
getObject_tcb_wp static_imp_wp
@ -2979,7 +2978,7 @@ lemma possibleSwitchTo_sch_act[wp]:
"\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace>
possibleSwitchTo t b
\<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp static_imp_wp threadSet_sch_act setQueue_sch_act threadGet_wp
| simp add: unless_def | wpc)+
apply (auto simp: obj_at'_def projectKOs tcb_in_cur_domain'_def)
@ -2992,7 +2991,7 @@ lemma possibleSwitchTo_valid_queues[wp]:
"\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace>
possibleSwitchTo t b
\<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp hoare_drop_imps | wpc | simp)+
apply (auto simp: valid_tcb'_def weak_sch_act_wf_def
dest: pred_tcb_at'
@ -3008,7 +3007,7 @@ lemma possibleSwitchTo_ksQ':
"\<lbrace>(\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> sch_act_not t' s) and K(t' \<noteq> t)\<rbrace>
possibleSwitchTo t same
\<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp static_imp_wp rescheduleRequired_ksQ' tcbSchedEnqueue_ksQ threadGet_wp
| wpc
| simp split del: split_if)+
@ -3025,7 +3024,7 @@ lemma possibleSwitchTo_valid_queues'[wp]:
and st_tcb_at' runnable' t\<rbrace>
possibleSwitchTo t b
\<lbrace>\<lambda>rv. valid_queues'\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp static_imp_wp threadGet_wp | wpc | simp)+
apply (auto simp: obj_at'_def)
done
@ -3042,7 +3041,7 @@ lemma possibleSwitchTo_iflive[wp]:
and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)\<rbrace>
possibleSwitchTo t b
\<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp | wpc | simp)+
apply (simp only: imp_conv_disj, wp hoare_vcg_all_lift hoare_vcg_disj_lift)
apply (wp threadGet_wp)
@ -3796,8 +3795,7 @@ lemma possibleSwitchTo_weak_sch_act[wp]:
"\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s\<rbrace>
possibleSwitchTo t b
\<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def
bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def)
apply (wp static_imp_wp rescheduleRequired_weak_sch_act_wf threadGet_wp | wpc)+
apply (clarsimp simp: obj_at'_def projectKOs weak_sch_act_wf_def
objBits_simps ps_clear_def)
@ -4430,8 +4428,7 @@ lemma setupCaller_pred_tcb_recv':
lemma possibleSwitchTo_sch_act_not:
"\<lbrace>sch_act_not t' and K (t \<noteq> t')\<rbrace> possibleSwitchTo t b \<lbrace>\<lambda>rv. sch_act_not t'\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def
bitmap_fun_defs)
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def)
apply (wp hoare_drop_imps | wpc | simp)+
done

3
proof/refine/Orphanage.thy
View File

@ -772,6 +772,7 @@ lemma chooseThread_no_orphans [wp]:
apply (wp assert_inv ThreadDecls_H_switchToThread_no_orphans)
apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def
valid_queues_def st_tcb_at'_def)
apply (fold lookupBitmapPriority_def)
apply (fastforce dest!: lookupBitmapPriority_obj_at' elim: obj_at'_weaken
simp: all_active_tcb_ptrs_def)
apply (simp add: bitmap_fun_defs | wp)+
@ -905,7 +906,7 @@ lemma possibleSwitchTo_almost_no_orphans [wp]:
"\<lbrace> \<lambda>s. almost_no_orphans target s \<and> valid_queues' s \<and> st_tcb_at' runnable' target s \<rbrace>
possibleSwitchTo target onSamePriority
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding possibleSwitchTo_def bitmap_fun_defs
unfolding possibleSwitchTo_def
apply (wp tcbSchedEnqueue_almost_no_orphans ssa_almost_no_orphans static_imp_wp | wpc | clarsimp)+
apply (wp hoare_drop_imps | clarsimp)+
done

174
proof/refine/Schedule_R.thy
View File

@ -43,6 +43,17 @@ lemma return_wp_exs_valid [wp]: "\<lbrace> P x \<rbrace> return x \<exists>\<lbr
lemma get_exs_valid [wp]: "\<lbrace>op = s\<rbrace> get \<exists>\<lbrace>\<lambda>r. op = s\<rbrace>"
by (simp add: get_def exs_valid_def)
lemma countLeadingZeros_word_clz[simp]:
"countLeadingZeros w = word_clz w"
unfolding countLeadingZeros_def word_clz_def
by (simp add: to_bl_upt)
lemma wordLog2_word_log2[simp]:
"wordLog2 = word_log2"
apply (rule ext)
unfolding wordLog2_def word_log2_def
by (simp add: word_size wordBits_def)
lemma invs_no_cicd'_queues:
"invs_no_cicd' s \<Longrightarrow> valid_queues s"
unfolding invs_no_cicd'_def
@ -326,20 +337,20 @@ lemma removeFromBitmap_valid_queues_no_bitmap[wp]:
" \<lbrace> valid_queues_no_bitmap \<rbrace>
removeFromBitmap d p
\<lbrace>\<lambda>_. valid_queues_no_bitmap \<rbrace>"
unfolding bitmapQ_defs valid_queues_no_bitmap_def
by (wp| clarsimp simp: bitmap_fun_defs comp_def pred_conj_def)+
unfolding bitmapQ_defs bitmap_fun_defs valid_queues_no_bitmap_def
by (wp, clarsimp)
lemma removeFromBitmap_valid_queues_no_bitmap_except[wp]:
" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
removeFromBitmap d p
\<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>"
unfolding bitmapQ_defs valid_queues_no_bitmap_except_def
by (wp| clarsimp simp: bitmap_fun_defs)+
unfolding bitmapQ_defs bitmap_fun_defs valid_queues_no_bitmap_except_def
by (wp, clarsimp)
lemma removeFromBitmap_bitmapQ:
"\<lbrace> \<lambda>s. True \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. \<not> bitmapQ d p s \<rbrace>"
unfolding bitmapQ_defs bitmap_fun_defs
apply (wp| clarsimp simp: bitmap_fun_defs)+
apply wp
apply (clarsimp simp: bitmapQ_def ucast_and_mask[symmetric] is_up unat_ucast_upcast)
apply (subst (asm) complement_nth_w2p, simp_all)
apply (fastforce intro!: order_less_le_trans[OF word_unat_mask_lt] simp: word_size wordRadix_def')
@ -512,8 +523,8 @@ crunch norq[wp]: threadSet "\<lambda>s. P (ksReadyQueues s)"
lemma removeFromBitmap_valid_queues'[wp]:
"\<lbrace> valid_queues' \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_queues' \<rbrace>"
unfolding valid_queues'_def
by (wp| simp add: bitmap_fun_defs)+
unfolding valid_queues'_def bitmap_fun_defs
by (wp, simp)
lemma threadSet_valid_queues'_dequeue: (* threadSet_valid_queues' is too weak for dequeue *)
"\<lbrace>\<lambda>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and>
@ -1702,13 +1713,70 @@ lemma switchToIdleThread_invs'[wp]:
done
lemma bind_dummy_ret_val:
"do y \<leftarrow> a;
b
od = do a; b od"
by simp
lemma valid_bitmapQ_bitmapQ_simp:
"\<lbrakk> valid_bitmapQ s \<rbrakk> \<Longrightarrow>
bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])"
unfolding valid_bitmapQ_def
by simp
lemma invs_bitmapQ_tcb_at_cur_domain'_hd:
"\<lbrakk> invs' s; bitmapQ (ksCurDomain s) p s;
st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s\<rbrakk>
\<Longrightarrow> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s"
apply (rule_tac xs="tl (ksReadyQueues s (ksCurDomain s, p))"
in invs_queues_tcb_in_cur_domain'[rotated], assumption, rule refl)
apply (drule invs_queues)
apply (clarsimp simp: valid_queues_def)
apply (simp add: valid_bitmapQ_bitmapQ_simp)
done
lemma shiftr_le_0:
"unat (w::'a::len word) < 2 ^ n \<Longrightarrow> w >> n = (0::'a::len word)"
by (rule word_unat.Rep_eqD) (simp add: shiftr_div_2n')
lemma prioToL1Index_l1IndexToPrio_or_id:
"\<lbrakk> unat (w'::priority) < 2 ^ wordRadix ; w < size w' \<rbrakk>
\<Longrightarrow> prioToL1Index ((l1IndexToPrio w) || w') = w"
unfolding l1IndexToPrio_def prioToL1Index_def
apply (simp add: shiftr_over_or_dist shiftr_le_0 wordRadix_def')
apply (subst shiftl_shiftr_id, simp, simp add: word_size)
apply (rule word_of_nat_less)
apply simp
apply (subst unat_of_nat_eq, simp_all add: word_size)
done
lemma word_exists_nth:
"(w::'a::len word) \<noteq> 0 \<Longrightarrow> \<exists>i. w !! i"
using word_log2_nth_same by blast
lemma bitmapQ_no_L1_orphansD:
"\<lbrakk> bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d !! i \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, i) \<noteq> 0 \<and> i < numPriorities div wordBits"
unfolding bitmapQ_no_L1_orphans_def by simp
lemma l1IndexToPrio_wordRadix_mask[simp]:
"l1IndexToPrio i && mask wordRadix = 0"
unfolding l1IndexToPrio_def
by (simp add: wordRadix_def')
definition (* convenience for use with proofs, used for chooseThread proofs *)
"lookupBitmapPriority d s \<equiv> l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) ||
of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d,
word_log2 (ksReadyQueuesL1Bitmap s d))))"
lemma bitmapQ_lookupBitmapPriority_simp: (* neater unfold, actual unfold is really ugly *)
"\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ;
valid_bitmapQ s ; bitmapQ_no_L1_orphans s \<rbrakk> \<Longrightarrow>
bitmapQ d (lookupBitmapPriority d s) s =
(ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d) \<and>
ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !!
word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))"
ksReadyQueuesL2Bitmap s (d, word_log2 (ksReadyQueuesL1Bitmap s d)) !!
word_log2 (ksReadyQueuesL2Bitmap s (d, word_log2 (ksReadyQueuesL1Bitmap s d))))"
unfolding bitmapQ_def lookupBitmapPriority_def
apply (drule word_log2_nth_same, clarsimp)
apply (drule (1) bitmapQ_no_L1_orphansD, clarsimp)
@ -1717,10 +1785,10 @@ lemma bitmapQ_lookupBitmapPriority_simp: (* neater unfold, actual unfold is real
apply (clarsimp simp: numPriorities_def wordBits_def word_size)
apply (subst prioToL1Index_l1IndexToPrio_or_id)
apply (simp add: wordRadix_def' unat_of_nat word_size)
apply (simp add: wordRadix_def' unat_of_nat word_size l2BitmapSize_def')
apply (simp add: wordRadix_def' unat_of_nat word_size)
apply (subst prioToL1Index_l1IndexToPrio_or_id)
apply (simp add: wordRadix_def' unat_of_nat word_size)
apply (simp add: wordRadix_def' unat_of_nat word_size l2BitmapSize_def')
apply (simp add: wordRadix_def' unat_of_nat word_size)
apply (simp add: word_ao_dist)
apply (subst less_mask_eq)
apply (fastforce intro: word_of_nat_less simp: wordRadix_def' unat_of_nat word_size)+
@ -1746,7 +1814,8 @@ lemma lookupBitmapPriority_obj_at':
(hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s"
apply (drule (2) bitmapQ_from_bitmap_lookup)
apply (simp add: valid_bitmapQ_bitmapQ_simp)
apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)", simp)
apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)") (* FIXME use a split rule?*)
apply simp
apply (clarsimp, rename_tac t ts)
apply (drule cons_set_intro)
apply (drule (2) valid_queues_no_bitmap_objD)
@ -1809,7 +1878,7 @@ lemma bitmapL1_highest_lookup:
apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def')
apply (simp add: word_size)
apply (drule (1) bitmapQ_no_L1_orphansD[where d=d and i="word_log2 _"])
apply (simp add: numPriorities_def wordBits_def word_size l2BitmapSize_def')
apply (simp add: numPriorities_def wordBits_def word_size)
apply simp
apply (rule prioToL1Index_le_index[rotated], simp)
apply (frule (2) bitmapQ_from_bitmap_lookup)
@ -1820,7 +1889,7 @@ lemma bitmapL1_highest_lookup:
apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size)
apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def')
apply (fastforce dest: bitmapQ_no_L1_orphansD
simp: wordBits_def numPriorities_def word_size l2BitmapSize_def')
simp: wordBits_def numPriorities_def word_size)
apply (erule word_log2_highest)
done
@ -1906,7 +1975,8 @@ lemma switchToIdleThread_curr_is_idle:
lemma chooseThread_it[wp]:
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
by (wp|clarsimp simp: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs|assumption)+
by (simp add: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs)
(wp, clarsimp)
lemma valid_queues_ct_update[simp]:
"Invariants_H.valid_queues (s\<lparr>ksCurThread := t\<rparr>) = Invariants_H.valid_queues s"
@ -2363,6 +2433,7 @@ proof -
"ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}) \<noteq> []")
apply (fastforce elim!: setcomp_Max_has_prop)+
apply (clarsimp dest!: invs_no_cicd'_queues)
apply (fold lookupBitmapPriority_def)
apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at')
done
qed
@ -2481,12 +2552,6 @@ lemma nextDomain_invs_no_cicd':
all_invs_but_ct_idle_or_in_cur_domain'_def)
done
lemma bind_dummy_ret_val:
"do y \<leftarrow> a;
b
od = do a; b od"
by simp
lemma schedule_ChooseNewThread_fragment_corres:
"corres dc (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread))
(do _ \<leftarrow> when (domainTime = 0) next_domain;
@ -2951,59 +3016,40 @@ lemma sbn_sch_act_sane:
apply (simp add: setBoundNotification_def)
apply (wp | simp add: threadSet_sch_act_sane sane_update)+
done
lemma possibleSwitchTo_corres:
"corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t)
(Invariants_H.valid_queues and valid_queues' and
(\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs')
(possible_switch_to t b)
(possibleSwitchTo t b)"
apply (simp add: possible_switch_to_def possibleSwitchTo_def cong: if_cong)
apply (simp add: possible_switch_to_def
possibleSwitchTo_def cong: if_cong)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ gct_corres])
apply simp
apply (rule corres_split[OF _ curDomain_corres])
apply (rule corres_split[OF _ ethreadget_corres[where r="op ="]])
apply (rule corres_split[OF _ ethreadget_corres[where r="op ="]])
apply (rule corres_split[OF _ ethreadget_corres[where r="op ="]])
apply (rule corres_split[OF _ get_sa_corres])
apply (rule corres_if)
apply (simp+)[2]
apply (rule tcbSchedEnqueue_corres)
apply (rule_tac r'="\<lambda>r r'. r = (r' = 0)" in corres_split)
apply (rename_tac no_sched_targets l1)
apply (rule_tac r'="\<lambda>rv rv'. no_sched_targets \<or> rv' = rv" in corres_split)
apply (rename_tac highest_prio highestPrio)
apply (rule corres_split[where r'=dc])
apply (case_tac action,simp_all)[1]
apply (rule rescheduleRequired_corres)
apply (rule corres_if)
apply (case_tac action,auto)[1]
apply (rule set_sa_corres)
apply simp
apply (rule tcbSchedEnqueue_corres)
apply (wp add: set_scheduler_action_wp del: ssa_lift | simp)+
apply (rule_tac Q="\<lambda>r. st_tcb_at' runnable' t and tcb_in_cur_domain' t" in valid_prove_more)
apply (rule ssa_lift)
apply (clarsimp simp: valid_queues'_def weak_sch_act_wf_def
Invariants_H.valid_queues_def
tcb_in_cur_domain'_def st_tcb_at'_def
valid_queues_no_bitmap_def bitmapQ_defs)
apply ((wp threadGet_wp | simp add: etcb_relation_def curDomain_def)+)[1]
apply (rule_tac P=\<top> and P'="\<lambda>s. Invariants_H.valid_queues s \<and>
l1 = ksReadyQueuesL1Bitmap s curDom"
in corres_inst)
apply (simp add: valid_queues_def, intro allI impI disjCI2)
apply (fastforce simp: lookupBitmapPriority_Max_eqI state_relation_def
ready_queues_relation_def)
apply ((wp threadGet_wp | simp add: etcb_relation_def curDomain_def)+)
apply (rule_tac P=\<top> and P'="Invariants_H.valid_queues" in corres_inst)
apply (simp add: valid_queues_def getReadyQueuesL1Bitmap_def, intro allI impI)
apply (fastforce simp add: bitmapL1_zero_ksReadyQueues state_relation_def ready_queues_relation_def)
apply ((wp threadGet_wp | simp add: etcb_relation_def curDomain_def)+)
apply (simp add: getReadyQueuesL1Bitmap_def)
apply ((wp threadGet_wp | simp add: etcb_relation_def curDomain_def)+)
apply (rule corres_split[OF _ ethreadget_corres[where r="op ="]])
apply (rule corres_split[OF _ ethreadget_corres[where r="op ="]])
apply (rule corres_split[OF _ ethreadget_corres[where r="op ="]])
apply (rule corres_split[OF _ get_sa_corres])
apply (rule corres_if)
apply (simp+)[2]
apply (rule tcbSchedEnqueue_corres)
apply (rule corres_split[where r'=dc])
apply (case_tac action,simp_all)[1]
apply (rule rescheduleRequired_corres)
apply (rule corres_if)
apply (case_tac action,simp_all)[1]
apply (rule set_sa_corres)
apply simp
apply (rule tcbSchedEnqueue_corres)
apply (wp add: set_scheduler_action_wp del: ssa_lift | simp)+
apply (rule_tac Q="\<lambda>r. st_tcb_at' runnable' t and tcb_in_cur_domain' t" in valid_prove_more)
apply (rule ssa_lift)
apply (clarsimp simp: valid_queues'_def weak_sch_act_wf_def Invariants_H.valid_queues_def
tcb_in_cur_domain'_def st_tcb_at'_def valid_queues_no_bitmap_def
bitmapQ_defs)
apply (wp threadGet_wp | simp add: etcb_relation_def curDomain_def)+
apply (clarsimp simp: is_etcb_at_def valid_sched_action_def weak_valid_sched_action_def)
apply (clarsimp simp: valid_sched_def etcb_at_def cur_tcb_def split: option.splits)
apply (frule st_tcb_at_tcb_at)

4
proof/refine/Syscall_R.thy
View File

@ -2115,9 +2115,7 @@ crunch sane [wp]: transferCaps "sch_act_sane"
lemma possibleSwitchTo_sane:
"\<lbrace>\<lambda>s. sch_act_sane s \<and> t \<noteq> ksCurThread s\<rbrace> possibleSwitchTo t b \<lbrace>\<lambda>_. sch_act_sane\<rbrace>"
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def
bitmap_fun_defs
cong: if_cong)
apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def cong: if_cong)
apply (wp hoare_drop_imps | wpc)+
apply (simp add: sch_act_sane_def)
done

228
proof/refine/TcbAcc_R.thy
View File

@ -30,75 +30,10 @@ declare complement_def[simp]
(* Auxiliaries and basic properties of priority bitmap functions *)
lemma countLeadingZeros_word_clz[simp]:
"countLeadingZeros w = word_clz w"
unfolding countLeadingZeros_def word_clz_def
by (simp add: to_bl_upt)
lemma wordLog2_word_log2[simp]:
"wordLog2 = word_log2"
apply (rule ext)
unfolding wordLog2_def word_log2_def
by (simp add: word_size wordBits_def)
lemmas bitmap_fun_defs = addToBitmap_def removeFromBitmap_def
modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
(* lookupBitmapPriority is a cleaner version of getHighestPrio *)
definition
"lookupBitmapPriority d s \<equiv>
l1IndexToPrio (word_log2 (ksReadyQueuesL1Bitmap s d)) ||
of_nat (word_log2 (ksReadyQueuesL2Bitmap s (d,
invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))"
lemma getHighestPrio_def'[simp]:
"getHighestPrio d = gets (lookupBitmapPriority d)"
unfolding getHighestPrio_def gets_def
by (fastforce simp: gets_def get_bind_apply lookupBitmapPriority_def bitmap_fun_defs)
lemma getHighestPrio_inv[wp]:
"\<lbrace> P \<rbrace> getHighestPrio d \<lbrace>\<lambda>_. P \<rbrace>"
unfolding bitmap_fun_defs by simp
lemma valid_bitmapQ_bitmapQ_simp:
"\<lbrakk> valid_bitmapQ s \<rbrakk> \<Longrightarrow>
bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])"
unfolding valid_bitmapQ_def
by simp
lemma invs_bitmapQ_tcb_at_cur_domain'_hd:
"\<lbrakk> invs' s; bitmapQ (ksCurDomain s) p s;
st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, p))) s\<rbrakk>
\<Longrightarrow> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, p))) s"
apply (rule_tac xs="tl (ksReadyQueues s (ksCurDomain s, p))"
in invs_queues_tcb_in_cur_domain'[rotated], assumption, rule refl)
apply (drule invs_queues)
apply (clarsimp simp: valid_queues_def)
apply (simp add: valid_bitmapQ_bitmapQ_simp)
done
lemma prioToL1Index_l1IndexToPrio_or_id:
"\<lbrakk> unat (w'::priority) < 2 ^ wordRadix ; w < size w' \<rbrakk>
\<Longrightarrow> prioToL1Index ((l1IndexToPrio w) || w') = w"
unfolding l1IndexToPrio_def prioToL1Index_def
apply (simp add: shiftr_over_or_dist shiftr_le_0 wordRadix_def')
apply (subst shiftl_shiftr_id, simp, simp add: word_size)
apply (rule word_of_nat_less)
apply simp
apply (subst unat_of_nat_eq, simp_all add: word_size)
done
lemma bitmapQ_no_L1_orphansD:
"\<lbrakk> bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d !! i \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize"
unfolding bitmapQ_no_L1_orphans_def by simp
lemma l1IndexToPrio_wordRadix_mask[simp]:
"l1IndexToPrio i && mask wordRadix = 0"
unfolding l1IndexToPrio_def
by (simp add: wordRadix_def')
definition
(* when in the middle of updates, a particular queue might not be entirely valid *)
valid_queues_no_bitmap_except :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool"
@ -114,12 +49,21 @@ lemma valid_queues_no_bitmap_exceptI[intro]:
by simp
lemma valid_queues_no_bitmap_exceptE:
"\<lbrakk> valid_queues_no_bitmap_except t s ;
"\<lbrakk> valid_queues_no_bitmap_except t s ;
\<And>d p. t \<in> set (ksReadyQueues s (d,p)) \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) t s \<rbrakk>
\<Longrightarrow> valid_queues_no_bitmap s"
\<Longrightarrow> valid_queues_no_bitmap s"
unfolding valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def
by fastforce
lemma bitmapL2_L1_limitD:
"\<lbrakk> ksReadyQueuesL2Bitmap s (d, i) !! j ; bitmapQ_no_L1_orphans s ; bitmapQ_no_L2_orphans s \<rbrakk>
\<Longrightarrow> i < numPriorities div wordBits"
unfolding bitmapQ_no_L1_orphans_def bitmapQ_no_L2_orphans_def
by blast
lemma valid_objs_valid_tcbE: "\<And>s t.\<lbrakk> valid_objs' s; tcb_at' t s; \<And>tcb. valid_tcb' tcb s \<Longrightarrow> R s tcb \<rbrakk> \<Longrightarrow> obj_at' (R s) t s"
apply (clarsimp simp add: projectKOs valid_objs'_def ran_def typ_at'_def
ko_wp_at'_def valid_obj'_def valid_tcb'_def obj_at'_def)
@ -1982,9 +1926,10 @@ lemma addToBitmap_if_null_corres_noop: (* used this way in Haskell code *)
lemma removeFromBitmap_corres_noop:
"corres dc \<top> \<top> (return ()) (removeFromBitmap tdom prioa)"
unfolding removeFromBitmap_def
unfolding removeFromBitmap_def modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def
modifyReadyQueuesL2Bitmap_def getReadyQueuesL2Bitmap_def
by (rule corres_noop)
(wp | simp add: bitmap_fun_defs state_relation_def | rule no_fail_pre)+
(wp | simp add: state_relation_def | rule no_fail_pre)+
crunch typ_at'[wp]: addToBitmap "\<lambda>s. P (typ_at' T p s)"
(wp: hoare_drop_imps setCTE_typ_at')
@ -2134,13 +2079,15 @@ lemmas threadSet_weak_sch_act_wf
lemma removeFromBitmap_nosch[wp]:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
unfolding removeFromBitmap_def
by (simp add: bitmap_fun_defs|wp setObject_nosch)+
unfolding removeFromBitmap_def getReadyQueuesL1Bitmap_def modifyReadyQueuesL1Bitmap_def
getReadyQueuesL2Bitmap_def modifyReadyQueuesL2Bitmap_def
by (simp|wp setObject_nosch)+
lemma addToBitmap_nosch[wp]:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> addToBitmap d p \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
unfolding addToBitmap_def
by (simp add: bitmap_fun_defs|wp setObject_nosch)+
unfolding addToBitmap_def getReadyQueuesL1Bitmap_def modifyReadyQueuesL1Bitmap_def
getReadyQueuesL2Bitmap_def modifyReadyQueuesL2Bitmap_def
by (simp|wp setObject_nosch)+
lemmas removeFromBitmap_weak_sch_act_wf[wp]
= weak_sch_act_wf_lift[OF removeFromBitmap_nosch]
@ -2167,15 +2114,19 @@ crunch obj_at'[wp]: addToBitmap "obj_at' P t"
lemma removeFromBitmap_tcb_in_cur_domain'[wp]:
"\<lbrace>tcb_in_cur_domain' t\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace>"
unfolding tcb_in_cur_domain'_def removeFromBitmap_def
modifyReadyQueuesL2Bitmap_def getReadyQueuesL2Bitmap_def
modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def
apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf)
apply (wp setObject_cte_obj_at_tcb' | simp add: bitmap_fun_defs)+
apply (wp setObject_cte_obj_at_tcb' | simp)+
done
lemma addToBitmap_tcb_in_cur_domain'[wp]:
"\<lbrace>tcb_in_cur_domain' t\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>ya. tcb_in_cur_domain' t\<rbrace>"
unfolding tcb_in_cur_domain'_def addToBitmap_def
modifyReadyQueuesL2Bitmap_def getReadyQueuesL2Bitmap_def
modifyReadyQueuesL1Bitmap_def getReadyQueuesL1Bitmap_def
apply (rule_tac f="\<lambda>s. ksCurDomain s" in hoare_lift_Pf)
apply (wp setObject_cte_obj_at_tcb' | simp add: bitmap_fun_defs)+
apply (wp setObject_cte_obj_at_tcb' | simp)+
done
lemma tcbSchedDequeue_weak_sch_act_wf[wp]:
@ -2798,16 +2749,6 @@ lemma threadGet_const:
apply (clarsimp simp: obj_at'_def)
done
schematic_goal l2BitmapSize_def': (* arch specific consequence *)
"l2BitmapSize = numeral ?X"
by (simp add: l2BitmapSize_def wordBits_def word_size numPriorities_def)
lemma prioToL1Index_size [simp]:
"prioToL1Index w < l2BitmapSize"
unfolding prioToL1Index_def wordRadix_def l2BitmapSize_def'
by (fastforce simp: shiftr_div_2n' nat_divide_less_eq
intro: order_less_le_trans[OF unat_lt2p])
lemma prioToL1Index_max:
"prioToL1Index p < 2 ^ wordRadix"
unfolding prioToL1Index_def wordRadix_def
@ -2815,8 +2756,8 @@ lemma prioToL1Index_max:
lemma prioToL1Index_bit_set:
"((2 :: 32 word) ^ prioToL1Index p) !! prioToL1Index p"
using l2BitmapSize_def'
by (fastforce simp: nth_w2p_same intro: order_less_le_trans[OF prioToL1Index_size])
using prioToL1Index_max[simplified wordRadix_def]
by (fastforce simp: nth_w2p_same)
lemma prioL2Index_bit_set:
fixes p :: priority
@ -2831,7 +2772,7 @@ lemma addToBitmap_bitmapQ:
unfolding addToBitmap_def
modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
by (wp, clarsimp simp: bitmap_fun_defs bitmapQ_def prioToL1Index_bit_set prioL2Index_bit_set)
by (wp, clarsimp simp: bitmapQ_def prioToL1Index_bit_set prioL2Index_bit_set)
lemma addToBitmap_valid_queues_no_bitmap_except:
" \<lbrace> valid_queues_no_bitmap_except t \<rbrace>
@ -2904,15 +2845,15 @@ lemma valid_queues_no_bitmap_except_objD:
lemma bitmapQ_no_L1_orphansE:
"\<lbrakk> bitmapQ_no_L1_orphans s ;
ksReadyQueuesL1Bitmap s d !! i \<rbrakk>
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0"
\<Longrightarrow> ksReadyQueuesL2Bitmap s (d, i) \<noteq> 0"
unfolding bitmapQ_no_L1_orphans_def
by clarsimp
lemma bitmapQ_no_L2_orphansE:
"\<lbrakk> bitmapQ_no_L2_orphans s ;
ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix) \<rbrakk>
ksReadyQueuesL2Bitmap s (d, prioToL1Index p) !! unat (p && mask wordRadix) \<rbrakk>
\<Longrightarrow> ksReadyQueuesL1Bitmap s d !! prioToL1Index p"
unfolding bitmapQ_no_L2_orphans_def using prioToL1Index_size
unfolding bitmapQ_no_L2_orphans_def
by blast
lemma valid_bitmapQ_exceptE:
@ -2921,34 +2862,25 @@ lemma valid_bitmapQ_exceptE:
unfolding valid_bitmapQ_except_def
by blast
lemma invertL1Index_eq_cancelD:
"\<lbrakk> invertL1Index i = invertL1Index j ; i < l2BitmapSize ; j < l2BitmapSize \<rbrakk>
\<Longrightarrow> i = j"
by (simp add: invertL1Index_def l2BitmapSize_def')
lemma invertL1Index_eq_cancel:
"\<lbrakk> i < l2BitmapSize ; j < l2BitmapSize \<rbrakk>
\<Longrightarrow> (invertL1Index i = invertL1Index j) = (i = j)"
by (rule iffI, simp_all add: invertL1Index_eq_cancelD)
lemma removeFromBitmap_bitmapQ_no_L1_orphans[wp]:
"\<lbrace> bitmapQ_no_L1_orphans \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>"
unfolding bitmap_fun_defs
apply (wp | simp add: bitmap_fun_defs bitmapQ_no_L1_orphans_def)+
apply (fastforce simp: invertL1Index_eq_cancel prioToL1Index_bit_not_set
prioToL1Index_complement_nth_w2p)
done
by (wp)
(fastforce simp: prioToL1Index_complement_nth_w2p bitmapQ_no_L1_orphans_def)
lemma removeFromBitmap_bitmapQ_no_L2_orphans[wp]:
"\<lbrace> bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans \<rbrace>
removeFromBitmap d p
\<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>"
unfolding bitmap_fun_defs
apply (wp, clarsimp simp: bitmap_fun_defs bitmapQ_no_L2_orphans_def)+
apply (rule conjI, clarsimp)
apply (rule conjI, clarsimp)
apply (clarsimp simp: complement_nth_w2p l2BitmapSize_def')
apply clarsimp
apply (wp, clarsimp)
apply (rule conjI)
apply (clarsimp simp: bitmapQ_no_L2_orphans_def prioToL1Index_complement_nth_w2p)
apply (subst prioToL1Index_complement_nth_w2p')
apply (rule order_less_le_trans[OF bitmapL2_L1_limitD], simp_all add: bitmapQ_no_L2_orphans_def)[1]
apply (simp add: word_size numPriorities_def wordBits_def)
apply simp
apply (clarsimp simp: bitmapQ_no_L2_orphans_def)
apply metis
done
@ -2980,7 +2912,7 @@ proof -
apply (clarsimp simp: bitmapQ_def)
apply (rule conjI; clarsimp)
apply (rename_tac p')
apply (rule conjI; clarsimp simp: invertL1Index_eq_cancel)
apply (rule conjI; clarsimp)
apply (drule_tac p=p' in valid_bitmapQ_exceptE[where d=d], clarsimp)
apply (clarsimp simp: bitmapQ_def)
apply (drule_tac n'="unat (p' && mask wordRadix)" in no_other_bits_set)
@ -2996,7 +2928,7 @@ proof -
(* after clearing bit in L2, some bits in L2 field are still set *)
apply clarsimp
apply (subst valid_bitmapQ_except_def, clarsimp)+
apply (clarsimp simp: bitmapQ_def invertL1Index_eq_cancel)
apply (clarsimp simp: bitmapQ_def)
apply (rule conjI; clarsimp)
apply (frule (1) prioToL1Index_bits_low_high_eq)
apply (drule_tac d=d and p=pa in valid_bitmapQ_exceptE, simp)
@ -3016,6 +2948,11 @@ lemma addToBitmap_bitmapQ_no_L1_orphans[wp]:
apply (clarsimp simp: word_or_zero prioToL1Index_bit_set ucast_and_mask[symmetric]
unat_ucast_upcast is_up wordRadix_def' word_size nth_w2p
wordBits_def numPriorities_def)
apply (clarsimp simp: prioToL1Index_def wordRadix_def')
apply (rule order_less_le_trans[OF unat_shiftr_less_t2n[where m="size p - wordRadix"]])
apply (simp add: wordRadix_def wordBits_def word_size)
apply (fastforce intro: order_less_le_trans[OF unat_lt2p] simp: word_size)
apply (simp add: wordRadix_def wordBits_def word_size)
done
lemma addToBitmap_bitmapQ_no_L2_orphans[wp]:
@ -3023,56 +2960,26 @@ lemma addToBitmap_bitmapQ_no_L2_orphans[wp]:
unfolding bitmap_fun_defs bitmapQ_defs
apply wp
apply clarsimp
apply (fastforce simp: invertL1Index_eq_cancel prioToL1Index_bit_set)
apply (metis prioToL1Index_bit_set)
done
(* FIXME move *)
schematic_goal wordBits_def': "wordBits = numeral ?n" (* arch-specific consequence *)
by (simp add: wordBits_def word_size)
(* FIXME move *)
lemma mask_wordRadix_less_wordBits:
assumes sz: "wordRadix \<le> size w"
shows "unat ((w::'a::len word) && mask wordRadix) < wordBits"
proof -
note pow_num = semiring_numeral_class.power_numeral
{ assume "wordRadix = size w"
hence ?thesis
by (fastforce intro!: unat_lt2p[THEN order_less_le_trans]
simp: wordRadix_def wordBits_def' word_size)
} moreover {
assume "wordRadix < size w"
hence ?thesis unfolding wordRadix_def wordBits_def' mask_def
apply simp
apply (subst unat_less_helper, simp_all)
apply (rule word_and_le1[THEN order_le_less_trans])
apply (simp add: word_size bintrunc_mod2p)
apply (subst int_mod_eq', simp_all)
apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp)
apply (simp del: pow_num)
apply (subst int_mod_eq', simp_all)
apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp)
apply (simp del: pow_num)
done
}
ultimately show ?thesis using sz by fastforce
qed
lemma priority_mask_wordRadix_size:
"unat ((w::priority) && mask wordRadix) < wordBits"
by (rule mask_wordRadix_less_wordBits, simp add: wordRadix_def word_size)
lemma addToBitmap_valid_bitmapQ_except:
"\<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans \<rbrace>
addToBitmap d p
\<lbrace>\<lambda>_. valid_bitmapQ_except d p \<rbrace>"
unfolding bitmap_fun_defs bitmapQ_defs
apply wp
apply (clarsimp simp: bitmapQ_def prioToL1Index_nth_w2p invertL1Index_eq_cancel
ucast_and_mask[symmetric] unat_ucast_upcast is_up nth_w2p)
apply (fastforce simp: priority_mask_wordRadix_size[simplified wordBits_def']
dest: prioToL1Index_bits_low_high_eq)
apply (clarsimp simp: bitmapQ_def prioToL1Index_bit_set prioToL1Index_nth_w2p)
apply (case_tac "ksReadyQueuesL2Bitmap s (d, prioToL1Index p) !! unat (pa && mask wordRadix)")
apply (subgoal_tac "ksReadyQueuesL1Bitmap s d !! prioToL1Index p")
prefer 2
apply fastforce
apply force
apply (case_tac "ksReadyQueuesL1Bitmap s d !! prioToL1Index p")
apply (clarsimp simp: ucast_and_mask[symmetric] unat_ucast_upcast is_up nth_w2p)
apply (fastforce dest: prioToL1Index_bits_low_high_eq)
apply (clarsimp simp: ucast_and_mask[symmetric] unat_ucast_upcast is_up nth_w2p)
apply (fastforce dest: prioToL1Index_bits_low_high_eq)
done
lemma addToBitmap_valid_bitmapQ:
@ -4495,7 +4402,7 @@ lemma addToBitmap_ksMachine[wp]:
lemma removeFromBitmap_ksMachine[wp]:
"\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> removeFromBitmap d p \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>"
unfolding bitmap_fun_defs
by (wp|simp add: bitmap_fun_defs)+
by (wp, simp)
lemma tcbSchedEnqueue_ksMachine[wp]:
"\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> tcbSchedEnqueue x \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>"
@ -4515,13 +4422,14 @@ lemma setThreadState_vms'[wp]:
lemma ct_not_inQ_addToBitmap[wp]:
"\<lbrace> ct_not_inQ \<rbrace> addToBitmap d p \<lbrace>\<lambda>_. ct_not_inQ \<rbrace>"
unfolding bitmap_fun_defs
unfolding addToBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
by (wp, clarsimp simp: ct_not_inQ_def)
lemma ct_not_inQ_removeFromBitmap[wp]:
"\<lbrace> ct_not_inQ \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. ct_not_inQ \<rbrace>"
unfolding bitmap_fun_defs
by (wp|simp add: bitmap_fun_defs ct_not_inQ_def comp_def)+
unfolding removeFromBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def
by (wp, clarsimp simp: ct_not_inQ_def)
lemma setBoundNotification_vms'[wp]:
"\<lbrace>valid_machine_state'\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>"
@ -4608,7 +4516,7 @@ lemma possibleSwitchTo_ct_not_inQ:
apply (simp add: possibleSwitchTo_def curDomain_def)
apply (wp static_imp_wp rescheduleRequired_ct_not_inQ tcbSchedEnqueue_ct_not_inQ threadGet_wp
| wpc
| clarsimp simp: ct_not_inQ_update_stt bitmap_fun_defs)+
| clarsimp simp: ct_not_inQ_update_stt)+
apply (fastforce simp: obj_at'_def)
done

9
spec/abstract/Deterministic_A.thy
View File

@ -321,7 +321,7 @@ definition reschedule_required :: "unit det_ext_monad" where
definition
possible_switch_to :: "obj_ref \<Rightarrow> bool \<Rightarrow> unit det_ext_monad" where
"possible_switch_to target cur_thread_will_block \<equiv> do
"possible_switch_to target on_same_prio \<equiv> do
cur \<leftarrow> gets cur_thread;
cur_dom \<leftarrow> gets cur_domain;
cur_prio \<leftarrow> ethread_get tcb_priority cur;
@ -330,12 +330,7 @@ definition
action \<leftarrow> gets scheduler_action;
if (target_dom \<noteq> cur_dom) then tcb_sched_action tcb_sched_enqueue target
else do
no_sched_targets \<leftarrow> gets (\<lambda>s. \<forall>prio. ready_queues s cur_dom prio = []);
highest_prio \<leftarrow> gets (\<lambda>s. Max {prio. ready_queues s cur_dom prio \<noteq> []});
if ((target_prio > cur_prio
\<or> (cur_thread_will_block
\<and> (target_prio = cur_prio \<or>
no_sched_targets \<or> target_prio \<ge> highest_prio)))
if ((target_prio > cur_prio \<or> (target_prio = cur_prio \<and> on_same_prio))
\<and> action = resume_cur_thread) then set_scheduler_action $ switch_thread target
else tcb_sched_action tcb_sched_enqueue target;
case action of switch_thread _ \<Rightarrow> reschedule_required | _ \<Rightarrow> return ()

6
spec/design/Structures_H.thy
View File

@ -2190,9 +2190,6 @@ maxPriority :: "priority"
consts'
maxDomain :: "priority"
consts'
l2BitmapSize :: "nat"
consts'
nullMDBNode :: "mdbnode"
@ -2271,9 +2268,6 @@ defs maxPriority_def:
defs maxDomain_def:
"maxDomain\<equiv> fromIntegral (numDomains - 1)"
defs l2BitmapSize_def:
"l2BitmapSize\<equiv> (numPriorities + wordBits - 1) div wordBits"
defs nullMDBNode_def:
"nullMDBNode \<equiv> MDB_ \<lparr>
mdbNext= nullPointer,

6
spec/design/ThreadDecls_H.thy
View File

@ -65,12 +65,6 @@ countLeadingZeros :: "('b :: {HS_bit, finiteBit}) \<Rightarrow> nat"
consts'
wordLog2 :: "('b :: {HS_bit, finiteBit}) \<Rightarrow> nat"
consts'
invertL1Index :: "nat \<Rightarrow> nat"
consts'
getHighestPrio :: "domain \<Rightarrow> (priority) kernel"
consts'
chooseThread :: "unit kernel"

38
spec/design/Thread_H.thy
View File

@ -173,26 +173,16 @@ defs countLeadingZeros_def:
defs wordLog2_def:
"wordLog2 w \<equiv> finiteBitSize w - 1 - countLeadingZeros w"
defs invertL1Index_def:
"invertL1Index i \<equiv> l2BitmapSize - 1 - i"
defs getHighestPrio_def:
"getHighestPrio d\<equiv> (do
l1 \<leftarrow> getReadyQueuesL1Bitmap d;
l1index \<leftarrow> return ( wordLog2 l1);
l1indexInverted \<leftarrow> return ( invertL1Index l1index);
l2 \<leftarrow> getReadyQueuesL2Bitmap d l1indexInverted;
l2index \<leftarrow> return ( wordLog2 l2);
return $ l1IndexToPrio l1index || fromIntegral l2index
od)"
defs chooseThread_def:
"chooseThread\<equiv> (do
curdom \<leftarrow> if numDomains > 1 then curDomain else return 0;
l1 \<leftarrow> getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0
then (do
prio \<leftarrow> getHighestPrio curdom;
l1index \<leftarrow> return ( wordLog2 l1);
l2 \<leftarrow> getReadyQueuesL2Bitmap curdom l1index;
l2index \<leftarrow> return ( wordLog2 l2);
prio \<leftarrow> return ( l1IndexToPrio l1index || fromIntegral l2index);
queue \<leftarrow> getQueue curdom prio;
thread \<leftarrow> return ( head queue);
runnable \<leftarrow> isRunnable thread;
@ -243,7 +233,7 @@ defs setPriority_def:
od)"
defs possibleSwitchTo_def:
"possibleSwitchTo target curThreadWillBlock\<equiv> (do
"possibleSwitchTo target onSamePriority\<equiv> (do
curThread \<leftarrow> getCurThread;
curDom \<leftarrow> curDomain;
curPrio \<leftarrow> threadGet tcbPriority curThread;
@ -253,12 +243,8 @@ defs possibleSwitchTo_def:
if (targetDom \<noteq> curDom)
then tcbSchedEnqueue target
else (do
l1 \<leftarrow> getReadyQueuesL1Bitmap curDom;
highestPrio \<leftarrow> getHighestPrio curDom;
if ((targetPrio > curPrio
\<or> (curThreadWillBlock
\<and> (targetPrio = curPrio
\<or> l1 = 0 \<or> targetPrio \<ge> highestPrio)))
\<or> (targetPrio = curPrio \<and> onSamePriority))
\<and> action = ResumeCurrentThread)
then setSchedulerAction $ SwitchToThread target
else tcbSchedEnqueue target;
@ -335,24 +321,20 @@ od)"
defs addToBitmap_def:
"addToBitmap tdom prio\<equiv> (do
l1index \<leftarrow> return ( prioToL1Index prio);
l1indexInverted \<leftarrow> return ( invertL1Index l1index);
l2bit \<leftarrow> return ( fromIntegral ((fromIntegral prio && mask wordRadix)::machine_word));
modifyReadyQueuesL1Bitmap tdom (\<lambda> w. w || bit l1index);
modifyReadyQueuesL2Bitmap tdom l1indexInverted
modifyReadyQueuesL2Bitmap tdom l1index
(\<lambda> w. w || bit l2bit)
od)"
defs removeFromBitmap_def:
"removeFromBitmap tdom prio\<equiv> (do
l1index \<leftarrow> return ( prioToL1Index prio);
l1indexInverted \<leftarrow> return ( invertL1Index l1index);
l2bit \<leftarrow> return ( fromIntegral((fromIntegral prio && mask wordRadix)::machine_word));
modifyReadyQueuesL2Bitmap tdom l1indexInverted $
(\<lambda> w. w && (complement $ bit l2bit));
l2 \<leftarrow> getReadyQueuesL2Bitmap tdom l1indexInverted;
modifyReadyQueuesL2Bitmap tdom l1index (\<lambda> w. w && (complement $ bit l2bit));
l2 \<leftarrow> getReadyQueuesL2Bitmap tdom l1index;
when (l2 = 0) $
modifyReadyQueuesL1Bitmap tdom $
(\<lambda> w. w && (complement $ bit l1index))
modifyReadyQueuesL1Bitmap tdom (\<lambda> w. w && (complement $ bit l1index))
od)"
defs tcbSchedEnqueue_def:

105
spec/design/version
View File

@ -1,30 +1,89 @@
Built from git repo at /home/rafalk/repos/invert-fastpath/l4v/spec/haskell by rafalk
Built from git repo at /home/tsewell/dev/verification2/l4v/spec/haskell by tsewell
Generated from changeset:
0743585 SELFOUR-242: REBASE: FOLD
68714cd CRefine proof for preemptible retype.
Warning - uncomitted changes used:
M ../../proof/crefine/ADT_C.thy
UU ../../proof/crefine/Fastpath_C.thy
M ../../proof/crefine/Finalise_C.thy
UU ../../proof/crefine/IpcCancel_C.thy
M ../../proof/crefine/Ipc_C.thy
UU ../../proof/crefine/Recycle_C.thy
UU ../../proof/crefine/Schedule_C.thy
M ../../proof/crefine/StateRelation_C.thy
M ../../proof/crefine/Syscall_C.thy
M ../../proof/invariant-abstract/DetSchedSchedule_AI.thy
M ../../proof/refine/Invariants_H.thy
M ../../proof/refine/IpcCancel_R.thy
M ../../proof/refine/Ipc_R.thy
M ../../proof/refine/Orphanage.thy
M ../../proof/refine/Schedule_R.thy
M ../../proof/refine/Syscall_R.thy
M ../../proof/refine/TcbAcc_R.thy
M ../abstract/Deterministic_A.thy
M ../../proof/crefine/Arch_C.thy
M ../../proof/crefine/Invoke_C.thy
M ../../proof/crefine/IpcCancel_C.thy
M ../../proof/crefine/Retype_C.thy
M ../../proof/crefine/StoreWord_C.thy
M ../../proof/drefine/Untyped_DR.thy
M ../../proof/refine/ADT_H.thy
M ../../proof/refine/CNodeInv_R.thy
M ../../proof/refine/Orphanage.thy
M ../capDL/Untyped_D.thy
M ../design/Structures_H.thy
M ../design/ThreadDecls_H.thy
M ../design/Thread_H.thy
M ../design/skel/Structures_H.thy
M ../design/version
M src/SEL4/Kernel/Thread.lhs
M src/SEL4/Object/Structures.lhs
?? ../../Test.thy
?? ../../camkes/glue-proofs/umm_types.txt
?? ../../lib/Test.thy
?? ../../lib/clib/Corres_C.thy.orig
?? ../../lib/foo.c
?? ../../patch
?? ../../proof/Ctac.thy
?? ../../proof/Old_Arch.thy
?? ../../proof/Old_Retype_C.thy
?? ../../proof/Old_Retype_R.thy
?? ../../proof/Old_Untyped_AI.thy
?? ../../proof/Test.thy
?? ../../proof/access-control/Arch_AC.thy.orig
?? ../../proof/access-control/DomainSepInv.thy.orig
?? ../../proof/access-control/Retype_AC.thy.orig
?? ../../proof/access-control/Syscall_AC.thy.orig
?? ../../proof/asmrefine/CFunDump.txt
?? ../../proof/crefine/ADT_C.thy.orig
?? ../../proof/crefine/Arch_C.thy.orig
?? ../../proof/crefine/CSpace_C.thy.orig
?? ../../proof/crefine/Invoke_C.thy.orig
?? ../../proof/crefine/Recycle_C.thy.orig
?? ../../proof/crefine/Retype_C.thy.orig
?? ../../proof/crefine/StateRelation_C.thy.orig
?? ../../proof/crefine/Tcb_C.thy.orig
?? ../../proof/crefine/Test.thy
?? ../../proof/drefine/Arch_DR.thy.orig
?? ../../proof/drefine/Untyped_DR.thy.orig
?? ../../proof/foo
?? ../../proof/infoflow/Arch_IF.thy.orig
?? ../../proof/infoflow/FinalCaps.thy.orig
?? ../../proof/infoflow/IRQMasks_IF.thy.orig
?? ../../proof/infoflow/Retype_IF.thy.orig
?? ../../proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy.orig
?? ../../proof/invariant-abstract/DetSchedAux_AI.thy.orig
?? ../../proof/invariant-abstract/Untyped_AI.thy.orig
?? ../../proof/lhs_pars.py
?? ../../proof/refine/Arch_R.thy.orig
?? ../../proof/refine/CNodeInv_R.thy.orig
?? ../../proof/refine/Invariants_H.thy.orig
?? ../../proof/refine/IpcCancel_R.thy.orig
?? ../../proof/refine/Ipc_R.thy.orig
?? ../../proof/refine/Orphanage.thy.orig
?? ../../proof/refine/Untyped_R.thy.orig
?? ../../proof/switch_glob.c
?? ../../proof/switch_glob.thy
?? ../../proof/untyped.c
?? ../abstract/Retype_A.thy.orig
?? ../capDL/Untyped_D.thy.orig
?? ../cspec/c/foo.c
?? ../cspec/c/foo.s
?? ../design/CNode_H.thy.orig
?? ../design/Untyped_H.thy.orig
?? ../design/version.orig
?? ../design1/
?? ../foo.c
?? src/SEL4/Kernel/Init.lhs.orig
?? src/SEL4/Kernel/Init.lhs.rej
?? src/SEL4/Kernel/VSpace/ARM.lhs.orig
?? src/SEL4/Object/ObjectType/ARM.lhs.rej
?? src/SEL4/Object/Structures.lhs.orig
?? src/SEL4/Object/Untyped.lhs.orig
?? src/SEL4/Object/Untyped.lhs.rej
?? ../patch
?? ../../tools/autocorres/doc/quickstart/umm_types.txt
?? ../../tools/autocorres/tests/umm_types.txt
?? ../../tools/haskell-translator/caseconvs.orig
?? ../../use-this-isabelle

40
spec/haskell/src/SEL4/Kernel/Thread.lhs
View File

@ -327,14 +327,11 @@ Threads are scheduled using a simple multiple-priority round robin algorithm.
It checks the priority bitmaps to find the highest priority with a non-empty
queue. It selects the first thread in that queue and makes it the current
thread.
Note that the ready queues are a separate structure in the kernel
model. In a real implementation, to avoid requiring
dynamically-allocated kernel memory, these queues would be linked
lists using the TCBs themselves as nodes.
Note also that the level 2 bitmap array is stored in reverse in order to get better cache locality for the more common case of higher priority threads.
> countLeadingZeros :: (Bits b, FiniteBits b) => b -> Int
> countLeadingZeros w =
> length . takeWhile not . reverse . map (testBit w) $ [0 .. finiteBitSize w - 1]
@ -342,25 +339,16 @@ Note also that the level 2 bitmap array is stored in reverse in order to get bet
> wordLog2 :: (Bits b, FiniteBits b) => b -> Int
> wordLog2 w = finiteBitSize w - 1 - countLeadingZeros w
> invertL1Index :: Int -> Int
> invertL1Index i = l2BitmapSize - 1 - i
> getHighestPrio :: Domain -> Kernel (Priority)
> getHighestPrio d = do
> l1 <- getReadyQueuesL1Bitmap d
> let l1index = wordLog2 l1
> let l1indexInverted = invertL1Index l1index
> l2 <- getReadyQueuesL2Bitmap d l1indexInverted
> let l2index = wordLog2 l2
> return $ l1IndexToPrio l1index .|. fromIntegral l2index
> chooseThread :: Kernel ()
> chooseThread = do
> curdom <- if numDomains > 1 then curDomain else return 0
> l1 <- getReadyQueuesL1Bitmap curdom
> if l1 /= 0
> then do
> prio <- getHighestPrio curdom
> let l1index = wordLog2 l1
> l2 <- getReadyQueuesL2Bitmap curdom l1index
> let l2index = wordLog2 l2
> let prio = l1IndexToPrio l1index .|. fromIntegral l2index
> queue <- getQueue curdom prio
> let thread = head queue
> runnable <- isRunnable thread
@ -437,7 +425,7 @@ Finally, if the thread is the current one, we run the scheduler to choose a new
A successful IPC transfer will normally wake a thread other than the current thread. This function conditionally switches to the woken thread; it enqueues the thread if unable to switch to it.
> possibleSwitchTo :: PPtr TCB -> Bool -> Kernel ()
> possibleSwitchTo target curThreadWillBlock = do
> possibleSwitchTo target onSamePriority = do
> curThread <- getCurThread
> curDom <- curDomain
> curPrio <- threadGet tcbPriority curThread
@ -447,12 +435,8 @@ A successful IPC transfer will normally wake a thread other than the current thr
> if (targetDom /= curDom)
> then tcbSchedEnqueue target
> else do
> l1 <- getReadyQueuesL1Bitmap curDom
> highestPrio <- getHighestPrio curDom
> if ((targetPrio > curPrio
> || (curThreadWillBlock
> && (targetPrio == curPrio
> || l1 == 0 || targetPrio >= highestPrio)))
> || (targetPrio == curPrio && onSamePriority))
> && action == ResumeCurrentThread)
> then setSchedulerAction $ SwitchToThread target
> else tcbSchedEnqueue target
@ -544,23 +528,19 @@ The following two functions place a thread at the beginning or end of its priori
> addToBitmap :: Domain -> Priority -> Kernel ()
> addToBitmap tdom prio = do
> let l1index = prioToL1Index prio
> let l1indexInverted = invertL1Index l1index
> let l2bit = fromIntegral ((fromIntegral prio .&. mask wordRadix)::Word)
> modifyReadyQueuesL1Bitmap tdom $ \w -> w .|. bit l1index
> modifyReadyQueuesL2Bitmap tdom l1indexInverted
> modifyReadyQueuesL2Bitmap tdom l1index
> (\w -> w .|. bit l2bit)
> removeFromBitmap :: Domain -> Priority -> Kernel ()
> removeFromBitmap tdom prio = do
> let l1index = prioToL1Index prio
> let l1indexInverted = invertL1Index l1index
> let l2bit = fromIntegral((fromIntegral prio .&. mask wordRadix)::Word)
> modifyReadyQueuesL2Bitmap tdom l1indexInverted $
> (\w -> w .&. (complement $ bit l2bit))
> l2 <- getReadyQueuesL2Bitmap tdom l1indexInverted
> modifyReadyQueuesL2Bitmap tdom l1index $ \w -> w .&. (complement $ bit l2bit)
> l2 <- getReadyQueuesL2Bitmap tdom l1index
> when (l2 == 0) $
> modifyReadyQueuesL1Bitmap tdom $
> (\w -> w .&. (complement $ bit l1index))
> modifyReadyQueuesL1Bitmap tdom $ \w -> w .&. (complement $ bit l1index)
> tcbSchedEnqueue :: PPtr TCB -> Kernel ()
> tcbSchedEnqueue thread = do

6
spec/haskell/src/SEL4/Model/StateData.lhs
View File

@ -31,7 +31,7 @@ The architecture-specific definitions are imported qualified with the "Arch" pre
\begin{impdetails}
> import SEL4.Config (numDomains)
> import SEL4.Config (numDomains,numPriorities)
> import SEL4.API.Types
> import {-# SOURCE #-} SEL4.Model.PSpace
> import SEL4.Object.Structures
@ -114,8 +114,6 @@ Note that this definition of "KernelState" assumes a single processor. The behav
Note that the priority bitmap is split up into two levels. In order to check to see whether a priority has a runnable thread on a 32-bit system with a maximum priority of 255, we use the high 3 bits of the priority as an index into the level 1 bitmap. If the bit at that index is set, we use those same three bits to obtain a word from the level 2 bitmap. We then use the remaining 5 bits to index into that word. If the bit is set, the queue for that priority is non-empty.
Note also that due the common case being scheduling high-priority threads, the level 2 bitmap array is reversed to improve cache locality.
\subsubsection{Monads}
Kernel functions are sequences of operations that transform a "KernelState" object. They are encapsulated in the monad "Kernel", which uses "StateT" to add a "KernelState" data structure to the monad that encapsulates the simulated machine, "MachineMonad". This allows functions to read and modify the kernel state.
@ -234,7 +232,7 @@ A new kernel state structure contains an empty physical address space, a set of
> ksReadyQueuesL1Bitmap = funPartialArray (const 0) (0, fromIntegral numDomains),
> ksReadyQueuesL2Bitmap =
> funPartialArray (const 0)
> ((0, 0), (fromIntegral numDomains, l2BitmapSize)),
> ((0, 0), (fromIntegral numDomains, numPriorities `div` wordBits + 1)),
> ksCurThread = error "No initial thread",
> ksIdleThread = error "Idle thread has not been created",
> ksSchedulerAction = error "scheduler action has not been set",

5
spec/haskell/src/SEL4/Object/Structures.lhs
View File

@ -304,11 +304,6 @@ The maximum domain is derived from the configuration parameter "numDomains"
> maxDomain :: Priority
> maxDomain = fromIntegral (numDomains - 1)
The size of the level 2 bitmap array in each domain.
> l2BitmapSize :: Int
> l2BitmapSize = (numPriorities + wordBits - 1) `div` wordBits
\subsection{Other Types}
\subsubsection{Mapping Database Node}