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.
  Proof.
    move⇒ [ | to]; rewrite /priority_bump ⇒ PB.
    { rewrite //= in PB; destruct (scheduled_job sched 0) eqn:SCHED1 ⇒ //.
      by rewrite //= H_priority_is_reflexive in PB.
    }
    have UNI := @overheads_proc_model_is_a_uniprocessor_model Job.
    rewrite -pred_Sn in PB.
    destruct (scheduled_job sched to) as [j1 | ] eqn:SCHED1,
          (scheduled_job sched to.+1) as [j2 | ] eqn:SCHED2 =>//.
    { have [/eqP EQ|NEQ] := boolP (j1 == j2).
      { by subst; rewrite H_priority_is_reflexive in PB. }
      { apply scheduled_at_iff_scheduled_job in SCHED1, SCHED2; apply first_moment_is_pt with (j := j2) ⇒ //.
        apply/negP ⇒ SCHED; move: NEQ ⇒ /negP NEQ; apply: NEQ; apply/eqP.
        by apply: overheads_proc_model_is_a_uniprocessor_model ⇒ //.
      }
    }
    { apply scheduled_at_iff_scheduled_job in SCHED2; apply first_moment_is_pt with (j := j2) ⇒ //.
      by apply/negP ⇒ SCHED; apply scheduled_at_iff_scheduled_job in SCHED; rewrite SCHED in SCHED1.
    }
  Qed.

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.
  Proof.
    move⇒ t t_arr NEQ1 NEQ2 NEQ3 PB.
    apply priority_bump_implies_preemption_time in PB.
    edestruct not_quiet_implies_exists_scheduled_hp_job_at_preemption_point as [jhp [ARR [HEP SCHED ]]] =>//.
    { lia. }
    ∃ jhp; split; try done.
    apply arrived_between_implies_in_arrivals ⇒ //; apply/andP; split.
    { by move: ARR ⇒ /andP []; lia. }
    { apply valid_schedule_implies_jobs_must_arrive_to_execute in H_valid_schedule.
      apply H_valid_schedule in SCHED.
      by unfold has_arrived in *; lia.
    }
  Qed.

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.
  Proof.
    move⇒ t NEQ; apply/negP ⇒ PB; unfold priority_bump in ×.
    destruct (scheduled_job sched t.-1) as [j1 | ] eqn:SCHED1;
      destruct (scheduled_job sched t) as [j2 | ] eqn:SCHED2; try done; last first.
    { edestruct job_scheduled_in_busy_interval_prefix with (t := t.-1) as [js SCHED] ⇒ //; first by lia.
      apply scheduled_at_iff_scheduled_job in SCHED.
      by rewrite SCHED in SCHED1; inversion SCHED1.
    }
    { rewrite H_JLFP_is_FIFO -ltnNge in PB.
      apply scheduled_at_iff_scheduled_job in SCHED1.
      apply scheduled_at_iff_scheduled_job in SCHED2.
      eapply early_hep_job_is_scheduled with (JLFP := hep_job) in PB ⇒ //; last first.
      { by intros ?; rewrite /hep_job_at /JLFP_to_JLDP //= !H_JLFP_is_FIFO; lia. }
      eapply completion_monotonic in PB.
      { by apply completed_implies_not_scheduled in PB ⇒ //; erewrite SCHED2 in PB. }
      { lia. }
    }
  Qed.

End PriorityBump.