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

 Require Export prosa.implementation.facts.generic_schedule.
 Require Export prosa.implementation.definitions.ideal_uni_scheduler.
 Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.model.schedule.limited_preemptive.
 
 (** * Properties of the Preemption-Aware Ideal Uniprocessor Scheduler *)
 
@@ -149,8 +150,7 @@ Section NPUniprocessorScheduler.
             move: (H_chooses_from_set _ _ _ IN).
             rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
             rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t') schedule j t'.+1) //.
-            rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule => t'' LT.
-            now rewrite (schedule_up_to_prefix_inclusion _  _  t'' t') //. }
+            by apply schedule_up_to_identical_prefix. }
           case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
           destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
           apply H_valid_preemption_behavior.
@@ -210,6 +210,39 @@ Section NPUniprocessorScheduler.
 
   End PreemptionTimes.
 
+  (** Finally, we establish the main feature: the generated schedule respects
+      the preemption-model semantics. *)
+  Section PreemptionCompliance.
+
+    (** 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.
+
+    (** 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.
+      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 !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.