update proofs for SELFOUR-30/291 "Reschedule on self-modification"

- SELFOUR-30 Reschedule when changing own IPC buffer
Previously if you invoked the TCB of the current thread and
changed the IPC buffer frame this would not immediately take
affect, as the kernels view of the current IPC buffer is
updated in Arch_switchToThread. This change forces Arch_switchToThread
to get called, even if we would switch back to the original
thread.

- SELFOUR-291 Reschedule when changing own registers
Previously if you wrote to TCB of the current thread and
changed the TLS_BASE this would not immediately take
affect, as the kernel only updates this register in
Arch_switchToThread. This change forces Arch_switchToThread
to get called, even if we would switch back to the original
thread.

proof/access-control/DomainSepInv.thy

@@ -1185,7 +1185,12 @@ lemma checked_cap_insert_domain_sep_inv:
   apply(erule (1) same_object_as_domain_sep_inv_cap)
   done
 
-crunch domain_sep_inv[wp]: bind_notification "domain_sep_inv irqs st"
+crunch domain_sep_inv[wp]: bind_notification,reschedule_required "domain_sep_inv irqs st"
+
+lemma dxo_domain_sep_inv[wp]:
+  "\<lbrace>domain_sep_inv irqs st\<rbrace> do_extended_op eop  \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>"
+  by (simp | wp dxo_wp_weak)+
+
 
 lemma set_mcpriority_domain_sep_inv[wp]:
   "\<lbrace>domain_sep_inv irqs st\<rbrace> set_mcpriority tcb_ref mcp \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>"

proof/drefine/Tcb_DR.thy

