two new utility lemmas on FIFO and job completion

analysis/facts/behavior/completion.v

@@ -11,6 +11,7 @@ Section CompletionFacts.
   (** Consider any job type,...*)
   Context {Job: JobType}.
   Context `{JobCost Job}.
+  Context `{JobArrival Job}.
 
   (** ...any kind of processor model,... *)
   Context {PState: Type}.
@@ -79,12 +80,24 @@ Section CompletionFacts.
     exact INCOMP.
   Qed.
 
-  (** Assume that completed jobs do not execute. *)
-  Hypothesis H_completed_jobs:
-    completed_jobs_dont_execute sched.
+
+  (** In the remainder of this section, we assume that schedules are
+      "well-formed": jobs are scheduled neither before their arrival
+      nor after their completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs : completed_jobs_dont_execute sched.
+
+  (** We observe that a job that is completed at the instant of its
+      arrival has a cost of zero. *)
+  Lemma completed_on_arrival_implies_zero_cost :
+    completed_by sched j (job_arrival j) ->
+    job_cost j = 0.
+  Proof.
+    by rewrite /completed_by no_service_before_arrival // leqn0 => /eqP.
+  Qed.
 
   (** Further, we note that if a job receives service at some time t, then its
-     remaining cost at this time is positive. *)
+      remaining cost at this time is positive. *)
   Lemma serviced_implies_positive_remaining_cost:
     forall t,
       service_at sched j t > 0 ->

analysis/facts/priority/fifo.v

@@ -26,8 +26,8 @@ Section BasicLemmas.
   (** 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 :
+  (** ...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
@@ -60,6 +60,25 @@ Section BasicLemmas.
     - by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
   Qed.
 
+  (** 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 :
+    forall j t,
+      scheduled_at sched j t ->
+      forall j_hp,
+        arrives_in arr_seq j_hp ->
+        ~~hep_job j j_hp ->
+        completed_by sched j_hp t.
+  Proof.
+    move => j' t SCHED j_hp ARRjhp HEP.
+    have EARLIER: job_arrival j_hp < job_arrival j' by rewrite -ltnNge in HEP.
+    eapply (early_hep_job_is_scheduled arr_seq _ sched _ _ _ _ j_hp j' _ _ _ t).
+    Unshelve. all : eauto with basic_facts.
+    move=> t'; apply /andP; split => //.
+    by apply ltnW.
+  Qed.
+
   (** The next lemma considers FIFO schedules in the context of tasks. *)
   Section SequentialTasks.