Theory Step_invariants

subsection ‹Preconditions and invariants for the atomic step \label{sect:step_invariants}›

theory Step_invariants
  imports Step
begin

text ‹The dynamic/implementation policies have to be compatible with the static configuration.›

definition "sp_subset s ≡
   (∀ p1 p2 . sp_impl_subj_subj s p1 p2 ⟶ Policy.sp_spec_subj_subj p1 p2)
   ∧ (∀ p1 p2 m. sp_impl_subj_obj s p1 p2 m ⟶ Policy.sp_spec_subj_obj p1 p2 m)"

text ‹The following predicate expresses the precondition for the atomic step. The precondition depends on the type of the atomic action.›
(*
[SK_IPC dir PREP partner page,SK_IPC dir WAIT partner page,SK_IPC dir (BUF page') partner page]
*)
definition atomic_step_precondition :: "state_t ⇒ thread_id_t ⇒ int_point_t ⇒ bool" where
  "atomic_step_precondition s tid ipt ≡
    case ipt of
       SK_IPC dir WAIT partner page ⇒
         ― ‹the thread managed it past PREP stage›
         ipc_precondition tid dir partner page s
     | SK_IPC dir (BUF page') partner page ⇒
         ― ‹both the calling thread and its communication partner managed it past PREP and WAIT stages›
         ipc_precondition tid dir partner page s
         ∧ ipc_precondition partner (opposite_ipc_direction dir) tid page' s
     | SK_EV_SIGNAL EV_SIGNAL_FINISH partner ⇒
        ev_signal_precondition tid partner s 
     | _ ⇒
         ― ‹No precondition for other interrupt points.›
         True"

text ‹The invariant to be preserved by the atomic step function. The invariant is independent from the type of the atomic action.›

definition atomic_step_invariant :: "state_t ⇒ bool" where
  "atomic_step_invariant s ≡
     sp_subset s"

subsubsection ‹Atomic steps of SK\_IPC preserve invariants›


lemma set_object_value_invariant:
  shows "atomic_step_invariant s = atomic_step_invariant (set_object_value ob va s)"
proof -
  show ?thesis
    unfolding atomic_step_invariant_def atomic_step_precondition_def ipc_precondition_def
      sp_subset_def set_object_value_def Let_def
    by (simp split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits)
qed

lemma set_thread_value_invariant:
  shows "atomic_step_invariant s = atomic_step_invariant (s ⦇ thread := thrst ⦈)"
proof -
  show ?thesis
    unfolding atomic_step_invariant_def atomic_step_precondition_def ipc_precondition_def
      sp_subset_def set_object_value_def Let_def
    by (simp split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits)
qed

lemma atomic_ipc_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ipc tid dir stage partner page s)"
proof -
  show ?thesis
    proof (cases stage)
    case PREP
      from this assms show ?thesis
        unfolding atomic_step_ipc_def atomic_step_invariant_def by auto
    next
    case WAIT
      from this assms show ?thesis
        unfolding atomic_step_ipc_def atomic_step_invariant_def by auto
    next
    case BUF
      show ?thesis
        using assms BUF set_object_value_invariant
        unfolding atomic_step_ipc_def
        by (simp split: ipc_direction_t.splits)
    qed
qed

lemma atomic_ev_wait_one_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ev_wait_one tid s)"
  proof -
   from assms show ?thesis
   unfolding atomic_step_ev_wait_one_def atomic_step_invariant_def sp_subset_def
   by auto  
 qed

lemma atomic_ev_wait_all_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ev_wait_all tid s)"
  proof -
   from assms show ?thesis
   unfolding atomic_step_ev_wait_all_def atomic_step_invariant_def sp_subset_def
   by auto  
 qed

lemma atomic_ev_signal_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step_ev_signal tid  partner s)"
  proof -
   from assms show ?thesis
   unfolding atomic_step_ev_signal_def atomic_step_invariant_def sp_subset_def
   by auto  
 qed

subsubsection ‹Summary theorems on atomic step invariants›

text ‹Now we are ready to show that an atomic step from the current interrupt point
        in any thread preserves invariants.›

theorem atomic_step_preserves_invariants:
  fixes s :: state_t
    and tid :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (atomic_step s a)"
proof (cases a)
  case SK_IPC 
    then show ?thesis unfolding atomic_step_def
    using assms atomic_ipc_preserves_invariants
    by simp
  next  case (SK_EV_WAIT ev_wait_stage consume)
    then show ?thesis 
    proof (cases consume)
     case EV_CONSUME_ALL
      then show ?thesis unfolding atomic_step_def
      using SK_EV_WAIT assms atomic_ev_wait_all_preserves_invariants
      by (simp split: ev_wait_stage_t.splits)
     next case EV_CONSUME_ONE
      then show ?thesis unfolding atomic_step_def
      using SK_EV_WAIT assms atomic_ev_wait_one_preserves_invariants
      by (simp split: ev_wait_stage_t.splits)
    qed
  next case SK_EV_SIGNAL
   then show ?thesis unfolding atomic_step_def
   using assms atomic_ev_signal_preserves_invariants  
   by (simp add: ev_signal_stage_t.splits)
  next case NONE
   then show ?thesis unfolding atomic_step_def
   using assms
   by auto  
qed

text ‹Finally, the invariants do not depend on the current thread. That is, 
the context switch preserves the invariants, and an atomic step that is 
not a context switch does not change the current thread.›

theorem cswitch_preserves_invariants:
  fixes s :: state_t
    and new_current :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "atomic_step_invariant (s ⦇ current := new_current ⦈)"
proof -
  let ?s1 = "s ⦇ current := new_current ⦈"
  have "sp_subset s = sp_subset ?s1"
    unfolding sp_subset_def by auto
  from assms this show ?thesis
    unfolding atomic_step_invariant_def by metis
qed

theorem atomic_step_does_not_change_current_thread:
  shows "current (atomic_step s ipt) = current s"
proof -
  show ?thesis
    unfolding atomic_step_def
          and atomic_step_ipc_def
          and set_object_value_def Let_def
          and atomic_step_ev_wait_one_def atomic_step_ev_wait_all_def
          and atomic_step_ev_signal_def
    by (simp split: int_point_t.splits ipc_stage_t.splits ipc_direction_t.splits 
                        ev_consume_t.splits ev_wait_stage_t.splits ev_signal_stage_t.splits)
qed

end