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

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.
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 ...
... and any ideal uniprocessor schedule of this arrival sequence.
Consider a JLFP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive.
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.
We assume that the schedule is valid and that all jobs come from the arrival sequence.
Next, we assume that the schedule is a work-conserving schedule...
... and the schedule respects the scheduling policy at every preemption point.
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.
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.
By combining the above facts we conclude that a job that is scheduled at time t has higher-or-equal priority.
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.
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.