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

Latest changes

parent ba46a30c
Require Import Vbase ScheduleDefs BertognaResponseTimeDefs divround helper
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeIterationFP.
Import Schedule ResponseTimeAnalysis.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Variable job_task: Job -> sporadic_task.
Variable num_cpus: nat.
Variable higher_eq_priority: fp_policy.
Hypothesis H_valid_policy: valid_fp_policy higher_eq_priority.
(* Consider a task set ts. *)
Variable ts: sporadic_taskset.
(*Load seq_nat_notation.*)
(* Next we define the fixed-point iteration for computing
Bertogna's response-time bound for any task in ts. *)
(* First, given a function containing known response-time bounds
for the higher-priority tasks, we compute the response-time bound
of tsk using the following fixed-point iteration:
R_tsk <- f^step (R_tsk),
where f is the response-time recurrence,
step is the number of iterations,
and f^0 = task_cost tsk. *)
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
tsk R_prev t higher_eq_priority)
num_cpus)
(task_cost tsk).
(* To ensure that the iteration converges, we will apply per_task_rta
a "sufficient" number of times: task_deadline tsk + 1.
Note that (deadline + 1) is pessimistic, but we don't care about
the precise runtime complexity here. *)
Definition max_steps (tsk: sporadic_task) := task_deadline tsk + 1.
(* Next, we compute the response-time bounds of the task set.
The function either returns a list of pairs (tsk, R_tsk) for the
entire taskset or None, if the analysis failed for some task.
Assume that the task set is sorted in increasing priority order. *)
Definition R_list_helper :=
fun 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 R_list' (ts: sporadic_taskset) : option (seq task_with_response_time) :=
foldl R_list_helper (Some [::]) ts.
(*Compute (foldl (fun prev x => rcons prev x) [::] [:: 1; 2; 3; 4]).*)
Definition R_list := R_list' ts.
Definition fp_schedulability_test := R_list != None.
Section AuxiliaryLemmas.
Lemma R_list_rcons_prefix :
forall ts hp_bounds tsk1 tsk2 R,
R_list' (rcons ts tsk1) = Some (rcons hp_bounds (tsk2, R)) ->
R_list' ts = Some hp_bounds.
Proof.
intros ts hp_bounds tsk1 tsk2 R SOME.
rewrite -cats1 in SOME.
unfold R_list' in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rewrite Heq; rename H0 into EQ.
move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ => /andP [/eqP EQ _].
by f_equal.
Qed.
Lemma R_list_rcons_task :
forall ts hp_bounds tsk1 tsk2 R,
R_list' (rcons ts tsk1) = Some (rcons hp_bounds (tsk2, R)) ->
tsk1 = tsk2.
Proof.
intros ts hp_bounds tsk1 tsk2 R SOME.
rewrite -cats1 in SOME.
unfold R_list' in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rename H0 into EQ.
move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ.
move: EQ => /andP [_ /eqP EQ].
by inversion EQ.
Qed.
Lemma R_list_rcons_response_time :
forall ts hp_bounds tsk R,
R_list' (rcons ts tsk) = Some (rcons hp_bounds (tsk, R)) ->
R = per_task_rta tsk hp_bounds (max_steps tsk).
Proof.
intros ts hp_bounds tsk R SOME.
rewrite -cats1 in SOME.
unfold R_list' in SOME.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in SOME.
desf; rename H0 into EQ; move: EQ => /eqP EQ.
rewrite eqseq_rcons in EQ; move: EQ => /andP [/eqP EQ1 /eqP EQ2].
by inversion EQ2; rewrite EQ1.
Qed.
Lemma R_list_contains_tasks :
forall ts rt_bounds tsk R,
R_list' ts = Some rt_bounds ->
((tsk, R) \in rt_bounds -> tsk \in ts).
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk R SOME.
by inversion SOME; subst; rewrite 2!in_nil.
}
{
intros rt_bounds tsk_i R SOME IN.
destruct (lastP rt_bounds) as [| rt_bounds (tsk_lst', R_lst)];
first by inversion SOME; desf.
rewrite mem_rcons in_cons in IN.
move: IN => /orP [/eqP HEAD | TAIL].
{
apply R_list_rcons_task in SOME; subst tsk_lst'.
by inversion HEAD; rewrite mem_rcons in_cons; apply/orP; left.
}
{
rewrite mem_rcons in_cons; apply/orP; right.
apply R_list_rcons_prefix in SOME.
by apply IHts with (rt_bounds := rt_bounds) (R := R); last by ins.
}
}
Qed.
Lemma R_list_le_deadline :
forall ts rt_bounds tsk R,
R_list' 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 R_list' in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper 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 R_list_rcons_prefix in SOME.
}
}
Qed.
Lemma R_list_ge_cost :
forall ts rt_bounds tsk R,
R_list' 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 R_list' in *.
rewrite foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper 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 R_list_rcons_prefix in SOME.
}
}
Qed.
Lemma R_list_non_empty :
forall ts rt_bounds tsk,
R_list' ts = Some rt_bounds ->
(tsk \in ts <->
exists R,
(tsk, R) \in rt_bounds).
Proof.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
intros rt_bounds tsk SOME.
inversion SOME; rewrite in_nil; split; first by ins.
by intro EX; des; rewrite in_nil in EX.
}
{
intros rt_bounds tsk_i SOME.
destruct (lastP rt_bounds) as [|rt_bounds (tsk_lst', R_lst)].
{
split; last first; intro EX; des; first by rewrite in_nil in EX.
unfold R_list' in *.
rewrite -cats1 foldl_cat in SOME.
simpl in SOME.
unfold R_list_helper in *; desf; rename H0 into EQ.
destruct l; first by ins.
by rewrite rcons_cons in EQ; inversion EQ.
}
split.
{
intros IN; rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | FRONT].
{
move: LAST => /eqP LAST; subst tsk_i.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_lst'; intro SOME.
exists R_lst.
by rewrite mem_rcons in_cons; apply/orP; left.
}
{
apply R_list_rcons_prefix in SOME.
exploit (IHts rt_bounds tsk_i); [by ins | intro EX].
apply EX in FRONT; des.
by exists R; rewrite mem_rcons in_cons; apply/orP; right.
}
}
{
intro IN; des.
rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
destruct IN as [LAST | FRONT].
{
move: LAST => /eqP LAST.
inversion LAST; subst tsk_i R; clear LAST.
apply R_list_rcons_task in SOME; subst.
by rewrite mem_rcons in_cons; apply/orP; left.
}
{
rewrite mem_rcons in_cons; apply/orP; right.
exploit (IHts rt_bounds tsk_i);
[by apply R_list_rcons_prefix in SOME | intro EX].
by apply EX; exists R.
}
}
}
Qed.
Lemma per_task_rta_fold :
forall tsk rt_bounds,
task_cost tsk +
div_floor (total_interference_bound_fp tsk rt_bounds
(per_task_rta tsk rt_bounds (max_steps tsk)) higher_eq_priority) num_cpus
= per_task_rta tsk rt_bounds (max_steps tsk).+1.
Proof.
by ins.
Qed.
End AuxiliaryLemmas.
Section Proof.
(* Assume that higher_eq_priority is a total order over the task set. *)
Hypothesis H_reflexive: reflexive higher_eq_priority.
Hypothesis H_transitive: transitive higher_eq_priority.
Hypothesis H_unique_priorities: antisymmetric higher_eq_priority.
Hypothesis H_total: total higher_eq_priority.
(* Assume the task set has no duplicates, ... *)
Hypothesis H_ts_is_a_set: uniq ts.
(* ...all tasks have valid parameters, ... *)
Hypothesis H_valid_task_parameters: valid_sporadic_taskset ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* ...and tasks are ordered by increasing priorities. *)
Hypothesis H_sorted_ts: sorted higher_eq_priority ts.
(* Next, consider any arrival sequence such that...*)
Context {arr_seq: arrival_sequence Job}.
(* ...all jobs come from task set ts, ...*)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
(* ...they have valid parameters,...*)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_sporadic_job job_cost job_deadline job_task j.
(* ... and satisfy the sporadic task model.*)
Hypothesis H_sporadic_tasks: sporadic_task_model arr_seq job_task.
(* Then, consider any platform with at least one CPU and unit
unit execution rate, where...*)
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
Hypothesis H_rate_equals_one :
forall j cpu, rate j cpu = 1.
(* ...jobs only execute after they arrived and no longer
than their execution costs,... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost rate sched.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* Assume the platform satisfies the global scheduling invariant. *)
Hypothesis H_global_scheduling_invariant:
forall (tsk: sporadic_task) (j: JobIn arr_seq) (t: time),
tsk \in ts ->
job_task j = tsk ->
backlogged job_cost rate sched j t ->
count
(fun tsk_other : _ =>
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.
(* Now we present the proofs of termination and correctness of
the schedulability test. *)
Lemma R_list_unzip1 :
forall ts tsk hp_bounds R,
uniq ts ->
sorted higher_eq_priority (rcons ts tsk) ->
R_list' (rcons ts tsk) = Some (rcons hp_bounds (tsk, R)) ->
[seq tsk_hp <- ts | is_interfering_task_fp tsk higher_eq_priority tsk_hp] =
unzip1 hp_bounds.
Proof.
clear H_sorted_ts H_global_scheduling_invariant H_no_parallelism H_completed_jobs_dont_execute
H_jobs_must_arrive_to_execute H_jobs_must_arrive_to_execute
H_rate_equals_one H_at_least_one_cpu sched rate H_sporadic_tasks H_all_jobs_from_taskset.
intros ts; induction ts as [| ts' tsk_lst] using last_ind.
{
admit.
}
{
intros tsk hp_bounds R UNIQ SORTED SOME; simpl.
destruct (lastP hp_bounds) as [| hp_bounds (tsk_lst', R_lst)].
{
admit.
}
rewrite filter_rcons.
assert (HP: is_interfering_task_fp tsk higher_eq_priority tsk_lst).
{
admit.
} rewrite HP.
assert (SHIFT: [seq tsk_hp <- ts' | is_interfering_task_fp tsk higher_eq_priority tsk_hp] = [seq tsk_hp <- ts' | is_interfering_task_fp tsk_lst higher_eq_priority tsk_hp]).
{
apply eq_filter. red.
admit.
} rewrite SHIFT.
unfold unzip1; rewrite map_rcons.
simpl; f_equal; last by admit.
apply R_list_rcons_prefix in SOME.
generalize SOME; apply R_list_rcons_task in SOME; subst tsk_lst'; intro SOME.
apply IHts with (R := R_lst); simpl in *; last by ins.
by rewrite rcons_uniq in UNIQ; move: UNIQ => /andP [_ UNIQ].
by apply sorted_rcons_prefix in SORTED.
}
Qed.
(* To prove convergence of R, we first show convergence of rt_rec. *)
Lemma per_task_rta_converges:
forall (tsk: sporadic_task) prev,
tsk \in ts ->
per_task_rta tsk prev (max_steps tsk) <= task_deadline tsk ->
per_task_rta tsk prev (max_steps tsk) =
per_task_rta tsk prev (max_steps tsk).+1.
Proof.
rename H_valid_task_parameters into TASKPARAMS.
unfold valid_sporadic_taskset, valid_sporadic_task in *.
(* To simplify, let's call the function f.*)
intros tsk prev INtsk LE; set (f := per_task_rta tsk prev); fold f in LE.
assert (INprev: forall i, i \in prev -> fst i \in ts).
{
unfold f in *.
admit.
}
assert (GE_COST: forall i,i \in prev -> snd i >= task_cost (fst i)).
admit.
(* First prove that f is monotonic.*)
assert (MON: forall x1 x2, x1 <= x2 -> f x1 <= f x2).
{
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.
unfold div_floor, total_interference_bound_fp.
rewrite big_seq_cond [\sum_(i <- _ | let '(tsk_other, _) := i in
_ && (tsk_other != tsk))_]big_seq_cond.
rewrite leq_add2l leq_div2r // leq_sum //.
intros i; specialize (INprev i); specialize (GE_COST i).
destruct i as [i R]; move => /andP [IN _].
unfold interference_bound; simpl.
rewrite leq_min; apply/andP; split.
{
apply leq_trans with (n := W i R x1);
first by apply geq_minl.
exploit (TASKPARAMS i); [by apply INprev | intro PARAMS; des].
by apply W_monotonic; try (by ins); apply GE_COST.
}
{
apply leq_trans with (n := x1 - task_cost tsk + 1);
first by apply geq_minr.
by rewrite leq_add2r leq_sub2r //.
}
}
(* Either f converges by the deadline or not. *)
unfold max_steps in *; rewrite -> addn1 in *.
destruct ([exists k in 'I_(task_deadline tsk).+1,
f k == f k.+1]) eqn:EX.
{
move: EX => /exists_inP EX; destruct EX as [k _ ITERk].
move: ITERk => /eqP ITERk.
by apply iter_fix with (k := k);
[by ins | by apply ltnW, ltn_ord].
}
apply negbT in EX; rewrite negb_exists_in in EX.
move: EX => /forall_inP EX.
assert (GROWS: forall k: 'I_(task_deadline tsk).+1,
f k < f k.+1).
{
intros k; rewrite ltn_neqAle; apply/andP; split; first by apply EX.
apply MON, leqnSn.
}
(* If it doesn't converge, then it becomes larger than the deadline.
But initialy we assumed otherwise. Contradiction! *)
assert (BY1: f (task_deadline tsk).+1 > task_deadline tsk).
{
clear MON LE EX.
induction (task_deadline tsk).+1; first by ins.
apply leq_ltn_trans with (n := f n);
last by apply (GROWS (Ordinal (ltnSn n))).
apply IHn; intros k.
by apply (GROWS (widen_ord (leqnSn n) k)).
}
by apply leq_ltn_trans with (m := f (task_deadline tsk).+1) in BY1;
[by rewrite ltnn in BY1 | by ins].
Qed.
Lemma R_list_has_response_time_bounds :
forall rt_bounds tsk R,
R_list = 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.
have CONV := per_task_rta_converges.
(*intros rt_bounds tsk R SOME IN.
exploit (R_list_non_empty ts rt_bounds tsk);
[by apply SOME| intro EX].
destruct EX as [_ EX].
exploit EX; [by exists R | intro IN'].
exploit (R_list_unzip1 tsk rt_bounds); [by ins | by ins | intro UNZIP].
clear IN' EX.
generalize dependent R.
generalize dependent tsk.
generalize dependent rt_bounds.*)
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.
{
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].