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

riscv crefine: rename isBlocked to isStopped 

This brings the proof in sync with seL4 d5d54a0d5596e7a708

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-05-11 14:56:10 +08:00
parent c3ef1c509e
commit 9a51fc110c
4 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
proof/crefine/RISCV64/IpcCancel_C.thy
View File

@ -399,10 +399,10 @@ lemma ccorres_exI1:
apply fastforce
done
lemma isBlocked_ccorres [corres]:
lemma isStopped_ccorres [corres]:
"ccorres (\<lambda>r r'. r = to_bool r') ret__unsigned_long_'
(tcb_at' thread) (UNIV \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) []
(isBlocked thread) (Call isBlocked_'proc)"
(isStopped thread) (Call isStopped_'proc)"
apply (cinit lift: thread_' simp: getThreadState_def)
apply (rule ccorres_pre_threadGet)
apply (rule ccorres_move_c_guard_tcb)
@ -1900,8 +1900,8 @@ lemma true_eq_from_bool [simp]:
"(scast true = from_bool P) = P"
by (simp add: true_def from_bool_def split: bool.splits)
lemma isBlocked_spec:
"\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isBlocked_'proc
lemma isStopped_spec:
"\<forall>s. \<Gamma> \<turnstile> ({s} \<inter> {s. cslift s (thread_' s) \<noteq> None}) Call isStopped_'proc
{s'. ret__unsigned_long_' s' = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s (thread_' s))))) \<in>
{scast ThreadState_BlockedOnReply,
scast ThreadState_BlockedOnNotification, scast ThreadState_BlockedOnSend,
@ -2357,7 +2357,7 @@ lemma scheduleTCB_ccorres':
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cscheduler_action_relation_def)
apply wp+
apply (simp add: isRunnable_def isBlocked_def)
apply (simp add: isRunnable_def isStopped_def)
apply wp
apply (simp add: guard_is_UNIV_def)
apply clarsimp
@ -2413,7 +2413,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre:
apply (clarsimp simp: rf_sr_def cstate_relation_def cscheduler_action_relation_def
split: scheduler_action.split_asm)
apply wp+
apply (simp add: isRunnable_def isBlocked_def)
apply (simp add: isRunnable_def isStopped_def)
apply wp
apply (simp add: guard_is_UNIV_def)
apply (clarsimp simp: st_tcb_at'_def obj_at'_def)
@ -2504,7 +2504,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple:
apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
cscheduler_action_relation_def)
apply wp+
apply (simp add: isRunnable_def isBlocked_def)
apply (simp add: isRunnable_def isStopped_def)
apply wp
apply (simp add: guard_is_UNIV_def)
apply clarsimp

4
proof/crefine/RISCV64/IsolatedThreadAction.thy
View File

@ -807,7 +807,7 @@ lemma rescheduleRequired_simple_rewrite:
lemma empty_fail_isRunnable:
"empty_fail (isRunnable t)"
by (simp add: isRunnable_def isBlocked_def)
by (simp add: isRunnable_def isStopped_def)
lemma setupCallerCap_rewrite:
"monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s))
@ -909,7 +909,7 @@ lemma oblivious_switchToThread_schact:
getCurThread_def setCurThread_def threadGet_def liftM_def
threadSet_def tcbSchedEnqueue_def unless_when asUser_def
getQueue_def setQueue_def storeWordUser_def setRegister_def
pointerInUserData_def isRunnable_def isBlocked_def
pointerInUserData_def isRunnable_def isStopped_def
getThreadState_def tcbSchedDequeue_def bitmap_fun_defs)
by (safe intro!: oblivious_bind
| simp_all add: oblivious_setVMRoot_schact)+

2
proof/crefine/RISCV64/Syscall_C.thy
View File

@ -1413,7 +1413,7 @@ lemma handleRecv_ccorres:
auto simp: pred_tcb_at'_def obj_at'_def objBits_simps projectKOs ct_in_state'_def)[1]
apply wp
apply clarsimp
apply (vcg exspec=isBlocked_modifies exspec=lookupCap_modifies)
apply (vcg exspec=isStopped_modifies exspec=lookupCap_modifies)
apply wp
apply clarsimp

2
proof/crefine/RISCV64/Tcb_C.thy
View File

@ -1084,7 +1084,7 @@ lemma restart_ccorres:
(UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) []
(restart thread) (Call restart_'proc)"
apply (cinit lift: target_')
apply (ctac(no_vcg) add: isBlocked_ccorres)
apply (ctac(no_vcg) add: isStopped_ccorres)
apply (simp only: when_def)
apply (rule ccorres_cond2[where R=\<top>])
apply (simp add: to_bool_def Collect_const_mem)