Remove hardcoded ideal processor model from aRTA

analysis/abstract/abstract_rta.v

@@ -23,14 +23,20 @@ Section Abstract_RTA.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
   Context `{JobPreemptable Job}.
+
+  (** Consider any kind of uni-service ideal processor state model. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
+  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.  
   
   (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
   Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-
-  (** Next, consider any uni-processor schedule of this arrival sequence...*)
-  Variable sched : schedule (ideal.processor_state Job).
+  
+  (** Next, consider any schedule of this arrival sequence...*)
+  Variable sched : schedule PState.
   Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
   
   (** ... where jobs do not execute before their arrival nor after completion. *) 
@@ -260,9 +266,9 @@ Section Abstract_RTA.
             move: H_busy_interval => [[/andP [GT LT] _] _].
             have ESERV :=
               @j_receives_at_least_run_to_completion_threshold
-                _ _ H1 H2 H3 arr_seq sched tsk interference interfering_workload
+                _ _ H1 H2 H3 PState H5 _ _  arr_seq sched tsk interference interfering_workload
                 _ j _ _ _ t1 t2 _ (job_run_to_completion_threshold j) _ ((A + F) - optimism). 
-            feed_n 5 ESERV; eauto 2.
+            feed_n 7 ESERV; eauto 2.
             specialize (ESERV H3 H4).
             feed_n 2 ESERV.
             { eapply job_run_to_completion_threshold_le_job_cost; eauto. }
@@ -489,9 +495,9 @@ Section Abstract_RTA.
           simpl in IB; rewrite H_equivalent in IB; last by apply ltn_trans with A.
           have ESERV :=
             @j_receives_at_least_run_to_completion_threshold
-              _ _ H1 H2 H3 arr_seq sched tsk
+              _ _ H1 H2 H3 PState H5 _ _ arr_seq sched tsk
               interference interfering_workload _ j _ _ _ t1 t2 _ (job_run_to_completion_threshold j) _ (A_sp + F_sp). 
-          feed_n 5 ESERV; eauto 2.
+          feed_n 7 ESERV; eauto 2.
           specialize (ESERV H3 H4).
           feed_n 2 ESERV; eauto using job_run_to_completion_threshold_le_job_cost.
             by rewrite {2}H_Asp_Fsp_fixpoint leq_add //; apply H_valid_run_to_completion_threshold.
@@ -541,4 +547,4 @@ Section Abstract_RTA.
                    with (j := j) (t1 := t1) (t2 := t2) (A_sp := A1) (F_sp := F1); auto.
   Qed.
 
-End Abstract_RTA.  
+End Abstract_RTA. 

analysis/abstract/abstract_seq_rta.v

@@ -683,6 +683,8 @@ Section Sequential_Abstract_RTA.
           (interference_bound_function :=
              fun tsk A R => task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A R)
           (interfering_workload0 := interfering_workload); eauto 2.
+      apply ideal_proc_model_ensures_ideal_progress.
+      apply ideal_proc_model_provides_unit_service.
       { clear ARR TSK H_R_is_maximum_seq R j.
         intros t1 t2 R j BUSY NEQ ARR TSK COMPL.
         move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].

analysis/abstract/definitions.v

@@ -21,11 +21,15 @@ Section AbstractRTADefinitions.
     Context `{JobArrival Job}.
     Context `{JobCost Job}.
 
+    (** Consider any kind of processor state model. *)
+    Context {PState : Type}.
+    Context `{ProcessorState Job PState}.
+    
     (** Consider any arrival sequence... *) 
     Variable arr_seq : arrival_sequence Job.
 
-    (** ... and any ideal uni-processor schedule of this arrival sequence. *)
-    Variable sched : schedule (ideal.processor_state Job).
+    (** ... and any schedule of this arrival sequence. *)
+    Variable sched : schedule PState.
 
     (** Let [tsk] be any task that is to be analyzed *)
     Variable tsk : Task.
@@ -218,4 +222,4 @@ Section AbstractRTADefinitions.
 
   End Definitions.
 
-End AbstractRTADefinitions.
\ No newline at end of file
+End AbstractRTADefinitions.

analysis/abstract/run_to_completion.v

@@ -27,12 +27,18 @@ Section AbstractRTARunToCompletionThreshold.
      mapping jobs to their preemption points. *)
   Context `{JobPreemptable Job}.
 
-  (** Consider any arrival sequence with consistent arrivals... *)
+  (** Consider any kind of uni-service ideal processor state model. *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
+  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-
-  (** Next, consider any ideal uni-processor schedule of this arrival sequence. *)
-  Variable sched : schedule (ideal.processor_state Job).
+  
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
 
   (** Assume that the job costs are no larger than the task costs. *)
   Hypothesis H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq.
@@ -99,10 +105,14 @@ Section AbstractRTARunToCompletionThreshold.
       move: (H_work_conserving j t1 t2 x) => Workj.
       feed_n 5 Workj; try done.
       { by apply/andP; split; eapply leq_trans; eauto 2. }
-      rewrite -/(service_at sched j x) service_at_is_scheduled_at.
-      have->: scheduled_at sched j x = ~~ interference j x.
-      { by apply/idP/negP; intuition. }
-      exact: addn_negb.
+      destruct interference.
+      - replace (service_in _ _) with 0; auto; symmetry.
+        apply no_service_not_scheduled; auto.
+        now apply/negP; intros SCHED; apply Workj in SCHED; apply SCHED.
+      - replace (service_in _ _) with 1; auto; symmetry.
+        apply/eqP; rewrite eqn_leq; apply/andP; split.
+        + apply H_unit_service_proc_model.
+        + now apply H_ideal_progress_proc_model, Workj.
     Qed.
 
   End InterferenceIsComplement.
@@ -188,11 +198,10 @@ Section AbstractRTARunToCompletionThreshold.
         rewrite big_nat_cond [in X in _ <= X]big_nat_cond.
         rewrite leq_sum //.
         move => t' /andP [NEQ _].
-        rewrite service_at_is_scheduled_at.
-          by rewrite lt0b; apply SCHED; rewrite addn1 addnS ltnS in NEQ.
+        apply H_ideal_progress_proc_model; apply SCHED.
+          by rewrite addn1 addnS ltnS in NEQ.
       }
-      eapply service_at_most_cost with (j0 := j) (t0 := t + job_last.+1) in H_completed_jobs_dont_execute; last first.
-      { by apply ideal_proc_model_provides_unit_service. }
+      eapply service_at_most_cost with (j0 := j) (t0 := t + job_last.+1) in H_completed_jobs_dont_execute; auto.
       move: H_completed_jobs_dont_execute; rewrite leqNgt; move => /negP T; apply: T.
       rewrite /service -(service_during_cat _ _ _ t); last by (apply/andP; split; last rewrite leq_addr).
       apply leq_trans with (job_run_to_completion_threshold j + service_during sched j t (t + job_last.+1));