Library prosa.analysis.facts.priority.fifo

In this section, we prove some fundamental properties of the FIFO policy.
Section BasicLemmas.

We assume the basic (i.e., Liu & Layland) readiness model under which any pending job is ready.
  #[local] Existing Instance basic_ready_instance.

Consider any type of jobs with arrival times and execution costs.
  Context `{Job : JobType} {Arrival : JobArrival Job} {Cost : JobCost Job}.

Consider any arrival sequence of such jobs ...
  Variable arr_seq : arrival_sequence Job.

... and the resulting ideal uniprocessor schedule. We assume that the schedule is valid and work-conserving.
Suppose jobs have preemption points ...
  Context `{JobPreemptable Job}.

...and that the preemption model is valid.
Assume that the schedule respects the FIFO scheduling policy whenever jobs are preemptable.
We observe that there is no priority inversion in a FIFO-compliant schedule.
  Lemma FIFO_implies_no_priority_inversion :
     j t,
      arrives_in arr_seq j
      pending sched j t
      ¬ priority_inversion sched j t.
  Proof.
    movej t ARRIVES /andP [ARRIVED /negP NCOMPL] [NSCHED [jlp /andP [SCHED PRIO]]].
    move: PRIO; rewrite /hep_job /FIFO -ltnNgeLT.
    apply: NCOMPL; eapply early_hep_job_is_scheduled; rt_eauto.
    by intros t'; apply/andP; split; unfold hep_job_at, JLFP_to_JLDP, hep_job, FIFO; lia.
  Qed.

In this section, we prove the cumulative priority inversion for any task is bounded by 0.
Consider any kind of tasks.
    Context `{Task : TaskType} `{JobTask Job Task}.

Consider a task tsk.
    Variable tsk : Task.

Assume the arrival times are consistent.
Assume that the schedule follows the FIFO policy at preemption time.
Assume the schedule is valid.
Assume there are no duplicates in the arrival sequence.
Then we prove that the amount of priority inversion is bounded by 0.
    Lemma FIFO_implies_no_pi :
      priority_inversion_is_bounded_by_constant arr_seq sched tsk 0.
    Proof.
      movej ARRIN TASK POS t1 t2 BUSY.
      rewrite /priority_inversion.cumulative_priority_inversion.
      have → : \sum_(t1 t < t2) priority_inversion_dec arr_seq sched j t = 0;
        last by done.
      rewrite big_nat_eq0t /andP[T1 T2].
      apply /eqP; rewrite eqb0.
      apply /negP ⇒ /priority_inversion_P INV.
      feed_n 3 INV; rt_eauto.
      move: INV ⇒ [NSCHED [j__lp /andP [SCHED LP]]].
      move: LP; rewrite /hep_job /FIFO -ltnNgeLT.
      have COMPL: completed_by sched j t.
      { apply: early_hep_job_is_scheduled; rt_eauto.
        movet'; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FIFO -ltnNge.
        by apply/andP; split; first apply ltnW. }
      move : BUSY ⇒ [LE [QT [NQT /andP[ARR1 ARR2]]]].
      move: T1; rewrite leq_eqVlt ⇒ /orP [/eqP EQ | GT].
      { subst t; apply completed_implies_scheduled_before in COMPL; rt_eauto.
        by case: COMPL ⇒ [t' [/andP [ARR3 LT__temp] SCHED__temp]]; lia. }
      { apply: NQT; first (apply/andP; split; [exact GT | lia]).
        intros ? ARR HEP ARRB; rewrite /hep_job /FIFO in HEP.
        eapply early_hep_job_is_scheduled; rt_eauto; first by lia.
        by movet'; apply/andP; split; rewrite /hep_job_at /FIFO /JLFP_to_JLDP /hep_job //=; lia. }
    Qed.

  End PriorityInversionBounded.

We prove that in a FIFO-compliant schedule, if a job j is scheduled, then all jobs with higher priority than j have been completed.
  Lemma scheduled_implies_higher_priority_completed :
     j t,
      scheduled_at sched j t
       j_hp,
        arrives_in arr_seq j_hp
        ~~hep_job j j_hp
        completed_by sched j_hp t.
  Proof.
    movej' t SCHED j_hp ARRjhp HEP.
    have EARLIER: job_arrival j_hp < job_arrival j' by rewrite -ltnNge in HEP.
    eapply (early_hep_job_is_scheduled arr_seq _ sched _ _ _ _ j_hp j' _ _ _ t).
    Unshelve. all : rt_eauto.
    movet'; apply /andP; split ⇒ //.
    by apply ltnW.
  Qed.

The next lemma considers FIFO schedules in the context of tasks.
  Section SequentialTasks.

If the scheduled jobs stem from a set of tasks, ...
    Context {Task : TaskType}.
    Context `{JobTask Job Task}.

... then the tasks in a FIFO-compliant schedule necessarily execute sequentially.
    Lemma tasks_execute_sequentially : sequential_tasks arr_seq sched.
    Proof.
      movej1 j2 t ARRj1 ARRj2 SAME_TASKx LT ⇒ //.
      eapply (early_hep_job_is_scheduled); try rt_eauto.
      by move⇒ ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
    Qed.

We also note that the FIFO policy respects sequential tasks.
    Fact fifo_respects_sequential_tasks : policy_respects_sequential_tasks.
    Proof. by movej1 j2 SAME ARRLE; rewrite /hep_job /FIFO. Qed.

  End SequentialTasks.

Finally, let us further assume that there are no needless preemptions among jobs of equal priority.
In the absence of superfluous preemptions and under assumption of the basic readiness model, there are no preemptions at all in a FIFO-compliant schedule.
  Lemma no_preemptions_under_FIFO :
     j t,
      ~~ preempted_at sched j t.
  Proof.
    movej t.
    apply /negP.
    intros CONTR.
    move: CONTR ⇒ /andP [/andP [SCHED1 NCOMPL] SCHED2].
    move : H_schedule_is_valid ⇒ [COME MUST].
    move: (ideal_proc_model_sched_case_analysis sched t) ⇒ [IDLE |[s INTER]].
    { specialize (H_work_conservation j t).
      destruct H_work_conservation as [j_other SCHEDj_other]; first by eapply (COME j t.-1 SCHED1).
      - do 2 (apply /andP; split; last by done).
        eapply scheduled_implies_pending in SCHED1; try rt_eauto.
        move : SCHED1 ⇒ /andP [HAS COMPL].
        by apply leq_trans with t.-1; [exact HAS| lia].
      - move: SCHEDj_other IDLE.
        rewrite scheduled_at_def ⇒ /eqP SCHED /eqP IDLE.
        by rewrite IDLE in SCHED. }
    { specialize (H_no_superfluous_preemptions t j s).
      have HEP : ~~ hep_job j s.
      {
        apply H_no_superfluous_preemptions; last by done.
        by repeat (apply /andP ; split; try by done).
      }
      rewrite /hep_job /fifo.FIFO -ltnNge in HEP.
      eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try rt_eauto.
      - apply scheduled_implies_not_completed in INTER; rt_eauto.
        by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move: INTER ⇒ /negP|lia].
      - by move⇒ ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. }
  Qed.

It immediately follows that FIFO schedules are non-preemptive.
We add the following lemmas to the basic facts database
Global Hint Resolve
  fifo_respects_sequential_tasks
  tasks_execute_sequentially
  : basic_rt_facts.