From a0579b475bd5ed940173487a8ca8e35a24b6af97 Mon Sep 17 00:00:00 2001
From: kimaya <f20171026@goa.bits-pilani.ac.in>
Date: Mon, 25 Oct 2021 16:37:30 +0200
Subject: [PATCH] add basic facts about the FIFO scheduling policy
- there is no priority inversion in FIFO schedules
- all jobs of a tasks necessarily execute in arrival order
- the FIFO policy never requires a job to be preempted
---
analysis/facts/priority/fifo.v | 128 +++++++++++++++++++++++++++++++++
1 file changed, 128 insertions(+)
create mode 100644 analysis/facts/priority/fifo.v
diff --git a/analysis/facts/priority/fifo.v b/analysis/facts/priority/fifo.v
new file mode 100644
index 000000000..b797c306c
--- /dev/null
+++ b/analysis/facts/priority/fifo.v
@@ -0,0 +1,128 @@
+Require Export prosa.model.task.sequentiality.
+Require Export prosa.model.schedule.nonpreemptive.
+Require Export prosa.model.priority.fifo.
+Require Export prosa.analysis.facts.priority.sequential.
+Require Export prosa.analysis.facts.readiness.basic.
+Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.readiness.basic.
+
+(** In this section, we prove some fundamental properties of the FIFO policy. *)
+Section BasicLemmas.
+
+ (** 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 length of non-preemptive segments is bounded. *)
+ Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
+ valid_preemption_model arr_seq sched.
+
+ (** Assume that the schedule respects the FIFO scheduling policy whenever jobs
+ are preemptable. *)
+ Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+
+ (** We observe that there is no priority inversion in a
+ FIFO-compliant schedule. *)
+ Lemma FIFO_implies_no_priority_inversion :
+ forall j t,
+ arrives_in arr_seq j ->
+ pending sched j t ->
+ ~~ is_priority_inversion sched j t.
+ Proof.
+ move => j t ARRIVES PENDINGj.
+ rewrite /is_priority_inversion.
+ move: (ideal_proc_model_sched_case_analysis sched t) => [/eqP -> //|[s INTER]].
+ have -> : sched t = Some s; first by apply /eqP; rewrite -scheduled_at_def.
+ apply /negP; apply /negPn.
+ rewrite Bool.negb_involutive.
+ destruct (s == j) eqn:EQ; first by move: EQ => /eqP ->; rewrite /hep_job /fifo.FIFO.
+ destruct (hep_job s j) eqn:HEP; first by done.
+ move : HEP => /negP/negP HEP.
+ rewrite -ltnNge in HEP.
+ contradict PENDINGj.
+ apply /negP; rewrite negb_and.
+ apply /orP; right; apply /negPn.
+ have -> : scheduled_at sched s t -> completed_by sched j t => //.
+ eapply (early_hep_job_is_scheduled); try eauto 2 with basic_facts.
+ - by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
+ Qed.
+
+ (** 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.
+ Proof.
+ move => j1 j2 t ARRj1 ARRj2 SAME_TASKx LT => //.
+ eapply (early_hep_job_is_scheduled); try eauto 2 with basic_facts.
+ by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
+ Qed.
+
+ 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 :
+ forall j t,
+ ~~ preempted_at sched j t.
+ Proof.
+ move => j t.
+ apply /negP.
+ intros CONTR.
+ move: CONTR => /andP [/andP [SCHED1 NCOMPL] SCHED2].
+ move : H_schedule_is_valid => [COME MUST].
+ move: (ideal_proc_model_sched_case_analysis sched t) => [IDLE |[s INTER]].
+ { specialize (H_work_conservation j t).
+ destruct H_work_conservation as [j_other SCHEDj_other]; first by eapply (COME j t.-1 SCHED1).
+ - do 2 (apply /andP; split; last by done).
+ eapply scheduled_implies_pending in SCHED1; try eauto with basic_facts.
+ move : SCHED1 => /andP [HAS COMPL].
+ by apply leq_trans with t.-1; [exact HAS| ssrlia].
+ - move: SCHEDj_other IDLE.
+ rewrite scheduled_at_def => /eqP SCHED /eqP IDLE.
+ by rewrite IDLE in SCHED. }
+ { specialize (H_no_superfluous_preemptions t j s).
+ have HEP : ~~ hep_job j s.
+ {
+ apply H_no_superfluous_preemptions; last by done.
+ by repeat (apply /andP ; split; try by done).
+ }
+ rewrite /hep_job /fifo.FIFO -ltnNge in HEP.
+ eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try eauto 2 with basic_facts.
+ - apply scheduled_implies_not_completed in INTER; eauto with basic_facts.
+ by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move: INTER => /negP|ssrlia].
+ - by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. }
+ Qed.
+
+ (** It immediately follows that FIFO schedules are
+ non-preemptive. *)
+ Corollary FIFO_is_nonpreemptive : nonpreemptive_schedule sched.
+ Proof.
+ by rewrite -no_preemptions_equiv_nonpreemptive; apply no_preemptions_under_FIFO.
+ Qed.
+
+End BasicLemmas.
+
--
GitLab