revise ideal uniprocessor schedule facts

- Slightly change `valid_nonpreemptive_readiness` so that `sched` is a
  parameter. This way, the proposition can be assumed to hold only for a
  certain schedule (making weaker assumptions).

- Modify `prev_job_nonpreemptive, to unconditionally get
  `jobs_must_be_ready_to_execute`.
  
- Revise lemmas accordingly. 

analysis/definitions/readiness.v

@@ -41,8 +41,8 @@ Section ReadinessModelProperties.
       ready. Consequently, in a valid preemption-policy-compliant schedule, a
       nonpreemptive job must remain ready until at least the end of its
       nonpreemptive section. *)
-  Definition valid_nonpreemptive_readiness :=
-     forall sched j t,
+  Definition valid_nonpreemptive_readiness sched :=
+     forall j t,
         ~~ job_preemptable j (service sched j t) -> job_ready sched j t.
   
 End ReadinessModelProperties.

implementation/definitions/ideal_uni_scheduler.v

@@ -31,9 +31,7 @@ Section UniprocessorScheduler.
   (** ** Preemption-Aware Scheduler *)
 
   (** First, we define the notion of a generic uniprocessor scheduler that is
-      cognizant of non-preemptive sections, ... *)
-
-  (** ... so consider any preemption model. *)
+      cognizant of non-preemptive sections, so consider any preemption model. *)
   Context `{JobPreemptable Job}.
 
   Section NonPreemptiveSectionAware.
@@ -61,7 +59,8 @@ Section UniprocessorScheduler.
         match t with
         | 0 => false
         | S t' => if sched_prefix t' is Some j then
-                    ~~job_preemptable j (service sched_prefix j t)
+                   job_ready sched_prefix j t &&
+                   ~~job_preemptable j (service sched_prefix j t)
                   else
                     false
         end.
@@ -76,8 +75,8 @@ Section UniprocessorScheduler.
           choose_job t (jobs_backlogged_at arr_seq sched_prefix t).
     End JobAllocation.
 
-    (* A preemption-policy-aware ideal uniprocessor schedule is then produced
-       when using [allocation_at] as the policy for the generic scheduler. *)
+    (** A preemption-policy-aware ideal uniprocessor schedule is then produced
+        when using [allocation_at] as the policy for the generic scheduler. *)
     Definition np_uni_schedule : schedule PState := generic_schedule allocation_at idle_state.
 
   End NonPreemptiveSectionAware.

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.task.sequentiality.
 Require Export prosa.model.schedule.limited_preemptive.
 
 (** * Properties of the Preemption-Aware Ideal Uniprocessor Scheduler *)
@@ -14,7 +15,7 @@ Require Import prosa.model.processor.ideal.
 Section NPUniprocessorScheduler.
 
   (** Consider any type of jobs with costs and arrival times, ... *)
-  Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.
+  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
 
   (** ... in the context of an ideal uniprocessor model. *)
   Let PState := ideal.processor_state Job.
