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 *)
 
@@ -210,6 +211,41 @@ Section NPUniprocessorScheduler.
 
   End PreemptionTimes.
 
+  (** In this section, we establish that the preemption-aware scheduler indeed 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.
+
+    (** ...we show that the generated schedule 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'.
+      { 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).
+    Qed.
+
+
+  End PreemptionCompliance.
+
 End NPUniprocessorScheduler.