Latest changes

BertognaResponseTimeDefs.v

 Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
                PlatformDefs WorkloadDefs SchedulabilityDefs PriorityDefs
                ResponseTimeDefs divround helper
-               ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+               ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
 
 Module ResponseTimeAnalysis.
 
-  Import SporadicTaskset Schedule Workload Schedulability ResponseTime Priority.
+  Import Job SporadicTaskset Schedule Workload Schedulability ResponseTime Priority SporadicTaskArrival.
 
+  Section TaskInterference.
+
+    Context {Job: eqType}.
+    Variable job_cost: Job -> nat.
+    Variable job_task: Job -> sporadic_task.
+    Context {arr_seq: arrival_sequence Job}.
+
+    Context {num_cpus: nat}.
+    Variable rate: Job -> processor num_cpus -> nat.
+    Variable sched: schedule num_cpus arr_seq.
+
+    Variable j: JobIn arr_seq.
+    Variable t1 delta: time.
+
+    (*Definition total_interference :=
+      delta - service_during rate sched j t1 (t1 + delta).*)
+
+    Variable tsk: sporadic_task.
+    
+    Definition job_is_backlogged (t: time) :=
+      backlogged job_cost rate sched j t.
+
+    Definition has_job_of_tsk (cpu: processor num_cpus) (t: time) :=
+      match (sched cpu t) with
+        | Some j' => job_task j' == tsk
+        | None => false
+      end.
+    
+    Definition tsk_is_scheduled (t: time) :=
+      [exists cpu in processor num_cpus, has_job_of_tsk cpu t].
+    
+    Definition task_interference :=
+      \sum_(t1 <= t < t1 + delta)
+        (job_is_backlogged t && tsk_is_scheduled t).
+
+  End TaskInterference.
+  
   Section InterferenceBound.
 
+    (* Let tsk \in ts be the task to be analyzed. *)
     Variable ts: sporadic_taskset.
     Variable tsk: sporadic_task.
 
-    (* Given a known response-time bound for each interfering task ... *)
+    (* Assume a known response-time bound for each interfering task ... *)
     Variable R_other: sporadic_task -> time.
-    (* ... and an interval length delta, ... *)
+    (* ... and an interval length delta. *)
     Variable delta: time.
 
