platform_fp.v 12.1 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 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
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
               rt.model.basic.task_arrival rt.model.basic.interference
               rt.model.basic.priority rt.model.basic.platform.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Module PlatformFP.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask SporadicTaskset SporadicTaskArrival Interference Priority Platform.

  Section Lemmas.
    
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    
    Context {Job: eqType}.
    Variable job_cost: Job -> nat.
    Variable job_deadline: Job -> nat.
    Variable job_task: Job -> sporadic_task.
    
    (* Assume any job arrival sequence... *)
    Context {arr_seq: arrival_sequence Job}.

    (* Consider any schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.
    
    (* Assume all jobs have valid parameters, ...*)
    Hypothesis H_valid_job_parameters:
      forall (j: JobIn arr_seq),
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    Section JobInvariantAsTaskInvariant.

      (* Assume any work-conserving priority-based scheduler. *)
      Variable higher_eq_priority: FP_policy sporadic_task.
      Hypothesis H_work_conserving: work_conserving job_cost sched.
      Hypothesis H_enforces_JLDP_policy:
        enforces_FP_policy job_cost job_task sched higher_eq_priority.

      (* Consider task set ts. *)
      Variable ts: taskset_of sporadic_task.

      (* Assume the task set has no duplicates, ... *)
      Hypothesis H_ts_is_a_set: uniq ts.
      (* ... and all jobs come from the taskset. *)
      Hypothesis H_all_jobs_from_taskset:
        forall (j: JobIn arr_seq), job_task j \in ts.

      (* Suppose that a single job does not execute in parallel, ...*)
      Hypothesis H_no_parallelism:
        jobs_dont_execute_in_parallel sched.
      (* ... jobs must arrive to execute, ... *)
      Hypothesis H_completed_jobs_dont_execute:
        completed_jobs_dont_execute job_cost sched.
      (* ... and jobs do not execute after completion. *)
      Hypothesis H_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute sched.

      (* Assume that the schedule satisfies the sporadic task model ...*)
      Hypothesis H_sporadic_tasks:
        sporadic_task_model task_period arr_seq job_task.

      (* Consider a valid task tsk, ...*)
      Variable tsk: sporadic_task.
      Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.

      (*... whose job j ... *)
      Variable j: JobIn arr_seq.
      Variable H_job_of_tsk: job_task j = tsk.

      (*... is backlogged at time t <= job_arrival j + task_period tsk. *)
      Variable t: time.
      Hypothesis H_j_backlogged: backlogged job_cost sched j t.
      Hypothesis H_t_before_period: t < job_arrival j + task_period tsk.

      Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk.

      (* Assume that any jobs of higher-priority tasks complete by their period. *)
      Hypothesis H_all_previous_jobs_completed :
        forall (j_other: JobIn arr_seq) tsk_other,
          job_task j_other = tsk_other ->
          can_interfere_with_tsk tsk_other ->
          completed job_cost sched j_other (job_arrival j_other + task_period tsk_other).

      (* Assume that any jobs of tsk prior to j complete by their period. *)
      Hypothesis H_all_previous_jobs_of_tsk_completed :
        forall j0 : JobIn arr_seq,
          job_task j0 = tsk ->
          job_arrival j0 < job_arrival j ->
          completed job_cost sched j0 (job_arrival j0 + task_period tsk).
      
      Definition scheduled_task_with_higher_eq_priority (tsk tsk_other: sporadic_task) :=
        task_is_scheduled job_task sched tsk_other t &&
        can_interfere_with_tsk tsk_other.
                             
      (* Then, there can be at most one pending job of higher-priority tasks at time t. *)
      Lemma platform_fp_no_multiple_jobs_of_interfering_tasks :
          forall j1 j2,
            pending job_cost sched j1 t ->
            pending job_cost sched j2 t ->
            job_task j1 = job_task j2 ->
            can_interfere_with_tsk (job_task j1) ->
            j1 = j2.
      Proof.
        unfold sporadic_task_model in *.
        rename H_sporadic_tasks into SPO, H_all_previous_jobs_of_tsk_completed into PREVtsk,
               H_all_previous_jobs_completed into PREV.
        intros j1 j2 PENDING1 PENDING2 SAMEtsk INTERF.
        apply/eqP; rewrite -[_ == _]negbK; apply/negP; red; move => /eqP DIFF.
        move: PENDING1 PENDING2 => /andP [ARRIVED1 /negP NOTCOMP1] /andP [ARRIVED2 /negP NOTCOMP2].
        destruct (leqP (job_arrival j1) (job_arrival j2)) as [BEFORE1 | BEFORE2].
        {
          specialize (SPO j1 j2 DIFF SAMEtsk BEFORE1).
          exploit (PREV j1 (job_task j1)); [by done | by apply INTERF | intros COMP1].
          apply NOTCOMP1.
          apply completion_monotonic with (t0 := job_arrival j1 + task_period (job_task j1));
            try (by done).
          by apply leq_trans with (n := job_arrival j2). 
        }
        {
          apply ltnW in BEFORE2.
          exploit (SPO j2 j1); [by red; ins; subst j2 | by rewrite SAMEtsk | by done | intro SPO' ].
          exploit (PREV j2 (job_task j2));
            [by done | by rewrite -SAMEtsk | intro COMP2 ].
          apply NOTCOMP2.
          apply completion_monotonic with (t0 := job_arrival j2 + task_period (job_task j2));
            try (by done).
          by apply leq_trans with (n := job_arrival j1).
        }
      Qed.
      
      (* Also, there can be at most one pending job of tsk at time t. *)
      Lemma platform_fp_no_multiple_jobs_of_tsk :
          forall j',
            pending job_cost sched j' t ->
            job_task j' = tsk ->
            j' = j.
      Proof.
        unfold sporadic_task_model in *.
        rename H_sporadic_tasks into SPO,
               H_valid_task into PARAMS,
               H_all_previous_jobs_of_tsk_completed into PREVtsk,
               H_all_previous_jobs_completed into PREV,
               H_j_backlogged into BACK, H_job_of_tsk into JOBtsk.
        intros j' PENDING' SAMEtsk.
        apply/eqP; rewrite -[_ == _]negbK; apply/negP; red; move => /eqP DIFF.
        move: BACK PENDING' => /andP [/andP [ARRIVED /negP NOTCOMP] NOTSCHED]
                               /andP [ARRIVED' /negP NOTCOMP'].
        destruct (leqP (job_arrival j') (job_arrival j)) as [BEFORE | BEFORE'].
        {
          exploit (SPO j' j DIFF); [by rewrite JOBtsk | by done | intro SPO'].
          apply NOTCOMP'.
          apply completion_monotonic with (t0 := job_arrival j' + task_period tsk); try (by done);
            first by apply leq_trans with (n := job_arrival j); [by rewrite -SAMEtsk | by done].
          {
            apply PREVtsk; first by done.
            apply leq_trans with (n := job_arrival j' + task_period tsk); last by rewrite -SAMEtsk.
            rewrite -addn1; apply leq_add; first by done.
            by unfold is_valid_sporadic_task in *; des.
          }
        }
        {
          unfold has_arrived in *.
          rewrite leqNgt in ARRIVED'; move: ARRIVED' => /negP BUG; apply BUG.
          apply leq_trans with (n := job_arrival j + task_period tsk); first by done.
          by rewrite -JOBtsk; apply SPO;
            [by red; ins; subst j' | by rewrite SAMEtsk | by apply ltnW].
        }
      Qed.
      
      (* Therefore, all processors are busy with tasks other than tsk. *)
      Lemma platform_fp_cpus_busy_with_interfering_tasks :      
        count (scheduled_task_with_higher_eq_priority tsk) ts = num_cpus.
      Proof.
        rename H_all_jobs_from_taskset into FROMTS,
               H_no_parallelism into SEQUENTIAL,
               H_work_conserving into WORK,
               H_enforces_JLDP_policy into PRIO,
               H_j_backlogged into BACK,
               H_job_of_tsk into JOBtsk,
               H_sporadic_tasks into SPO,
               H_valid_job_parameters into JOBPARAMS,
               H_valid_task into TASKPARAMS,
               H_all_previous_jobs_completed into PREV,
               H_completed_jobs_dont_execute into COMP,
               H_all_previous_jobs_of_tsk_completed into PREVtsk,
               H_jobs_must_arrive_to_execute into ARRIVE.
192
        apply work_conserving_eq_work_conserving_count in WORK.
193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
        unfold valid_sporadic_job, valid_realtime_job,
               enforces_FP_policy, enforces_JLDP_policy, FP_to_JLDP,
               task_precedence_constraints, completed_jobs_dont_execute,
               sporadic_task_model, is_valid_sporadic_task,
               jobs_of_same_task_dont_execute_in_parallel,
               jobs_dont_execute_in_parallel,
               can_interfere_with_tsk in *.
        have UNIQ := platform_fp_no_multiple_jobs_of_interfering_tasks.
        have UNIQ' := platform_fp_no_multiple_jobs_of_tsk. 
        apply/eqP; rewrite eqn_leq; apply/andP; split.
        {
          apply leq_trans with (n := count (fun x => task_is_scheduled job_task sched x t) ts);
            first by apply sub_count; red; move => x /andP [SCHED _].
          unfold task_is_scheduled.
          apply count_exists; first by done.
          {
            intros cpu x1 x2 SCHED1 SCHED2.
210
            unfold schedules_job_of_task in *.
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
            destruct (sched cpu t); last by done.
            move: SCHED1 SCHED2 => /eqP SCHED1 /eqP SCHED2.
            by rewrite -SCHED1 -SCHED2.
          }
        }
        {
          rewrite -(WORK j t) // -count_predT.
          apply leq_trans with (n := count (fun j: JobIn arr_seq =>
            scheduled_task_with_higher_eq_priority tsk (job_task j)) (jobs_scheduled_at sched t));
            last first.
          {
            rewrite -count_map.
            apply leq_trans with (n := count predT [seq x <- (map (fun (j: JobIn arr_seq) => job_task j) (jobs_scheduled_at sched t)) | scheduled_task_with_higher_eq_priority tsk x]);
              first  by rewrite count_filter; apply sub_count; red; ins.
            apply leq_trans with (n := count predT [seq x <- ts | scheduled_task_with_higher_eq_priority tsk x]);
              last by rewrite count_predT size_filter.
            apply count_sub_uniqr;
              last first.
            {
              red; intros tsk' IN'.
              rewrite mem_filter in IN'; move: IN' => /andP [SCHED IN'].
              rewrite mem_filter; apply/andP; split; first by done.
              by move: IN' => /mapP [j' _] ->; apply FROMTS.
            }
            {
              rewrite filter_map.
              rewrite map_inj_in_uniq; first by apply filter_uniq, scheduled_jobs_uniq.
              red; intros j1 j2 SCHED1 SCHED2 SAMEtsk.
              rewrite 2!mem_filter in SCHED1 SCHED2.
              move: SCHED1 SCHED2 => /andP [/andP [_ HP1] SCHED1] /andP [/andP [_ HP2] SCHED2].
              rewrite 2!mem_scheduled_jobs_eq_scheduled in SCHED1 SCHED2.
              apply scheduled_implies_pending with (job_cost0 := job_cost) in SCHED1; try (by done).
              apply scheduled_implies_pending with (job_cost0 := job_cost) in SCHED2; try (by done).
              by apply UNIQ.
            }
          }
          {
            apply sub_in_count; intros j' SCHED' _.
            rewrite mem_scheduled_jobs_eq_scheduled in SCHED'.
            apply/andP; split.
            {
              move: SCHED' => /exists_inP [cpu INcpu /eqP SCHED'].
              apply/exists_inP; exists cpu; first by done.
254
              by unfold schedules_job_of_task; rewrite SCHED' eq_refl.
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272
            }
            apply/andP; split; first by rewrite -JOBtsk; apply PRIO with (t := t).
            {
              apply/eqP; red; intro SAMEtsk.
              generalize SCHED'; intro PENDING'.
              apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING'; try (by done).
              specialize (UNIQ' j' PENDING' SAMEtsk); subst j'.
              by move: BACK => /andP [_ NOTSCHED]; rewrite SCHED' in NOTSCHED.
            }
          }
        }
      Qed.

    End JobInvariantAsTaskInvariant.

  End Lemmas.
  
End PlatformFP.