Library prosa.analysis.facts.priority.fifo

Require Import prosa.model.readiness.basic.
Require Export prosa.model.task.sequentiality.
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.busy_interval.all.
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Require Export prosa.analysis.facts.priority.inversion.
Require Export prosa.analysis.facts.busy_interval.service_inversion.

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, ...

Context {JLFP : JLFP_policy Job}.
Hypothesis H_policy_is_FIFO : policy_is_FIFO JLFP.

... ~~ 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 ).

Combining the above fact with the definition of FIFO scheduling, 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.

... 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.

A FIFO policy is reflexive since a job arrives no later than itself.

Fact FIFO_policy_is_reflexive :
reflexive_job_priorities JLFP.

A FIFO policy is transitive since arrival order is transitive.

Fact FIFO_policy_is_transitive :
transitive_job_priorities JLFP.

Next, we note that FIFO priorities are compatible with sequential task models.

Consider the tasks corresponding to the jobs under consideration.

Context {Task : TaskType} `{JobTask Job Task}.

FIFO priorities respect sequential tasks because jobs of the same task inherit priority from their arrival order.

Fact FIFO_policy_respects_sequential_tasks :
policy_respects_sequential_tasks JLFP.

End PriorityFacts.

We add the following lemmas to the basic facts database

Global Hint Resolve
  FIFO_policy_is_reflexive
  FIFO_policy_is_transitive
  FIFO_policy_respects_sequential_tasks
  : basic_rt_facts.

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}.

Assume FIFO scheduling.

Consider any valid arrival sequence of such jobs ...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

... 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.

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.

  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_policy_is_FIFO : policy_is_FIFO JLFP.
  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

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.

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.

In this section, we prove the cumulative priority inversion for any task is bounded by 0.

Section PriorityInversionBounded.

Consider any kind of tasks.

Context `{Task : TaskType} `{JobTask Job Task}.

Consider a task tsk.

Variable tsk : Task.

Assume the arrival times are consistent.

Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.

Assume that the schedule follows the FIFO policy at preemption time.

Hypothesis H_respects_policy_at_preemption_point :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

Assume the schedule is valid.

Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

Assume there are no duplicates in the arrival sequence.

Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq.

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).

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).

  End PriorityInversionBounded.

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.