+    (* Based on Bertogna and Cirinei's workload bound, ... *)
     Definition workload_bound (tsk_other: sporadic_task) :=
       W tsk_other (R_other tsk_other) delta.
     
-    (* the interference incurred by tsk due to tsk_other is bounded by the
-       workload of tsk_other. *)
-    Definition interference_caused_by (tsk_other: sporadic_task) :=
-      if tsk_other != tsk then
-        workload_bound tsk_other
-      else 0.
-    
-    (* Then, Bertogna and Cirinei define two interference bounds: one for FP and another
-       for JLFP scheduling. *)
+    (* ... we define interference bounds for FP and JLFP scheduling. *)
+    Definition interference_bound (tsk_other: sporadic_task) :=
+      minn (workload_bound tsk_other) (delta - (task_cost tsk) + 1).
+
     Section InterferenceFP.
 
+      (* Assume an FP policy. *)
       Variable higher_eq_priority: fp_policy.
 
-      Definition is_interfering_task :=
-        fun tsk_other => higher_eq_priority tsk_other tsk.
-      
-      (* Under FP scheduling, only the higher-priority tasks cause interference.
-         The total interference incurred by tsk is bounded by: *)
+      (* Under FP scheduling, lower-priority tasks do not cause interference. *)
+      Let interference_caused_by (tsk_other: sporadic_task) :=
+        if (higher_eq_priority tsk_other tsk) && (tsk_other != tsk) then
+          interference_bound tsk_other
+        else 0.
+          
+      (* The total interference incurred by tsk is thus bounded by: *)
       Definition total_interference_fp :=
-        \sum_(tsk_other <- ts | is_interfering_task tsk_other)
+        \sum_(tsk_other <- ts)
            interference_caused_by tsk_other.
   
     End InterferenceFP.
 
     Section InterferenceJLFP.
+
+      (* Under JLFP scheduling, all the other tasks may cause interference. *)
+      Let interference_caused_by (tsk_other: sporadic_task) :=
+        if tsk_other != tsk then
+          interference_bound tsk_other
+        else 0.
       
-      (* Under JLFP scheduling, every task other than tsk can cause interference.
-         The total interference incurred by tsk is bounded by: *)
+      (* The total interference incurred by tsk is thus bounded by: *)
       Definition total_interference_jlfp :=
         \sum_(tsk_other <- ts)
            interference_caused_by tsk_other.
@@ -64,12 +106,32 @@ Module ResponseTimeAnalysis.
     Variable job_task: Job -> sporadic_task.
     
     Context {arr_seq: arrival_sequence Job}.
-  
+
+    Hypothesis sporadic_tasks: sporadic_task_model arr_seq job_task.
+    
     Variable num_cpus: nat.
     Variable rate: Job -> processor num_cpus -> nat.
     Variable sched: schedule num_cpus arr_seq.
 
+    Hypothesis H_jobs_must_arrive_to_execute:
+      jobs_must_arrive_to_execute sched.
+    Hypothesis H_completed_jobs_dont_execute:
+      completed_jobs_dont_execute job_cost rate sched.
+
+    Hypothesis H_no_parallelism:
+      jobs_dont_execute_in_parallel sched.
+    Hypothesis H_rate_equals_one :
+      forall j cpu, rate j cpu = 1.
+    
     Variable ts: sporadic_taskset.
+    Hypothesis H_valid_task_parameters: valid_sporadic_taskset ts.
+    Hypothesis H_valid_job_parameters:
+      forall (j: JobIn arr_seq),
+        (valid_sporadic_task_job job_cost job_deadline job_task) j.
+
+    Hypothesis H_restricted_deadlines:
+      forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
+    
     Variable tsk: sporadic_task.
     Hypothesis task_in_ts: tsk \in ts.
 
@@ -85,32 +147,122 @@ Module ResponseTimeAnalysis.
 
       Variable higher_eq_priority: fp_policy.
 
-      Hypothesis response_time_of_interfering_tasks_is_known:
+      Definition is_interfering_task (tsk_other: sporadic_task) :=
+        tsk_other \in ts /\
+        tsk_other != tsk /\
+        higher_eq_priority tsk_other tsk.
+
+      Hypothesis H_response_time_of_interfering_tasks_is_known:
+        forall tsk_other job_cost,
+          is_interfering_task tsk_other ->
+          is_response_time_bound_of_task job_cost job_task tsk_other rate sched (R_other tsk_other).
+
+      Hypothesis H_interfering_tasks_miss_no_deadlines:
         forall tsk_other,
-          tsk_other \in ts -> (* --> ugly, convert this to some predicate *)
-          tsk_other != tsk ->
-          higher_eq_priority tsk_other tsk ->
-          is_response_time_bound tsk_other (R_other tsk_other).
+          is_interfering_task tsk_other ->
+          task_misses_no_deadline job_cost job_deadline job_task rate sched tsk_other.
 
       (* Bertogna and Cirinei's response-time bound recurrence *)
       Definition response_time_recurrence_fp R :=
-        R <= task_cost tsk + div_floor
+        R = task_cost tsk + div_floor
                                (total_interference_fp ts tsk R_other R higher_eq_priority)
                                num_cpus.
 
       Variable R: time.
 
-      Hypothesis response_time_recurrence_holds:
+      Hypothesis H_response_time_recurrence_holds:
         response_time_recurrence_fp R.
 
-      Hypothesis response_time_no_larger_than_deadline:
+      Hypothesis H_response_time_no_larger_than_deadline:
         R <= task_deadline tsk.
       
       Theorem bertogna_cirinei_response_time_bound_fp :
         is_response_time_bound tsk R.
       Proof.
-        unfold response_time_recurrence_fp; ins.      
-      Admitted.
+        unfold response_time_recurrence_fp,
+               is_response_time_bound, is_response_time_bound_of_task,
+               job_has_completed_by, completed,
+               completed_jobs_dont_execute,
+               valid_sporadic_task_job in *.
+        rename H_completed_jobs_dont_execute into COMP,
+               H_response_time_recurrence_holds into REC,
+               H_valid_job_parameters into PARAMS,
+               H_valid_task_parameters into TASK_PARAMS,
+               H_restricted_deadlines into RESTR,
+               H_response_time_of_interfering_tasks_is_known into RESP_OTHER,
+               H_interfering_tasks_miss_no_deadlines into NOMISS,
+               H_rate_equals_one into RATE.
+        intros j JOBtsk.
+        rewrite eqn_leq; apply/andP; split; first by apply COMP.
+        set X := R - service rate sched j (job_arrival j + R).
+        rewrite -(leq_add2l X).
+        unfold X; rewrite [R - _ + service _ _ _ _]subh1; last first.
+        
+        unfold service; rewrite service_before_arrival_eq_service_during; ins.
+        apply leq_trans with (\sum_(job_arrival j <= t < job_arrival j + R) 1); last by rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA // subnn addn0 leqnn.
+        by apply leq_sum; ins; apply service_at_le_max_rate; ins; rewrite RATE.
+
+        move: JOBtsk => /eqP JOBtsk.
+        rewrite -addnBA // subnn addn0.
+        fold X; rewrite REC.
+        apply leq_trans with (n := task_cost tsk + X);
+          first by specialize (PARAMS j); des; rewrite addnC leq_add2r -JOBtsk; apply PARAMS0.
+
+        rewrite leq_add2l.
+        set x := fun tsk_other =>
+          if higher_eq_priority tsk_other tsk && (tsk_other != tsk) then
+            task_interference job_cost job_task rate sched j
+                     (job_arrival j) R tsk_other
+          else 0.
+
+
+        apply leq_trans
+          with (n := div_floor
+                       (\sum_(k <- ts) minn (x k) (R - task_cost tsk + 1))
+                       num_cpus);
+          last first.
+        {
+          (* First show that the workload bound is an interference bound.*)
+          apply leq_div2r; unfold total_interference_fp, x.
+          rewrite big_seq_cond [\sum_(_ <- _ | true)_]big_seq_cond.
+          apply leq_sum; intro tsk_k; rewrite andbT; intro INk.
+          destruct (higher_eq_priority tsk_k tsk && (tsk_k != tsk)) eqn:OTHER;
+            last by rewrite min0n.
+          move: OTHER => /andP [HPother NEQother].
+          unfold interference_bound.
+          rewrite leq_min; apply/andP; split; last by apply geq_minr.
+          apply leq_trans with (n := task_interference job_cost job_task rate sched j (job_arrival j) R tsk_k); first by apply geq_minl.
+
+          apply leq_trans with (n := workload job_task rate sched tsk_k
+                                     (job_arrival j) (job_arrival j + R));
+            last by apply workload_bounded_by_W with (job_cost := job_cost)
+                                        (job_deadline := job_deadline); ins;
+              [ by rewrite RATE
+              | by apply TASK_PARAMS
+              | by apply RESTR
+              | by red; ins; red; apply RESP_OTHER
+              | by red; red; ins; apply NOMISS with (tsk_other := tsk_k);
+                      repeat split].
+
+          unfold task_interference, workload.
+          apply leq_sum; intros t _.
+          rewrite -mulnb -[\sum_(_ < _) _]mul1n.
+          apply leq_mul; first by apply leq_b1.
+          destruct (tsk_is_scheduled job_task sched tsk_k t) eqn:SCHED;
+            last by ins.
+          unfold tsk_is_scheduled in SCHED.
+          move: SCHED =>/exists_inP SCHED; destruct SCHED as [cpu _ HAScpu].
+          rewrite -> bigD1 with (j := cpu); simpl; last by ins.
+          apply ltn_addr.
+          unfold service_of_task, has_job_of_tsk in *.
+          by destruct (sched cpu t); [by rewrite HAScpu mul1n RATE|by ins].
+        }
+
+        {
+          (* Show that X <= 1/m * \sum_k min(x_k, delta - e_k + 1) *)
+          admit.
+        }
+      Qed.         
 
     End UnderFPScheduling.
 

ScheduleDefs.v

@@ -388,6 +388,15 @@ Module Schedule.
         by apply leq_trans with (n := t2); ins.
       Qed.
 
+      Lemma service_before_arrival_eq_service_during :
+        forall t0 t (LT: t0 <= job_arrival j),
+          \sum_(t0 <= t < job_arrival j + t) service_at rate sched j t =
+          \sum_(job_arrival j <= t < job_arrival j + t) service_at rate sched j t.
+      Proof.
+        ins; rewrite -> big_cat_nat with (n := job_arrival j); [| by ins | by apply leq_addr].
+        by rewrite /= sum_service_before_arrival; [by rewrite add0n | by apply leqnn].
+      Qed.
+      
     End Arrival.
 
   End ServiceProperties.

WorkloadDefs.v

@@ -107,7 +107,7 @@ Module Workload.
     Definition max_jobs :=
       div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).
 
-    (* Bertogna and Ciritnei's bound on the workload of a task in an interval of length delta *)
+    (* Bertogna and Cirinei's bound on the workload of a task in an interval of length delta *)
     Definition W :=
       let e_k := (task_cost tsk) in
       let d_k := (task_deadline tsk) in
@@ -123,11 +123,12 @@ Module Workload.
     Variable job_task: Job -> sporadic_task.
     Variable job_deadline: Job -> nat.
 
+    Variable arr_seq: arrival_sequence Job.
+
     (* Assume that all jobs have valid parameters *)
     Hypothesis jobs_have_valid_parameters :
-      forall j, valid_sporadic_task_job job_cost job_deadline job_task j.
-
-    Variable arr_seq: arrival_sequence Job.
+      forall (j: JobIn arr_seq),
+        valid_sporadic_task_job job_cost job_deadline job_task j.
     
     Variable num_cpus: nat.
     Variable rate: Job -> processor num_cpus -> nat.
@@ -200,7 +201,7 @@ Module Workload.
     Hypothesis no_deadline_misses_during_interval: no_deadline_misses_by tsk (t1 + delta).
 
     (* Then the workload of the task in the interval is bounded by W. *)
-    Theorem workload_bound :
+    Theorem workload_bounded_by_W :
       workload_of tsk t1 (t1 + delta) <= W tsk R_tsk delta.
     Proof.
       rename jobs_have_valid_parameters into job_properties,