Library prosa.analysis.facts.interference

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType} {jt : JobTask Job Task}.

Consider any kind of processor state model.
  Context {PState : ProcessorState Job}.

Consider any arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... and any schedule.
  Variable sched : schedule PState.

Consider a reflexive FP-policy and a JLFP policy compatible with it.
We establish a higher-or-equal job of another task causing interference, can be due to a higher priority task or an equal priority task.
  Lemma hep_interference_another_task_split :
     (j: Job) (t : instant),
      another_task_hep_job_interference arr_seq sched j t
      = hep_job_from_hp_task_interference arr_seq sched j t
        || hep_job_from_other_ep_task_interference arr_seq sched j t.
  Proof.
    movej t.
    rewrite -has_predU; apply: eq_in_hasj' IN //=.
    case: (receives_service_at _ _ _); [rewrite !andbT|rewrite !andbF //].
    rewrite /another_task_hep_job/hp_task_hep_job
      /other_ep_task_hep_job/ep_task_hep_job.
    case HEP: (hep_job j' j); [rewrite !andTb|rewrite !andFb //].
    case HPT: (job_task _ != job_task _);
      last by rewrite andbF orbF; move: HPT ⇒ /eqP ->; rewrite hp_task_irrefl.
    rewrite andbT -hep_hp_ep_task; symmetry.
    by move: H_compatible ⇒ [+ _]; apply.
  Qed.

Now, assuming a uniprocessor model,...
  Hypothesis H_uniproc : uniprocessor_model PState.

...the previous lemma allows us to establish that the cumulative interference incurred by a job is equal to the sum of the cumulative interference from higher-or-equal-priority jobs belonging to strictly higher-priority tasks (FP) and the cumulative interference from higher-or-equal-priority jobs belonging to equal-priority tasks (GEL).
  Lemma cumulative_hep_interference_split_tasks_new: j t1 Δ,
    cumulative_another_task_hep_job_interference arr_seq sched j t1 (t1 + Δ)
    = cumulative_interference_from_hep_jobs_from_hp_tasks arr_seq sched j t1 (t1 + Δ)
      + cumulative_interference_from_hep_jobs_from_other_ep_tasks arr_seq sched j t1 (t1 + Δ).
  Proof.
    movej t1 Δ.
    rewrite -big_split //=; apply: eq_big_seqt IN.
    rewrite hep_interference_another_task_split.
    have: a b, (~~ (a && b)) nat_of_bool (a || b) = a + b by case; case.
    apply. apply/negP ⇒ /andP [/hasP [j' _ /andP [HP SERV']]
/hasP [j'' _ /andP [/andP [EP _] SERV'']]].
    move: HP EP; have ->: j' = j'' by apply: recv_service_impl_same_job; eauto.
    by move⇒ /andP [_ /andP [_ /negP +]] /andP [_ /andP [_ +]].
  Qed.

End InterferenceProperties.