Working on W_CI

WorkloadDefs.v

@@ -1208,16 +1208,366 @@ Module Workload.
 
       Let is_carry_in_job := carried_in job_cost rate sched.
 
-      Hypothesis H_no_carry_in:
+      (* Assume that task tsk has a carry-in job in the interval. *)
+      Hypothesis H_has_carry_in:
         exists (j: JobIn arr_seq),
           job_task j = tsk /\ is_carry_in_job j t1.
 
       Let workload_bound := W_CI task_cost task_period.
-    
+
+      (* Then, according to Guan et al.'s schedulability analysis,
+         the workload of tsk is bounded by W_CI. *)
       Theorem workload_bounded_by_W_CI :
         workload_of tsk t1 (t1 + delta) <= workload_bound tsk R_tsk delta.
       Proof.
+        rename jobs_have_valid_parameters into job_properties,
+               no_deadline_misses_during_interval into no_dl_misses,
+               valid_task_parameters into task_properties,
+               H_completed_jobs_dont_execute into COMP.
+        unfold valid_sporadic_job, valid_realtime_job, restricted_deadline_model,
+               valid_sporadic_taskset, is_valid_sporadic_task, sporadic_task_model,
+               workload_of, response_time_bound_of, no_deadline_misses_by,
+               workload_bound, W_CI in *; ins; des.
+
+        (* Simplify names *)
+        set t2 := t1 + delta.
+        set n_k := max_jobs_CI task_cost task_period tsk delta.
+
+        (* Use the definition of workload based on list of jobs. *)
+        rewrite workload_eq_workload_joblist; unfold workload_joblist.
+        
+        (* Identify the subset of jobs that actually cause interference *)
+        set interfering_jobs :=
+          filter (fun (x: JobIn arr_seq) =>
+                    (job_task x == tsk) && (service_during rate sched x t1 t2 != 0))
+                      (jobs_scheduled_between sched t1 t2).
+    
+        (* Remove the elements that we don't care about from the sum *)
+        assert (SIMPL:
+          \sum_(i <- jobs_scheduled_between sched t1 t2 | job_task i == tsk)
+             service_during rate sched i t1 t2 =
+          \sum_(i <- interfering_jobs) service_during rate sched i t1 t2).
+        {
+          unfold interfering_jobs.
+          rewrite (bigID (fun x => service_during rate sched x t1 t2 == 0)) /=.
+          rewrite (eq_bigr (fun x => 0)); last by move => j_i /andP JOBi; des; apply /eqP.
+          rewrite big_const_seq iter_addn mul0n add0n add0n.
+          by rewrite big_filter.
+        } rewrite SIMPL; clear SIMPL.
+
+        (* Remember that for any job of tsk, service <= task_cost tsk *)
+        assert (LTserv: forall j_i (INi: j_i \in interfering_jobs),
+                          service_during rate sched j_i t1 t2 <= task_cost tsk).
+        {
+          ins; move: INi; rewrite mem_filter; move => /andP xxx; des.
+          move: xxx; move => /andP JOBi; des; clear xxx0 JOBi0.
+          have PROP := job_properties j_i; des.
+          move: JOBi => /eqP JOBi; rewrite -JOBi.
+          apply leq_trans with (n := job_cost j_i); last by ins. 
+          by apply service_interval_le_cost.
+        }
+
+        (* Order the sequence of interfering jobs by arrival time, so that
+           we can identify the first and last jobs. *)
+        set order := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
+        set sorted_jobs := (sort order interfering_jobs).
+        assert (SORT: sorted order sorted_jobs);
+          first by apply sort_sorted; unfold total, order; ins; apply leq_total.
+        rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort order).
+   
+        (* Remember that both sequences have the same set of elements *)
+        assert (INboth: forall x, (x \in interfering_jobs) = (x \in sorted_jobs)).
+          by apply perm_eq_mem; rewrite -(perm_sort order).
+          
+        (* Find some dummy element to use in the nth function *)
+        destruct (size sorted_jobs == 0) eqn:SIZE0;
+          first by move: SIZE0 =>/eqP SIZE0; rewrite (size0nil SIZE0) big_nil.
+        apply negbT in SIZE0; rewrite -lt0n in SIZE0.
+        assert (EX: exists elem: JobIn arr_seq, True); des.
+          destruct sorted_jobs; [by rewrite ltn0 in SIZE0 | by exists s].
+        clear EX SIZE0.
+
+        (* Remember that the jobs are ordered by arrival. *)
+        assert (ALL: forall i (LTsort: i < (size sorted_jobs).-1),
+                       order (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1)).
+        by destruct sorted_jobs; [by ins| by apply/pathP; apply SORT].
+        
+        (* Now we start the proof. First, we show that the workload bound
+           holds if n_k is no larger than the number of interferings jobs. *)
+        destruct (size sorted_jobs <= n_k) eqn:NUM.
+        {
+          rewrite -2![\sum_(_ <- _ | _) _]addn0 leq_add // leq_add //.
+          apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk);
+            last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
+          {
+            rewrite [\sum_(_ <- _) service_during _ _ _ _ _]big_seq_cond.
+            rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
+            by apply leq_sum; intros j_i; move/andP => xxx; des; apply LTserv; rewrite INboth.
+          }
+        }
+        apply negbT in NUM; rewrite -ltnNge in NUM.
+
+        (* Now we index the sum to access the first and last elements. *)
+        rewrite (big_nth elem).
+
+        (* First and last only exist if there are at least 2 jobs. Thus, we must show
+           that the bound holds for the empty list. *)
+        destruct (size sorted_jobs) eqn:SIZE; first by rewrite big_geq.
+        rewrite SIZE.
+        
+        (* Let's derive some properties about the first element. *)
+        exploit (mem_nth elem); last intros FST.
+          by instantiate (1:= sorted_jobs); instantiate (1 := 0); rewrite SIZE.
+          
+        move: FST (FST) => FST; rewrite -INboth mem_filter.
+        move => /andP [/andP [FSTtsk FSTserv] FSTin].
+
+        (* Now we show that the bound holds for a singleton set of interfering jobs. *)
+        destruct n.
+        {
+          destruct n_k eqn:EQnk; last by ins.
+          {
+            rewrite mul0n add0n big_nat_recl // big_geq // addn0.
+            rewrite -[service_during _ _ _ _ _]addn0 leq_add //.
+            by apply LTserv; rewrite INboth.
+          }
+        } rewrite [nth]lock /= -lock in ALL.
+        
+        (*    unfold n_k, max_jobs_NC, div_floor in EQnk.
+            rewrite -subndiv_eq_mod EQnk mul0n subn0.
+            rewrite leq_min; apply/andP; split; last first.
+            {
+              apply leq_trans with (n := job_cost (nth elem sorted_jobs 0));
+                first by apply service_interval_le_cost.
+              by rewrite -FSTtask; have PROP := job_properties (nth elem sorted_jobs 0); des.
+            }
+            {
+              apply leq_trans with (n := \sum_(t1 <= t < t2) 1).
+                by apply leq_sum; ins; apply service_at_le_max_rate.
+                by unfold t2; rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA// subnn addn0.
+            }
+          }
+        } rewrite [nth]lock /= -lock in ALL.*)
+    
+        (* Knowing that we have at least two elements, we take first and last out of the sum *) 
+        rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.
+        rewrite addnA addnC addnA.
+        set j_fst := (nth elem sorted_jobs 0).
+        set j_lst := (nth elem sorted_jobs n.+1).
+                       
+        (* Now we infer some facts about how first and last are ordered in the timeline *)
+        assert (INlst: j_lst \in interfering_jobs).
+        {
+            by unfold j_lst; rewrite INboth; apply mem_nth; rewrite SIZE.
+        }
+        move: INlst; rewrite mem_filter.
+        move => /andP [/andP [LSTtsk LSTserv] LSTin].
+
+        assert (AFTERt1: t1 <= job_arrival j_fst + R_tsk).
+        {
+          rewrite leqNgt; apply /negP; unfold not; intro LTt1.
+          move: FSTserv => /eqP FSTserv; apply FSTserv.
+          by apply (sum_service_after_rt_zero job_cost job_task tsk) with (R := R_tsk); try (by ins);
+           [by apply/eqP | by apply ltnW].
+        }
+
+        (*assert (AFTERt1: t1 <= job_arrival j_fst).
+        {
+          rewrite leqNgt; apply /negP; unfold not; intro LTt1.
+          apply H_no_carry_in; exists j_fst; split; first by apply/eqP.
+          unfold is_carry_in_job, carried_in; apply/andP; split; first by done.
+          unfold completed_jobs_dont_execute, completed in *.
+          apply/negP; intro COMPLETED.
+          specialize (COMP j_fst t2); rewrite leqNgt in COMP.
+          move: COMP => /negP COMP; apply COMP.
+          unfold service; rewrite -> big_cat_nat with (n := t1);
+            [simpl | by done | by apply leq_addr].
+          move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
+          apply leq_trans with (n := service rate sched j_fst t1 + 1);
+            first by rewrite addn1.
+          by rewrite leq_add2l lt0n.
+        }*)
+
+        (*assert (AFTERt1': t1 <= job_arrival j_lst).
+        {
+          rewrite leqNgt; apply /negP; unfold not; intro LTt1.
+          apply H_no_carry_in; exists j_lst; split; first by apply/eqP.
+          unfold is_carry_in_job, carried_in; apply/andP; split; first by done.
+          unfold completed_jobs_dont_execute, completed in *.
+          apply/negP; intro COMPLETED.
+          specialize (COMP j_lst t2); rewrite leqNgt in COMP.
+          move: COMP => /negP COMP; apply COMP.
+          unfold service; rewrite -> big_cat_nat with (n := t1);
+            [simpl | by done | by apply leq_addr].
+          move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
+          apply leq_trans with (n := service rate sched j_lst t1 + 1);
+            first by rewrite addn1.
+          by rewrite leq_add2l lt0n.
+        }*)
+
+        assert (BEFOREt2: job_arrival j_lst < t2).
+        {
+          rewrite leqNgt; apply/negP; unfold not; intro LT2.
+          assert (LTsize: n.+1 < size sorted_jobs).
+            by destruct sorted_jobs; ins; rewrite SIZE; apply ltnSn.
+          apply (mem_nth elem) in LTsize; rewrite -INboth in LTsize.
+          rewrite -/interfering_jobs mem_filter in LTsize.
+          move: LTsize => /andP [LTsize _]; des.
+          move: LTsize => /andP [_ SERV].
+          move: SERV => /eqP SERV; apply SERV.
+          by unfold service_during; rewrite sum_service_before_arrival.
+        }
+
+        assert (BEFOREarr: job_arrival j_fst <= job_arrival j_lst).
+        {
+          unfold j_fst, j_lst; rewrite -[n.+1]add0n.
+          apply prev_le_next; last by rewrite add0n SIZE leqnn.
+          by unfold order in ALL; intro i; rewrite SIZE; apply ALL.
+        }
+        
+        (* Now we upper-bound the service of the middle jobs. *)
+        assert (BOUNDmid: \sum_(0 <= i < n)
+                           service_during rate sched (nth elem sorted_jobs i.+1) t1 t2 <=
+                             n * task_cost tsk).
+        {
+          apply leq_trans with (n := n * task_cost tsk);
+            last by rewrite leq_mul2l; apply/orP; right. 
+          apply leq_trans with (n := \sum_(0 <= i < n) task_cost tsk);
+            last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
+          rewrite big_nat_cond [\sum_(0 <= i < n) task_cost _]big_nat_cond.
+          apply leq_sum; intros i; rewrite andbT; move => /andP LT; des.
+          by apply LTserv; rewrite INboth mem_nth // SIZE ltnS leqW.
+        }
+
+        (* Conclude that the distance between first and last is at least n + 1 periods,
+           where n is the number of middle jobs. *)
+        assert (DIST: job_arrival j_lst - job_arrival j_fst >= n.+1 * (task_period tsk)).
+        {
+          assert (EQnk: n.+1=(size sorted_jobs).-1); first by rewrite SIZE. 
+          unfold j_fst, j_lst; rewrite EQnk telescoping_sum; last by rewrite SIZE.
+          rewrite -[_ * _ tsk]addn0 mulnC -iter_addn -{1}[_.-1]subn0 -big_const_nat. 
+          rewrite big_nat_cond [\sum_(0 <= i < _)(_-_)]big_nat_cond.
+          apply leq_sum; intros i; rewrite andbT; move => /andP LT; des.
+          {
+            (* To simplify, call the jobs 'cur' and 'next' *)
+            set cur := nth elem sorted_jobs i.
+            set next := nth elem sorted_jobs i.+1.
+            clear BOUNDmid LT LTserv j_fst j_lst
+                  FSTin FSTserv FSTtsk LSTin LSTserv LSTtsk
+                  BEFOREarr AFTERt1 BEFOREt2.
+
+            (* Show that cur arrives earlier than next *)
+            assert (ARRle: job_arrival cur <= job_arrival next).
+            {
+              unfold cur, next; rewrite -addn1; apply prev_le_next; first by rewrite SIZE.
+              by apply leq_trans with (n := i.+1); try rewrite addn1.
+            }
+             
+            (* Show that both cur and next are in the arrival sequence *)
+            assert (INnth: cur \in interfering_jobs /\
+                           next \in interfering_jobs).
+              rewrite 2!INboth; split.
+              by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs; ins.
+              by apply mem_nth; destruct sorted_jobs; ins.
+            rewrite 2?mem_filter in INnth; des.
+
+            (* Use the sporadic task model to conclude that cur and next are separated
+               by at least (task_period tsk) units. Of course this only holds if cur != next.
+               Since we don't know much about the list (except that it's sorted), we must
+               also prove that it doesn't contain duplicates. *)
+            assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) <= job_arrival next).
+            {
+              apply sporadic_tasks; last by ins.
+              unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
+              rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; intuition.
+                by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
+                by destruct sorted_jobs; ins.
+                by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
+                by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.  
+            }
+            by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
+          }
+        }
+
+        (* Prove that n_k is at least the number of jobs - 2 *)
+        assert (NK: n_k >= n.+2).
+        {
+          admit.
+          (*rewrite leqNgt; apply/negP; unfold not; intro LTnk.
+          unfold n_k, max_jobs_NC in LTnk.
+          rewrite ltn_divLR in LTnk; last by done.
+          apply (leq_trans LTnk) in DIST.
+          move: LSTserv => /negP BUG; apply BUG.
+          unfold service_during; rewrite sum_service_before_arrival; try (by ins). 
+          unfold t2. apply leq_trans with (n := job_arrival j_fst + delta);
+            first by rewrite leq_add2r.
+          rewrite -(ltn_add2l (job_arrival j_fst)) addnBA // in DIST.
+          rewrite [_ + _ j_lst]addnC -addnBA // subnn addn0 in DIST.
+          by apply ltnW.*) 
+        }
+         
+        (* If n_k = num_jobs - 1, then we just need to prove that the
+           extra term with min() suffices to bound the workload. *)
         admit.
