# 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, 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').
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).
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.
... 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.
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 ...
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.
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 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 (FIFO Job).
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.
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.
We also note that the FIFO policy respects sequential tasks.
Fact fifo_respects_sequential_tasks : policy_respects_sequential_tasks (FIFO Job).
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.
We add the following lemmas to the basic facts database
Global Hint Resolve
fifo_respects_sequential_tasks
tasks_execute_sequentially
: basic_rt_facts.