Commit c1775426 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Remove redundant (service != 0) from interfering_jobs in workload_bound.v

parent 2ba684fa
......@@ -163,8 +163,8 @@ Module Schedule.
Qed.
(* If the cumulative service during a time interval is not zero, there
must be a time t in this interval where the service is not 0. *)
Lemma job_scheduled_during_interval :
must be a time t in this interval where the service is not 0, ... *)
Lemma cumulative_service_implies_service :
forall t1 t2,
service_during sched j t1 t2 != 0 ->
exists t,
......@@ -188,6 +188,21 @@ Module Schedule.
by rewrite GT andTb negbK in EX; apply/eqP.
}
Qed.
(* ... and vice versa. *)
Lemma service_implies_cumulative_service:
forall t t1 t2,
t1 <= t < t2 ->
service_at sched j t != 0 ->
service_during sched j t1 t2 != 0.
Proof.
intros t t1 t2 LE NONZERO.
unfold service_during.
rewrite (bigD1_seq t) /=;
[| by rewrite mem_index_iota | by apply iota_uniq].
rewrite -lt0n -addn1 addnC.
by apply leq_add; first by rewrite lt0n.
Qed.
End Basic.
......@@ -506,7 +521,28 @@ Module ScheduleOfSporadicTask.
Import SporadicTask Job.
Export Schedule.
Section Properties.
Section ScheduledJobs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job -> sporadic_task.
(* Consider any schedule. *)
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* Given a task tsk, ...*)
Variable tsk: sporadic_task.
(* ..., we define the list of jobs scheduled during [t1, t2). *)
Definition jobs_of_task_scheduled_between (t1 t2: time) :=
filter (fun (j: JobIn arr_seq) => job_task j == tsk)
(jobs_scheduled_between sched t1 t2).
End ScheduledJobs.
Section ScheduleProperties.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
......@@ -531,7 +567,7 @@ Module ScheduleOfSporadicTask.
job_arrival j < job_arrival j' ->
pending job_cost sched j t -> ~~ scheduled sched j' t.
End Properties.
End ScheduleProperties.
Section BasicLemmas.
......
......@@ -178,15 +178,23 @@ Section BigCatLemmas.
Lemma mem_bigcat_nat_exists :
forall (T: eqType) x m n (f: nat -> list T),
x \in \cat_(m <= i < n) (f i) ->
exists i, x \in (f i).
exists i, x \in (f i) /\
m <= i < n.
Proof.
intros T x m n f IN.
induction n; first by rewrite big_geq // in IN.
destruct (leqP m n); last by rewrite big_geq ?in_nil // ltnW in IN.
rewrite big_nat_recr // /= mem_cat in IN.
move: IN => /orP [HEAD | TAIL].
by apply IHn in HEAD; destruct HEAD; exists x0.
by exists n.
{
apply IHn in HEAD; destruct HEAD; exists x0; des.
split; first by done.
by apply/andP; split; [by done | by apply ltnW].
}
{
exists n; split; first by done.
apply/andP; split; [by done | by apply ltnSn].
}
Qed.
Lemma mem_bigcat_ord:
......
......@@ -4,7 +4,7 @@ Require Import Vbase job task schedule task_arrival response_time
Module Workload.
Import Job SporadicTaskset Schedule SporadicTaskArrival ResponseTime Schedulability.
Import Job SporadicTaskset ScheduleOfSporadicTask SporadicTaskArrival ResponseTime Schedulability.
(* Let's define the workload. *)
Section WorkloadDef.
......@@ -40,17 +40,16 @@ Module Workload.
during [t1,t2) of the scheduled jobs, but only those spawned
by the task that we care about. *)
Definition workload_joblist (t1 t2: time) :=
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk)
\sum_(j <- jobs_of_task_scheduled_between job_task sched tsk t1 t2)
service_during sched j t1 t2.
(* Next, we show that the two definitions are equivalent. *)
Lemma workload_eq_workload_joblist :
forall t1 t2,
workload t1 t2 = workload_joblist t1 t2.
Proof.
intros t1 t2; unfold workload, workload_joblist, service_during.
rewrite [\sum_(j <- jobs_scheduled_between _ _ _ | _) _]exchange_big /=.
rewrite big_filter [\sum_(j <- jobs_scheduled_between _ _ _ | _) _]exchange_big /=.
apply eq_big_nat; unfold service_at; intros t LEt.
rewrite [\sum_(i <- jobs_scheduled_between _ _ _ | _) _](eq_bigr (fun i =>
\sum_(cpu < num_cpus) (sched cpu t == Some i)));
......
......@@ -207,11 +207,10 @@ Module WorkloadBound.
Let n_k := max_jobs task_cost task_period tsk R_tsk delta.
Let workload_bound := W task_cost task_period tsk R_tsk delta.
(* Identify the subset of jobs that actually cause interference *)
(* Since we only care about the interference caused by tsk,
we identify the set of jobs of that task in [t1, t2). *)
Let interfering_jobs :=
filter (fun (j: JobIn arr_seq) =>
(job_task j == tsk) && (service_during sched j t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
(* Now, let's consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
......@@ -220,25 +219,16 @@ Module WorkloadBound.
(* The first step consists in simplifying the sum corresponding
to the workload. *)
Section SimplifyJobSequence.
(* Remove the elements that we don't care about from the sum *)
Lemma workload_bound_simpl_by_filtering_interfering_jobs :
\sum_(i <- jobs_scheduled_between sched t1 t2 | job_task i == tsk)
service_during sched i t1 t2 =
\sum_(i <- interfering_jobs) service_during sched i t1 t2.
Proof.
unfold interfering_jobs.
rewrite (bigID (fun x => service_during sched x t1 t2 == 0)) /=.
rewrite (eq_bigr (fun x => 0)); last by move => j_i /andP JOBi; des; apply /eqP.
by rewrite big_const_seq iter_addn mul0n add0n add0n big_filter.
Qed.
(* Consider the sum over the sorted sequence of jobs. *)
(* After switching to the definition of workload based on a list
of jobs, we show that sorting the list preserves the sum. *)
Lemma workload_bound_simpl_by_sorting_interfering_jobs :
\sum_(i <- interfering_jobs) service_during sched i t1 t2 =
workload_joblist job_task sched tsk t1 t2 =
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
unfold workload_joblist; fold interfering_jobs.
rewrite (eq_big_perm sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.
(* Remember that both sequences have the same set of elements *)
......@@ -259,8 +249,14 @@ Module WorkloadBound.
j_i \in jobs_scheduled_between sched t1 t2.
Proof.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi.
by move: LTi => /andP [/andP [/eqP JOBi SERVi] INi]; repeat split.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
repeat split; [by apply/eqP | | by done].
unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
apply mem_bigcat_nat_exists in LTi0; des.
rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
apply service_implies_cumulative_service with (t := i);
first by apply/andP; split.
by rewrite -not_scheduled_no_service negbK.
Qed.
(* Remember that consecutive jobs are ordered by arrival. *)
......@@ -732,10 +728,7 @@ Module WorkloadBound.
fold n_k.
(* Use the definition of workload based on list of jobs. *)
rewrite workload_eq_workload_joblist; unfold workload_joblist.
(* We only care about the jobs that cause interference. *)
rewrite workload_bound_simpl_by_filtering_interfering_jobs.
rewrite workload_eq_workload_joblist.
(* Now we order the list by job arrival time. *)
rewrite workload_bound_simpl_by_sorting_interfering_jobs.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment