rt spec+proof: add sporadic implies active invariant

This adds an invariant to active_scs_valid (part of valid_sched) which
states that every scheduling context which is sporadic is active.

Several changes to the specs were made, in particular

 - a sched context is made not sporadic during the finalisation process.
   This was required to prove the invariant holds.

 - the update to the sc_sporadic field within
   invoke_sched_control_configure_flags is now made towards the end of
   the function, so as to ensure that the field is updated only after the
   scheduling context is made active. This means that the new invariant is
   not broken temporarily, and eases the proofs. In addition, the update
   to the sc_badge field is moved.

 - if_cond_refill_unblock_check is modified, taking into account the
   new invariant.

Signed-off-by: Michael McInerney <[email protected]>

proof/invariant-abstract/AInvs.thy

@@ -213,8 +213,8 @@ lemma invoke_sched_context_cur_sc_tcb_are_bound_imp_cur_sc_active:
   apply (cases iv; clarsimp)
   apply (rule hoare_weaken_pre)
    apply (rule_tac f=cur_sc in hoare_lift_Pf2)
-    apply (wpsimp wp: update_sched_context_wp)
-   apply (wpsimp wp: update_sched_context_wp)
+    apply wpsimp
+   apply (wpsimp wp: update_sched_context_wp hoare_vcg_all_lift hoare_drop_imps)
   apply (clarsimp simp: active_sc_def MIN_REFILLS_def vs_all_heap_simps)
   done
 
@@ -655,19 +655,10 @@ lemma invoke_sched_control_configure_flags_schact_is_rct_imp_ct_not_in_release_q
   "\<lbrace>ct_not_in_release_q and invs and schact_is_rct and valid_sched_control_inv iv\<rbrace>
    invoke_sched_control_configure_flags iv
    \<lbrace>\<lambda>_ s. schact_is_rct s \<longrightarrow> ct_not_in_release_q s\<rbrace>"
+  (is "\<lbrace>_\<rbrace> _ \<lbrace>?post\<rbrace>")
   apply (simp add: invoke_sched_control_configure_flags_def)
   apply (cases iv; clarsimp)
   apply (rename_tac sc_ptr budget period mrefills badge flag)
