Library prosa.classic.analysis.global.parallel.bertogna_fp_comp
Require Import prosa.classic.util.all.
Require Import prosa.classic.analysis.global.parallel.bertogna_fp_theory.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
Import ResponseTimeAnalysisFP.
Section Analysis.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Let task_with_response_time := (sporadic_task × time)%type.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Variable higher_priority: FP_policy sporadic_task.
Definition per_task_rta (tsk: sporadic_task)
(R_prev: seq task_with_response_time) (step: nat) :=
iter step
(fun t ⇒ task_cost tsk +
div_floor
(total_interference_bound_fp task_cost task_period R_prev t)
num_cpus)
(task_cost tsk).
Definition max_steps (tsk: sporadic_task) := task_deadline tsk - task_cost tsk + 1.
Definition fp_bound_of_task hp_pairs tsk :=
if hp_pairs is Some rt_bounds then
let R := per_task_rta tsk rt_bounds (max_steps tsk) in
if R ≤ task_deadline tsk then
Some (rcons rt_bounds (tsk, R))
else None
else None.
Definition fp_claimed_bounds (ts: seq sporadic_task) :=
foldl fp_bound_of_task (Some [::]) ts.
Definition fp_schedulable (ts: seq sporadic_task) :=
fp_claimed_bounds ts != None.
Section SimpleLemmas.
Lemma fp_claimed_bounds_unzip :
∀ ts hp_bounds,
fp_claimed_bounds ts = Some hp_bounds →
unzip1 hp_bounds = ts.
Proof.
unfold fp_claimed_bounds in *; intros ts.
induction ts using last_ind; first by destruct hp_bounds.
{
intros hp_bounds SOME.
destruct (lastP hp_bounds) as [| hp_bounds'].
{
rewrite -cats1 foldl_cat /= in SOME.
unfold fp_bound_of_task at 1 in SOME; simpl in *; desf.
by destruct l.
}
rewrite -cats1 foldl_cat /= in SOME.
unfold fp_bound_of_task at 1 in SOME; simpl in *; desf.
move: H0 ⇒ /eqP EQSEQ.
rewrite eqseq_rcons in EQSEQ.
move: EQSEQ ⇒ /andP [/eqP SUBST /eqP EQSEQ]; subst.
unfold unzip1; rewrite map_rcons; f_equal.
by apply IHts.
}
Qed.
Lemma fp_claimed_bounds_rcons :
∀ ts' hp_bounds tsk1 tsk2 R,
(fp_claimed_bounds (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) →
(fp_claimed_bounds ts' = Some hp_bounds ∧
tsk1 = tsk2 ∧
R = per_task_rta tsk1 hp_bounds (max_steps tsk1) ∧
R ≤ task_deadline tsk1)).
Proof.
intros ts hp_bounds tsk tsk' R.
rewrite -cats1.
unfold fp_claimed_bounds in ×.
rewrite foldl_cat /=.
unfold fp_bound_of_task at 1; simpl; desf.
intros EQ; inversion EQ; move: EQ H0 ⇒ _ /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ ⇒ /andP [/eqP EQ /eqP RESP].
by inversion RESP; repeat split; subst.
Qed.
Lemma fp_claimed_bounds_take :
∀ ts hp_bounds i,
fp_claimed_bounds ts = Some hp_bounds →
i ≤ size hp_bounds →
fp_claimed_bounds (take i ts) = Some (take i hp_bounds).
Proof.
intros ts hp_bounds i SOME LTi.
have UNZIP := fp_claimed_bounds_unzip ts hp_bounds SOME.
rewrite <- UNZIP in ×.
rewrite -[hp_bounds]take_size /unzip1 map_take in SOME.
fold (unzip1 hp_bounds) in *; clear UNZIP.
rewrite leq_eqVlt in LTi.
move: LTi ⇒ /orP [/eqP EQ | LTi]; first by subst.
remember (size hp_bounds) as len; apply eq_leq in Heqlen.
induction len; first by rewrite ltn0 in LTi.
{
assert (TAKElen: fp_claimed_bounds (take len (unzip1 (hp_bounds))) =
Some (take len (hp_bounds))).
{
assert (∃ p, p \in hp_bounds).
{
destruct hp_bounds; first by rewrite ltn0 in Heqlen.
by ∃ t; rewrite in_cons eq_refl orTb.
} destruct H as [[tsk R] _].
rewrite (take_nth tsk) in SOME; last by rewrite size_map.
rewrite (take_nth (tsk,R)) in SOME; last by done.
destruct (nth (tsk, R) hp_bounds len) as [tsk_len R_len].
by apply fp_claimed_bounds_rcons in SOME; des.
}
rewrite ltnS leq_eqVlt in LTi.
move: LTi ⇒ /orP [/eqP EQ | LESS]; first by subst.
apply ltnW in Heqlen.
by specialize (IHlen Heqlen TAKElen LESS).
}
Qed.
Lemma fp_claimed_bounds_le_deadline :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk_i R SOME IN.
destruct (lastP rt_bounds) as [|rt_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 | FRONT].
{
move: LAST ⇒ /eqP LAST.
rewrite -cats1 in SOME.
unfold fp_claimed_bounds in ×.
rewrite foldl_cat /= in SOME.
unfold fp_bound_of_task in SOME.
desf; rename H0 into EQ.
move: EQ ⇒ /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ ⇒ /andP [_ /eqP EQ].
inversion EQ; subst.
by apply Heq0.
}
{
apply IHts with (rt_bounds := rt_bounds); last by ins.
by apply fp_claimed_bounds_rcons in SOME; des.
}
}
Qed.
Lemma fp_claimed_bounds_ge_cost :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≥ task_cost tsk.
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk_i R SOME IN.
destruct (lastP rt_bounds) as [|rt_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 | FRONT].
{
move: LAST ⇒ /eqP LAST.
rewrite -cats1 in SOME.
unfold fp_claimed_bounds in ×.
rewrite foldl_cat /= in SOME.
unfold fp_bound_of_task in SOME.
desf; rename H0 into EQ.
move: EQ ⇒ /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ ⇒ /andP [_ /eqP EQ].
inversion EQ; subst.
by destruct (max_steps tsk_lst');
[by apply leqnn | by apply leq_addr].
}
{
apply IHts with (rt_bounds := rt_bounds); last by ins.
by apply fp_claimed_bounds_rcons in SOME; des.
}
}
Qed.
Lemma per_task_rta_fold :
∀ tsk rt_bounds,
task_cost tsk +
div_floor (total_interference_bound_fp task_cost task_period rt_bounds
(per_task_rta tsk rt_bounds (max_steps tsk))) num_cpus
= per_task_rta tsk rt_bounds (max_steps tsk).+1.
Proof.
by done.
Qed.
End SimpleLemmas.
Section HighPriorityTasks.
Variable ts: taskset_of sporadic_task.
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable hp_bounds: seq task_with_response_time.
Variable R: time.
Hypothesis H_analysis_succeeds: fp_claimed_bounds ts = Some hp_bounds.
Variable elem: sporadic_task.
Let TASK := nth elem ts.
Lemma fp_claimed_bounds_hp_tasks_have_smaller_index :
∀ hp_idx idx,
hp_idx < size ts →
idx < size ts →
hp_idx != idx →
higher_priority (TASK hp_idx) (TASK idx) →
hp_idx < idx.
Proof.
unfold TASK; clear TASK.
rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in ×.
intros hp_idx idx LThp LT NEQ HP.
rewrite ltn_neqAle; apply/andP; split; first by done.
by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
Qed.
End HighPriorityTasks.
Section Convergence.
Variable ts_hp: seq sporadic_task.
Variable rt_bounds: seq task_with_response_time.
Hypothesis H_test_succeeds: fp_claimed_bounds ts_hp = Some rt_bounds.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline (rcons ts_hp tsk).
Let f := per_task_rta tsk rt_bounds.
Hypothesis H_no_larger_than_deadline: f (max_steps tsk) ≤ task_deadline tsk.
Lemma bertogna_fp_comp_f_monotonic :
∀ x1 x2, x1 ≤ x2 → f x1 ≤ f x2.
Proof.
unfold valid_sporadic_taskset, is_valid_sporadic_task in ×.
rename H_test_succeeds into SOME,
H_valid_task_parameters into VALID.
intros x1 x2 LEx; unfold f, per_task_rta.
apply fun_mon_iter_mon; [by ins | by ins; apply leq_addr |].
clear LEx x1 x2; intros x1 x2 LEx.
rewrite leq_add2l leq_div2r //.
unfold total_interference_bound_fp.
rewrite big_seq_cond.
rewrite [\sum_(_ <- _ | true) _]big_seq_cond.
apply leq_sum; move ⇒ i /andP [IN _].
destruct i as [i R].
have GE_COST := fp_claimed_bounds_ge_cost ts_hp rt_bounds i R SOME IN.
have UNZIP := fp_claimed_bounds_unzip ts_hp rt_bounds SOME.
unfold interference_bound_generic; simpl.
apply W_monotonic; try (by done).
have INts: i \in ts_hp by rewrite -UNZIP; apply/mapP; ∃ (i, R).
by exploit (VALID i);
[by rewrite mem_rcons in_cons INts orbT | by ins; des].
Qed.
Lemma bertogna_fp_comp_f_converges_early :
(∃ k, k ≤ max_steps tsk ∧ f k = f k.+1) →
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed.
Section DerivingContradiction.
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps tsk → f k != f k.+1.
Lemma bertogna_fp_comp_f_increases :
∀ k,
k ≤ max_steps tsk →
f k < f k.+1.
Proof.
intros k LT.
rewrite ltn_neqAle; apply/andP; split.
by apply H_keeps_diverging.
by apply bertogna_fp_comp_f_monotonic, leqnSn.
Qed.
Lemma bertogna_fp_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps tsk →
f k > k + task_cost tsk - 1.
Proof.
have INC := bertogna_fp_comp_f_increases.
rename H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
induction k.
{
intros _; rewrite add0n -addn1 addnBAC;
first by rewrite -addnBA // subnn addn0 /= leqnn.
by apply PARAMS.
}
{
intros LT.
specialize (IHk (ltnW LT)).
apply leq_ltn_trans with (n := f k); last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
rewrite addnBAC in IHk;
last by apply leq_trans with (n := task_cost tsk);
[by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
}
Qed.
End DerivingContradiction.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
have TOOMUCH := bertogna_fp_comp_rt_grows_too_much.
have INC := bertogna_fp_comp_f_increases.
rename H_no_larger_than_deadline into LE,
H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
destruct ([∃ k in 'I_(max_steps tsk).+1, f k == f k.+1]) eqn:EX.
{
move: EX ⇒ /exists_inP EX; destruct EX as [k _ ITERk].
apply bertogna_fp_comp_f_converges_early.
by ∃ k; split; [by rewrite -ltnS; apply ltn_ord | by apply/eqP].
}
apply negbT in EX; rewrite negb_exists_in in EX.
move: EX ⇒ /forall_inP EX.
rewrite leqNgt in LE; move: LE ⇒ /negP LE.
exfalso; apply LE.
assert (DIFF: ∀ k : nat, k ≤ max_steps tsk → f k != f k.+1).
{
intros k LEk; rewrite -ltnS in LEk.
by exploit (EX (Ordinal LEk)); [by done | intro DIFF; apply DIFF].
}
exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
rewrite addnBAC; last by apply PARAMS2.
rewrite -addnBA // subnn addn0 subn1 prednK //.
intros LT; apply (leq_ltn_trans LT).
by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
Qed.
End Convergence.
Section MainProof.
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_is_total:
FP_is_total_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable sched: schedule Job num_cpus.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_respects_FP_policy:
respects_FP_policy job_arrival job_cost job_task arr_seq sched higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Theorem fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In fp_claimed_bounds ts →
response_time_bounded_by tsk R.
Proof.
rename H_valid_job_parameters into JOBPARAMS, H_valid_task_parameters into TASKPARAMS.
unfold valid_sporadic_taskset in ×.
intros tsk R MATCH.
assert (SOME: ∃ hp_bounds, fp_claimed_bounds ts = Some hp_bounds ∧
(tsk, R) \in hp_bounds).
{
destruct (fp_claimed_bounds ts); last by done.
by ∃ l; split.
} clear MATCH; des; rename SOME0 into IN.
have UNZIP := fp_claimed_bounds_unzip ts hp_bounds SOME.
set elem := (tsk,R).
move: IN ⇒ /(nthP elem) [idx LTidx EQ].
set NTH := fun k ⇒ nth elem hp_bounds k.
set TASK := fun k ⇒ (NTH k).1.
set RESP := fun k ⇒ (NTH k).2.
cut (response_time_bounded_by (TASK idx) (RESP idx));
first by unfold TASK, RESP, NTH; rewrite EQ.
clear EQ.
assert (PAIR: ∀ idx, (TASK idx, RESP idx) = NTH idx).
by intros i; unfold TASK, RESP; destruct (NTH i).
assert (SUBST: ∀ i, i < size hp_bounds → TASK i = nth tsk ts i).
by intros i LTi; rewrite /TASK /NTH -UNZIP (nth_map elem) //.
assert (SIZE: size hp_bounds = size ts).
by rewrite -UNZIP size_map.
induction idx as [idx IH'] using strong_ind.
assert (IH: ∀ tsk_hp R_hp, (tsk_hp, R_hp) \in take idx hp_bounds → response_time_bounded_by tsk_hp R_hp).
{
intros tsk_hp R_hp INhp.
move: INhp ⇒ /(nthP elem) [k LTk EQ].
rewrite size_take LTidx in LTk.
rewrite nth_take in EQ; last by done.
cut (response_time_bounded_by (TASK k) (RESP k));
first by unfold TASK, RESP, NTH; rewrite EQ.
by apply IH'; try (by done); apply (ltn_trans LTk).
} clear IH'.
unfold response_time_bounded_by in ×.
exploit (fp_claimed_bounds_rcons (take idx ts) (take idx hp_bounds) (TASK idx) (TASK idx) (RESP idx)).
{
by rewrite PAIR SUBST // -2?take_nth -?SIZE // (fp_claimed_bounds_take _ hp_bounds).
}
intros [_ [_ [REC DL]]].
try ( apply bertogna_cirinei_response_time_bound_fp with
(task_cost0 := task_cost) (task_period0 := task_period)
(task_deadline0 := task_deadline) (job_deadline0 := job_deadline) (tsk0 := (TASK idx))
(job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
(higher_eq_priority := higher_priority); try (by done) ) ||
apply bertogna_cirinei_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (job_deadline := job_deadline) (tsk := (TASK idx))
(job_task := job_task) (ts := ts) (hp_bounds := take idx hp_bounds)
(higher_eq_priority := higher_priority); try (by done).
{
cut (NTH idx \in hp_bounds = true);
[intros IN | by apply mem_nth].
by rewrite set_mem -UNZIP; apply/mapP; ∃ (TASK idx, RESP idx); rewrite PAIR.
}
{
intros hp_tsk IN INTERF.
∃ (RESP (index hp_tsk ts)).
move: (IN) ⇒ INDEX; apply nth_index with (x0 := tsk) in INDEX.
rewrite -{1}[hp_tsk]INDEX -SUBST; last by rewrite SIZE index_mem.
assert (UNIQ: uniq hp_bounds).
{
apply map_uniq with (f := fst); unfold unzip1 in *; rewrite UNZIP.
by destruct ts.
}
rewrite -filter_idx_lt_take //.
{
rewrite PAIR mem_filter; apply/andP; split;
last by apply mem_nth; rewrite SIZE index_mem.
{
rewrite /NTH index_uniq; [| by rewrite SIZE index_mem | by done ].
{
move: INTERF ⇒ /andP [HP NEQ].
apply fp_claimed_bounds_hp_tasks_have_smaller_index with
(ts := ts) (elem := tsk) (hp_bounds := hp_bounds);
try (by done);
[by rewrite index_mem | by rewrite -SIZE | | by rewrite INDEX -SUBST].
apply/eqP; intro BUG; subst idx.
rewrite SUBST -{1}INDEX in NEQ;
first by rewrite eq_refl in NEQ.
by rewrite SIZE index_mem INDEX.
}
}
}
}
{
rewrite REC per_task_rta_fold.
apply per_task_rta_converges with (ts_hp := take idx ts);
[by apply fp_claimed_bounds_take; try (by apply ltnW) | | by rewrite -REC ].
rewrite SUBST // -take_nth -?SIZE //.
by intros i IN; eapply TASKPARAMS, mem_take, IN.
}
Qed.
Hypothesis H_test_succeeds: fp_schedulable ts.
Theorem taskset_schedulable_by_fp_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Proof.
have RLIST := (fp_analysis_yields_response_time_bounds).
have UNZIP := (fp_claimed_bounds_unzip ts).
have DL := (fp_claimed_bounds_le_deadline ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
fp_schedulable, valid_sporadic_job in ×.
rename H_valid_job_parameters into JOBPARAMS.
move ⇒ tsk INtsk j ARRj JOBtsk.
destruct (fp_claimed_bounds ts) as [rt_bounds |]; last by ins.
feed (UNZIP rt_bounds); first by done.
assert (EX: ∃ R, (tsk, R) \in rt_bounds).
{
rewrite set_mem -UNZIP in INtsk; move: INtsk ⇒ /mapP EX.
by destruct EX as [p]; destruct p as [tsk' R]; simpl in *; subst tsk'; ∃ R.
} des.
exploit (RLIST tsk R); eauto 1; intro COMPLETED.
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in ×.
apply extend_sum; rewrite // leq_add2l.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
by done.
Qed.
Theorem jobs_schedulable_by_fp_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
Proof.
intros j ARRj.
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); try (by done).
by apply H_all_jobs_from_taskset.
Qed.
End MainProof.
End Analysis.
End ResponseTimeIterationFP.
Require Import prosa.classic.analysis.global.parallel.bertogna_fp_theory.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
Import ResponseTimeAnalysisFP.
Section Analysis.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Let task_with_response_time := (sporadic_task × time)%type.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Variable higher_priority: FP_policy sporadic_task.
Definition per_task_rta (tsk: sporadic_task)
(R_prev: seq task_with_response_time) (step: nat) :=
iter step
(fun t ⇒ task_cost tsk +
div_floor
(total_interference_bound_fp task_cost task_period R_prev t)
num_cpus)
(task_cost tsk).
Definition max_steps (tsk: sporadic_task) := task_deadline tsk - task_cost tsk + 1.
Definition fp_bound_of_task hp_pairs tsk :=
if hp_pairs is Some rt_bounds then
let R := per_task_rta tsk rt_bounds (max_steps tsk) in
if R ≤ task_deadline tsk then
Some (rcons rt_bounds (tsk, R))
else None
else None.
Definition fp_claimed_bounds (ts: seq sporadic_task) :=
foldl fp_bound_of_task (Some [::]) ts.
Definition fp_schedulable (ts: seq sporadic_task) :=
fp_claimed_bounds ts != None.
Section SimpleLemmas.
Lemma fp_claimed_bounds_unzip :
∀ ts hp_bounds,
fp_claimed_bounds ts = Some hp_bounds →
unzip1 hp_bounds = ts.
Proof.
unfold fp_claimed_bounds in *; intros ts.
induction ts using last_ind; first by destruct hp_bounds.
{
intros hp_bounds SOME.
destruct (lastP hp_bounds) as [| hp_bounds'].
{
rewrite -cats1 foldl_cat /= in SOME.
unfold fp_bound_of_task at 1 in SOME; simpl in *; desf.
by destruct l.
}
rewrite -cats1 foldl_cat /= in SOME.
unfold fp_bound_of_task at 1 in SOME; simpl in *; desf.
move: H0 ⇒ /eqP EQSEQ.
rewrite eqseq_rcons in EQSEQ.
move: EQSEQ ⇒ /andP [/eqP SUBST /eqP EQSEQ]; subst.
unfold unzip1; rewrite map_rcons; f_equal.
by apply IHts.
}
Qed.
Lemma fp_claimed_bounds_rcons :
∀ ts' hp_bounds tsk1 tsk2 R,
(fp_claimed_bounds (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) →
(fp_claimed_bounds ts' = Some hp_bounds ∧
tsk1 = tsk2 ∧
R = per_task_rta tsk1 hp_bounds (max_steps tsk1) ∧
R ≤ task_deadline tsk1)).
Proof.
intros ts hp_bounds tsk tsk' R.
rewrite -cats1.
unfold fp_claimed_bounds in ×.
rewrite foldl_cat /=.
unfold fp_bound_of_task at 1; simpl; desf.
intros EQ; inversion EQ; move: EQ H0 ⇒ _ /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ ⇒ /andP [/eqP EQ /eqP RESP].
by inversion RESP; repeat split; subst.
Qed.
Lemma fp_claimed_bounds_take :
∀ ts hp_bounds i,
fp_claimed_bounds ts = Some hp_bounds →
i ≤ size hp_bounds →
fp_claimed_bounds (take i ts) = Some (take i hp_bounds).
Proof.
intros ts hp_bounds i SOME LTi.
have UNZIP := fp_claimed_bounds_unzip ts hp_bounds SOME.
rewrite <- UNZIP in ×.
rewrite -[hp_bounds]take_size /unzip1 map_take in SOME.
fold (unzip1 hp_bounds) in *; clear UNZIP.
rewrite leq_eqVlt in LTi.
move: LTi ⇒ /orP [/eqP EQ | LTi]; first by subst.
remember (size hp_bounds) as len; apply eq_leq in Heqlen.
induction len; first by rewrite ltn0 in LTi.
{
assert (TAKElen: fp_claimed_bounds (take len (unzip1 (hp_bounds))) =
Some (take len (hp_bounds))).
{
assert (∃ p, p \in hp_bounds).
{
destruct hp_bounds; first by rewrite ltn0 in Heqlen.
by ∃ t; rewrite in_cons eq_refl orTb.
} destruct H as [[tsk R] _].
rewrite (take_nth tsk) in SOME; last by rewrite size_map.
rewrite (take_nth (tsk,R)) in SOME; last by done.
destruct (nth (tsk, R) hp_bounds len) as [tsk_len R_len].
by apply fp_claimed_bounds_rcons in SOME; des.
}
rewrite ltnS leq_eqVlt in LTi.
move: LTi ⇒ /orP [/eqP EQ | LESS]; first by subst.
apply ltnW in Heqlen.
by specialize (IHlen Heqlen TAKElen LESS).
}
Qed.
Lemma fp_claimed_bounds_le_deadline :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk_i R SOME IN.
destruct (lastP rt_bounds) as [|rt_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 | FRONT].
{
move: LAST ⇒ /eqP LAST.
rewrite -cats1 in SOME.
unfold fp_claimed_bounds in ×.
rewrite foldl_cat /= in SOME.
unfold fp_bound_of_task in SOME.
desf; rename H0 into EQ.
move: EQ ⇒ /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ ⇒ /andP [_ /eqP EQ].
inversion EQ; subst.
by apply Heq0.
}
{
apply IHts with (rt_bounds := rt_bounds); last by ins.
by apply fp_claimed_bounds_rcons in SOME; des.
}
}
Qed.
Lemma fp_claimed_bounds_ge_cost :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≥ task_cost tsk.
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
}
{
intros rt_bounds tsk_i R SOME IN.
destruct (lastP rt_bounds) as [|rt_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 | FRONT].
{
move: LAST ⇒ /eqP LAST.
rewrite -cats1 in SOME.
unfold fp_claimed_bounds in ×.
rewrite foldl_cat /= in SOME.
unfold fp_bound_of_task in SOME.
desf; rename H0 into EQ.
move: EQ ⇒ /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ ⇒ /andP [_ /eqP EQ].
inversion EQ; subst.
by destruct (max_steps tsk_lst');
[by apply leqnn | by apply leq_addr].
}
{
apply IHts with (rt_bounds := rt_bounds); last by ins.
by apply fp_claimed_bounds_rcons in SOME; des.
}
}
Qed.
Lemma per_task_rta_fold :
∀ tsk rt_bounds,
task_cost tsk +
div_floor (total_interference_bound_fp task_cost task_period rt_bounds
(per_task_rta tsk rt_bounds (max_steps tsk))) num_cpus
= per_task_rta tsk rt_bounds (max_steps tsk).+1.
Proof.
by done.
Qed.
End SimpleLemmas.
Section HighPriorityTasks.
Variable ts: taskset_of sporadic_task.
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable hp_bounds: seq task_with_response_time.
Variable R: time.
Hypothesis H_analysis_succeeds: fp_claimed_bounds ts = Some hp_bounds.
Variable elem: sporadic_task.
Let TASK := nth elem ts.
Lemma fp_claimed_bounds_hp_tasks_have_smaller_index :
∀ hp_idx idx,
hp_idx < size ts →
idx < size ts →
hp_idx != idx →
higher_priority (TASK hp_idx) (TASK idx) →
hp_idx < idx.
Proof.
unfold TASK; clear TASK.
rename ts into ts'; destruct ts' as [ts UNIQ]; simpl in ×.
intros hp_idx idx LThp LT NEQ HP.
rewrite ltn_neqAle; apply/andP; split; first by done.
by apply sorted_rel_implies_le_idx with (leT := higher_priority) (xs := ts) (default := elem).
Qed.
End HighPriorityTasks.
Section Convergence.
Variable ts_hp: seq sporadic_task.
Variable rt_bounds: seq task_with_response_time.
Hypothesis H_test_succeeds: fp_claimed_bounds ts_hp = Some rt_bounds.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline (rcons ts_hp tsk).
Let f := per_task_rta tsk rt_bounds.
Hypothesis H_no_larger_than_deadline: f (max_steps tsk) ≤ task_deadline tsk.
Lemma bertogna_fp_comp_f_monotonic :
∀ x1 x2, x1 ≤ x2 → f x1 ≤ f x2.
Proof.
unfold valid_sporadic_taskset, is_valid_sporadic_task in ×.
rename H_test_succeeds into SOME,
H_valid_task_parameters into VALID.
intros x1 x2 LEx; unfold f, per_task_rta.
apply fun_mon_iter_mon; [by ins | by ins; apply leq_addr |].
clear LEx x1 x2; intros x1 x2 LEx.
rewrite leq_add2l leq_div2r //.
unfold total_interference_bound_fp.
rewrite big_seq_cond.
rewrite [\sum_(_ <- _ | true) _]big_seq_cond.
apply leq_sum; move ⇒ i /andP [IN _].
destruct i as [i R].
have GE_COST := fp_claimed_bounds_ge_cost ts_hp rt_bounds i R SOME IN.
have UNZIP := fp_claimed_bounds_unzip ts_hp rt_bounds SOME.
unfold interference_bound_generic; simpl.
apply W_monotonic; try (by done).
have INts: i \in ts_hp by rewrite -UNZIP; apply/mapP; ∃ (i, R).
by exploit (VALID i);
[by rewrite mem_rcons in_cons INts orbT | by ins; des].
Qed.
Lemma bertogna_fp_comp_f_converges_early :
(∃ k, k ≤ max_steps tsk ∧ f k = f k.+1) →
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
by intros EX; des; apply fixedpoint.iter_fix with (k := k).
Qed.
Section DerivingContradiction.
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps tsk → f k != f k.+1.
Lemma bertogna_fp_comp_f_increases :
∀ k,
k ≤ max_steps tsk →
f k < f k.+1.
Proof.
intros k LT.
rewrite ltn_neqAle; apply/andP; split.
by apply H_keeps_diverging.
by apply bertogna_fp_comp_f_monotonic, leqnSn.
Qed.
Lemma bertogna_fp_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps tsk →
f k > k + task_cost tsk - 1.
Proof.
have INC := bertogna_fp_comp_f_increases.
rename H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
induction k.
{
intros _; rewrite add0n -addn1 addnBAC;
first by rewrite -addnBA // subnn addn0 /= leqnn.
by apply PARAMS.
}
{
intros LT.
specialize (IHk (ltnW LT)).
apply leq_ltn_trans with (n := f k); last by apply INC, ltnW.
rewrite -addn1 -addnA [1 + _]addnC addnA -addnBA // subnn addn0.
rewrite -(ltn_add2r 1) in IHk.
rewrite addnBAC in IHk;
last by apply leq_trans with (n := task_cost tsk);
[by apply PARAMS | by apply leq_addl].
by rewrite -addnBA // subnn addn0 addn1 ltnS in IHk.
}
Qed.
End DerivingContradiction.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
Proof.
have TOOMUCH := bertogna_fp_comp_rt_grows_too_much.
have INC := bertogna_fp_comp_f_increases.
rename H_no_larger_than_deadline into LE,
H_valid_task_parameters into TASK_PARAMS.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *; des.
destruct ([∃ k in 'I_(max_steps tsk).+1, f k == f k.+1]) eqn:EX.
{
move: EX ⇒ /exists_inP EX; destruct EX as [k _ ITERk].
apply bertogna_fp_comp_f_converges_early.
by ∃ k; split; [by rewrite -ltnS; apply ltn_ord | by apply/eqP].
}
apply negbT in EX; rewrite negb_exists_in in EX.
move: EX ⇒ /forall_inP EX.
rewrite leqNgt in LE; move: LE ⇒ /negP LE.
exfalso; apply LE.
assert (DIFF: ∀ k : nat, k ≤ max_steps tsk → f k != f k.+1).
{
intros k LEk; rewrite -ltnS in LEk.
by exploit (EX (Ordinal LEk)); [by done | intro DIFF; apply DIFF].
}
exploit TOOMUCH; [by apply DIFF | by apply leq_addr |].
exploit (TASK_PARAMS tsk);
[by rewrite mem_rcons in_cons eq_refl orTb | intro PARAMS; des].
rewrite addnBAC; last by apply PARAMS2.
rewrite -addnBA // subnn addn0 subn1 prednK //.
intros LT; apply (leq_ltn_trans LT).
by rewrite /max_steps [_ - _ + 1]addn1; apply INC, leq_addr.
Qed.
End Convergence.
Section MainProof.
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_is_total:
FP_is_total_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable sched: schedule Job num_cpus.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_respects_FP_policy:
respects_FP_policy job_arrival job_cost job_task arr_seq sched higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Theorem fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In fp_claimed_bounds ts →
response_time_bounded_by tsk R.
Proof.
rename H_valid_job_parameters into JOBPARAMS, H_valid_task_parameters into TASKPARAMS.
unfold valid_sporadic_taskset in ×.
intros tsk R MATCH.
assert (SOME: ∃ hp_bounds, fp_claimed_bounds ts = Some hp_bounds ∧
(tsk, R) \in hp_bounds).
{
destruct (fp_claimed_bounds ts); last by done.
by ∃ l; split.
} clear MATCH; des; rename SOME0 into IN.
have UNZIP := fp_claimed_bounds_unzip ts hp_bounds SOME.
set elem := (tsk,R).
move: IN ⇒ /(nthP elem) [idx LTidx EQ].
set NTH := fun k ⇒ nth elem hp_bounds k.
set TASK := fun k ⇒ (NTH k).1.
set RESP := fun k ⇒ (NTH k).2.
cut (response_time_bounded_by (TASK idx) (RESP idx));
first by unfold TASK, RESP, NTH; rewrite EQ.
clear EQ.
assert (PAIR: ∀ idx, (TASK idx, RESP idx) = NTH idx).
by intros i; unfold TASK, RESP; destruct (NTH i).
assert (SUBST: ∀ i, i < size hp_bounds → TASK i = nth tsk ts i).
by intros i LTi; rewrite /TASK /NTH -UNZIP (nth_map elem) //.
assert (SIZE: size hp_bounds = size ts).
by rewrite -UNZIP size_map.
induction idx as [idx IH'] using strong_ind.
assert (IH: ∀ tsk_hp R_hp, (tsk_hp, R_hp) \in take idx hp_bounds → response_time_bounded_by tsk_hp R_hp).
{
intros tsk_hp R_hp INhp.
move: INhp ⇒ /(nthP elem) [k LTk EQ].
rewrite size_take LTidx in LTk.
rewrite nth_take in EQ; last by done.
cut (response_time_bounded_by (TASK k) (RESP k));
first by unfold TASK, RESP, NTH; rewrite EQ.
by apply IH'; try (by done); apply (ltn_trans LTk).
} clear IH'.
unfold response_time_bounded_by in ×.
exploit (fp_claimed_bounds_rcons (take idx ts) (take idx hp_bounds) (TASK idx) (TASK idx) (RESP idx)).
{
by rewrite PAIR SUBST // -2?take_nth -?SIZE // (fp_claimed_bounds_take _ hp_bounds).
}
intros [_ [_ [REC DL]]].
try ( apply bertogna_cirinei_response_time_bound_fp with
(task_cost0 := task_cost) (task_period0 := task_period)
(task_deadline0 := task_deadline) (job_deadline0 := job_deadline) (tsk0 := (TASK idx))
(job_task0 := job_task) (ts0 := ts) (hp_bounds0 := take idx hp_bounds)
(higher_eq_priority := higher_priority); try (by done) ) ||
apply bertogna_cirinei_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (job_deadline := job_deadline) (tsk := (TASK idx))
(job_task := job_task) (ts := ts) (hp_bounds := take idx hp_bounds)
(higher_eq_priority := higher_priority); try (by done).
{
cut (NTH idx \in hp_bounds = true);
[intros IN | by apply mem_nth].
by rewrite set_mem -UNZIP; apply/mapP; ∃ (TASK idx, RESP idx); rewrite PAIR.
}
{
intros hp_tsk IN INTERF.
∃ (RESP (index hp_tsk ts)).
move: (IN) ⇒ INDEX; apply nth_index with (x0 := tsk) in INDEX.
rewrite -{1}[hp_tsk]INDEX -SUBST; last by rewrite SIZE index_mem.
assert (UNIQ: uniq hp_bounds).
{
apply map_uniq with (f := fst); unfold unzip1 in *; rewrite UNZIP.
by destruct ts.
}
rewrite -filter_idx_lt_take //.
{
rewrite PAIR mem_filter; apply/andP; split;
last by apply mem_nth; rewrite SIZE index_mem.
{
rewrite /NTH index_uniq; [| by rewrite SIZE index_mem | by done ].
{
move: INTERF ⇒ /andP [HP NEQ].
apply fp_claimed_bounds_hp_tasks_have_smaller_index with
(ts := ts) (elem := tsk) (hp_bounds := hp_bounds);
try (by done);
[by rewrite index_mem | by rewrite -SIZE | | by rewrite INDEX -SUBST].
apply/eqP; intro BUG; subst idx.
rewrite SUBST -{1}INDEX in NEQ;
first by rewrite eq_refl in NEQ.
by rewrite SIZE index_mem INDEX.
}
}
}
}
{
rewrite REC per_task_rta_fold.
apply per_task_rta_converges with (ts_hp := take idx ts);
[by apply fp_claimed_bounds_take; try (by apply ltnW) | | by rewrite -REC ].
rewrite SUBST // -take_nth -?SIZE //.
by intros i IN; eapply TASKPARAMS, mem_take, IN.
}
Qed.
Hypothesis H_test_succeeds: fp_schedulable ts.
Theorem taskset_schedulable_by_fp_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Proof.
have RLIST := (fp_analysis_yields_response_time_bounds).
have UNZIP := (fp_claimed_bounds_unzip ts).
have DL := (fp_claimed_bounds_le_deadline ts).
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
fp_schedulable, valid_sporadic_job in ×.
rename H_valid_job_parameters into JOBPARAMS.
move ⇒ tsk INtsk j ARRj JOBtsk.
destruct (fp_claimed_bounds ts) as [rt_bounds |]; last by ins.
feed (UNZIP rt_bounds); first by done.
assert (EX: ∃ R, (tsk, R) \in rt_bounds).
{
rewrite set_mem -UNZIP in INtsk; move: INtsk ⇒ /mapP EX.
by destruct EX as [p]; destruct p as [tsk' R]; simpl in *; subst tsk'; ∃ R.
} des.
exploit (RLIST tsk R); eauto 1; intro COMPLETED.
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in ×.
apply extend_sum; rewrite // leq_add2l.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
by done.
Qed.
Theorem jobs_schedulable_by_fp_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
Proof.
intros j ARRj.
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); try (by done).
by apply H_all_jobs_from_taskset.
Qed.
End MainProof.
End Analysis.
End ResponseTimeIterationFP.