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

Cleanup

parent 65dfc546
......@@ -64,7 +64,7 @@ Module ResponseTimeIterationFP.
(* The schedulability test simply checks if we got a list of
response-time bounds (i.e., if the computation did not fail). *)
Definition fp_schedulability_test (ts: sporadic_taskset) :=
Definition fp_schedulable (ts: sporadic_taskset) :=
R_list ts != None.
Section AuxiliaryLemmas.
......@@ -522,139 +522,145 @@ Module ResponseTimeIterationFP.
is_interfering_task_fp tsk higher_eq_priority tsk_other &&
task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
Definition no_deadline_missed_by (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task
rate sched tsk.
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline rate sched.
(* Now we prove correctness of the schedulability test. *)
Lemma R_list_has_response_time_bounds :
forall rt_bounds tsk R,
R_list ts = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
Proof.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR,
H_completed_jobs_dont_execute into COMP,
H_jobs_must_arrive_to_execute into MUSTARRIVE,
H_global_scheduling_invariant into INVARIANT,
H_sorted_ts into SORT,
H_transitive into TRANS,
H_unique_priorities into UNIQ,
H_total into TOTAL,
H_all_jobs_from_taskset into ALLJOBS,
H_ts_is_a_set into SET.
clear ALLJOBS.
Section HelperLemma.
unfold fp_schedulability_test, R_list in *.
induction ts as [| ts' tsk_i] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk R SOME IN j JOBj.
destruct (lastP rt_bounds) as [| hp_bounds (tsk_lst, R_lst)];
first by rewrite in_nil in IN.
rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | BEGINNING]; last first.
(* The following lemma states that the response-time bounds
computed using R_list are valid. *)
Lemma R_list_has_response_time_bounds :
forall rt_bounds tsk R,
R_list ts = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
Proof.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR,
H_completed_jobs_dont_execute into COMP,
H_jobs_must_arrive_to_execute into MUSTARRIVE,
H_global_scheduling_invariant into INVARIANT,
H_sorted_ts into SORT,
H_transitive into TRANS,
H_unique_priorities into UNIQ,
H_total into TOTAL,
H_all_jobs_from_taskset into ALLJOBS,
H_ts_is_a_set into SET.
clear ALLJOBS.
unfold fp_schedulable, R_list in *.
induction ts as [| ts' tsk_i] using last_ind.
{
apply IHs with (rt_bounds := hp_bounds) (tsk := tsk); try (by ins).
by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
by ins; red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
by apply sorted_rcons_prefix in SORT.
{
intros tsk0 j0 t IN0 JOB0 BACK0.
exploit (INVARIANT tsk0 j0 t); try (by ins);
[by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
rewrite -cats1 count_cat /= in INV.
unfold is_interfering_task_fp in INV.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
assert (HP: higher_eq_priority tsk_lst tsk0 = false).
{
apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
apply negbTE; apply/negP; unfold not; intro BUG.
exploit UNIQ; [by apply/andP; split; [by apply SORT | by ins] | intro EQ].
by rewrite rcons_uniq -EQ IN0 in SET.
}
by rewrite HP 2!andFb 2!addn0 in INV.
}
by apply R_list_rcons_prefix in SOME.
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
move: LAST => /eqP LAST.
inversion LAST as [[EQ1 EQ2]].
rewrite -> EQ1 in *; rewrite -> EQ2 in *; clear EQ1 EQ2 LAST.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
generalize SOME; apply R_list_rcons_prefix in SOME; intro SOME'.
have BOUND := bertogna_cirinei_response_time_bound_fp.
unfold is_response_time_bound_of_task, job_has_completed_by in BOUND.
apply BOUND with (job_deadline := job_deadline) (job_task := job_task) (tsk := tsk_lst)
(ts := rcons ts' tsk_lst) (hp_bounds := hp_bounds)
(higher_eq_priority := higher_eq_priority); clear BOUND; try (by ins).
by apply R_list_unzip1 with (R := R_lst).
intros rt_bounds tsk R SOME IN j JOBj.
destruct (lastP rt_bounds) as [| hp_bounds (tsk_lst, R_lst)];
first by rewrite in_nil in IN.
rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | BEGINNING]; last first.
{
intros hp_tsk R0 HP j0 JOB0.
apply IHs with (rt_bounds := hp_bounds) (tsk := hp_tsk); try (by ins).
apply IHs with (rt_bounds := hp_bounds) (tsk := tsk); try (by ins).
by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
by red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
by ins; red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
by apply sorted_rcons_prefix in SORT.
{
intros tsk0 j1 t IN0 JOB1 BACK0.
exploit (INVARIANT tsk0 j1 t); try (by ins);
intros tsk0 j0 t IN0 JOB0 BACK0.
exploit (INVARIANT tsk0 j0 t); try (by ins);
[by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
rewrite -cats1 count_cat /= addn0 in INV.
rewrite -cats1 count_cat /= in INV.
unfold is_interfering_task_fp in INV.
assert (NOINTERF: higher_eq_priority tsk_lst tsk0 = false).
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
assert (HP: higher_eq_priority tsk_lst tsk0 = false).
{
apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
apply negbTE; apply/negP; unfold not; intro BUG.
exploit UNIQ; [by apply/andP; split; [by apply BUG | by ins] | intro EQ].
by rewrite rcons_uniq EQ IN0 in SET.
}
by rewrite NOINTERF 2!andFb addn0 in INV.
exploit UNIQ; [by apply/andP; split; [by apply SORT | by ins] | intro EQ].
by rewrite rcons_uniq -EQ IN0 in SET.
}
by rewrite HP 2!andFb 2!addn0 in INV.
}
by apply R_list_rcons_prefix in SOME.
}
by ins; apply R_list_ge_cost with (ts' := ts') (rt_bounds := hp_bounds).
by ins; apply R_list_le_deadline with (ts' := ts') (rt_bounds := hp_bounds).
{
ins; exploit (INVARIANT tsk_lst j0 t); try (by ins).
by rewrite mem_rcons in_cons; apply/orP; left.
}
{
rewrite [R_lst](R_list_rcons_response_time ts' hp_bounds tsk_lst); last by ins.
rewrite per_task_rta_fold.
apply per_task_rta_converges with (ts' := ts'); try (by ins).
move: LAST => /eqP LAST.
inversion LAST as [[EQ1 EQ2]].
rewrite -> EQ1 in *; rewrite -> EQ2 in *; clear EQ1 EQ2 LAST.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
generalize SOME; apply R_list_rcons_prefix in SOME; intro SOME'.
have BOUND := bertogna_cirinei_response_time_bound_fp.
unfold is_response_time_bound_of_task, job_has_completed_by in BOUND.
apply BOUND with (job_deadline := job_deadline) (job_task := job_task) (tsk := tsk_lst)
(ts := rcons ts' tsk_lst) (hp_bounds := hp_bounds)
(higher_eq_priority := higher_eq_priority); clear BOUND; try (by ins).
by apply R_list_unzip1 with (R := R_lst).
{
red; ins; apply TASKPARAMS.
by rewrite mem_rcons in_cons; apply/orP; right.
intros hp_tsk R0 HP j0 JOB0.
apply IHs with (rt_bounds := hp_bounds) (tsk := hp_tsk); try (by ins).
by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
by red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
by apply sorted_rcons_prefix in SORT.
{
intros tsk0 j1 t IN0 JOB1 BACK0.
exploit (INVARIANT tsk0 j1 t); try (by ins);
[by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
rewrite -cats1 count_cat /= addn0 in INV.
unfold is_interfering_task_fp in INV.
assert (NOINTERF: higher_eq_priority tsk_lst tsk0 = false).
{
apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
apply negbTE; apply/negP; unfold not; intro BUG.
exploit UNIQ; [by apply/andP; split; [by apply BUG | by ins] | intro EQ].
by rewrite rcons_uniq EQ IN0 in SET.
}
by rewrite NOINTERF 2!andFb addn0 in INV.
}
}
by ins; apply R_list_ge_cost with (ts' := ts') (rt_bounds := hp_bounds).
by ins; apply R_list_le_deadline with (ts' := ts') (rt_bounds := hp_bounds).
{
ins; exploit (INVARIANT tsk_lst j0 t); try (by ins).
by rewrite mem_rcons in_cons; apply/orP; left.
}
apply R_list_le_deadline with (ts' := rcons ts' tsk_lst)
{
rewrite [R_lst](R_list_rcons_response_time ts' hp_bounds tsk_lst); last by ins.
rewrite per_task_rta_fold.
apply per_task_rta_converges with (ts' := ts'); try (by ins).
{
red; ins; apply TASKPARAMS.
by rewrite mem_rcons in_cons; apply/orP; right.
}
apply R_list_le_deadline with (ts' := rcons ts' tsk_lst)
(rt_bounds := rcons hp_bounds (tsk_lst, R_lst));
first by apply SOME'.
rewrite mem_rcons in_cons; apply/orP; left; apply/eqP.
f_equal; symmetry.
by apply R_list_rcons_response_time with (ts' := ts').
first by apply SOME'.
rewrite mem_rcons in_cons; apply/orP; left; apply/eqP.
f_equal; symmetry.
by apply R_list_rcons_response_time with (ts' := ts').
}
}
}
}
Qed.
Qed.
(* Finally, we show that if the schedulability test suceeds, ...*)
Hypothesis H_test_passes: fp_schedulability_test ts.
End HelperLemma.
(* If the schedulability test suceeds, ...*)
Hypothesis H_test_succeeds: fp_schedulable ts.
(*..., then no task misses its deadline. *)
(*..., then no task misses its deadline,... *)
Theorem taskset_schedulable_by_fp_rta :
forall tsk, tsk \in ts -> no_deadline_missed_by tsk.
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
unfold no_deadline_missed_by, task_misses_no_deadline,
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
fp_schedulability_test,
fp_schedulable,
valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
......@@ -667,7 +673,7 @@ Module ResponseTimeIterationFP.
H_unique_priorities into UNIQ,
H_total into TOTAL,
H_all_jobs_from_taskset into ALLJOBS,
H_test_passes into TEST.
H_test_succeeds into TEST.
move => tsk INtsk j /eqP JOBtsk.
have RLIST := (R_list_has_response_time_bounds).
......@@ -691,6 +697,43 @@ Module ResponseTimeIterationFP.
by apply COMPLETED.
Qed.
(* ..., and the schedulability test yields safe response-time
bounds for each task. *)
Theorem fp_schedulability_test_yields_response_time_bounds :
forall tsk,
tsk \in ts ->
exists R,
R <= task_deadline tsk /\
forall (j: JobIn arr_seq),
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
Proof.
intros tsk IN.
unfold fp_schedulable in *.
have TASKS := R_list_non_empty ts.
have BOUNDS := (R_list_has_response_time_bounds).
have DL := (R_list_le_deadline ts).
destruct (R_list ts) as [rt_bounds |]; last by ins.
exploit (TASKS rt_bounds tsk); [by ins | clear TASKS; intro EX].
destruct EX as [EX _]; specialize (EX IN); des.
exists R; split.
by apply DL with (rt_bounds0 := rt_bounds).
by ins; apply (BOUNDS rt_bounds tsk).
Qed.
(* For completeness, since all jobs of the arrival sequence
are spawned by the task set, we conclude that no job misses
its deadline. *)
Theorem jobs_schedulable_by_fp_rta :
forall (j: JobIn arr_seq), no_deadline_missed_by_job j.
Proof.
intros j.
have SCHED := taskset_schedulable_by_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
apply SCHED with (tsk := job_task j); last by rewrite eq_refl.
by apply H_all_jobs_from_taskset.
Qed.
End Proof.
End ResponseTimeIterationFP.
\ 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