Commit 95379048 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Define scheduled using scheduled_on

parent 4b4a1336
......@@ -145,7 +145,7 @@ Module ConcreteScheduler.
apply eq_big_nat; move => t0 /andP [_ LT].
unfold service_at; apply eq_bigl; red; intros cpu'.
fold (schedule_prefix job_cost num_cpus arr_seq higher_eq_priority).
by rewrite 2?scheduler_same_prefix ?leqnn //.
by rewrite /scheduled_on 2?scheduler_same_prefix ?leqnn //.
}
Qed.
......@@ -203,9 +203,10 @@ Module ConcreteScheduler.
unfold pending; f_equal; f_equal.
unfold completed; f_equal.
unfold service; apply eq_big_nat; move => i /andP [_ LTi].
unfold service_at; apply eq_bigl; red; intro cpu; f_equal.
unfold service_at; apply eq_bigl; red; intro cpu.
unfold scheduled_on; f_equal.
fold (schedule_prefix job_cost num_cpus arr_seq higher_eq_priority).
by rewrite scheduler_same_prefix //.
by rewrite scheduler_same_prefix.
}
Qed.
......@@ -293,6 +294,7 @@ Module ConcreteScheduler.
rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
apply eq_bigr; move => i /andP [/andP [_ LT] _].
apply eq_bigl; red; ins.
unfold scheduled_on; f_equal.
fold (schedule_prefix job_cost num_cpus arr_seq higher_eq_priority).
by rewrite scheduler_same_prefix.
}
......
......@@ -146,6 +146,7 @@ Module ConcreteScheduler.
unfold completed, service; f_equal.
apply eq_big_nat; move => t0 /andP [_ LT].
unfold service_at; apply eq_bigl; red; intros cpu'.
unfold scheduled_on; f_equal.
fold (schedule_prefix job_cost job_jitter num_cpus arr_seq higher_eq_priority).
by rewrite 2?scheduler_same_prefix ?leqnn //.
}
......@@ -207,7 +208,8 @@ Module ConcreteScheduler.
unfold pending; f_equal; f_equal.
unfold completed; f_equal.
unfold service; apply eq_big_nat; move => i /andP [_ LTi].
unfold service_at; apply eq_bigl; red; intro cpu; f_equal.
unfold service_at; apply eq_bigl; red; intro cpu.
unfold scheduled_on; f_equal.
fold (schedule_prefix job_cost job_jitter num_cpus arr_seq higher_eq_priority).
by rewrite scheduler_same_prefix //.
}
......@@ -295,6 +297,7 @@ Module ConcreteScheduler.
rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
apply eq_bigr; move => i /andP [/andP [_ LT] _].
apply eq_bigl; red; ins.
unfold scheduled_on; f_equal.
fold (schedule_prefix job_cost job_jitter num_cpus arr_seq higher_eq_priority).
by rewrite scheduler_same_prefix.
}
......
......@@ -192,6 +192,7 @@ Module Interference.
rename SCHED into EQtsk0, Heq into SCHED; move: EQtsk0 => /eqP EQtsk0.
assert (SCHEDULED: scheduled sched j0 t).
{
unfold scheduled, scheduled_on.
apply/existsP; exists x; apply/andP; split; [by done | by rewrite SCHED eq_refl].
}
rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
......@@ -224,7 +225,7 @@ Module Interference.
apply negbTE; rewrite negb_exists; apply/forallP.
intros x; rewrite negb_and.
specialize (BACK x); rewrite negb_and in BACK; ins.
unfold schedules_job_of_tsk in BACK.
unfold schedules_job_of_tsk in BACK; unfold scheduled_on.
destruct (sched x t) eqn:SCHED; last by ins.
apply/negP; unfold not; move => /eqP BUG; inversion BUG; subst.
by move: Heq => /eqP Heq; rewrite Heq eq_refl in BACK.
......@@ -258,6 +259,7 @@ Module Interference.
rewrite -addn1 addnC; apply leq_add; last by done.
rewrite EQtsk0 eq_refl BACK andTb.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
unfold scheduled, scheduled_on.
by apply/exists_inP; exists x; [by done | by rewrite SCHED].
}
{
......
......@@ -49,7 +49,7 @@ Module Schedule.
(* A job j is scheduled at time t iff there exists a cpu where it is mapped.*)
Definition scheduled (t: time) :=
[exists cpu in 'I_(num_cpus), sched cpu t == Some j].
[exists cpu in 'I_(num_cpus), scheduled_on cpu t].
(* A processor cpu is idle at time t if it doesn't contain any jobs. *)
Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
......@@ -59,7 +59,7 @@ Module Schedule.
where it is scheduled on. Note that we use a sum to account for
parallelism if required. *)
Definition service_at (t: time) :=
\sum_(cpu < num_cpus | sched cpu t == Some j) 1.
\sum_(cpu < num_cpus | scheduled_on cpu t) 1.
(* The cumulative service received by job j during [0, t'). *)
Definition service (t': time) := \sum_(0 <= t < t') service_at t.
......@@ -147,7 +147,7 @@ Module Schedule.
forall t,
~~ scheduled sched j t = (service_at sched j t == 0).
Proof.
unfold scheduled, service_at; intros t; apply/idP/idP.
unfold scheduled, service_at, scheduled_on; intros t; apply/idP/idP.
{
intros NOTSCHED.
rewrite negb_exists_in in NOTSCHED.
......@@ -343,6 +343,7 @@ Module Schedule.
rewrite -> eq_bigr with (F2 := fun cpu => 0);
first by rewrite big_const_seq iter_addn mul0n addn0.
intros i SCHED; move: ARR; rewrite negb_exists_in; move => /forall_inP ARR.
unfold scheduled_on in *.
by exploit (ARR i); [by ins | ins]; destruct (sched i t == Some j).
Qed.
......@@ -429,7 +430,7 @@ Module Schedule.
forall j t,
j \in jobs_scheduled_at sched t = scheduled sched j t.
Proof.
unfold jobs_scheduled_at, scheduled.
unfold jobs_scheduled_at, scheduled, scheduled_on.
intros j t; apply/idP/idP.
{
intros IN.
......
......@@ -170,6 +170,7 @@ Module Interference.
rename SCHED into EQtsk0, Heq into SCHED; move: EQtsk0 => /eqP EQtsk0.
assert (SCHEDULED: scheduled sched j0 t).
{
unfold scheduled, scheduled_on.
apply/existsP; exists x; apply/andP; split; [by done | by rewrite SCHED eq_refl].
}
rewrite big_mkcond (bigD1_seq j0) /=; last by rewrite undup_uniq.
......@@ -202,7 +203,7 @@ Module Interference.
apply negbTE; rewrite negb_exists; apply/forallP.
intros x; rewrite negb_and.
specialize (BACK x); rewrite negb_and in BACK; ins.
unfold schedules_job_of_tsk in BACK.
unfold schedules_job_of_tsk in BACK; unfold scheduled_on.
destruct (sched x t) eqn:SCHED; last by ins.
apply/negP; unfold not; move => /eqP BUG; inversion BUG; subst.
by move: Heq => /eqP Heq; rewrite Heq eq_refl in BACK.
......@@ -236,6 +237,7 @@ Module Interference.
rewrite -addn1 addnC; apply leq_add; last by done.
rewrite EQtsk0 eq_refl BACK andTb.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
unfold scheduled, scheduled_on.
by apply/exists_inP; exists x; [by done | by rewrite SCHED].
}
{
......
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