@@ -61,9 +62,9 @@ Section NPUniprocessorScheduler.
       elim: t => [|t _]; first by apply H_non_idling.
       rewrite /allocation_at /prev_job_nonpreemptive.
       elim: (sched t) => [j'|]; last by apply H_non_idling.
-      rewrite if_neg.
-      elim: (job_preemptable j' (service sched j' t.+1)); first by apply H_non_idling.
-      by discriminate.
+      move=> SCHED.
+      destruct (job_ready sched j' t.+1 && ~~ job_preemptable j' (service sched j' t.+1)) => //.
+      by apply (H_non_idling t.+1).
     Qed.
 
     (** As a stepping stone, we observe that the generated schedule is idle at
@@ -110,63 +111,116 @@ Section NPUniprocessorScheduler.
       sequence and only ready jobs are scheduled. *)
   Section Validity.
 
-    (** Any reasonable job selection policy will not create jobs "out of thin
-        air," i.e., if a job is selected, it was among those given to choose
-        from. *)
-    Hypothesis H_chooses_from_set:
-      forall t s j, choose_job t s = Some j -> j \in s.
-
-    (** For the schedule to be valid, we require the notion of readiness to be
-        consistent with the preemption model: a non-preemptive job remains
-        ready until (at least) the end of its current non-preemptive
-        section. *)
-    Hypothesis H_valid_preemption_behavior:
-      valid_nonpreemptive_readiness RM.
-
-    (** First, we show that if a job is chosen from the list of backlogged jobs, then it must be ready. *)
-    Lemma choose_job_implies_job_ready:
-      forall t j,
-      choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1) = Some j
-      -> job_ready schedule j t.+1.
+    (** First, any reasonable job selection policy will not create jobs "out 
+        of thin air," i.e., if a job is selected, it was among those given
+        to choose from. *)
+    Hypothesis H_chooses_from_set: forall t s j, choose_job t s = Some j -> j \in s.
+    
+    (** Second, for the schedule to be valid, we require the notion of readiness 
+        to be consistent with the preemption model: a non-preemptive job remains
+        ready until (at least) the end of its current non-preemptive section. *)
+    Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule.
+    
+    (** Finally, we assume the readiness model to be non-clairvoyant. *)
+    Hypothesis H_nonclairvoyant_readiness: nonclairvoyant_readiness RM.
+    
+    (** For notational convenience, recall the definition of a prefix of the
+        schedule based on which the next decision is made. *)
+    Let sched_prefix t :=
+      if t is t'.+1 then schedule_up_to policy None t' else empty_schedule idle_state.
+
+    (** We begin by showing that any job in the schedule must come from the arrival 
+        sequence used to generate it. *)
+    Lemma np_schedule_jobs_from_arrival_sequence:
+      jobs_come_from_arrival_sequence schedule arr_seq.
+    Proof.
+      move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
+      elim: t => [/eqP | t'  IH /eqP].
+      - rewrite schedule_up_to_def  /allocation_at  /prev_job_nonpreemptive => IN.
+        move: (H_chooses_from_set _ _ _ IN).
+        by apply backlogged_job_arrives_in.
+      - rewrite schedule_up_to_def  /allocation_at.
+        case: (prev_job_nonpreemptive  (schedule_up_to _ _ t') t'.+1) => [|IN].
+        + by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.
+        + move: (H_chooses_from_set _ _ _ IN).
+          by apply backlogged_job_arrives_in.
+    Qed.
+
+    (** Next, we show that any job selected by the job selection policy must 
+        be ready. *)
+    Theorem chosen_job_is_ready:
+      forall j t,
+        choose_job t (jobs_backlogged_at arr_seq (sched_prefix t) t) == Some j ->
+        job_ready schedule j t.
     Proof.
-      move=> t j IN.
-      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) //.
-      by apply schedule_up_to_identical_prefix.
+      move=> j t /eqP SCHED.
+      apply H_chooses_from_set in SCHED.
+      move: SCHED; rewrite mem_filter => /andP [/andP[READY _] IN].
+      rewrite (H_nonclairvoyant_readiness _ (sched_prefix t) j t) //.
+      move=> t' LEQt'.
+      rewrite /schedule /np_uni_schedule /generic_schedule
+              schedule_up_to_def /sched_prefix.
+      destruct t => //=.
+      rewrite -schedule_up_to_def.
+      by apply (schedule_up_to_prefix_inclusion policy).
     Qed.
 
-    (** Next, we show that, under these natural assumptions, the generated schedule is valid. *)
+    (** Starting from the previous result we show that, at any instant, only
+        a ready job can be scheduled. *)
+    Theorem jobs_must_be_ready:
+      jobs_must_be_ready_to_execute schedule.
+    Proof.
+      move=> j t SCHED.
+      rewrite scheduled_at_def /schedule /uni_schedule /np_uni_schedule
+              /allocation_at /generic_schedule schedule_up_to_def //= in SCHED.
+      destruct (prev_job_nonpreemptive _) eqn:PREV.
+      { destruct t => //; rewrite //= in SCHED, PREV.
+        destruct (schedule_up_to) => //.
+        move: PREV => /andP [READY _].
+        move: SCHED=> /eqP SCHED.
+        injection SCHED => EQ; rewrite -> EQ in *.
+        erewrite (H_nonclairvoyant_readiness _ _ j t.+1); [by apply READY| |by done].
+        move=> t' LT.
+        rewrite /schedule /np_uni_schedule /generic_schedule //=.
+        rewrite /allocation_at //=.
+        by apply (schedule_up_to_prefix_inclusion policy). }
+      { by apply chosen_job_is_ready. }
+    Qed.
+
+    (** Finally, we show that the generated schedule is valid. *)
     Theorem np_schedule_valid:
       valid_schedule schedule arr_seq.
     Proof.
-      split; move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
-      { elim: t => [/eqP | t'  IH /eqP].
-        - rewrite schedule_up_to_def  /allocation_at  /prev_job_nonpreemptive => IN.
-          move: (H_chooses_from_set _ _ _ IN).
-          by apply backlogged_job_arrives_in.
-        - rewrite schedule_up_to_def  /allocation_at.
-          case: (prev_job_nonpreemptive  (schedule_up_to _ _ t') t'.+1) => [|IN];
-                first by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.
-          move: (H_chooses_from_set _ _ _ IN).
-          by apply backlogged_job_arrives_in. }
-      { elim: t => [/eqP |t'  IH /eqP].
-        - rewrite schedule_up_to_def  /allocation_at  /prev_job_nonpreemptive => IN.
+      rewrite /valid_schedule; split; first by apply np_schedule_jobs_from_arrival_sequence.
+      move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
+      elim: t => [/eqP |t'  IH /eqP].
+      { rewrite schedule_up_to_def  /allocation_at  /prev_job_nonpreemptive => IN.
+        move: (H_chooses_from_set _ _ _ IN).
+        rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
+        now rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0). }
+      { rewrite schedule_up_to_def  /allocation_at /prev_job_nonpreemptive.
+        have JOB: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state  t') t'.+1)
+                  = Some j
+                  -> job_ready schedule j t'.+1.
+        { move=> IN.
           move: (H_chooses_from_set _ _ _ IN).
           rewrite mem_filter /backlogged => /andP [/andP [READY _]  _].
-          by rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0).
-        - rewrite schedule_up_to_def  /allocation_at /prev_job_nonpreemptive.
-          case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply choose_job_implies_job_ready.
-          destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply choose_job_implies_job_ready.
-          apply H_valid_preemption_behavior.
-          injection EQ => <-.
-          move: NP.
-          have <-: (service (schedule_up_to policy idle_state t') j' t'.+1
-                    = service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1) => //.
-          rewrite /service.
-          apply equal_prefix_implies_same_service_during => t /andP [_ BOUND].
-          by rewrite (schedule_up_to_prefix_inclusion _  _ t t'). }
-    Qed.
+          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') //. }
+        case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
+        destruct (job_ready _ _ _ && ~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
+        apply H_valid_preemption_behavior.
+        injection EQ => <-.
+        move: NP.
+        have <-: (service (schedule_up_to policy idle_state t') j' t'.+1
+                  = service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1) => //.
+        rewrite /service.
+        apply equal_prefix_implies_same_service_during => t /andP [_ BOUND].
+        now rewrite (schedule_up_to_prefix_inclusion _  _ t t').
+        rewrite //=.
+        by move=> /andP [? ?]. }
+    Qed. 
 
   End Validity.
 
@@ -210,7 +264,8 @@ Section NPUniprocessorScheduler.
                 service (schedule_up_to policy idle_state t) j t.+1) => //.
       rewrite /service.
       apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].
-      by rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
+      rewrite (schedule_up_to_prefix_inclusion _ _ t' t) //. 
+      by move=> /andP [? ?].
     Qed.
 
   End PreemptionTimes.
@@ -226,6 +281,11 @@ Section NPUniprocessorScheduler.
       forall j,
         arrives_in arr_seq j ->
         job_cannot_become_nonpreemptive_before_execution j.
+    
+    (** Second, for the schedule to be valid, we require the notion of readiness 
+        to be consistent with the preemption model: a non-preemptive job remains
+        ready until (at least) the end of its current non-preemptive section. *)
+    Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule.
 
     (** Given such a valid preemption model, we establish that the generated
         schedule indeed respects the preemption model semantics. *)
@@ -233,7 +293,7 @@ Section NPUniprocessorScheduler.
       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).
+      elim => [| t' IH];[by rewrite service0=>ARR /negP ?;move:(H_valid_preemption_function j ARR)|].
       move=> ARR NP.
       have: scheduled_at schedule j t'.
       { apply contraT => NOT_SCHED.
@@ -242,8 +302,12 @@ Section NPUniprocessorScheduler.
         by 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.
+      rewrite /prev_job_nonpreemptive SCHED.
+      rewrite (identical_prefix_service _ schedule); last by apply schedule_up_to_identical_prefix.
+      apply /andP; split => //.
+      rewrite (H_nonclairvoyant_job_readiness _ schedule _ t'.+1) //.
+      - by apply H_valid_preemption_behavior.
+      - by apply schedule_up_to_identical_prefix.
     Qed.
 
   End PreemptionCompliance.

implementation/facts/ideal_uni/prio_aware.v

@@ -19,12 +19,11 @@ Section PrioAwareUniprocessorScheduler.
   Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.
 
   (** ... a non-clairvoyant readiness model, ... *)
-  Context {RM: JobReady Job (ideal.processor_state Job)}.
+  Context {RM : JobReady Job (ideal.processor_state Job)}.
   Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.
 
-  (** ... a preemption model that is consistent with the readiness model, ... *)
-  Context `{JobPreemptable Job}.
-  Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM.
+  (** ... a preemption model, ... *)
+  Context `{JobPreemptable Job}.      
 
   (** ... and reflexive, total, and transitive JLDP priority policy. *)
   Context `{JLDP : JLDP_policy Job}.
@@ -33,9 +32,14 @@ Section PrioAwareUniprocessorScheduler.
   Hypothesis H_transitive: transitive_priorities.
 
   (** Consider the schedule generated by the preemption-policy- and
-      priority-aware ideal uniprocessor scheduler. *)
+      priority-aware ideal uniprocessor scheduler... *)
   Let schedule := uni_schedule arr_seq.
 
+  (** ...and assume that the preemption model is consistent with the 
+      readiness model. *)
+  Hypothesis H_valid_preemption_behavior:
+    valid_nonpreemptive_readiness RM schedule.
+
   (** First, we note that the priority-aware job selection policy obviously
      maintains work-conservation. *)
   Corollary uni_schedule_work_conserving:
@@ -54,7 +58,7 @@ Section PrioAwareUniprocessorScheduler.
   Proof.
     apply np_schedule_valid => //.
     move=> t jobs j.
-    now apply supremum_in.
+    by apply supremum_in.
   Qed.
 
   (** Third, the schedule respects also the preemption model semantics. *)
@@ -77,7 +81,7 @@ Section PrioAwareUniprocessorScheduler.
     Qed.
 
   End PreemptionCompliance.
-
+  
   (** Now we proceed to the main property of the priority-aware scheduler: in
       the following section we establish that [uni_schedule arr_seq] is
       compliant with the given priority policy whenever jobs are
@@ -88,9 +92,7 @@ Section PrioAwareUniprocessorScheduler.
         policy and a prefix of the schedule based on which the next decision is
         made. *)
     Let policy := allocation_at arr_seq choose_highest_prio_job.
-    Let prefix t := if t is t'.+1
-                    then schedule_up_to policy idle_state t'
-                    else empty_schedule idle_state.
+    Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.
 
     (** To start, we observe that, at preemption times, the scheduled job is a
         supremum w.r.t. to the priority order and the set of backlogged
@@ -120,7 +122,7 @@ Section PrioAwareUniprocessorScheduler.
       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. }
+        by apply H_reflexive_priorities. }
       { move: BACK_j1.
         have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.
         { apply backlogged_prefix_invariance' with (h := t) => //.
@@ -139,3 +141,4 @@ Section PrioAwareUniprocessorScheduler.
   End Priority.
 
 End PrioAwareUniprocessorScheduler.
+