+        (*move: NK; rewrite leq_eqVlt orbC; move => /orP NK; des;
+          first by rewrite ltnS leqNgt NK in NUM.
+        {
+          move: NK => /eqP NK; rewrite -NK.
+          rewrite -addnA addnC; apply leq_add.
+          rewrite mulSn; apply leq_add.
+          {
+            apply leq_trans with (n := job_cost (nth elem sorted_jobs 0));
+              first by apply service_interval_le_cost.
+            by rewrite -FSTtask; have PROP := job_properties (nth elem sorted_jobs 0); des.
+          }
+          {
+            rewrite mulnC -{2}[n]subn0 -[_*_]addn0 -iter_addn -big_const_nat.
+            rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
+            apply leq_sum; intros i; rewrite andbT; move => /andP [_ LE].
+            apply leq_trans with (n := job_cost (nth elem sorted_jobs i.+1));
+              first by apply service_interval_le_cost.
+            assert (TASKnth: job_task (nth elem sorted_jobs i.+1) = tsk).
+            {
+              exploit (mem_nth elem); last intros IN.
+              instantiate (1:= sorted_jobs); instantiate (1 := i.+1);
+                by rewrite SIZE ltnS ltnW //.
+              move: IN; rewrite -INboth mem_filter.
+              by move => /andP [/andP [IN _] _]; apply/eqP.
+            }
+            by rewrite -TASKnth; have PROP := job_properties (nth elem sorted_jobs i.+1); des.
+          }
+          rewrite leq_min; apply/andP; split; last first.
+          {
+            move: INlst => /eqP INlst; rewrite -INlst.
+            apply leq_trans with (n := job_cost j_lst);
+              first by apply service_interval_le_cost.
+            by have PROP := job_properties j_lst; des.
+          }
+          {
+            unfold service_during.
+            rewrite -> big_cat_nat with (n := job_arrival j_lst); simpl;
+              try (by ins); last by apply ltnW.            
+            rewrite sum_service_before_arrival ?leqnn // add0n.
+            apply leq_trans with (n := \sum_(job_arrival j_lst <= i < t2) 1).
+            apply leq_sum; first by ins; apply service_at_le_max_rate.
+            rewrite big_const_nat iter_addn mul1n addn0.
+            rewrite -(leq_add2r (job_arrival j_lst)).
+            rewrite [t2 - _ + _]subh1; last by apply ltnW.
+            unfold t2; rewrite -addnBA // subnn addn0.
+            apply leq_trans with (n := job_arrival j_fst + delta);
+              first by rewrite leq_add2r.
+            rewrite -leq_subLR -addnBA;
+              last by rewrite -subndiv_eq_mod leq_subLR leq_addl.
+            rewrite -subndiv_eq_mod.
+            rewrite subnBA; last by apply leq_trunc_div.
+            rewrite [delta + _]addnC -addnBA // subnn addn0.
+            rewrite -(leq_add2r (job_arrival j_fst)) in DIST.
+            rewrite subh1 in DIST; last by apply BEFOREarr.
+            rewrite -addnBA // subnn addn0 addnC NK in DIST.
+            by unfold n_k, max_jobs_NC, div_floor in DIST.
+          }
+        }*)
+
       Qed.
 
     End GuanCarry.