@@ -636,11 +636,17 @@ lemma invoke_tcb_corres_write_regs:
   apply (rule corres_symb_exec_r)
      apply (rule corres_guard_imp)
        apply (rule corres_split [where r'=dc])
-          apply (rule corres_cases [where R=resume])
+          apply (rule corres_dummy_return_l)
+          apply (rule corres_split [where r'=dc])
+             apply (rule corres_split_noop_rhs[OF corres_trivial])
+               apply simp
+              apply (clarsimp simp: when_def)
+              apply (rule reschedule_required_dcorres[THEN corres_trivial])
+             apply wp
+            apply (clarsimp simp: when_def)
+            apply (clarsimp simp: dc_def, rule restart_corres [unfolded dc_def])
            apply (clarsimp simp: when_def)
-           apply (rule corres_bind_return_r)
-           apply (clarsimp simp: dc_def, rule restart_corres [unfolded dc_def])
-          apply (clarsimp simp: when_def)
+          apply (wpsimp wp: hoare_when_wp restart_invs')+
          apply (rule corrupt_tcb_intent_as_user_corres)
         apply (wp wp_post_taut | simp add:invs_def valid_state_def | fastforce)+
   done
@@ -740,59 +746,67 @@ lemma invoke_tcb_corres_copy_regs:
   "\<lbrakk> t' = tcb_invocation.CopyRegisters obj_id' target_id' a b c d e;
      t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> dc) \<top>
-   (invs and tcb_at obj_id' and tcb_at target_id' and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs)
+   (invs and tcb_at obj_id' and tcb_at target_id' and Tcb_AI.tcb_inv_wf t' and not_idle_thread target_id' and not_idle_thread obj_id' and valid_etcbs)
      (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
   apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def)
   apply (rule corres_guard_imp)
     apply (rule corres_split [where r'=dc])
        apply (rule corres_split [where r'=dc])
           apply (rule corres_corrupt_tcb_intent_dupl)
           apply (rule corres_split [where r'=dc])
-             apply (rule corres_cases [where R="d"])
-              apply (clarsimp simp: when_def)
-              apply (rule corres_bind_ignore_ret_rhs)
-              apply (rule corres_return_dc_rhs)
+             apply (rule corres_dummy_return_l)
+                apply (rule corres_split [where r'=dc])
+                   apply (rule corres_symb_exec_r)
+                     apply (rule corres_split_noop_rhs[OF corres_trivial])
+                    apply simp
+                    apply (clarsimp simp: when_def)
+                   apply (rule reschedule_required_dcorres[THEN corres_trivial])
+              apply wp+
+               apply (rule corres_cases [where R="d"])
+               apply (clarsimp simp: when_def)
               apply (rule invoke_tcb_corres_copy_regs_loop)
-             apply (clarsimp simp: when_def)
+              apply (clarsimp simp: when_def)
              apply (rule dummy_corrupt_tcb_intent_corres)
-            apply (rule corres_cases [where R="c"])
-             apply (clarsimp simp: when_def)
-             apply (rule corres_bind_ignore_ret_rhs)
-             apply (rule corres_corrupt_tcb_intent_dupl)
-             apply (rule corres_split [where r'=dc])
-                apply (unfold K_bind_def)
-                apply (rule corres_symb_exec_r)
-                   apply (simp add:setNextPC_def set_register_rewrite)
-                   apply (rule Intent_DR.set_register_corres[unfolded dc_def], simp)
-                  apply (wp | clarsimp simp:getRestartPC_def)+
-               apply (rule invoke_tcb_corres_copy_regs_loop, simp)
-             apply (wp mapM_x_wp [where S=UNIV])
-             apply simp
+           apply wp+
+           apply (rule corres_cases [where R="c"])
             apply (clarsimp simp: when_def)
-            apply (rule dummy_corrupt_tcb_intent_corres)
-           apply wp
-          apply (wp mapM_x_wp [where S=UNIV])[1]
+            apply (rule corres_bind_ignore_ret_rhs)
+            apply (rule corres_corrupt_tcb_intent_dupl)
+            apply (rule corres_split [where r'=dc])
+               apply (unfold K_bind_def)
+               apply (rule corres_symb_exec_r)
+                  apply (simp add:setNextPC_def set_register_rewrite)
+                  apply (rule Intent_DR.set_register_corres[unfolded dc_def], simp)
+                 apply (wp | clarsimp simp:getRestartPC_def)+
+              apply (rule invoke_tcb_corres_copy_regs_loop, simp)
+            apply (wp mapM_x_wp [where S=UNIV])
+            apply simp
+           apply simp
+           apply (rule dummy_corrupt_tcb_intent_corres)
           apply simp
+         apply wpsimp+
+         apply (wp mapM_x_wp [where S=UNIV])[1]
+         apply simp
          apply (rule corres_cases [where R="b"])
           apply (clarsimp simp: when_def)
           apply (rule corres_alternate1)
           apply (rule restart_corres, simp)
          apply (rule corres_alternate2)
          apply (rule corres_free_return [where P="\<top>" and P'="\<top>"])
         apply (wp wp_post_taut)
-       apply (clarsimp simp:conj_comms)
-       apply (clarsimp simp: not_idle_thread_def | wp)+
+       apply (clarsimp simp:conj_comms pred_conj_def split del: if_splits cong: if_cong)
+       apply (wpsimp simp: not_idle_thread_def | rule conjI | strengthen invs_cur)+
       apply (rule corres_cases [where R="a"])
        apply (clarsimp simp: when_def)
        apply (rule corres_alternate1)
        apply (rule suspend_corres)
       apply (clarsimp simp: when_def dc_def[symmetric])+
       apply (rule corres_alternate2)
       apply (rule corres_free_return [where P="\<top>" and P'="\<top>"])
-
      apply clarsimp
-     apply (wp alternative_wp)
-    apply (clarsimp simp:not_idle_thread_def | wp | rule conjI)+
+    apply (clarsimp simp:conj_comms pred_conj_def split del: if_splits cong: if_cong)
+    apply (clarsimp simp:not_idle_thread_def invs_valid_objs dest!: idle_no_ex_cap
+           | wp suspend_nonz_cap_to_tcb | rule conjI |strengthen invs_cur)+
   done
 
 lemma cnode_cap_unique_bits:
@@ -1034,7 +1048,9 @@ lemma dcorres_tcb_update_ipc_buffer:
                                     (\<lambda>new_cap src_slot.
                                         check_cap_at new_cap src_slot $
                                         check_cap_at (cap.ThreadCap obj_id') a' $ cap_insert new_cap src_slot (obj_id', tcb_cnode_index 4)))
-                                  frame
+                                  frame;
+                              cur \<leftarrow> liftE $ gets cur_thread;
+                              liftE $ when (obj_id' = cur) (do_extended_op reschedule_required)
                              odE))
                        ipc_buffer';
                   returnOk []
@@ -1054,6 +1070,13 @@ lemma dcorres_tcb_update_ipc_buffer:
           apply (rule corres_dummy_return_pl)
           apply (rule corres_split[OF _ dcorres_idempotent_as_user_strong])
              apply (rule corres_trivial,clarsimp simp:returnOk_def)
+             apply (rule corres_symb_exec_r)
+                apply (rule corres_guard_imp)
+                  apply (rule corres_split_noop_rhs[OF corres_trivial])
+                    apply simp
+                   apply (clarsimp simp: when_def)
+                   apply (rule reschedule_required_dcorres[THEN corres_trivial])
+                  apply wpsimp+
        apply (wp|simp add:transform_tcb_slot_4)+
      apply (rule validE_validE_R)
      apply (rule_tac Q = "\<lambda>r s. invs s \<and> valid_etcbs s \<and> not_idle_thread obj_id' s  \<and> tcb_at obj_id' s"
@@ -1082,11 +1105,17 @@ lemma dcorres_tcb_update_ipc_buffer:
          apply (rule corres_split[OF _ get_cap_corres])
             apply (clarsimp simp:liftE_def returnOk_def)
             apply (rule corres_split[OF _ corres_when])
-                apply (rule corres_trivial)
-                apply clarsimp
-               apply (rule arch_same_obj_as_lift)
-                  apply (simp add:valid_ipc_buffer_cap_def is_arch_cap_def split:cap.splits)
-                 apply (clarsimp simp: valid_cap_def is_arch_cap_def valid_ipc_buffer_cap_def
+                   apply (rule corres_trivial,clarsimp simp:returnOk_def)
+                   apply (rule corres_symb_exec_r)
+                      apply (rule corres_guard_imp)
+                      apply (rule corres_split_noop_rhs[OF corres_trivial])
+                      apply simp
+                      apply (clarsimp simp: when_def)
+                      apply (rule reschedule_required_dcorres[THEN corres_trivial])
+                      apply wpsimp+
+                  apply (rule arch_same_obj_as_lift)
+                     apply (simp add:valid_ipc_buffer_cap_def is_arch_cap_def split:cap.splits)
+                    apply (clarsimp simp: valid_cap_def is_arch_cap_def valid_ipc_buffer_cap_def
                                 split: cap.split_asm arch_cap.split_asm)+
               apply (rule corres_split[OF _ get_cap_corres])
                  apply (rule corres_when)

proof/infoflow/Tcb_IF.thy

@@ -424,6 +424,10 @@ lemma invoke_tcb_NotificationControl_globals_equiv:
 
 crunch globals_equiv: set_mcpriority "globals_equiv st"
 
+lemma dxo_globals_equiv[wp]:
+  "\<lbrace>globals_equiv st\<rbrace> do_extended_op eop  \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
+  by (simp | wp dxo_wp_weak)+
+
 lemma invoke_tcb_globals_equiv:
   "\<lbrace> invs and globals_equiv st and Tcb_AI.tcb_inv_wf ti\<rbrace>
    invoke_tcb ti
@@ -657,22 +661,33 @@ lemma bind_notification_reads_respects:
 
 lemmas thread_get_reads_respects_f = reads_respects_f[OF thread_get_reads_respects, where Q="\<top>", simplified, OF thread_get_silc_inv]
 
+crunch silc_inv[wp]: reschedule_required, restart "silc_inv aag st"
+lemmas reschedule_required_reads_respects_f = reads_respects_f[OF reschedule_required_reads_respects, where Q="\<top>", simplified, OF reschedule_required_silc_inv]
+crunch pas_refined[wp]: restart "pas_refined aag"
+
 lemma invoke_tcb_reads_respects_f:
   notes validE_valid[wp del]
         static_imp_wp [wp]
   shows
   "reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and Tcb_AI.tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)"
   including no_pre
   apply(case_tac ti)
-        apply(wp thread_get_reads_respects_f when_ev restart_reads_respects_f as_user_reads_respects_f static_imp_wp thread_get_wp'| simp)+
+        apply(wpsimp wp: thread_get_reads_respects_f when_ev restart_reads_respects_f
+                         reschedule_required_reads_respects_f as_user_reads_respects_f
+                         static_imp_wp thread_get_wp' restart_silc_inv restart_pas_refined
+                         hoare_vcg_if_lift)+
         apply(auto intro: requiv_cur_thread_eq
                   intro!: det_zipWithM
                     simp: det_setRegister det_getRestartPC det_setNextPC authorised_tcb_inv_def reads_equiv_f_def)[1]
        apply(wp as_user_reads_respects_f suspend_silc_inv when_ev suspend_reads_respects_f[where st=st]
                 | simp | elim conjE, assumption)+
        apply(auto simp: authorised_tcb_inv_def  det_getRegister reads_equiv_f_def
                 intro!: det_mapM[OF _ subset_refl])[1]
-      apply(wp when_ev mapM_x_ev'' as_user_reads_respects_f[where st=st]  hoare_vcg_ball_lift mapM_x_wp' restart_reads_respects_f restart_silc_inv hoare_vcg_if_lift suspend_reads_respects_f suspend_silc_inv
+      apply(wp when_ev mapM_x_ev'' reschedule_required_reads_respects_f[where st=st]
+               as_user_reads_respects_f[where st=st] hoare_vcg_ball_lift mapM_x_wp'
+               restart_reads_respects_f restart_silc_inv hoare_vcg_if_lift
+               suspend_reads_respects_f suspend_silc_inv hoare_drop_imp
+               restart_silc_inv restart_pas_refined
            | simp split del: if_split add: det_setRegister det_setNextPC)+
       apply(auto simp: authorised_tcb_inv_def
                        idle_no_ex_cap[OF invs_valid_global_refs invs_valid_objs] det_getRestartPC
@@ -689,7 +704,34 @@ lemma invoke_tcb_reads_respects_f:
         | rule_tac Q=\<top> and st=st in reads_respects_f)+)[2]
 -- "ThreadControl"
   apply (simp add: split_def cong: option.case_cong)
-  apply(wp reads_respects_f[OF cap_insert_reads_respects, where st=st]
+  apply (wpsimp wp: hoare_vcg_const_imp_lift_R simp: when_def | wpc)+
+                      apply (rule conjI)
+                       apply ((wpsimp wp: reschedule_required_reads_respects_f)+)[4]
+                   apply((wp reads_respects_f[OF cap_insert_reads_respects, where st=st]
+                             reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]
+                             set_priority_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
+                             set_mcpriority_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
+                             check_cap_inv[OF check_cap_inv[OF cap_insert_valid_list]]
+                             check_cap_inv[OF check_cap_inv[OF cap_insert_valid_sched]]
+                             check_cap_inv[OF check_cap_inv[OF cap_insert_simple_sched_action]]
+                             get_thread_state_rev[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
+                             hoare_vcg_all_lift_R hoare_vcg_all_lift
+                             cap_delete_reads_respects[where st=st] itr_wps(19) cap_insert_pas_refined
+                             thread_set_pas_refined reads_respects_f[OF checked_insert_reads_respects, where st=st]
+                             checked_cap_insert_silc_inv[where st=st] cap_delete_silc_inv[where st=st]
+                             checked_cap_insert_only_timer_irq_inv[where st=st' and irq=irq]
+                             cap_delete_only_timer_irq_inv[where st=st' and irq=irq]
+                             set_priority_only_timer_irq_inv[where st=st' and irq=irq]
+                             set_mcpriority_only_timer_irq_inv[where st=st' and irq=irq]
+                             cap_delete_deletes cap_delete_valid_cap cap_delete_cte_at
+                             cap_delete_pas_refined itr_wps(12) itr_wps(14) cap_insert_cte_at
+                             checked_insert_no_cap_to hoare_vcg_const_imp_lift_R hoare_vcg_conj_lift
+                             as_user_reads_respects_f
+                            |wpc
+                            |simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
+                                       tcb_at_st_tcb_at when_def
+                            |strengthen use_no_cap_to_obj_asid_strg)+)[9]
+     apply(wp reads_respects_f[OF cap_insert_reads_respects, where st=st]
             reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]
             set_priority_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
             set_mcpriority_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
@@ -709,9 +751,9 @@ lemma invoke_tcb_reads_respects_f:
             cap_delete_pas_refined itr_wps(12) itr_wps(14) cap_insert_cte_at
             checked_insert_no_cap_to hoare_vcg_const_imp_lift_R
             as_user_reads_respects_f
-       |wpc 
+       |wpc
        |simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
-                  tcb_at_st_tcb_at
+                  tcb_at_st_tcb_at when_def
        |strengthen use_no_cap_to_obj_asid_strg)+
     apply(simp add: option_update_thread_def tcb_cap_cases_def
          | wp static_imp_wp static_imp_conj_wp reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]

proof/invariant-abstract/DetSchedSchedule_AI.thy

@@ -1654,6 +1654,32 @@ lemma set_mcpriority_valid_sched[wp]:
 
 crunch simple_sched_action[wp]: set_priority,set_mcpriority simple_sched_action
 
+lemma set_nonmember_if_cong: "(a \<notin> set (if P then x else y)) = (if P then a \<notin> set x else a \<notin> set y)"
+  by auto
+
+lemma reschedule_preserves_valid_shed: "\<lbrace> valid_sched \<rbrace> reschedule_required \<lbrace> \<lambda>rv. valid_sched \<rbrace>"
+  unfolding reschedule_required_def set_scheduler_action_def tcb_sched_action_def
+  apply (rule hoare_pre)
+  apply (wp|wpc)+
+  apply clarsimp
+  apply (rule conjI)
+   apply (clarsimp simp: valid_sched_2_def ct_not_in_q_2_def valid_blocked_2_def)
+  apply (rule conjI)
+   defer
+   apply (clarsimp simp: valid_sched_2_def ct_not_in_q_2_def valid_blocked_2_def)
+  apply (clarsimp simp only: etcb_at_def)
+  apply (case_tac "ekheap s x"; simp)
+  apply (clarsimp simp: valid_sched_2_def)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_queues_2_def valid_sched_action_2_def tcb_sched_enqueue_def
+     weak_valid_sched_action_2_def etcb_at_conj_is_etcb_at)
+  apply (rule conjI)
+   apply (clarsimp simp: ct_not_in_q_2_def)
+  apply (clarsimp simp:  valid_blocked_2_def)
+  apply (clarsimp simp:  not_queued_def)
+  apply (erule_tac x=t in allE; simp)
+  by (clarsimp simp:  set_nonmember_if_cong tcb_sched_enqueue_def split: if_split_asm; blast)
+
 context DetSchedSchedule_AI begin
 
 crunch valid_sched[wp]: arch_tcb_set_ipc_buffer valid_sched
@@ -1666,7 +1692,8 @@ lemma tc_valid_sched[wp]:
   apply (simp add: split_def set_mcpriority_def cong: option.case_cong)
   apply (rule hoare_vcg_precond_imp)
    by (wp check_cap_inv thread_set_not_state_valid_sched hoare_vcg_all_lift gts_wp static_imp_wp
-         | wpc | simp add: option_update_thread_def)+
+         | wpc | simp add: option_update_thread_def | rule reschedule_preserves_valid_shed
+         | wp_once hoare_drop_imps )+
 
 end
 
@@ -1776,7 +1803,7 @@ context DetSchedSchedule_AI begin
 lemma invoke_tcb_valid_sched[wp]:
   "\<lbrace>invs and valid_sched and simple_sched_action and tcb_inv_wf ti\<rbrace> invoke_tcb ti \<lbrace>\<lambda>rv. valid_sched\<rbrace>"
   apply (cases ti, simp_all only:)
-        apply (wp mapM_x_wp | simp | rule subset_refl | clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap | intro impI conjI)+
+        apply (wp mapM_x_wp | simp | rule subset_refl | rule reschedule_preserves_valid_shed | clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap | intro impI conjI)+
    apply (rename_tac option)
    apply (case_tac option)
     apply (wp mapM_x_wp | simp | rule subset_refl | clarsimp simp:invs_valid_objs invs_valid_global_refs idle_no_ex_cap | intro impI conjI)+