Clean-up workload definitions

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_fp.v workload_guan.v workload_jitter.v workload.v 
+# coq_makefile arrival_sequence.v bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_bound.v workload_guan.v workload_jitter.v workload.v 
 #
 
 .DEFAULT_GOAL := all
@@ -80,7 +80,8 @@ endif
 #                    #
 ######################
 
-VFILES:=bertogna_edf_comp.v\
+VFILES:=arrival_sequence.v\
+  bertogna_edf_comp.v\
   bertogna_edf_theory.v\
   bertogna_fp_comp.v\
   bertogna_fp_jitter_comp.v\
@@ -103,7 +104,7 @@ VFILES:=bertogna_edf_comp.v\
   util_divround.v\
   util_lemmas.v\
   Vbase.v\
-  workload_fp.v\
+  workload_bound.v\
   workload_guan.v\
   workload_jitter.v\
   workload.v

bertogna_edf_comp.v

 Require Import Vbase schedule bertogna_edf_theory util_divround util_lemmas
         ssreflect ssrbool eqtype ssrnat seq fintype bigop div path
-        workload_fp.
+        workload_bound.
 
 Module ResponseTimeIterationEDF.
 
-  Import Schedule ResponseTimeAnalysisEDF WorkloadBoundFP.
+  Import Schedule ResponseTimeAnalysisEDF WorkloadBound.
 
   Section Analysis.
     

bertogna_edf_theory.v

 Require Import Vbase task job task_arrival schedule platform
-        workload workload_fp schedulability priority response_time
+        workload workload_bound schedulability priority response_time
         bertogna_fp_theory util_divround util_lemmas
         ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
 
-  Export Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime Priority SporadicTaskArrival ResponseTimeAnalysis WorkloadBoundFP.
+  Export Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
+         Priority SporadicTaskArrival ResponseTimeAnalysis WorkloadBound.
 
   Section InterferenceBoundEDF.
 

bertogna_fp_comp.v

 Require Import Vbase schedule bertogna_fp_theory util_divround util_lemmas
         ssreflect ssrbool eqtype ssrnat seq fintype bigop div path
-        workload_fp.
+        workload_bound.
 
 Module ResponseTimeIterationFP.
 
-  Import Schedule ResponseTimeAnalysis WorkloadBoundFP.
+  Import Schedule ResponseTimeAnalysis WorkloadBound.
 
   Section Analysis.
     

bertogna_fp_theory.v

-Require Import Vbase task job task_arrival schedule platform workload workload_fp
+Require Import Vbase task job task_arrival schedule platform workload workload_bound
                schedulability priority response_time interference
                util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
 
 Module ResponseTimeAnalysis.
 
-  Export Job SporadicTaskset Schedule Workload Interference Platform Schedulability ResponseTime Priority SporadicTaskArrival WorkloadBoundFP.
+  Export Job SporadicTaskset Schedule Workload Interference Platform Schedulability
+         ResponseTime Priority SporadicTaskArrival WorkloadBound.
   
   Section InterferenceBoundFP.
 

workload.v

@@ -36,8 +36,7 @@ Module Workload.
       \sum_(t1 <= t < t2)
         \sum_(cpu < num_cpus)
           service_of_task cpu (sched cpu t).
-
-    
+ 
     (* Now, we define workload by summing up the cumulative service
        during [t1,t2) of the scheduled jobs, but only those spawned
        by the task that we care about. *)
@@ -45,74 +44,6 @@ Module Workload.
       \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk)
         service_during rate sched j t1 t2.
 
