Ideal Uniprocessor Scheduler Implementation

This MR introduces the first part of refactored Prosa's implementation folder, namely a generic function for computing valid work-conserving uniprocessor schedules for given priority policies, readiness models, and preemption policies.

This will be useful for future assumption-free instantiations of analyses in Prosa.

@mmaida @sbozhko: please review. In particular, please check out the two new readiness model classes nonclairvoyant_readiness and valid_nonpreemptive_readiness.

implementation/facts/ideal_uni/prio_aware.v

@@ -40,7 +40,7 @@ Section PrioAwareUniprocessorScheduler.
       priority-aware ideal uniprocessor scheduler. *)
   Let schedule := uni_schedule arr_seq.
 
-  (* First, we note that the priority-aware job selection policy obviously
+  (** First, we note that the priority-aware job selection policy obviously
      maintains work-conservation. *)
   Corollary uni_schedule_work_conserving:
     work_conserving arr_seq schedule.
@@ -52,7 +52,7 @@ Section PrioAwareUniprocessorScheduler.
     - by move=> ->.
   Qed.
 
-  (* Second, we similarly note that schedule validity is also maintained. *)
+  (** Second, we similarly note that schedule validity is also maintained. *)
   Corollary uni_schedule_valid:
     valid_schedule schedule arr_seq.
   Proof.
@@ -87,12 +87,12 @@ Section PrioAwareUniprocessorScheduler.
       { apply contraL with (b := preemption_time (uni_schedule arr_seq) t) => //.
         now apply np_consistent. }
       move: SCHED.
-      rewrite  scheduled_at_def => /eqP.
+      rewrite scheduled_at_def => /eqP.
       rewrite {1}/schedule/uni_schedule/np_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).
       rewrite ifF //.
       now apply negbTE.
     Qed.
-
+ 
     (** From the preceding facts, we conclude that [uni_schedule arr_seq]
         respects the priority policy at preemption times. *)
     Theorem schedule_respects_policy :
@@ -100,24 +100,22 @@ Section PrioAwareUniprocessorScheduler.
     Proof.
       move=> j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
       case: (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) => [SCHED_j1|NOT_SCHED_j1].
-      - have <-: j1 = j2 by apply (ideal_proc_model_is_a_uniprocessor_model j1 j2 (uni_schedule arr_seq) t).
-        now apply H_reflexive_priorities.
-      - move: BACK_j1.
+      { have <-: j1 = j2 by apply (ideal_proc_model_is_a_uniprocessor_model j1 j2 (uni_schedule arr_seq) t).
+        now apply H_reflexive_priorities. }
+      { move: BACK_j1.
         have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.
-        { have NOT_SCHED_j1':  ~~ scheduled_at (prefix t) j1 t.
-          { rewrite /prefix scheduled_at_def.
-            induction t => //.
-            now rewrite schedule_up_to_empty. }
-          apply backlogged_prefix_invariance' with (h := t) => //.
+        { apply backlogged_prefix_invariance' with (h := t) => //.
           rewrite /identical_prefix /uni_schedule /prefix => t' LT.
           induction t => //.
-          rewrite /np_uni_schedule/generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //. }
+          rewrite /np_uni_schedule /generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.
+          rewrite /prefix scheduled_at_def.
+          induction t => //.
+          now rewrite schedule_up_to_empty. }
         move=> BACK_j1.
-        have MEM_j1: j1 \in jobs_backlogged_at arr_seq (prefix t) t by
-            apply mem_backlogged_jobs.
         move: (scheduled_job_is_supremum j2 t SCHED_j2 PREEMPT) => SUPREMUM.
         apply supremum_spec with (s := jobs_backlogged_at arr_seq (prefix t) t) => //.
-    Qed.
+        now apply mem_backlogged_jobs. }
+    Qed.    
 
   End Priority.