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

Require Export prosa.analysis.abstract.ideal_jlfp_rta.

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.

Require Export prosa.analysis.abstract.ideal_jlfp_rta.

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

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.

Consider any arrival sequence of such jobs ...

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

Hypothesis H_schedule_is_valid : valid_schedule sched arr_seq.

Hypothesis H_work_conservation : work_conserving arr_seq sched.

Suppose jobs have preemption points ...

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

∀ j t,

arrives_in arr_seq j →

pending sched j t →

¬ priority_inversion sched j t.

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

Consider any kind of tasks.

Consider a task tsk.

Assume the arrival times are consistent.

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 (FIFO Job).

respects_JLFP_policy_at_preemption_point arr_seq sched (FIFO Job).

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.

End PriorityInversionBounded.

priority_inversion_is_bounded_by_constant arr_seq sched tsk 0.

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.

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

If the scheduled jobs stem from a set of tasks, ...

... then the tasks in a FIFO-compliant schedule necessarily
execute sequentially.

We also note that the FIFO policy respects sequential tasks.

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.

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.

fifo_respects_sequential_tasks

tasks_execute_sequentially

: basic_rt_facts.