Library prosa.analysis.facts.priority.fifo

We first make some trivial observations about the FIFO priority policy to avoid having to re-reason these steps repeatedly in the subsequent proofs.
Section PriorityFacts.

Consider any type of jobs.
  Context `{Job : JobType} {Arrival : JobArrival Job}.

Under FIFO scheduling, hep_job is simply a statement about arrival times.
  Fact hep_job_arrival_FIFO :
     j j',
      hep_job j j' = (job_arrival j job_arrival j').
    movej j'.
    by rewrite /hep_job /FIFO.

Similarly, ~~ hep_job implies a strict inequality on arrival times.
  Fact not_hep_job_arrival_FIFO :
     j j',
      ~~ hep_job j j' = (job_arrival j' < job_arrival j).
  Proof. by movej j'; rewrite hep_job_arrival_FIFO -ltnNge. Qed.

Combining the above two facts, we get that, trivially, ~~ hep_job j j' implies hep_job j' j, ...
  Fact not_hep_job_FIFO :
     j j',
      ~~ hep_job j j' hep_job j' j.
    movej j'; rewrite not_hep_job_arrival_FIFO hep_job_arrival_FIFO.
    exact: ltnW.

... from which we can infer always_higher_priority.
  Fact not_hep_job_always_higher_priority_FIFO :
     j j',
      ~~ hep_job j j' always_higher_priority j' j.
    movej j' NHEP.
    rewrite always_higher_priority_jlfp; apply/andP; split ⇒ //.
    exact: not_hep_job_FIFO.

End PriorityFacts.

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 valid arrival sequence of such jobs ...
... and the resulting uniprocessor schedule.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uniproc : uniprocessor_model PState.
  Variable sched : schedule PState.
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 arr_seq sched j t.
    movej t IN /andP[ARR]; apply: contraNNpijt.
    have [j' + PRIO] : exists2 j', scheduled_at sched j' t & ~~ hep_job j' j
      by exact/uni_priority_inversion_P.
    apply: (early_hep_job_is_scheduled arr_seq) ⇒ //.
    - by rewrite -not_hep_job_arrival_FIFO.
    - exact: not_hep_job_always_higher_priority_FIFO.

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
        arrives_in arr_seq j_hp
        ~~ hep_job j j_hp
        completed_by sched j_hp t.
    movej' t SCHED j_hp ARRjhp HEP.
    apply: early_hep_job_is_scheduled ⇒ //.
    - by rewrite -not_hep_job_arrival_FIFO.
    - exact: not_hep_job_always_higher_priority_FIFO.

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 arr_seq sched tsk (constant 0).
      movej ARRIN TASK POS t1 t2 BUSY.
      rewrite leqn0; apply/eqP; rewrite big_nat_eq0t /andP[T1 T2].
      apply/eqP; rewrite eqb0.
      apply: contraT ⇒ /negPn pijt.
      have [j' SCHED NHEP] : exists2 j', scheduled_at sched j' t & ~~ hep_job j' j
        by exact/uni_priority_inversion_P.
      move: T1; rewrite leq_eqVlt ⇒ /orP [/eqP EQ | GT].
      { have /completed_implies_scheduled_before [//|//|t' [/andP [+ +] _]]:
          completed_by sched j t by apply: (scheduled_implies_higher_priority_completed j').
        by have: t1 job_arrival j by []; rewrite -EQ; lia. }
      { exfalso; apply: busy_interval_prefix_no_quiet_time ⇒ // [|? ARR HEP ARRB];
          first by apply/andP; split; [|exact: T2].
        apply: (scheduled_implies_higher_priority_completed j') ⇒ //.
        move: NHEP; rewrite !not_hep_job_arrival_FIFO.
        by apply: leq_trans. }

As a corollary, FIFO implies the absence of service inversion.
    Corollary FIFO_implies_no_service_inversion :
      service_inversion_is_bounded_by arr_seq sched tsk (constant 0).
      movej ARR TSK POS t1 t2 PREF.
      rewrite (leqRW (cumul_service_inv_le_cumul_priority_inv _ _ _ _ _ _ _ _ _ _)) //=.
      by apply FIFO_implies_no_pi.

  End PriorityInversionBounded.

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.
      movej1 j2 t ARRj1 ARRj2 SAME_TASKx LT ⇒ //.
      apply: (early_hep_job_is_scheduled) ⇒ //.
      apply: not_hep_job_always_higher_priority_FIFO.
      by rewrite not_hep_job_arrival_FIFO.

We also note that the FIFO policy respects sequential tasks.
    Fact fifo_respects_sequential_tasks : policy_respects_sequential_tasks (FIFO Job).
    Proof. by movej1 j2 SAME ARRLE; rewrite hep_job_arrival_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.
    movej t; apply /negP ⇒ /andP [/andP [SCHED1 NCOMPL] SCHED2].
    case SJA: (scheduled_job_at arr_seq sched t) ⇒ [j'|].
    { move: SJA ⇒ /eqP; rewrite scheduled_job_at_scheduled_at // ⇒ SCHED'.
      have: ~~ hep_job j j'.
      { apply: H_no_superfluous_preemptions; last exact: SCHED'.
        by repeat (apply /andP ; split). }
      rewrite /hep_job /fifo.FIFO -ltnNgeEARLIER.
      eapply (early_hep_job_is_scheduled arr_seq) with (JLFP:=FIFO Job) in SCHED1 ⇒ //.
      - apply scheduled_implies_not_completed in SCHED' ⇒ //.
        by eapply (incompletion_monotonic sched j' t.-1 t) in SCHED'; [move: SCHED' ⇒ /negP|lia].
      - by move⇒ ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. }
    { move: SJA; rewrite scheduled_job_at_none ⇒ // NSCHED.
      have [j' SCHED']: j', scheduled_at sched j' t.
      { apply: (H_work_conservation j t) ⇒ //.
        apply/andP; split ⇒ //.
        rewrite /job_ready/basic_ready_instance/pending.
        apply/andP; split ⇒ //.
        have: has_arrived j t.-1; last by rewrite /has_arrived; lia.
        exact: has_arrived_scheduled. }
      by move: (NSCHED j') ⇒ /negP. }

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