-    (* ??? *)
-    Lemma scheduled_between_helper :
-      forall j t,
-        (forall cpu t, rate cpu t > 0) ->
-        (j \in \big[cat/[::]]_(cpu < num_cpus) make_sequence (sched cpu t))
-          = (service_at rate sched j t != 0).
-    Proof.
-      unfold service_at; intros j t RATE.
-      rewrite [\sum_(_ < _ | _) _]big_mkcond.
-      destruct num_cpus; first by rewrite 2!big_ord0 in_nil.
-      assert (LT0: 0 < n.+1); first by done.
-      rewrite 2!(big_nth (Ordinal LT0)).
-      set m := size (index_enum (ordinal_finType n.+1)).
-      induction m; first by rewrite big_geq // big_geq //.
-      {
-        rewrite big_nat_recr; last by done.
-        rewrite big_nat_recr; last by done.
-        rewrite mem_cat IHm.
-        destruct ( (j
-         \in make_sequence
-               (sched
-                  (nth (Ordinal (n:=n.+1) (m:=0) LT0)
-                       (index_enum (ordinal_finType n.+1)) m) t))) eqn: SUBST.
-        {
-          rewrite orbT.
-          unfold make_sequence in SUBST.
-          destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m) t); last by done.
-          rewrite mem_seq1 in SUBST.
-          move: SUBST => /eqP SUBST; subst.
-          rewrite eq_refl.
-          symmetry; rewrite -lt0n.
-          apply leq_trans with (0 + 1); first by done.
-          apply leq_add; first by done.
-          by rewrite RATE.
-        }
-        {
-          unfold make_sequence in SUBST.
-          destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m ) t);
-            last by desf; rewrite orbF /= addn0.
-          {
-            rewrite mem_seq1 in SUBST.
-            destruct (Some j0 == Some j) eqn:SOME;
-              last by rewrite SOME orbF /= addn0.
-            move: SOME SUBST => /eqP SOME /eqP SUBST; inversion SOME.
-            by rewrite H0 in SUBST.
-          }
-        }
-      }
-    Qed.
-
-    (* If a job i scheduled in an time interval, it will get service in this interval. *)
-    Lemma scheduled_between_implies_service :
-      forall j t1 t2,
-        (forall j cpu, rate j cpu > 0) ->
-        (j \in jobs_scheduled_between sched t1 t2) =
-        (service_during rate sched j t1 t2 != 0).
-    Proof.
-      intros j t1 t2 RATE; unfold service_during; rewrite mem_undup.
-      induction t2;
-        first by rewrite 2?big_geq //.      
-      destruct (leqP t1 t2) as [LE | GT]; last by rewrite 2?big_geq //.
-      unfold service_during; rewrite 2?big_nat_recr ?mem_cat /= //.
-      rewrite IHt2.
-      destruct (\sum_(t1 <= t < t2) service_at rate sched j t);
-        last by done.
-      rewrite eq_refl orFb add0n.
-      by apply scheduled_between_helper, RATE.
-    Qed.
 
     (* Next, we show that the two definitions are equivalent. *)
     Lemma workload_eq_workload_joblist :

workload_fp.v → workload_bound.v

@@ -2,9 +2,11 @@ Require Import workload Vbase job task schedule task_arrival response_time
                schedulability util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
 
-Module WorkloadBoundFP.
- Import Job SporadicTaskset ScheduleOfSporadicTask SporadicTaskArrival ResponseTime Schedulability Workload.
-  Section WorkloadBound.
+Module WorkloadBound.
+  
+  Import Job SporadicTaskset ScheduleOfSporadicTask SporadicTaskArrival ResponseTime Schedulability Workload.
+
+  Section WorkloadBoundDef.
 
     Context {sporadic_task: eqType}.
     Variable task_cost: sporadic_task -> nat.
@@ -24,7 +26,7 @@ Module WorkloadBoundFP.
       let p_k := (task_period tsk) in            
         minn e_k (delta + R_tsk - e_k - max_jobs * p_k) + max_jobs * e_k.
 
-  End WorkloadBound.
+  End WorkloadBoundDef.
   
   Section BasicLemmas.
 
@@ -241,8 +243,8 @@ Module WorkloadBoundFP.
         Lemma workload_bound_simpl_by_sorting_interfering_jobs :
           \sum_(i <- interfering_jobs) service_during rate sched i t1 t2 =
            \sum_(i <- sorted_jobs) service_during rate sched i t1 t2.
