# Library prosa.analysis.facts.model.overheads.priority_bump

Require Export prosa.model.readiness.basic.
Require Export prosa.model.processor.overheads.
Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.facts.priority.sequential.
Require Export prosa.analysis.facts.model.overheads.schedule.
Require Export prosa.analysis.definitions.overheads.priority_bump.
In this section, we prove several properties of the notion of a priority bump.
Section PriorityBump.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this 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.
We assume the basic model of readiness.
#[local] Existing Instance basic_ready_instance.
Consider any valid arrival sequence...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any explicit-overhead uni-processor schedule of this arrival sequence.
Variable sched : schedule (overheads.processor_state Job).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Assume that the preemption model is valid.
Context `{JobPreemptable Job}.
Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.
Assume that the schedule respects the JLFP policy.
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
If a priority bump occurs at time t, then t is a preemption time.
Lemma priority_bump_implies_preemption_time :
∀ (t : instant),
priority_bump sched t →
preemption_time arr_seq sched t.
Consider an arbitrary job j with positive cost.
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Consider any busy-interval prefix `[t1, t2)` of job j.
Variables t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2.
A priority bump within a busy-interval prefix can only be caused by a job that arrived within the same busy-interval prefix.
Lemma priority_bump_implies_hp_arrival_in_prefix :
∀ (t t_arr : instant),
t1 ≤ t →
t < t_arr →
t_arr ≤ t2 →
priority_bump sched t →
∃ jhp,
scheduled_at sched jhp t
∧ jhp \in arrivals_between arr_seq t1 t_arr.
In the following, we assume that the JLFP policy corresponds to FIFO: a job has higher or equal priority if and only if it arrived earlier.
Hypothesis H_JLFP_is_FIFO : ∀ j1 j2, hep_job j1 j2 = (job_arrival j1 ≤ job_arrival j2).
Under the FIFO policy, no priority bumps occur during `(t1, t2]` since jobs are scheduled in arrival order and thus priorities never increase.
Lemma no_priority_bumps_in_fifo :
∀ (t : instant),
t1 < t ≤ t2 →
~~ priority_bump sched t.
End PriorityBump.