move general preemption lemmas

... out of the priority-inversion file, where they are used, but
topically don't belong.

analysis/facts/busy_interval/priority_inversion.v

@@ -5,76 +5,11 @@ Require Export prosa.analysis.definitions.job_properties.
 Require Export prosa.analysis.definitions.busy_interval.
 Require Export prosa.analysis.facts.model.ideal_schedule.
 Require Export prosa.analysis.facts.busy_interval.busy_interval.
+Require Export prosa.analysis.facts.model.preemption.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
 
-(** In preparation of the derivation of the priority inversion bound, we
-    establish two basic facts on preemption times. *)
-Section PreemptionTimes.
-
-  (** Consider any type of tasks ... *)
-  Context {Task : TaskType}.
-  Context `{TaskCost Task}.
-  Context `{TaskMaxNonpreemptiveSegment Task}.
-
-  (**  ... and any type of jobs associated with these tasks. *)
-  Context {Job : JobType}.
-  Context `{JobTask Job Task}.
-  Context `{JobArrival Job}.
-  Context `{JobCost Job}.
-
-  (** In addition, we assume the existence of a function mapping a
-      task to its maximal non-preemptive segment ... *)
-  Context `{TaskMaxNonpreemptiveSegment Task}.
-
-  (** ... and the existence of a function mapping a job and
-      its progress to a boolean value saying whether this job is
-      preemptable at its current point of execution. *)
-  Context `{JobPreemptable Job}.
-
-  (** Consider any arrival sequence with consistent arrivals. *)
-  Variable arr_seq : arrival_sequence Job.
-  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-
-  (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
-  Variable sched : schedule (ideal.processor_state Job).
-  Hypothesis H_jobs_come_from_arrival_sequence:
-    jobs_come_from_arrival_sequence sched arr_seq.
-
-  (** Consider a valid model with bounded nonpreemptive segments. *)
-  Hypothesis H_model_with_bounded_nonpreemptive_segments:
-    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
-
-  (** Then, we show that time 0 is a preemption time. *)
-  Lemma zero_is_pt: preemption_time sched 0.
-  Proof.
-    unfold preemption_time.
-    case SCHED: (sched 0) => [j | ]; last by done.
-    move: (SCHED) => /eqP; rewrite -scheduled_at_def; move => ARR.
-    apply H_jobs_come_from_arrival_sequence in ARR.
-    rewrite /service /service_during big_geq; last by done.
-    destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
-    by move: (T1 j ARR) => [PP _].
-  Qed.
-
-  (** Also, we show that the first instant of execution is a preemption time. *)
-  Lemma first_moment_is_pt:
-    forall j prt,
-      arrives_in arr_seq j ->
-      ~~ scheduled_at sched j prt ->
-      scheduled_at sched j prt.+1 ->
-      preemption_time sched prt.+1.
-  Proof.
-    intros s pt ARR NSCHED SCHED.
-    unfold preemption_time.
-    move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
-    destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
-    by move: (T1 s ARR) => [_ [_ [_ P]]]; apply P.
-  Qed.
-
-End PreemptionTimes.
-
 (** * Priority inversion is bounded *)
 (** In this module we prove that any priority inversion that occurs in the model with bounded 
     nonpreemptive segments defined in module prosa.model.schedule.uni.limited.platform.definitions 

analysis/facts/model/preemption.v

+Require Export prosa.model.schedule.priority_driven.
+Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.analysis.facts.behavior.completion.
+
+
+(** In this section, we establish two basic facts about preemption times. *)
+Section PreemptionTimes.
+  
+  (** Consider any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** In addition, we assume the existence of a function mapping a job and
+      its progress to a boolean value saying whether this job is
+      preemptable at its current point of execution. *)
+  Context `{JobPreemptable Job}.
+
+  (** Consider any arrival sequence with consistent arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+  (** Next, consider any ideal uniprocessor schedule of this arrival sequence... *)
+  Variable sched : schedule (ideal.processor_state Job).
+
+  (** ...where, jobs come from the arrival sequence. *)
+  Hypothesis H_jobs_come_from_arrival_sequence:
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** Consider a valid preemption model. *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched. 
+
+  (**  We show that time 0 is a preemption time. *)
+  Lemma zero_is_pt: preemption_time sched 0.
+  Proof.
+    unfold preemption_time.
+    case SCHED: (sched 0) => [j | ]; last by done.
+    move: (SCHED) => /eqP; rewrite -scheduled_at_def; move => ARR.
+    apply H_jobs_come_from_arrival_sequence in ARR.
+    rewrite /service /service_during big_geq; last by done.
+    by move: (H_valid_preemption_model j ARR) => [PP _].
+  Qed.
+  (** Also, we show that the first instant of execution is a preemption time. *)
+  Lemma first_moment_is_pt:
+    forall j prt,
+      arrives_in arr_seq j ->
+      ~~ scheduled_at sched j prt ->
+      scheduled_at sched j prt.+1 ->
+      preemption_time sched prt.+1.
+  Proof.
+    intros s pt ARR NSCHED SCHED.
+    unfold preemption_time.
+    move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
+    by move: (H_valid_preemption_model s ARR) => [_ [_ [_ P]]]; apply P.
+  Qed.
+
+End PreemptionTimes.
+
+(** In this section, we prove a lemma relating scheduling and preemption times. *)
+Section PreemptionFacts.
+
+  (** Consider any type of jobs. *)
+  Context {Job : JobType}.
+  Context `{Arrival : JobArrival Job}.
+  Context `{Cost : JobCost Job}.
+  Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+
+  (** Consider any arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
+  Variable sched : schedule (ideal.processor_state Job).
+  
+  (** ...and, assume that the schedule is valid. *)
+  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+  (** In addition, we assume the existence of a function mapping jobs to their preemption points ... *)
+  Context `{JobPreemptable Job}.
+
+  (** ... and assume that it defines a valid preemption model. *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** We prove that every nonpreemptive segment always begins with a preemption time. *)
+  Lemma scheduling_of_any_segment_starts_with_preemption_time:
+    forall j t,
+      scheduled_at sched j t ->
+      exists pt,
+        job_arrival j <= pt <= t /\
+          preemption_time sched pt /\
+          (forall t', pt <= t' <= t -> scheduled_at sched j t').
+  Proof.
+    intros s t SCHEDst.
+    have EX: exists t', (t' <= t) && (scheduled_at sched s t')
+                   && (all (fun t'' => scheduled_at sched  s t'') (index_iota t' t.+1 )).
+    { exists t. apply/andP; split; [ by apply/andP; split | ].
+      apply/allP; intros t'.
+      by rewrite mem_index_iota ltnS -eqn_leq; move => /eqP <-.  
+    }
+    have MATE : jobs_must_arrive_to_execute sched by eauto with basic_facts. 
+    move :  (H_sched_valid) =>  [COME_ARR READY].
+    have MIN := ex_minnP EX. 
+    move: MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
+    destruct mpt.
+    - exists 0; repeat split.
+      + by apply/andP; split => //; apply MATE.
+      +  eapply (zero_is_pt arr_seq); eauto 2.
+      + by intros; apply ALL; rewrite mem_iota subn0 add0n ltnS.
+    - have NSCHED: ~~ scheduled_at sched  s mpt.
+      { apply/negP; intros SCHED.
+        enough (F : mpt < mpt); first by rewrite ltnn in F.
+        apply MIN.
+        apply/andP; split; [by apply/andP; split; [ apply ltnW | ] | ].
+        apply/allP; intros t'.
+        rewrite mem_index_iota; move => /andP [GE LE].
+        move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LT].
+        - by subst t'. 
+        - by apply ALL; rewrite mem_index_iota; apply/andP; split. 
+      }         
+      have PP: preemption_time sched mpt.+1 by eapply (first_moment_is_pt arr_seq)  with (j := s); eauto 2.
+      exists mpt.+1; repeat split; try done.
+      + apply/andP; split; last by done.
+       by apply MATE in SCHEDsmpt.
+      + move => t' /andP [GE LE].
+        by apply ALL; rewrite mem_index_iota; apply/andP; split.
+  Qed.
+
+End PreemptionFacts.