Library prosa.analysis.facts.busy_interval.ideal.hep_job_scheduled

Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.busy_interval.busy_interval.

Throughout this file, we assume ideal uni-processor schedules.
Require Import prosa.model.processor.ideal.

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_arrival_times_are_consistent : consistent_arrival_times arr_seq.

... and any ideal uniprocessor schedule of this arrival sequence.
  Variable sched : schedule (ideal.processor_state Job).

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_priorities.
  Hypothesis H_priority_is_transitive: transitive_priorities.

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 (ideal.processor_state Job) 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.
  Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence 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 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 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.