# 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.

Require Export prosa.analysis.facts.busy_interval.busy_interval.

Throughout this file, we assume ideal uni-processor schedules.

# Processor Executes HEP jobs at Preemption Point

Consider any type of jobs associated with these tasks.

Consider any arrival sequence with consistent arrivals ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

... 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.

Context {JLFP : JLFP_policy Job}.

Hypothesis H_priority_is_reflexive: reflexive_priorities.

Hypothesis H_priority_is_transitive: transitive_priorities.

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.

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.

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.

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...

... 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.

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.

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.

Hypothesis H_t_in_busy_interval : t1 ≤ t < t2.

Hypothesis H_t_preemption_time : preemption_time 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.

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.

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.

∀ 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.

∀ jhp,

scheduled_at sched jhp t →

arrived_between jhp t1 t2.