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.