diff --git a/implementation/basic/schedule.v b/implementation/basic/schedule.v
index 8435ae225fd7c11d447bdcbac8dde1944dd041bb..0a546122efc26c66e8bf56c1b450637ae492cc7e 100644
--- a/implementation/basic/schedule.v
+++ b/implementation/basic/schedule.v
@@ -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.
}
diff --git a/implementation/jitter/schedule.v b/implementation/jitter/schedule.v
index 21d18bb3a81e951da845cf7c5edc7b2a5d4c9d76..72a593d1b4cc096e988a364064a1e199069c5d2a 100644
--- a/implementation/jitter/schedule.v
+++ b/implementation/jitter/schedule.v
@@ -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.
}
diff --git a/model/basic/interference.v b/model/basic/interference.v
index df50ade5e10b5e54184073af2d8695f94bd7f015..f9d92cb7d25e205d2867430da5f95bf4a0474839 100644
--- a/model/basic/interference.v
+++ b/model/basic/interference.v
@@ -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].
}
{
diff --git a/model/basic/schedule.v b/model/basic/schedule.v
index ae17d3efc8cb37179e6cc02dc513bed07ada1ca5..7ac13307904927dfea87c3338bea30bad0886066 100644
--- a/model/basic/schedule.v
+++ b/model/basic/schedule.v
@@ -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.
diff --git a/model/jitter/interference.v b/model/jitter/interference.v
index b428c33467ea419f95cbdf3cc84e6b38c941beed..6c6fedc5df3ee1fc8f586f27d9e591917bd87d61 100644
--- a/model/jitter/interference.v
+++ b/model/jitter/interference.v
@@ -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].
}
{