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
      ~~ is_priority_inversion sched j t.

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.

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.
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.
It immediately follows that FIFO schedules are non-preemptive.