Library prosa.analysis.facts.priority.fifo

Require Import prosa.model.readiness.basic.
Require Export prosa.model.task.sequentiality.
Require Export prosa.model.schedule.nonpreemptive.
Require Export prosa.model.priority.fifo.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.facts.priority.sequential.
Require Export prosa.analysis.facts.readiness.basic.
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.

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.
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_schedule_is_valid : valid_schedule sched arr_seq.
  Hypothesis H_work_conservation : work_conserving arr_seq sched.

Suppose jobs have preemption points ...
  Context `{JobPreemptable Job}.

...and that the preemption model is valid.
  Hypothesis H_valid_preemption_model :
    valid_preemption_model arr_seq sched.

Assume that the schedule respects the FIFO scheduling policy whenever jobs are preemptable.
  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).

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.

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.

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.

  End SequentialTasks.

Finally, let us further assume that there are no needless preemptions among jobs of equal priority.
  Hypothesis H_no_superfluous_preemptions : no_superfluous_preemptions sched.

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.
  Corollary FIFO_is_nonpreemptive : nonpreemptive_schedule sched.

End BasicLemmas.