Commit 02b83aea authored by Felipe Cerqueira's avatar Felipe Cerqueira

Incomplete proof of task scheduling invariant

parent 6083f8e5
Require Import Vbase task schedule job priority interference util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop.
ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module Platform.
......@@ -104,13 +104,65 @@ Module Platform.
by rewrite ltnn in BUG.
Qed.
(* Assume all jobs are from the taskset ... *)
Hypothesis all_jobs_from_taskset:
(* Assume the task set has no duplicates. *)
Hypothesis H_ts_is_a_set: uniq ts.
(* Assume all jobs are from the taskset, ... *)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
(* ... and jobs from the same task don't execute in parallel. *)
Hypothesis no_intra_task_parallelism:
(* ..., a single job does not execute in parallel, ...*)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* ... and jobs from the same task do not execute in parallel. *)
Hypothesis H_no_intra_task_parallelism:
jobs_of_same_task_dont_execute_in_parallel job_task sched.
Lemma scheduled_jobs_unique :
jobs_dont_execute_in_parallel sched ->
forall t,
uniq (jobs_scheduled_at sched t).
Proof.
intros _ t; rename H_no_parallelism into SEQUENTIAL.
unfold jobs_dont_execute_in_parallel in SEQUENTIAL.
clear -SEQUENTIAL.
unfold jobs_scheduled_at.
induction num_cpus; first by rewrite big_ord0.
{
rewrite big_ord_recr cat_uniq; apply/andP; split.
{
apply bigcat_ord_uniq;
first by intro i; unfold make_sequence; desf.
intros x i1 i2 IN1 IN2; unfold make_sequence in *.
desf; move: Heq0 Heq => SOME1 SOME2.
rewrite mem_seq1 in IN1; rewrite mem_seq1 in IN2.
move: IN1 IN2 => /eqP IN1 /eqP IN2; subst x j0.
specialize (SEQUENTIAL j t (widen_ord (leqnSn n) i1)
(widen_ord (leqnSn n) i2) SOME1 SOME2).
by inversion SEQUENTIAL; apply ord_inj.
}
apply/andP; split; last by unfold make_sequence; destruct (sched ord_max).
{
rewrite -all_predC; apply/allP; unfold predC; simpl.
intros x INx.
unfold make_sequence in INx.
destruct (sched ord_max t) eqn:SCHED;
last by rewrite in_nil in INx.
apply/negP; unfold not; intro IN'.
have EX := mem_bigcat_ord_exists _ x n.
apply EX in IN'; des; clear EX.
unfold make_sequence in IN'.
desf; rename Heq into SCHEDi.
rewrite mem_seq1 in INx; rewrite mem_seq1 in IN'.
move: INx IN' => /eqP INx /eqP IN'; subst x j0.
specialize (SEQUENTIAL j t ord_max (widen_ord (leqnSn n) i) SCHED SCHEDi).
inversion SEQUENTIAL; destruct i as [i EQ]; simpl in *.
clear SEQUENTIAL SCHEDi.
by rewrite H0 ltnn in EQ.
}
}
Qed.
(* If a job isn't scheduled, the processor are busy with interfering tasks. *)
Lemma cpus_busy_with_interfering_tasks :
forall (j: JobIn arr_seq) tsk t,
......@@ -122,29 +174,126 @@ Module Platform.
task_is_scheduled job_task sched j t)
ts = num_cpus.
Proof.
rename all_jobs_from_taskset into FROMTS,
no_intra_task_parallelism into NOINTRA,
rename H_all_jobs_from_taskset into FROMTS,
H_no_parallelism into SEQUENTIAL,
H_no_intra_task_parallelism into NOINTRA,
H_invariant_holds into INV.
unfold JLFP_JLDP_scheduling_invariant_holds in *.
intros j tsk t JOBtsk BACK.
apply eq_trans with (y := count (fun j_other => higher_eq_priority t j_other j) (jobs_scheduled_at sched t));
last by apply INV.
unfold jobs_scheduled_at, task_is_scheduled.
induction num_cpus.
rewrite <- INV with (j := j) (t := t); last by done.
assert (EQ: (preim (fun j0 : JobIn arr_seq => job_task j0)
(fun j0 : sporadic_task =>
is_interfering_task_jlfp tsk j0 &&
task_is_scheduled job_task sched j0 t)) =1 (fun j0 => higher_eq_priority t j0 j && (j0 \in jobs_scheduled_at sched t))).
{
rewrite big_ord0 /=.
apply eq_trans with (y := count pred0 ts); last by apply count_pred0.
apply eq_count; red; ins.
apply negbTE; rewrite negb_and; apply/orP; right.
apply/negP; red; intro BUG; move: BUG => /existsP BUG.
by destruct BUG as [x0]; destruct x0.
red; intro j'; unfold preim; simpl.
destruct (j' \in jobs_scheduled_at sched t) eqn:SCHED'.
{
rewrite SCHED'.
destruct (higher_eq_priority t j' j) eqn:HP'.
{
rewrite andbT; apply/andP; split.
{
unfold is_interfering_task_jlfp; apply/eqP; red; intro BUG.
subst tsk.
(* This requires further assumptions. *)
admit.
}
{
unfold jobs_scheduled_at in *.
apply mem_bigcat_ord_exists in SCHED'; des.
apply/exists_inP; exists i; first by done.
unfold schedules_job_of_tsk, make_sequence in *.
destruct (sched i t); last by done.
by rewrite mem_seq1 in SCHED'; move: SCHED' => /eqP EQj; subst.
}
}
{
exfalso; apply negbT in HP'; move: HP' => /negP HP'; apply HP'.
apply interfering_job_has_higher_eq_prio; first by done.
apply mem_bigcat_ord_exists in SCHED'; des.
unfold scheduled, jobs_scheduled_at, make_sequence in *.
apply/exists_inP; exists i; first by done.
destruct (sched i t); last by done.
by rewrite mem_seq1 in SCHED'; move: SCHED' => /eqP EQj; subst.
}
}
{
destruct (is_interfering_task_jlfp tsk (job_task j')) eqn:INTERF'.
{
rewrite andTb SCHED' andbF.
admit. (* This requires further assumptions. *)
}
{
by rewrite SCHED' andbF andFb.
}
}
}
rewrite -[count _ (jobs_scheduled_at _ _)]size_filter.
assert (SUBST: [seq j_other <- jobs_scheduled_at sched t | higher_eq_priority t j_other j] = [seq j_other <- jobs_scheduled_at sched t | higher_eq_priority t j_other j && (j_other \in jobs_scheduled_at sched t)]).
{
rewrite big_ord_recr /=.
admit.
}
by apply eq_in_filter; red; intros x IN; rewrite IN andbT.
}
rewrite SUBST; clear SUBST.
rewrite size_filter.
rewrite -(eq_count EQ).
rewrite -[count _ (jobs_scheduled_at _ _)]count_filter.
rewrite -count_filter.
rewrite -[count _ [seq _ <- jobs_scheduled_at _ _ | _]]count_map.
apply/perm_eqP.
apply uniq_perm_eq; first by apply filter_uniq.
{
rewrite map_inj_in_uniq;
first by apply filter_uniq; apply scheduled_jobs_unique.
unfold jobs_of_same_task_dont_execute_in_parallel in NOINTRA.
red; intros x y INx INy EQtask.
apply NOINTRA with (t := t); try (by done).
{
rewrite mem_filter in INx; move: INx => /andP [_ SCHEDx].
apply mem_bigcat_ord_exists in SCHEDx; destruct SCHEDx as [cpu SCHEDx].
apply/existsP; exists cpu; apply/andP; split; first by done.
by unfold make_sequence in SCHEDx; destruct (sched cpu t);
[ by rewrite mem_seq1 eq_sym in SCHEDx; apply/eqP; f_equal; apply/eqP
| by rewrite in_nil in SCHEDx].
}
{
rewrite mem_filter in INy; move: INy => /andP [_ SCHEDy].
apply mem_bigcat_ord_exists in SCHEDy; destruct SCHEDy as [cpu SCHEDy].
apply/existsP; exists cpu; apply/andP; split; first by done.
by unfold make_sequence in SCHEDy; destruct (sched cpu t);
[ by rewrite mem_seq1 eq_sym in SCHEDy; apply/eqP; f_equal; apply/eqP
| by rewrite in_nil in SCHEDy].
}
}
{
red; intro x; apply/idP/idP.
{
unfold task_is_scheduled in *.
intros IN; rewrite mem_filter in IN; move: IN => /andP [/exists_inP SCHED IN].
destruct SCHED as [cpu INcpu SCHED].
generalize SCHED; intro SCHEDjob.
unfold schedules_job_of_tsk in SCHEDjob.
destruct (sched cpu t) as [j'|] eqn:SCHEDj'; last by done.
move: SCHEDjob => /eqP SCHEDjob; subst x.
apply/mapP; exists j'; last by done.
rewrite mem_filter; apply/andP; split;
first by apply/exists_inP; exists cpu.
unfold jobs_scheduled_at.
apply mem_bigcat_ord with (j := cpu); first by apply ltn_ord.
by unfold make_sequence; rewrite SCHEDj' mem_seq1 eq_refl.
}
{
intros IN; rewrite mem_filter.
move: IN => /mapP IN; destruct IN as [j' IN]; subst x.
rewrite mem_filter in IN; move: IN => /andP [SCHEDj' IN].
apply/andP; split; first by done.
by apply FROMTS.
}
}
Qed.
End BasicLemmas.
End JLDP.
......
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