main_theorem.v 12.2 KB
Newer Older
Martin PORTALIER's avatar
Martin PORTALIER committed
1 2
From rt.restructuring.model Require Export task task_cost arrival.sporadic priority_based.priorities
  priority_based.preemptive workload.
Xiaojie Guo's avatar
Xiaojie Guo committed
3

Martin PORTALIER's avatar
Martin PORTALIER committed
4 5 6
From rt.restructuring.analysis Require Export
  schedulability.
From rt.restructuring.analysis.fpp_implicit_deadline Require Export
Xiaojie Guo's avatar
Xiaojie Guo committed
7
  workload_bound_fp intermediate.
Xiaojie Guo's avatar
Xiaojie Guo committed
8 9 10
From rt.restructuring.behavior.schedule Require Export ideal.

From mathcomp Require Import seq.
Martin PORTALIER's avatar
Martin PORTALIER committed
11
From rt.util Require Import div_mod sum tactics ssromega.
Xiaojie Guo's avatar
Xiaojie Guo committed
12

Martin PORTALIER's avatar
Martin PORTALIER committed
13 14 15
Section main.

Context (Task: TaskType).
Xiaojie Guo's avatar
Xiaojie Guo committed
16 17 18
Context `{TaskDeadline Task}.

Context {Job: JobType}.
Xiaojie Guo's avatar
Xiaojie Guo committed
19
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Xiaojie Guo's avatar
Xiaojie Guo committed
20

Martin PORTALIER's avatar
Martin PORTALIER committed
21
Context `{SporadicModel Task} `{TaskCost Task}.
Xiaojie Guo's avatar
Xiaojie Guo committed
22
Context `{FP_policy Task }.
Xiaojie Guo's avatar
Xiaojie Guo committed
23

Martin PORTALIER's avatar
Martin PORTALIER committed
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
(* Let ts be any task set with valid task parameters. *)
Variable ts: list Task.
Hypothesis H_valid_task_parameters: forall tsk, tsk \in ts ->
  (task_cost tsk) > 0 /\ (task_min_inter_arrival_time tsk) > 0
  /\ (task_deadline tsk) > 0 /\ (task_cost tsk) <= (task_deadline tsk)
  /\ (task_cost tsk) <= (task_min_inter_arrival_time tsk)
  /\ task_deadline tsk <= task_min_inter_arrival_time tsk.

