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

VER-825: Change representation of SchedulerAction_ChooseNewThread from ~0 to 1 

This change was a result of the constant "(tcb_t*)~0" being defined as
0x00000000FFFFFFFF on x86-64 (0 is implicitly a 32-bit integer) rather
than 0xFFFFFFFFFFFFFFFF as expected.
This commit is contained in:
Joel Beeren 2017-12-07 11:30:25 +11:00
parent ffc0640869
commit af2b7c7792
11 changed files with 31 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
proof/crefine/ARM/ADT_C.thy
View File

@ -261,7 +261,7 @@ lemma setUserMem_C_def_foldl:
definition
"cscheduler_action_to_H p \<equiv>
if p = NULL then ResumeCurrentThread
else if p = Ptr (~~ 0) then ChooseNewThread
else if p = Ptr 1 then ChooseNewThread
else SwitchToThread (ctcb_ptr_to_tcb_ptr p)"
@ -288,9 +288,10 @@ lemma csch_act_rel_to_H:
cscheduler_action_to_H_def)
apply safe
apply (simp_all add: tcb_ptr_to_ctcb_ptr_def ctcb_ptr_to_tcb_ptr_def
ctcb_offset_defs is_aligned_mask mask_def max_word_def
ctcb_offset_defs is_aligned_mask mask_def
objBits_defs)
apply (word_bitwise, simp)
apply (word_bitwise, simp)
apply (word_bitwise, clarsimp)
done
definition

2
proof/crefine/ARM/Finalise_C.thy
View File

@ -54,7 +54,7 @@ lemma tcbSchedEnqueue_cslift_spec:
lemma setThreadState_cslift_spec:
"\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. ksSchedulerAction_' (globals s) = tcb_Ptr x
\<and> x \<noteq> 0 \<and> x \<noteq> ~~ 0
\<and> x \<noteq> 0 \<and> x \<noteq> 1
\<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s) (tcb_Ptr x) = Some v
\<and> v \<le> ucast maxPrio
\<and> option_map2 tcbDomain_C (cslift s) (tcb_Ptr x) = Some d

20
proof/crefine/ARM/IpcCancel_C.thy
View File

