Preemption model compliance

In this MR, we prove that the ideal uniprocessor schedules that are implemented in prosa.implementation.definitions.ideal_uni_scheduler respect the preemption model.

implementation/facts/ideal_uni/preemption_aware.v

@@ -210,39 +210,37 @@ Section NPUniprocessorScheduler.
 
   End PreemptionTimes.
 
-  (** In this section, we establish that the preemption-aware scheduler indeed respects
-      the preemption model semantics. *)
+  (** Finally, we establish the main feature: the generated schedule respects
+      the preemption-model semantics. *)
   Section PreemptionCompliance.
 
-    (** Assuming that every job in [arr_seq] adheres by the rule that jobs must
-        start execution to become nonpreemptive,... *)
-    Hypothesis H_valid_preemption_function : forall j, arrives_in arr_seq j ->
-                                                  job_cannot_become_nonpreemptive_before_execution j.
+    (** As a minimal validity requirement (which is a part of
+        [valid_preemption_model]), we require that any job in [arr_seq] must
+        start execution to become nonpreemptive. *)
+    Hypothesis H_valid_preemption_function :
+      forall j,
+        arrives_in arr_seq j ->
+        job_cannot_become_nonpreemptive_before_execution j.
 
-    (** ...we show that the generated schedule respects the preemption model semantics. *)
+    (** Given such a valid preemption model, we establish that the generated
+        schedule indeed respects the preemption model semantics. *)
     Lemma np_respects_preemption_model :
       schedule_respects_preemption_model arr_seq schedule.
     Proof.
-      rewrite /schedule_respects_preemption_model => j.
-      elim => [| t' IH];
-               first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR) => P; exfalso.
-      move => ARR NP.
-      have SCHED : scheduled_at schedule j t'.
+      move=> j; elim => [| t' IH];
+        first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR) => P; exfalso.
+      move=> ARR NP.
+      have: scheduled_at schedule j t'.
       { apply contraT => NOT_SCHED.
         move: (not_scheduled_implies_no_service _ _ _ NOT_SCHED) => NO_SERVICE.
         rewrite -(service_last_plus_before) NO_SERVICE addn0 in NP; apply IH in NP => //.
         now move /negP in NOT_SCHED. }
-      rewrite /schedule/np_uni_schedule scheduled_at_def /generic_schedule schedule_up_to_def /allocation_at /prev_job_nonpreemptive.
-      rewrite /schedule /np_uni_schedule scheduled_at_def /generic_schedule /allocation_at in SCHED.
-      move /eqP in SCHED; rewrite SCHED.
-      rewrite (identical_prefix_service _ schedule).
-      rewrite ifT => //.
-      rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule.
-      move => h LT; rewrite ltnS in LT.
-      now rewrite (schedule_up_to_prefix_inclusion _ _ _ _ LT h).
+      rewrite !scheduled_at_def /schedule/np_uni_schedule/generic_schedule => /eqP SCHED.
+      rewrite -SCHED (schedule_up_to_prefix_inclusion _ _ t' t'.+1) // np_job_remains_scheduled //.
+      rewrite /prev_job_nonpreemptive SCHED (identical_prefix_service _ schedule) //.
+      by apply schedule_up_to_identical_prefix.
     Qed.
 
-
   End PreemptionCompliance.
 
 End NPUniprocessorScheduler.