(* Let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Hypothesis H_uniq: uniq ts.

(* Suppose that the task deadlines are implicit. *)
Hypothesis H_implicit_deadline: forall tsk',
  task_deadline tsk' = task_min_inter_arrival_time tsk'.

(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Xiaojie Guo's avatar
Xiaojie Guo committed
42
Variable arr_seq : arrival_sequence Job.
Martin PORTALIER's avatar
Martin PORTALIER committed
43
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
Xiaojie Guo's avatar
Xiaojie Guo committed
44

Martin PORTALIER's avatar
Martin PORTALIER committed
45 46 47 48 49 50 51
(* Suppose that the task model is sporadic. *)
Hypothesis H_sporadic_tasks: respects_sporadic_task_model arr_seq.

(* All jobs considered are in arr_seq: they arrive at the instant 'job_arrival jb' *)
Hypothesis H_arrives_in : forall jb, arrives_in arr_seq jb.

(* Consider any schedule with valid parameters such as work conserving or seqential arrival. *)
Xiaojie Guo's avatar
Xiaojie Guo committed
52
Variable sched : schedule (processor_state Job).
Martin PORTALIER's avatar
Martin PORTALIER committed
53
Hypothesis H_valid_sched : valid_schedule sched arr_seq.
Martin PORTALIER's avatar
Martin PORTALIER committed
54
Hypothesis H_work_conserving: work_conserving arr_seq sched.
Martin PORTALIER's avatar
Martin PORTALIER committed
55
Hypothesis H_sequential_jobs: sequential_jobs sched.
Martin PORTALIER's avatar
Martin PORTALIER committed
56 57
Hypothesis H_sched_none : forall t, sched t = None -> arr_seq t = [::].

Martin PORTALIER's avatar
Martin PORTALIER committed
58 59 60
(* Assume that all jobs come from the task set ...*)
Hypothesis H_all_jobs_from_taskset: forall j,
  arrives_in arr_seq j -> job_task j \in ts.
Martin PORTALIER's avatar
Martin PORTALIER committed
61

Martin PORTALIER's avatar
Martin PORTALIER committed
62 63 64
(* ...and have valid parameters. *)
Hypothesis H_valid_job_parameters: forall j,
  arrives_in arr_seq j -> job_cost j > 0 /\
Martin PORTALIER's avatar
Martin PORTALIER committed
65 66
    job_cost j <= task_cost (job_task j)/\ job_cost j <= job_deadline j
      /\ job_deadline j = task_deadline (job_task j).
Xiaojie Guo's avatar
Xiaojie Guo committed
67

Martin PORTALIER's avatar
Martin PORTALIER committed
68
(* Assume any fixed-priority policy with valid properties... *)
Xiaojie Guo's avatar
Xiaojie Guo committed
69
Let higher_eq_priority := hep_task.
Martin PORTALIER's avatar
Martin PORTALIER committed
70
Let jl_hep := (fun j1 j2 => higher_eq_priority (job_task j1) (job_task j2)).
Martin PORTALIER's avatar
Martin PORTALIER committed
71
Hypothesis H_fpp : respects_preemptive_priorities arr_seq sched.
Xiaojie Guo's avatar
Xiaojie Guo committed
72

Martin PORTALIER's avatar
Martin PORTALIER committed
73 74 75 76
(* ...which is an order relation. *)
Hypothesis H_reflexive : reflexive higher_eq_priority /\ reflexive jl_hep.
Hypothesis H_antisymmetric: antisymmetric higher_eq_priority.
Hypothesis H_transitive : transitive jl_hep.
Martin PORTALIER's avatar
Martin PORTALIER committed
77

Martin PORTALIER's avatar
Martin PORTALIER committed
78
(* Definition of the task workload bound. *)
Martin PORTALIER's avatar
Martin PORTALIER committed
79 80 81
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.

Definition formula (delta : duration) : nat :=
Martin PORTALIER's avatar
Martin PORTALIER committed
82
  \sum_(x <- ts | is_hep_task x && (x != tsk))
Martin PORTALIER's avatar
Martin PORTALIER committed
83
    (task_workload_bound_FP x delta) + task_cost tsk.
Xiaojie Guo's avatar
Xiaojie Guo committed
84

Martin PORTALIER's avatar
Martin PORTALIER committed
85
(* Suppose that the task workload bound has a fixpoint R lower than the task deadline. *)
Xiaojie Guo's avatar
Xiaojie Guo committed
86
Variable R : duration.
Martin PORTALIER's avatar
Martin PORTALIER committed
87
Hypothesis H_valid_R : formula R = R /\ R > 0 /\ R <= task_deadline tsk.
Xiaojie Guo's avatar
Xiaojie Guo committed
88

Martin PORTALIER's avatar
Martin PORTALIER committed
89 90
(* In this section we prove that all jobs terminate.
    Then we can define the exact instant t2 when it happens. *)
Xiaojie Guo's avatar
Xiaojie Guo committed
91 92
Section exists_t2.

Martin PORTALIER's avatar
Martin PORTALIER committed
93
  Let workload_bound := formula.
Xiaojie Guo's avatar
Xiaojie Guo committed
94

Martin PORTALIER's avatar
Martin PORTALIER committed
95
  Lemma exists_t2 : forall delta,
Xiaojie Guo's avatar
minor  
Xiaojie Guo committed
96 97
      delta > 0 -> workload_bound delta = delta
      -> delta <= task_deadline tsk
Martin PORTALIER's avatar
Martin PORTALIER committed
98 99 100
      -> (forall j, arrives_in arr_seq j -> job_task j = tsk ->
    exists t2, job_arrival j < t2 /\ completes_at sched j t2).
  Proof.
Xiaojie Guo's avatar
Xiaojie Guo committed
101
  Admitted.
Martin PORTALIER's avatar
Martin PORTALIER committed
102 103 104

End exists_t2.

Martin PORTALIER's avatar
Martin PORTALIER committed
105 106 107 108
(* In this section we prove that the fixpoint R of the workload
    is a bound for the task reponse time of tsk. *)
Section Fixpoint_bound.

Martin PORTALIER's avatar
Martin PORTALIER committed
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
  (* Lemma about rewrite the formula and the workload_bound. *)
  Lemma rwt_formula: forall r,
    0 < r -> r <= task_deadline tsk
    -> formula r = \sum_(x <- ts | higher_eq_priority x tsk)
        task_workload_bound_FP x r.
  Proof.
    move => r H_pos H_inf. unfold task_workload_bound_FP.
    rewrite big_mkcond (bigD1_seq tsk)/=; auto.
    have ->: higher_eq_priority tsk tsk by apply H_reflexive.
    rewrite addnC -big_mkcondl/=. unfold formula.
    unfold task_workload_bound_FP. unfold max_jobs. rewrite ceil_eq1.
    rewrite mul1n. auto. easy. apply leq_trans with (n:=task_deadline tsk).
    easy. apply H_valid_task_parameters; auto.
  Qed.

Martin PORTALIER's avatar
Martin PORTALIER committed
124 125 126 127 128 129 130 131 132
  (* Main theorem of this section. *)
  Theorem fpp_implicit_deadline :
    task_response_time_bound arr_seq sched tsk R.
  Proof.
    unfold task_response_time_bound.
    move => j H_arrives H_job_task.
    have [t2 H_t2]: exists t2, job_arrival j < t2 /\ completes_at sched j t2.
      apply exists_t2 with (delta:=R); easy.
    apply resp_time_bound with (arr_seq0:=arr_seq)
Martin PORTALIER's avatar
Martin PORTALIER committed
133
    (higher_eq_priority0:=jl_hep) (end_of_analyse_interval:=t2)
Martin PORTALIER's avatar
Martin PORTALIER committed
134 135 136 137 138 139 140 141
        (workload_bound:=formula); try easy.
    move => j0; apply H_valid_job_parameters; auto.
    move => jb. apply H_valid_task_parameters. apply H_all_jobs_from_taskset; auto.
    move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
    unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
    unfold jl_hep in H_and. apply H_antisymmetric. auto.
    set t1 := start_of_analyse_interval arr_seq sched jl_hep j.
    unfold workload_of_jobs.
Martin PORTALIER's avatar
Martin PORTALIER committed
142
    apply leq_trans with (n:=\sum_(j0 <- jobs_arrived_between arr_seq t1 (t1 + R) | 
Martin PORTALIER's avatar
Martin PORTALIER committed
143 144 145 146 147
            higher_eq_priority (job_task j0) (job_task j)) job_cost j0).
    apply inf_workload; auto.
    move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
    unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
    unfold jl_hep in H_and. apply H_antisymmetric. auto. have H_fix: formula R = R by easy. rewrite H_fix.
Martin PORTALIER's avatar
Martin PORTALIER committed
148 149
    apply fp_workload_bound_holds with (ts0:=ts); auto.
    rewrite -{1}H_fix. rewrite rwt_formula; try easy. rewrite H_job_task; auto.
Martin PORTALIER's avatar
Martin PORTALIER committed
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
  Qed.

End Fixpoint_bound.

(* In this section we prove that the bound is reached.
   In other words, there exists a job j and an arrival sequence such that
    its reponse time is equal to the fixpoint R. *)
Section Reached_bound.

  (* Suppose that R is the smallest fixpoint. *)
  Hypothesis H_smallest_fixpoint:
    forall r, formula r = r -> R <= r.

  (* Suppose that all jobs cost are maximised. *)
  Hypothesis H_task_cost: forall jb,
    job_cost jb = task_cost (job_task jb).

  (* Suppose that as soon as it is possible, there exists a jobs that arrives.
     In others words, the arrival sequence model is periodic. *)
  Hypothesis H_periodic: forall j1 t,
    j1 \in jobs_arriving_at arr_seq t -> exists j2,
      j2 \in jobs_arriving_at arr_seq (t + task_min_inter_arrival_time (job_task j1))
        /\ same_task j1 j2.

  (* Consider a job j from the task tsk. *)
  Variable j: Job.
  Hypothesis H_job_task: job_task j = tsk.

  (* Suppose that all job from a highest priority than j
      arrive exactly at the same time of j. *)
  Hypothesis H_all_arrives:
    forall tsk', higher_eq_priority tsk' tsk
      -> exists jb, jb \in jobs_arriving_at arr_seq (job_arrival j)
        /\ job_task jb = tsk'.

  (* Suppose that the system is schedulable:
      all jobs terminate before their deadline. *)
  Hypothesis H_is_schedulable: forall jb,
    completed_by sched jb (job_arrival jb + (job_deadline jb)).

  (* Main theorem of this section:
    the job j completes exactly at the instant (job_arrival j) + R. *)
  Theorem max_bound_reach:
    completes_at sched j ((job_arrival j) + R).
  Proof.
    have [t2 H_t2]: exists t2, job_arrival j < t2 /\ completes_at sched j t2.
      apply exists_t2 with (delta:=R); easy.
    set t1 := start_of_analyse_interval arr_seq sched jl_hep j.
    have H_t1: t1 = start_of_analyse_interval arr_seq sched jl_hep j by auto.
    have H_start_interval_arrival: t1 = job_arrival j. rewrite H_t1.
      rewrite -> start_interval_arrival with (task_hep:=higher_eq_priority)
      (workload_bound:=formula) (r:=R); try easy.
    move => tsk' H_hp. apply H_all_arrives. rewrite -H_job_task. auto.
    move => jb. have ->: job_deadline jb = task_deadline (job_task jb).
Martin PORTALIER's avatar
Martin PORTALIER committed
204
    apply H_valid_job_parameters; auto. apply H_implicit_deadline.
Martin PORTALIER's avatar
Martin PORTALIER committed
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
    have H_arr_inf: job_arrival j < t2 by easy.
    have H_main: t2 - (job_arrival j) = R. {
      rewrite -H_start_interval_arrival. apply /eqP. rewrite eqn_leq.
      apply vlib__leq_split.
      apply len_inf_r with (workload_bound:=formula); try easy.
      move => j0; apply H_valid_job_parameters; auto.
      move => jb. apply H_valid_task_parameters. apply H_all_jobs_from_taskset; auto.
      move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
      unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
      unfold jl_hep in H_and. apply H_antisymmetric. auto. unfold workload_of_jobs.
      apply leq_trans with (n:=\sum_(j0 <- jobs_arrived_between arr_seq t1 (t1 + R) | 
            higher_eq_priority (job_task j0) (job_task j)) job_cost j0).
      apply inf_workload; auto.
      move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
      unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
      unfold jl_hep in H_and. apply H_antisymmetric. auto. have H_fix: formula R = R by easy. rewrite H_fix.
      apply fp_workload_bound_holds with (ts0:=ts); auto.
      rewrite -{1}H_fix. rewrite rwt_formula; try easy. rewrite H_job_task; auto.
      apply H_smallest_fixpoint. rewrite rwt_formula.
      rewrite H_start_interval_arrival. unfold task_workload_bound_FP.
      rewrite <- pre_workload_reach with (r:=(t2 - job_arrival j)) (j0:=j) (ts0:=ts)
        (arr_seq0:=arr_seq) (higher_eq_priority0:=higher_eq_priority) (tsk0:=tsk)
          (R0:=R); try easy.
      rewrite rwt_hp_workload.
      rewrite -H_start_interval_arrival. apply esym.
      rewrite {1}service_eq_nat_len; try easy. rewrite serv_eq_workload; try easy.
      rewrite -> rewrite_workload with (task_hep:=higher_eq_priority)
       (workload_bound:=formula) (r:=R) (arr_seq0:=arr_seq) (end_of_analyse_interval:=t2)
         (j0:=j) (higher_eq_priority0:=jl_hep) (sched0:=sched); try easy.
      rewrite -H_t1. unfold jl_hep. rewrite H_job_task; auto.
      move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
      unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
      unfold jl_hep in H_and. apply H_antisymmetric. auto.
      rewrite H_job_task; auto. move => jb.
      have ->: job_deadline jb = task_deadline (job_task jb).
      apply H_valid_job_parameters; auto. apply H_implicit_deadline.
      move => jb. apply H_valid_task_parameters. apply H_all_jobs_from_taskset; auto.
      move => j1 j2. split. move => H_same. move /eqP in H_same. apply /andP. split;
      unfold jl_hep; rewrite H_same; apply H_reflexive. move => H_and. apply /eqP.
      unfold jl_hep in H_and. apply H_antisymmetric. auto.
      move => jb. apply H_valid_job_parameters; auto.
      have {1}<-: formula R = R by easy. rewrite rwt_formula; try easy.
      ssromega. rewrite H_start_interval_arrival.
      have H_tmp: job_arrival j < t2 by easy. ssromega.
      have H_inf1: t2 <= t1 + task_deadline tsk.
        have H_comp: completes_at sched j t2 by easy.
        case E: (job_arrival j + job_deadline j < t2). apply lt_leq1 in E.
        unfold completes_at in H_comp. move /andP in H_comp.
        have H_no_comp: ~~ completed_by sched j t2.-1 by easy.
        apply decr_no_completed with (t:=job_arrival j + job_deadline j) in H_no_comp; auto.
        have H_contr: completed_by sched j (job_arrival j + job_deadline j)
        by apply H_is_schedulable. move /negP in H_no_comp. auto.
        apply leq_ltn_trans with (n:=job_arrival j); auto.
        have E': t2 <= job_arrival j + job_deadline j. ssromega.
        rewrite H_start_interval_arrival. rewrite -H_job_task.
        have <-: job_deadline j = task_deadline (job_task j).
        apply H_valid_job_parameters; auto. easy. ssromega. }
    have <-: t2 = job_arrival j + R by ssromega. easy.
  Qed.

End Reached_bound.
Martin PORTALIER's avatar
Martin PORTALIER committed
266

Martin PORTALIER's avatar
Martin PORTALIER committed
267
End main.