Start response-time bound defs

BertognaResponseTimeDefs.v

+Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
+               PlatformDefs WorkloadDefs SchedulabilityDefs
+               ResponseTimeDefs divround helper
+               ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module ResponseTimeAnalysis.
+
+  Import SporadicTaskset Schedule Workload Schedulability ResponseTime.
+
+  Section Interference.
+
+    Variable ts: sporadic_taskset.
+    Variable tsk: sporadic_task.
+
+    Variable delta: time.
+    
+    (* Interference caused by tsk due to tsk_other *)
+    Definition interference_incurred_by (tsk tsk_other: sporadic_task) :=
+      delta.
+          
+    Definition total_interference :=
+      \sum_(tsk_other <- ts)
+         (interference_incurred_by tsk) tsk_other.
+
+  End Interference.
+  
+  Section ResponseTimeBound.
+    
+    Context {Job: eqType}.
+    Variable job_cost: Job -> nat.
+    Variable job_deadline: Job -> nat.
+    Variable job_task: Job -> sporadic_task.
+    
+    Context {arr_seq: arrival_sequence Job}.
+  
+    Variable num_cpus: nat.
+    Variable rate: Job -> processor num_cpus -> nat.
+    Variable sched: schedule num_cpus arr_seq.
+
+    Variable ts: sporadic_taskset.
+    Variable tsk: sporadic_task.
+    Hypothesis task_in_ts: tsk \in ts.
+
+    (* Bertogna and Cirinei's response-time bound recurrence *)
+    Definition response_time_recurrence R :=
+      R <= task_cost tsk + div_floor
+                             (total_interference ts tsk R)
+                             num_cpus.
+
+    Definition no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
+      task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
+
+    Definition response_time_bounded_by :=
+      is_response_time_bound_of_task job_cost job_task tsk rate sched.
+    
+    Theorem bertogna_cirinei_response_time_bound :
+      forall R,
+        response_time_recurrence R ->
+        R <= task_deadline tsk ->
+        response_time_bounded_by R.
+    Proof.
+      Admitted.
+    
+  End ResponseTimeBound.
+  
+End ResponseTimeAnalysis.
\ No newline at end of file

ResponseTimeDefs.v

-Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs PlatformDefs helper
-                ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
+               PlatformDefs WorkloadDefs helper
+               ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module ResponseTime.
 
@@ -176,118 +177,4 @@ Module ResponseTime.
 
   End LowerBoundOfResponseTimeBound.
     
-End ResponseTime.
-
-
-
-  (*Section Schedule.
-
-    Require Import ScheduleDefs.
-    Import SporadicTaskset Schedule.
-    
-    Record MyJob :=
-    {
-      myjob_index : nat;
-      myjob_cost: nat;
-      myjob_deadline: nat;
-      myjob_task: sporadic_task               
-    }.
-
-    Definition my_ts := [ :: (3, 5, 5) ; (5, 10, 10)].
-    Definition nth_elem x := nth (0,0,0) my_ts x.
-    
-    Definition create_sync_arrival (ts: sporadic_taskset) :=
-      fun t =>
-        if t == 0 then
-          map (fun x => Build_MyJob
-                        x
-                        (task_cost (nth_elem x))
-                        (task_deadline (nth_elem x))
-                        (nth_elem x))
-              (iota 0 (size my_ts))
-        else [::].
-
-    Check (create_sync_arrival my_ts).
-
-
-    
-    Definition my_cost (j: my_Job) :=
-      if j == j1 then 2
-      else if j == j2 then 4
-      else 0.
-
-    Definition my_deadline (j: my_Job) :=
-      if j == j1 then 5
-      else if j == j2 then 10
-      else 0.
-
-    End bla3.*)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-  
-     (* Problems:
-         1) We cannot create a set of jobs with only j.
-            If there are other jobs, how do we define the schedule
-            function for them?
-            If we only schedule j, this schedule won't be work-conserving
-            for the other jobs.
- 
-        2) The schedule function has to satisfy all the constraints
-           specified by its platform (e.g. affinities). Otherwise, we need
-           to prove one lemma for each platform.
-            
-           We can avoid constructing the schedule if we have this:
-
-           Defininition valid_platform (plat: platform):
-             for every arrival sequence,
-               exists schedule that satisfies the constraints
-               of the platform.
-
-           That is to be proved for each platform.
-
-      *)
-
-
-
-
-
-
-
-
-
-
-(*
-
-forall jobsets, forall tasks, forall sched, forall R, R is bertogna bound,
-           then forall j response time of j <= R.
-
-forall tasksets, forall R, R is solution of Bertogna's equation,
-               forall arrival sequence, forall sched, forall j,
-                                                 resp j <= R.
-
-*)
\ No newline at end of file
+End ResponseTime.
\ No newline at end of file

helper.v

@@ -47,19 +47,17 @@ Proof.
 Qed.
 
 Definition fun_ord_to_nat {n} {T} (x0: T) (f: 'I_n -> T) : nat -> T.
-(* if x < n, return the Ordinal time x: 'I_n, else return default x0. *)
+(* if x < n, apply the function f in the (Ordinal x: 'I_n), else return default x0. *)
   intro x; destruct (x < n) eqn:LT;
     [by apply (f (Ordinal LT)) | by apply x0].
 Defined.
 
 (* For all x: 'I_n (i.e., x < n), the conversion preserves equality. *)
 Lemma eq_fun_ord_to_nat :
-  forall n T x0 (f: 'I_n -> T) (x: 'I_n),
+  forall n {T: eqType} x0 (f: 'I_n -> T) (x: 'I_n),
     (fun_ord_to_nat x0 f) x = f x.
 Proof.
-  unfold fun_ord_to_nat; ins.
-  have LT := ltn_ord x.
-  Require Import Coq.Program.Equality.
+  
 Admitted.
 
 Lemma eq_bigr_ord T n op idx r (P : pred 'I_n)