-          Proof.
-            by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort order).
+        Proof.
+          by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort order).
         Qed.
 
         (* Remember that both sequences have the same set of elements *)
@@ -790,4 +792,4 @@ Module WorkloadBoundFP.
     
   End ProofWorkloadBound.
 
-End WorkloadBoundFP.
\ No newline at end of file
+End WorkloadBound.
\ No newline at end of file

workload_guan.v

@@ -258,8 +258,77 @@ Module WorkloadBoundGuan.
       job_task j = tsk ->
       job_arrival j + R_tsk < t1 + delta ->
       job_has_completed_by j (job_arrival j + R_tsk).
-   
-   Section GuanNoCarry.
+
+    (* If a job i scheduled in an time interval, it will get service in this interval. *)
+    (*Lemma scheduled_between_implies_service :
+      forall j t1 t2,
+        (forall j cpu, rate j cpu > 0) ->
+        (j \in jobs_scheduled_between sched t1 t2) =
+        (service_during rate sched j t1 t2 != 0).
+    Proof.
+      intros j t1 t2 RATE; unfold service_during; rewrite mem_undup.
+      induction t2;
+        first by rewrite 2?big_geq //.      
+      destruct (leqP t1 t2) as [LE | GT]; last by rewrite 2?big_geq //.
+      unfold service_during; rewrite 2?big_nat_recr ?mem_cat /= //.
+      rewrite IHt2.
+      destruct (\sum_(t1 <= t < t2) service_at rate sched j t);
+        last by done.
+      rewrite eq_refl orFb add0n.
+      by apply scheduled_between_helper, RATE.
+    Qed.*)
+
+        (* ??? *)
+    (*Lemma scheduled_between_helper :
+      forall j t,
+        (forall cpu t, rate cpu t > 0) ->
+        (j \in \big[cat/[::]]_(cpu < num_cpus) make_sequence (sched cpu t))
+          = (service_at rate sched j t != 0).
+    Proof.
+      unfold service_at; intros j t RATE.
+      rewrite [\sum_(_ < _ | _) _]big_mkcond.
+      destruct num_cpus; first by rewrite 2!big_ord0 in_nil.
+      assert (LT0: 0 < n.+1); first by done.
+      rewrite 2!(big_nth (Ordinal LT0)).
+      set m := size (index_enum (ordinal_finType n.+1)).
+      induction m; first by rewrite big_geq // big_geq //.
+      {
+        rewrite big_nat_recr; last by done.
+        rewrite big_nat_recr; last by done.
+        rewrite mem_cat IHm.
+        destruct ( (j
+         \in make_sequence
+               (sched
+                  (nth (Ordinal (n:=n.+1) (m:=0) LT0)
+                       (index_enum (ordinal_finType n.+1)) m) t))) eqn: SUBST.
+        {
+          rewrite orbT.
+          unfold make_sequence in SUBST.
+          destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m) t); last by done.
+          rewrite mem_seq1 in SUBST.
+          move: SUBST => /eqP SUBST; subst.
+          rewrite eq_refl.
+          symmetry; rewrite -lt0n.
+          apply leq_trans with (0 + 1); first by done.
+          apply leq_add; first by done.
+          by rewrite RATE.
+        }
+        {
+          unfold make_sequence in SUBST.
+          destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m ) t);
+            last by desf; rewrite orbF /= addn0.
+          {
+            rewrite mem_seq1 in SUBST.
+            destruct (Some j0 == Some j) eqn:SOME;
+              last by rewrite SOME orbF /= addn0.
+            move: SOME SUBST => /eqP SOME /eqP SUBST; inversion SOME.
+            by rewrite H0 in SUBST.
+          }
+        }
+      }
+    Qed.*)
+
+   (*Section GuanNoCarry.
        
       Let is_carry_in_job := carried_in job_cost rate sched.
 
@@ -1032,7 +1101,7 @@ Module WorkloadBoundGuan.
         admit.
       Qed.
 
-   End GuanCarry.
+   End GuanCarry.*)
    
   End ProofWorkloadBound.