Library prosa.analysis.facts.busy_interval.hep_at_pt

Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.util.tactics.
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.analysis.facts.model.preemption.

Processor Executes HEP jobs at Preemption Point

In this file, we show that, given a busy interval of a job j, the processor is always busy scheduling a higher-or-equal-priority job at any preemptive point inside the busy interval.
Section ProcessorBusyWithHEPJobAtPreemptionPoints.

Consider any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.

Consider any arrival sequence with consistent arrivals ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

... and any uniprocessor schedule of this arrival sequence.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uni : uniprocessor_model PState.
  Variable sched : schedule PState.

Consider a JLFP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.

In addition, we assume the existence of a function mapping a job and its progress to a boolean value saying whether this job is preemptable at its current point of execution.
  Context `{JobPreemptable Job}.

Further, allow for any work-bearing notion of job readiness.
  Context `{@JobReady Job PState Cost Arrival}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

We assume that the schedule is valid and that all jobs come from the arrival sequence.
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.

Next, we assume that the schedule is a work-conserving schedule...
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

... and the schedule respects the scheduling policy at every preemption point.
  Hypothesis H_respects_policy :
    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

Consider any job j with positive job cost.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Consider any busy interval prefix [t1, t2) of job j.
  Variable t1 t2 : instant.
  Hypothesis H_busy_interval_prefix :
    busy_interval_prefix arr_seq sched j t1 t2.

Consider an arbitrary preemption time t ∈ [t1,t2).
  Variable t : instant.
  Hypothesis H_t_in_busy_interval : t1 ≤ t < t2.
  Hypothesis H_t_preemption_time : preemption_time arr_seq sched t.

First note since t lies inside the busy interval, the processor cannot be idle at time t.
  Lemma instant_t_is_not_idle:
    ¬ is_idle arr_seq sched t.

Next we consider two cases: (1) t is less than t2 - 1 and (2) t is equal to t2 - 1.
In case when t < t2 - 1, we use the fact that time instant t+1 is not a quiet time. The later implies that there is a pending higher-or-equal priority job at time t. Thus, the assumption that the schedule respects priority policy at preemption points implies that the scheduled job must have a higher-or-equal priority.
  Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_lt:
    t < t2.-1 →
    ∀ jhp,
      scheduled_at sched jhp t →
      hep_job jhp j.

In the case when t = t2 - 1, we cannot use the same proof since t+1 = t2, but t2 is a quiet time. So we do a similar case analysis on the fact that t1 = t ∨ t1 < t.
  Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_eq:
    t = t2.-1 →
    ∀ jhp,
      scheduled_at sched jhp t →
      hep_job jhp j.

By combining the above facts we conclude that a job that is scheduled at time t has higher-or-equal priority.
  Corollary scheduled_at_preemption_time_implies_higher_or_equal_priority:
    ∀ jhp,
      scheduled_at sched jhp t →
      hep_job jhp j.

Since a job that is scheduled at time t has higher-or-equal priority, by properties of a busy interval it cannot arrive before time instant t1.
  Lemma scheduled_at_preemption_time_implies_arrived_between_within_busy_interval:
    ∀ jhp,
      scheduled_at sched jhp t →
      arrived_between jhp t1 t2.

From the above lemmas we prove that there is a job jhp that is (1) scheduled at time t, (2) has higher-or-equal priority, and (3) arrived between t1 and t2.
  Corollary not_quiet_implies_exists_scheduled_hp_job_at_preemption_point:
    ∃ j_hp,
      arrived_between j_hp t1 t2
      ∧ hep_job j_hp j
      ∧ scheduled_at sched j_hp t.

End ProcessorBusyWithHEPJobAtPreemptionPoints.

Processor Executes HEP Jobs after Preemption Point

In this section, we prove that at any time instant after any preemption point (inside the busy interval), the processor is always busy scheduling a job with higher or equal priority.
Section ProcessorBusyWithHEPJobAfterPreemptionPoints.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

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

Consider any arrival sequence with consistent arrivals ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

... and any uniprocessor schedule of this arrival sequence.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uni : uniprocessor_model PState.
  Variable sched : schedule PState.

Consider a JLFP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.

Consider a valid preemption model with known maximum non-preemptive segment lengths.
  Context `{TaskMaxNonpreemptiveSegment Task} `{JobPreemptable Job}.
  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.

Further, allow for any work-bearing notion of job readiness.
  Context `{!JobReady Job PState}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

We assume that the schedule is valid.
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.

Next, we assume that the schedule is work-conserving ...
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

... and the schedule respects the scheduling policy at every preemption point.
  Hypothesis H_respects_policy :
    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

Consider any job j with positive job cost.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Consider any busy interval prefix [t1, t2) of job j.
  Variable t1 t2 : instant.
  Hypothesis H_busy_interval_prefix :
    busy_interval_prefix arr_seq sched j t1 t2.

First, recall from the above section that the processor at any preemption time is always busy scheduling a job with higher or equal priority.
We show that, at any time instant after a preemption point, the processor is always busy with a job with higher or equal priority.
  Lemma not_quiet_implies_exists_scheduled_hp_job_after_preemption_point:
    ∀ tp t,
      preemption_time arr_seq sched tp →
      t1 ≤ tp < t2 →
      tp ≤ t < t2 →
      ∃ j_hp,
        arrived_between j_hp t1 t.+1 ∧
          hep_job j_hp j ∧
          scheduled_at sched j_hp t.

Now, suppose there exists some constant K that bounds the distance to a preemption time from the beginning of the busy interval.
  Variable K : duration.
  Hypothesis H_preemption_time_exists :
    ∃ pr_t, preemption_time arr_seq sched pr_t ∧ t1 ≤ pr_t ≤ t1 + K.

Then we prove that the processor is always busy with a job with higher-or-equal priority after time instant t1 + K.
  Lemma not_quiet_implies_exists_scheduled_hp_job:
    ∀ t,
      t1 + K ≤ t < t2 →
      ∃ j_hp,
        arrived_between j_hp t1 t.+1 ∧
          hep_job j_hp j ∧
          scheduled_at sched j_hp t.

End ProcessorBusyWithHEPJobAfterPreemptionPoints.