Library prosa.analysis.facts.readiness_interference

Require Export prosa.analysis.definitions.readiness_interference.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.facts.interference.
Require Export prosa.analysis.definitions.service_inversion.readiness_aware.

In this file, we establish facts about readiness interference.

Section ReadinessInterference.
Consider any kind of jobs with arrival times and execution costs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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

Consider any notion of job readiness.
  Context `{!JobReady Job PState}.

Consider any valid arrival sequence of jobs ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any valid schedule of the given arrival sequence.
  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

Allow for any JLFP priority policy.
  Context {JLFP : JLFP_policy Job}.

First, note that readiness interference is exclusive of the interference due to other higher-or-equal-priority jobs.
  Lemma no_hep_ready_implies_no_another_hep_interference :
    ∀ j t,
      ~~ some_hep_job_ready arr_seq sched j t →
      ~~ another_hep_job_interference arr_seq sched j t.

Next, we observe that readiness interference is exclusive of service inversion.
  Lemma no_hep_ready_implies_no_service_inversion :
    ∀ j t,
      ~~ some_hep_job_ready arr_seq sched j t →
      ~~ service_inversion arr_seq sched j t.

End ReadinessInterference.