@ -2053,16 +2053,12 @@ lemma scheduler_action_case_switch_to_if:
then f (case act of SwitchToThread t \<Rightarrow> t) else g)"
by (simp split: scheduler_action.split)
lemma tcb_at_max_word:
"tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr max_word"
lemma tcb_at_1:
"tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr 1"
apply (drule is_aligned_tcb_ptr_to_ctcb_ptr)
apply (clarsimp simp add: is_aligned_def max_word_def ctcb_size_bits_def)
done
lemma scast_max_word [simp]:
"scast (max_word :: 32 signed word) = (max_word :: 32 word)"
by (clarsimp simp: max_word_def)
lemma rescheduleRequired_ccorres:
"ccorres dc xfdc (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs')
UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)"
@ -2075,7 +2071,7 @@ lemma rescheduleRequired_ccorres:
in ccorres_cond)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cscheduler_action_relation_def)
subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_max_word tcb_at_not_NULL
subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
split: scheduler_action.split_asm dest!: pred_tcb_at')
apply (ctac add: tcbSchedEnqueue_ccorres)
apply (rule ccorres_return_Skip)
@ -2093,8 +2089,8 @@ lemma rescheduleRequired_ccorres:
apply (simp add: getSchedulerAction_def)
apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
Let_def cscheduler_action_relation_def)
by (auto simp: tcb_at_not_NULL tcb_at_max_word
tcb_at_not_NULL[THEN not_sym] tcb_at_max_word[THEN not_sym]
by (auto simp: tcb_at_not_NULL tcb_at_1
tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
split: scheduler_action.split_asm)
lemma getReadyQueuesL1Bitmap_sp:
@ -2585,7 +2581,7 @@ lemma rescheduleRequired_ccorres_valid_queues'_simple:
in ccorres_cond)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cscheduler_action_relation_def)
apply (clarsimp simp: weak_sch_act_wf_def tcb_at_max_word tcb_at_not_NULL
apply (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
split: scheduler_action.split_asm dest!: st_tcb_strg'[rule_format])
apply (ctac add: tcbSchedEnqueue_ccorres)
apply (rule ccorres_return_Skip)
@ -2603,8 +2599,8 @@ lemma rescheduleRequired_ccorres_valid_queues'_simple:
apply (simp add: getSchedulerAction_def)
apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
Let_def cscheduler_action_relation_def)
by (auto simp: tcb_at_not_NULL tcb_at_max_word
tcb_at_not_NULL[THEN not_sym] tcb_at_max_word[THEN not_sym]
by (auto simp: tcb_at_not_NULL tcb_at_1
tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
split: scheduler_action.split_asm)
lemma scheduleTCB_ccorres_valid_queues'_pre_simple:

2
proof/crefine/ARM/Schedule_C.thy
View File

@ -673,7 +673,7 @@ lemma schedule_ccorres:
apply (clarsimp dest!: rf_sr_cscheduler_relation invs_sch_act_wf'
simp: cscheduler_action_relation_def)
apply (intro conjI impI allI; clarsimp simp: typ_heap_simps ctcb_relation_def to_bool_def)
apply (fastforce simp: tcb_at_not_NULL tcb_at_max_word dest: pred_tcb_at')+
apply (fastforce simp: tcb_at_not_NULL tcb_at_1 dest: pred_tcb_at')+
done
(* FIXME: move *)

2
proof/crefine/ARM/StateRelation_C.thy
View File

@ -635,7 +635,7 @@ definition
where
"cscheduler_action_relation a p \<equiv> case a of
ResumeCurrentThread \<Rightarrow> p = NULL
| ChooseNewThread \<Rightarrow> p = Ptr (~~ 0)
| ChooseNewThread \<Rightarrow> p = Ptr 1
| SwitchToThread p' \<Rightarrow> p = tcb_ptr_to_ctcb_ptr p'"
definition

7
proof/crefine/ARM_HYP/ADT_C.thy
View File

@ -283,7 +283,7 @@ lemma setUserMem_C_def_foldl:
definition
"cscheduler_action_to_H p \<equiv>
if p = NULL then ResumeCurrentThread
else if p = Ptr (~~ 0) then ChooseNewThread
else if p = Ptr 1 then ChooseNewThread
else SwitchToThread (ctcb_ptr_to_tcb_ptr p)"
@ -310,9 +310,10 @@ lemma csch_act_rel_to_H:
cscheduler_action_to_H_def)
apply safe
apply (simp_all add: tcb_ptr_to_ctcb_ptr_def ctcb_ptr_to_tcb_ptr_def
ctcb_offset_defs is_aligned_mask mask_def max_word_def
ctcb_offset_defs is_aligned_mask mask_def
objBits_defs)
apply (word_bitwise, simp)
apply (word_bitwise, simp)
apply (word_bitwise, clarsimp)
done
definition

2
proof/crefine/ARM_HYP/Finalise_C.thy
View File

@ -54,7 +54,7 @@ lemma tcbSchedEnqueue_cslift_spec:
lemma setThreadState_cslift_spec:
"\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> \<lbrace>s. s \<Turnstile>\<^sub>c \<acute>tptr \<and> (\<forall>x. ksSchedulerAction_' (globals s) = tcb_Ptr x
\<and> x \<noteq> 0 \<and> x \<noteq> ~~ 0
\<and> x \<noteq> 0 \<and> x \<noteq> 1
\<longrightarrow> (\<exists>d v. option_map2 tcbPriority_C (cslift s) (tcb_Ptr x) = Some v
\<and> v \<le> ucast maxPrio
\<and> option_map2 tcbDomain_C (cslift s) (tcb_Ptr x) = Some d

20
proof/crefine/ARM_HYP/IpcCancel_C.thy
View File

@ -2065,16 +2065,12 @@ lemma scheduler_action_case_switch_to_if:
then f (case act of SwitchToThread t \<Rightarrow> t) else g)"
by (simp split: scheduler_action.split)
lemma tcb_at_max_word:
"tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr max_word"
lemma tcb_at_1:
"tcb_at' t s \<Longrightarrow> tcb_ptr_to_ctcb_ptr t \<noteq> tcb_Ptr 1"
apply (drule is_aligned_tcb_ptr_to_ctcb_ptr)
apply (clarsimp simp add: is_aligned_def max_word_def ctcb_size_bits_def)
done
lemma scast_max_word [simp]:
"scast (max_word :: 32 signed word) = (max_word :: 32 word)"
by (clarsimp simp: max_word_def)
lemma rescheduleRequired_ccorres:
"ccorres dc xfdc (valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs')
UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)"
@ -2087,7 +2083,7 @@ lemma rescheduleRequired_ccorres:
in ccorres_cond)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cscheduler_action_relation_def)
subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_max_word tcb_at_not_NULL
subgoal by (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
split: scheduler_action.split_asm dest!: pred_tcb_at')
apply (ctac add: tcbSchedEnqueue_ccorres)
apply (rule ccorres_return_Skip)
@ -2105,8 +2101,8 @@ lemma rescheduleRequired_ccorres:
apply (simp add: getSchedulerAction_def)
apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
Let_def cscheduler_action_relation_def)
by (auto simp: tcb_at_not_NULL tcb_at_max_word
tcb_at_not_NULL[THEN not_sym] tcb_at_max_word[THEN not_sym]
by (auto simp: tcb_at_not_NULL tcb_at_1
tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
split: scheduler_action.split_asm)
lemma getReadyQueuesL1Bitmap_sp:
@ -2597,7 +2593,7 @@ lemma rescheduleRequired_ccorres_valid_queues'_simple:
in ccorres_cond)
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cscheduler_action_relation_def)
apply (clarsimp simp: weak_sch_act_wf_def tcb_at_max_word tcb_at_not_NULL
apply (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
split: scheduler_action.split_asm dest!: st_tcb_strg'[rule_format])
apply (ctac add: tcbSchedEnqueue_ccorres)
apply (rule ccorres_return_Skip)
@ -2615,8 +2611,8 @@ lemma rescheduleRequired_ccorres_valid_queues'_simple:
apply (simp add: getSchedulerAction_def)
apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
Let_def cscheduler_action_relation_def)
by (auto simp: tcb_at_not_NULL tcb_at_max_word
tcb_at_not_NULL[THEN not_sym] tcb_at_max_word[THEN not_sym]
by (auto simp: tcb_at_not_NULL tcb_at_1
tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
split: scheduler_action.split_asm)
lemma scheduleTCB_ccorres_valid_queues'_pre_simple:

2
proof/crefine/ARM_HYP/Schedule_C.thy
View File

@ -671,7 +671,7 @@ lemma schedule_ccorres:
apply (clarsimp dest!: rf_sr_cscheduler_relation invs_sch_act_wf'
simp: cscheduler_action_relation_def)
apply (intro conjI impI allI; clarsimp simp: typ_heap_simps ctcb_relation_def to_bool_def)
apply (fastforce simp: tcb_at_not_NULL tcb_at_max_word dest: pred_tcb_at')+
apply (fastforce simp: tcb_at_not_NULL tcb_at_1 dest: pred_tcb_at')+
done
(* FIXME: move *)

2
proof/crefine/ARM_HYP/StateRelation_C.thy
View File

@ -683,7 +683,7 @@ definition
where
"cscheduler_action_relation a p \<equiv> case a of
ResumeCurrentThread \<Rightarrow> p = NULL
| ChooseNewThread \<Rightarrow> p = Ptr (~~ 0)
| ChooseNewThread \<Rightarrow> p = Ptr 1
| SwitchToThread p' \<Rightarrow> p = tcb_ptr_to_ctcb_ptr p'"
definition

2
proof/crefine/X64/StateRelation_C.thy
View File

@ -749,7 +749,7 @@ definition
where
"cscheduler_action_relation a p \<equiv> case a of
ResumeCurrentThread \<Rightarrow> p = NULL
| ChooseNewThread \<Rightarrow> p = Ptr (~~ 0)
| ChooseNewThread \<Rightarrow> p = Ptr 1
| SwitchToThread p' \<Rightarrow> p = tcb_ptr_to_ctcb_ptr p'"
definition