-  apply (rule_tac B="\<lambda>_ s. ct_not_in_release_q s \<and> invs s \<and> schact_is_rct s
-                           \<and> ex_nonz_cap_to sc_ptr s"
-               in hoare_seq_ext[rotated])
-   apply (wpsimp wp: update_sc_badge_invs')
-   apply (fastforce dest: ex_nonz_cap_to_not_idle_sc_ptr
-                    simp: sc_at_pred_n_def obj_at_def)
-  apply (rule hoare_seq_ext_skip)
-   apply (wpsimp wp: update_sc_sporadic_invs')
-   apply (fastforce dest: ex_nonz_cap_to_not_idle_sc_ptr
-                    simp: sc_at_pred_n_def obj_at_def)
   apply (rule hoare_seq_ext[OF _ get_sched_context_sp])
   apply (rule_tac B="\<lambda>_ s. ct_not_in_release_q s \<and> invs s \<and> schact_is_rct s
                            \<and> ex_nonz_cap_to sc_ptr s
@@ -682,19 +673,21 @@ lemma invoke_sched_control_configure_flags_schact_is_rct_imp_ct_not_in_release_q
   apply (rule hoare_seq_ext_skip)
    apply (wpsimp wp: refill_update_invs gts_wp)
    apply (fastforce dest: ex_nonz_cap_to_not_idle_sc_ptr)
-  apply (rule hoare_when_cases, simp)
-  apply (rule hoare_seq_ext[OF _ assert_opt_sp])
-  apply (rule hoare_seq_ext[OF _ gts_sp])
-  apply (rule_tac B="\<lambda>_ s. in_release_q (cur_thread s) s \<longrightarrow> tcb_ptr = cur_thread s"
-               in hoare_seq_ext[rotated])
-   apply (wpsimp wp: hoare_vcg_imp_lift' sched_context_resume_ct_not_in_release_q)
-   apply (clarsimp simp: vs_all_heap_simps sc_at_pred_n_def obj_at_def)
-  apply (rule hoare_seq_ext[OF _ gets_sp])
-  apply (rule hoare_if)
-   apply (rule_tac Q="\<lambda>_ s. scheduler_action s = choose_new_thread" in hoare_post_imp)
-    apply (clarsimp simp: schact_is_rct_def)
-   apply (wpsimp wp: reschedule_cnt)
-  apply (wpsimp wp: hoare_drop_imps)
+  apply (rule_tac B="?post" in hoare_seq_ext[rotated])
+   apply (rule hoare_when_cases, simp)
+   apply (rule hoare_seq_ext[OF _ assert_opt_sp])
+   apply (rule hoare_seq_ext[OF _ gts_sp])
+   apply (rule_tac B="\<lambda>_ s. in_release_q (cur_thread s) s \<longrightarrow> tcb_ptr = cur_thread s"
+                in hoare_seq_ext[rotated])
+    apply (wpsimp wp: hoare_vcg_imp_lift' sched_context_resume_ct_not_in_release_q)
+    apply (clarsimp simp: vs_all_heap_simps sc_at_pred_n_def obj_at_def)
+   apply (rule hoare_seq_ext[OF _ gets_sp])
+   apply (rule hoare_if)
+    apply (rule_tac Q="\<lambda>_ s. scheduler_action s = choose_new_thread" in hoare_post_imp)
+     apply (clarsimp simp: schact_is_rct_def)
+    apply (wpsimp wp: reschedule_cnt)
+   apply (wpsimp wp: hoare_drop_imps)
+  apply wpsimp
   done
 
 crunches cancel_badged_sends

proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy

@@ -274,14 +274,22 @@ lemma perform_asid_control_invocation_pred_map_sc_refill_cfgs_of:
   by (wpsimp wp: delete_objects_pred_map_sc_refill_cfgs_of
            comb: hoare_drop_imp)
 
-lemma perform_asid_control_invocation_inactive_implies_zero_budget:
+lemma perform_asid_control_invocation_implies_zero_budget:
   "perform_asid_control_invocation aci
-   \<lbrace>\<lambda>s. pred_map inactive_scrc (sc_refill_cfgs_of s) p
+   \<lbrace>\<lambda>s. pred_map Q (sc_refill_cfgs_of s) p
         \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"
   unfolding perform_asid_control_invocation_def
   by (wpsimp wp: delete_objects_pred_map_sc_refill_cfgs_of
            comb: hoare_drop_imp)
 
+lemma perform_asid_control_invocation_sporadic_implies:
+  "perform_asid_control_invocation aci
+   \<lbrace>\<lambda>s. pred_map (\<lambda>cfg. scrc_sporadic cfg) (sc_refill_cfgs_of s) p
+        \<longrightarrow> pred_map Q (sc_refill_cfgs_of s) p\<rbrace>"
+  unfolding perform_asid_control_invocation_def
+  by (wpsimp wp: delete_objects_pred_map_sc_refill_cfgs_of
+           comb: hoare_drop_imp)
+
 crunches perform_asid_control_invocation
   for valid_machine_time[wp]: "valid_machine_time"
   and cur_sc[wp]: "\<lambda>s. P (cur_sc s)"
@@ -303,7 +311,8 @@ lemma perform_asid_control_invocation_valid_sched:
                                    perform_asid_control_invocation_sc_at_pred_n
                                    perform_asid_control_invocation_valid_idle
                                    perform_asid_control_invocation_pred_map_sc_refill_cfgs_of
-                                   perform_asid_control_invocation_inactive_implies_zero_budget
+                                   perform_asid_control_invocation_implies_zero_budget
+                                   perform_asid_control_invocation_sporadic_implies
                                    hoare_vcg_all_lift
                              simp: ipc_queued_thread_state_live live_sc_def)+
   done

proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy

@@ -1149,9 +1149,9 @@ crunch valid_pdpt_objs[wp]: end_timeslice "valid_pdpt_objs::det_state \<Rightarr
   (wp: crunch_wps hoare_drop_imps hoare_vcg_if_lift2)
 
 crunches check_budget_restart, invoke_sched_control_configure_flags
-  for valid_pdpt_objs[wp]: "valid_pdpt_objs::det_state \<Rightarrow> _"
+  for valid_pdpt_objs[wp]: "valid_pdpt_objs :: det_state \<Rightarrow> _"
   (wp: hoare_drop_imps hoare_vcg_if_lift2 whileLoop_valid_inv hoare_vcg_all_lift
-  simp: Let_def ignore: tcb_release_remove)
+   simp: Let_def crunch_simps ignore: tcb_release_remove)
 
 lemma perform_invocation_valid_pdpt[wp]:
   "\<lbrace>invs and ct_active and valid_invocation i and valid_pdpt_objs and

proof/invariant-abstract/DetSchedAux_AI.thy

@@ -258,9 +258,9 @@ lemma retype_region_active_sc_props[wp]:
   apply (clarsimp simp: active_sc_def default_sched_context_def)
   done
 
-lemma retype_region_inactive_implies_zero_budget[wp]:
+lemma retype_region_implies_zero_budget[wp]:
   "retype_region ptr numObjects o_bits type dev
-   \<lbrace>\<lambda>s. pred_map inactive_scrc (sc_refill_cfgs_of s) p
+   \<lbrace>\<lambda>s. pred_map Q (sc_refill_cfgs_of s) p
         \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"
   unfolding retype_region_def
   apply wp
@@ -269,6 +269,17 @@ lemma retype_region_inactive_implies_zero_budget[wp]:
   apply (clarsimp simp: active_sc_def default_sched_context_def)
   done
 
+lemma retype_region_sporadic_implies[wp]:
+  "retype_region ptr numObjects o_bits type dev
+   \<lbrace>\<lambda>s. pred_map (\<lambda>cfg. scrc_sporadic cfg) (sc_refill_cfgs_of s) p
+        \<longrightarrow> pred_map Q (sc_refill_cfgs_of s) p\<rbrace>"
+  unfolding retype_region_def
+  apply wp
+  apply (clarsimp simp del: fun_upd_apply simp add: vs_all_heap_simps foldr_fun_upd_value)
+  apply (case_tac type; simp add: default_object_def)
+  apply (clarsimp simp: active_sc_def default_sched_context_def)
+  done
+
 crunches retype_region
   for cur_time_cur_sc[wp]: "\<lambda>s. P (cur_time s) (cur_sc s)"
 
@@ -282,20 +293,12 @@ lemma retype_region_active_sc_props''[wp]:
 
 lemma delete_objects_pred_map_sc_refill_cfgs_of[wp]:
   "delete_objects base sz
-   \<lbrace>\<lambda>s. pred_map active_scrc (sc_refill_cfgs_of s) p
+   \<lbrace>\<lambda>s. pred_map Q (sc_refill_cfgs_of s) p
         \<longrightarrow> pred_map (P (consumed_time s) (cur_time s) (cur_sc s)) (sc_refill_cfgs_of s) p\<rbrace>"
   unfolding delete_objects_def2
   apply wpsimp
   by (clarsimp simp: detype_def vs_all_heap_simps split: if_splits)
 
-lemma delete_objects_inactive_implies_zero_budget[wp]:
-  "delete_objects base sz
-   \<lbrace>\<lambda>s. pred_map inactive_scrc (sc_refill_cfgs_of s) p
-        \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"
-  unfolding delete_objects_def2
-  apply wpsimp
-  by (clarsimp simp: detype_def vs_all_heap_simps split: if_splits)
-
 lemma delete_objects_active_scs_valid[wp]:
   "delete_objects base sz \<lbrace>active_scs_valid\<rbrace>"
   apply (clarsimp simp: active_scs_valid_def)
@@ -314,35 +317,32 @@ lemma (in DetSchedAux_AI) delete_objects_pred_map_sc_refill_cfgs_of_cur_sc[wp]:
 
 lemma reset_untyped_cap_pred_map_sc_refill_cfgs_of:
   "reset_untyped_cap slot
-   \<lbrace>\<lambda>s. pred_map active_scrc (sc_refill_cfgs_of s) p
-        \<longrightarrow> pred_map P (sc_refill_cfgs_of s) p\<rbrace>"
+   \<lbrace>\<lambda>s. pred_map Q (sc_refill_cfgs_of s) p \<longrightarrow> pred_map P (sc_refill_cfgs_of s) p\<rbrace>"
   unfolding reset_untyped_cap_def
   by (wpsimp wp: mapME_x_wp_inv preemption_point_inv
                  delete_objects_pred_map_sc_refill_cfgs_of
                  comb: hoare_drop_imp hoare_drop_imp[THEN hoare_vcg_conj_lift])
 
-lemma reset_untyped_cap_inactive_implies_zero_budget:
-  "reset_untyped_cap slot
-   \<lbrace>\<lambda>s. pred_map inactive_scrc (sc_refill_cfgs_of s) p
-        \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"
-  unfolding reset_untyped_cap_def
-  by (wpsimp wp: mapME_x_wp_inv preemption_point_inv
-                 delete_objects_pred_map_sc_refill_cfgs_of
-           comb: hoare_drop_imp hoare_drop_imp[THEN hoare_vcg_conj_lift])
-
 lemma invoke_untyped_pred_map_sc_refill_cfgs_of:
   "invoke_untyped ui
    \<lbrace>\<lambda>s. pred_map active_scrc (sc_refill_cfgs_of s) p
         \<longrightarrow> pred_map P (sc_refill_cfgs_of s) p\<rbrace>"
   unfolding invoke_untyped_def
   by (wpsimp wp: mapM_x_wp_inv reset_untyped_cap_pred_map_sc_refill_cfgs_of)
 
-lemma invoke_untyped_inactive_implies_zero_budget:
+lemma invoke_untyped_implies_zero_budget:
   "invoke_untyped ui
-   \<lbrace>\<lambda>s. pred_map inactive_scrc (sc_refill_cfgs_of s) p
+   \<lbrace>\<lambda>s. pred_map Q (sc_refill_cfgs_of s) p
         \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"
   unfolding invoke_untyped_def
-  by (wpsimp wp: mapM_x_wp_inv reset_untyped_cap_inactive_implies_zero_budget)
+  by (wpsimp wp: mapM_x_wp_inv reset_untyped_cap_pred_map_sc_refill_cfgs_of)
+
+lemma invoke_untyped_sporadic_implies:
+  "invoke_untyped ui
+   \<lbrace>\<lambda>s. pred_map (\<lambda>cfg. scrc_sporadic cfg) (sc_refill_cfgs_of s) p
+        \<longrightarrow> pred_map Q (sc_refill_cfgs_of s) p\<rbrace>"
+  unfolding invoke_untyped_def
+  by (wpsimp wp: mapM_x_wp_inv reset_untyped_cap_pred_map_sc_refill_cfgs_of)
 
 lemma cur_time_detype[simp]:
   "cur_time (detype r s) = cur_time s"
@@ -665,11 +665,17 @@ lemma valid_sched_tcb_state_preservation_gen:
     "\<And>P. \<lbrace>\<lambda>s. (\<forall>p. pred_map active_scrc (sc_refill_cfgs_of s) p \<longrightarrow> pred_map P (sc_refill_cfgs_of s) p) \<and> I s\<rbrace>
             f \<lbrace>\<lambda>rv s. \<forall>p. pred_map active_scrc (sc_refill_cfgs_of s) p \<longrightarrow> pred_map P (sc_refill_cfgs_of s) p\<rbrace>"
   assumes sc_refill_cfg3:
-    "\<And>P. \<lbrace>\<lambda>s. (\<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p
+    "\<lbrace>\<lambda>s. (\<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p
                     \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p)
-               \<and> I s\<rbrace>
-          f \<lbrace>\<lambda>_ s. \<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p
-                       \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"
+          \<and> I s\<rbrace>
+     f \<lbrace>\<lambda>_ s. \<forall>p. pred_map (\<lambda>cfg. \<not> active_scrc cfg) (sc_refill_cfgs_of s) p
+                  \<longrightarrow> pred_map (\<lambda>cfg. scrc_budget cfg = 0) (sc_refill_cfgs_of s) p\<rbrace>"
+  assumes sc_refill_cfg4:
+    "\<lbrace>\<lambda>s. (\<forall>p. pred_map (\<lambda>cfg. scrc_sporadic cfg) (sc_refill_cfgs_of s) p
+               \<longrightarrow> pred_map (\<lambda>cfg. active_scrc cfg) (sc_refill_cfgs_of s) p)
+          \<and> I s\<rbrace>
+     f \<lbrace>\<lambda>_ s. \<forall>p. pred_map (\<lambda>cfg. scrc_sporadic cfg) (sc_refill_cfgs_of s) p
+                  \<longrightarrow> pred_map (\<lambda>cfg. active_scrc cfg) (sc_refill_cfgs_of s) p\<rbrace>"
   assumes valid_machine_time: "f \<lbrace>valid_machine_time\<rbrace>"
   assumes cur_time_nondecreasing:
     "\<And>val. \<lbrace>\<lambda>s. cur_time s = val \<and> valid_machine_time s\<rbrace> f \<lbrace>\<lambda>_ s. val \<le> cur_time s\<rbrace>"
@@ -846,7 +852,9 @@ lemma valid_sched_tcb_state_preservation_gen:
                                          (sc_refill_cfgs_of s') p"
                   in spec)
     apply (clarsimp simp: bounded_release_time_def  word_le_nat_alt vs_all_heap_simps pred_conj_def)
-   apply (fastforce dest!: use_valid[OF _ sc_refill_cfg3])
+   apply (rule conjI)
+    apply (fastforce dest!: use_valid[OF _ sc_refill_cfg3])
+   apply (fastforce dest:  use_valid[OF _ sc_refill_cfg4])
    done
   apply (prop_tac "active_reply_scs s'")
    subgoal for s r s'
@@ -1155,7 +1163,8 @@ lemma invoke_untyped_valid_sched:
                                    invoke_untyped_pred_map_sc_refill_cfgs_of
                                    invoke_untyped_valid_idle invoke_untyped_valid_sched_pred_misc
                                    invoke_untyped_cur_time_monotonic
-                                   invoke_untyped_inactive_implies_zero_budget
+                                   invoke_untyped_implies_zero_budget
+                                   invoke_untyped_sporadic_implies
                                    hoare_vcg_all_lift
                              simp: ipc_queued_thread_state_live live_sc_def)+
   done