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

Define work conserving and prove that for EDF scheduling invariant

parent 30cac1cb
......@@ -67,6 +67,17 @@ Module Platform.
End JLDP.
Section WorkConserving.
(* A scheduler is work-conserving iff when a job j is backlogged,
all processors are busy with other jobs. *)
Definition is_work_conserving :=
forall (j: JobIn arr_seq) (t: time),
backlogged job_cost sched j t ->
size (jobs_scheduled_at sched t) = num_cpus.
End WorkConserving.
Section Lemmas.
Section InterferingJobHasHigherPriority.
......@@ -188,6 +199,7 @@ Module Platform.
jobs_of_same_task_dont_execute_in_parallel,
jobs_dont_execute_in_parallel in *.
clear PREC.
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);
......@@ -238,9 +250,10 @@ Module Platform.
destruct (ltnP (job_arrival j) (job_arrival j_hp)) as [LTarr | GEarr].
{
move: BACK => /andP [PEND NOTSCHED].
apply PREC with (t := t) in LTarr;
admit.
(*apply PREC with (t := t) in LTarr;
[ | by rewrite SAMEtsk JOBtsk | by done].
by rewrite SCHED in LTarr.
by rewrite SCHED in LTarr.*)
} subst tsk.
exploit (SPO j_hp j); try (by done).
{
......
......@@ -346,6 +346,27 @@ Module PlatformEDF.
End JobInvariantAsTaskInvariant.*)
Section WorkConserving.
(* We show that the EDF scheduling invariant implies work conservation. *)
Lemma edf_invariant_implies_work_conservation:
is_work_conserving job_cost num_cpus sched.
Proof.
rename H_global_scheduling_invariant into INV.
unfold is_work_conserving,
JLFP_JLDP_scheduling_invariant_holds in *.
intros j t BACK.
specialize (INV j t BACK).
apply/eqP; rewrite eqn_leq; apply/andP; split;
first by apply num_scheduled_jobs_le_num_cpus.
eapply leq_trans;
first by apply eq_leq; symmetry; apply INV.
by apply leq_trans with (n := count predT (jobs_scheduled_at sched t));
[by apply sub_count | by apply count_size].
Qed.
End WorkConserving.
End Lemmas.
End PlatformEDF.
\ No newline at end of file
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