Skip to content
Snippets Groups Projects
Commit 1a7a0dae authored by Felix Stutz's avatar Felix Stutz
Browse files

Correctness EDF

parent 322842e8
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
BertognaResponseTimeDefsEDF.v
+ 85
− 47
View file @ 1a7a0dae
Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
PlatformDefs WorkloadDefs SchedulabilityDefs PriorityDefs
ResponseTimeDefs BertognaResponseTimeDefs divround helper
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
PlatformDefs WorkloadDefs SchedulabilityDefs PriorityDefs
ResponseTimeDefs BertognaResponseTimeDefs divround helper
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeAnalysisEDF.
......@@ -189,7 +189,8 @@ Module ResponseTimeAnalysisEDF.
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_rate_equals_one into RATE,
H_global_scheduling_invariant into INVARIANT,
H_response_time_bounds_ge_cost into GE_COST.
H_response_time_bounds_ge_cost into GE_COST,
H_response_time_is_fixed_point into FIX.
intros j JOBtsk.
(* For simplicity, let x denote per-task interference under FP
......@@ -205,8 +206,12 @@ Module ResponseTimeAnalysisEDF.
set workload_bound := fun (tup: task_with_response_time) =>
let (tsk_k, R_k) := tup in
if is_interfering_task_jlfp tsk tsk_k then
W task_cost task_period tsk_k R_k R
else 0.
interference_bound_edf task_cost task_period task_deadline tsk R (tsk_k, R_k) (*add EDF-term*)
else 0.
assert (INtsk: tsk \in ts).
{
admit.
}
(* Now we start the proof. Assume by contradiction that job j
is not complete at time (job_arrival j + R). *)
......@@ -222,17 +227,17 @@ Module ResponseTimeAnalysisEDF.
first by apply leqnn.
rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
admit.
(* In order to derive a contradiction, we first show that
the interference x_k of any task is no larger than the
workload bound W_k. *)
(*assert (WORKLOAD: forall tsk_k,
(tsk_k \in ts) && interferes_with_tsk tsk_k ->
assert (WORKLOAD: forall tsk_k,
(tsk_k \in ts) && is_interfering_task_jlfp tsk tsk_k ->
forall R_k,
(tsk_k, R_k) \in hp_bounds ->
(tsk_k, R_k) \in rt_bounds ->
x tsk_k <= workload_bound (tsk_k, R_k)).
{
{ admit.
(*
move => tsk_k /andP [INk INTERk] R_k HPk.
unfold x, workload_bound; rewrite INk INTERk andbT.
exploit (exists_R tsk_k); [by ins | by ins | intro INhp; des].
......@@ -264,7 +269,7 @@ Module ResponseTimeAnalysisEDF.
rewrite PARAMS1 JOBtsk'.
apply completion_monotonic with (t := job_arrival j' + R0); ins;
[by rewrite leq_add2l; apply NOMISS | by apply (RESP tsk_k)].
}
}*)
}
(* In the remaining of the proof, we show that the workload bound
......@@ -273,7 +278,7 @@ Module ResponseTimeAnalysisEDF.
(* 1) We show that the total interference X >= R - e_k + 1.
Otherwise, job j would have completed on time. *)
assert (INTERF: X >= R - task_cost tsk + 1).
assert (IunfoldNTERF: X >= R - task_cost tsk + 1).
{
unfold completed in COMPLETED.
rewrite addn1.
......@@ -304,7 +309,7 @@ Module ResponseTimeAnalysisEDF.
apply leq_trans with (n := job_cost j); first by ins.
apply leq_trans with (n := task_cost tsk);
first by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
by rewrite REC; apply leq_addr.
by rewrite [R](FIX tsk); first by apply leq_addr.
}
}
......@@ -322,16 +327,18 @@ Module ResponseTimeAnalysisEDF.
[by rewrite big_const_seq iter_addn mul0n addn0 mul0n|by ins].
rewrite big_mkcond mul1n /=.
rewrite (eq_bigr (fun i =>
(if (i \in ts) && interferes_with_tsk i &&
(if (i \in ts) && is_interfering_task_jlfp tsk i &&
task_is_scheduled job_task sched i t then 1 else 0))); last first.
{
ins; destruct ((i \in ts) && interferes_with_tsk i) eqn:IN;
ins; destruct ((i \in ts) && is_interfering_task_jlfp tsk i) eqn:IN;
[by rewrite andTb | by rewrite andFb].
}
rewrite (eq_bigr (fun i => if (i \in ts) && true then (if interferes_with_tsk i && task_is_scheduled job_task sched i t then 1 else 0) else 0));
rewrite (eq_bigr (fun i => if (i \in ts) && true then (if is_interfering_task_jlfp tsk i && task_is_scheduled job_task sched i t then 1 else 0) else 0));
last by ins; destruct (i \in ts) eqn:IN; rewrite ?andTb ?andFb.
by rewrite -big_mkcond -big_seq_cond -big_mkcond sum1_count; apply (INVARIANT j).
rewrite -big_mkcond -big_seq_cond -big_mkcond sum1_count.
apply (INVARIANT tsk j); try (by done).
}
(* 3) Next, we prove the auxiliary lemma from the paper. *)
assert (MINSERV: \sum_(tsk_k <- ts) x tsk_k >=
......@@ -380,13 +387,13 @@ Module ResponseTimeAnalysisEDF.
{
set some_interference_A := fun t =>
backlogged job_cost rate sched j t &&
has (fun tsk_k => (interferes_with_tsk tsk_k &&
has (fun tsk_k => (is_interfering_task_jlfp tsk tsk_k &&
((x tsk_k) >= R - task_cost tsk + 1) &&
task_is_scheduled job_task sched tsk_k t)) ts.
set total_interference_B := fun t =>
backlogged job_cost rate sched j t *
count (fun tsk_k =>
interferes_with_tsk tsk_k &&
is_interfering_task_jlfp tsk tsk_k &&
((x tsk_k) < R - task_cost tsk + 1) &&
task_is_scheduled job_task sched tsk_k t) ts.
......@@ -397,7 +404,7 @@ Module ResponseTimeAnalysisEDF.
move: HASa => /hasP HASa; destruct HASa as [tsk_a INa LEa].
apply leq_trans with (n := x tsk_a); first by apply LEa.
unfold x, task_interference, some_interference_A.
destruct ((tsk_a \in ts) && interferes_with_tsk tsk_a) eqn:INTERFa;
destruct ((tsk_a \in ts) && is_interfering_task_jlfp tsk tsk_a) eqn:INTERFa;
last by ins.
move: INTERFa => /andP INTERFa; des.
apply leq_sum; ins.
......@@ -419,7 +426,7 @@ Module ResponseTimeAnalysisEDF.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
[rewrite andTb mul1n | by ins].
destruct (has (fun tsk_k : sporadic_task =>
interferes_with_tsk tsk_k &&
is_interfering_task_jlfp tsk tsk_k &&
(R - task_cost tsk + 1 <= x tsk_k) &&
task_is_scheduled job_task sched tsk_k t) ts) eqn:HAS;
last by ins.
......@@ -428,18 +435,18 @@ Module ResponseTimeAnalysisEDF.
move: H => /andP [/andP [INTERFk LEk] SCHEDk].
exploit INVARIANT;
[by apply JOBtsk | by apply BACK | intro COUNT].
[by apply INtsk | by apply JOBtsk | by apply BACK | intro COUNT].
unfold cardA.
set interfering_tasks_at_t :=
[seq tsk_k <- ts | interferes_with_tsk tsk_k &&
[seq tsk_k <- ts | is_interfering_task_jlfp tsk tsk_k &&
task_is_scheduled job_task sched tsk_k t].
rewrite -(count_filter (fun i => true)) in COUNT.
fold interfering_tasks_at_t in COUNT.
rewrite count_predT in COUNT.
apply leq_trans with (n := num_cpus -
count (fun i => interferes_with_tsk i &&
count (fun i => is_interfering_task_jlfp tsk i &&
(x i >= R - task_cost tsk + 1) &&
task_is_scheduled job_task sched i t) ts).
{
......@@ -447,7 +454,7 @@ Module ResponseTimeAnalysisEDF.
rewrite -2!sum1_count big_mkcond /=.
rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
apply leq_sum; intros i _.
unfold x; destruct (interferes_with_tsk i);
unfold x; destruct (is_interfering_task_jlfp tsk i);
[rewrite andTb | by rewrite 2!andFb].
destruct (task_is_scheduled job_task sched i t);
[by rewrite andbT | by rewrite andbF].
......@@ -457,11 +464,11 @@ Module ResponseTimeAnalysisEDF.
rewrite -count_predUI.
apply leq_trans with (n :=
count (predU (fun i : sporadic_task =>
interferes_with_tsk i &&
is_interfering_task_jlfp tsk i &&
(R - task_cost tsk + 1 <= x i) &&
task_is_scheduled job_task sched i t)
(fun tsk_k0 : sporadic_task =>
interferes_with_tsk tsk_k0 &&
is_interfering_task_jlfp tsk tsk_k0 &&
(x tsk_k0 < R - task_cost tsk + 1) &&
task_is_scheduled job_task sched tsk_k0 t))
ts); last by apply leq_addr.
......@@ -472,7 +479,7 @@ Module ResponseTimeAnalysisEDF.
rewrite leq_eqVlt; apply/orP; left; apply/eqP.
apply eq_count; red; simpl.
intros i.
destruct (interferes_with_tsk i),
destruct (is_interfering_task_jlfp tsk i),
(task_is_scheduled job_task sched i t);
rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
by rewrite leqNgt orNb.
......@@ -481,12 +488,12 @@ Module ResponseTimeAnalysisEDF.
unfold x at 2, task_interference.
rewrite [\sum_(i <- ts | _) _](eq_bigr
(fun i => \sum_(job_arrival j <= t < job_arrival j + R)
(i \in ts) && interferes_with_tsk i &&
(i \in ts) && is_interfering_task_jlfp tsk i &&
backlogged job_cost rate sched j t &&
task_is_scheduled job_task sched i t));
last first.
{
ins; destruct ((i \in ts) && interferes_with_tsk i) eqn:INTERi;
ins; destruct ((i \in ts) && is_interfering_task_jlfp tsk i) eqn:INTERi;
first by move: INTERi => /andP [_ INTERi]; apply eq_bigr; ins; rewrite INTERi andTb.
by rewrite (eq_bigr (fun i => 0));
[by rewrite big_const_nat iter_addn mul0n addn0 | by ins].
......@@ -513,23 +520,49 @@ Module ResponseTimeAnalysisEDF.
(* 4) Now, we prove that the Bertogna's interference bound
is not enough to cover the sum of the "minimum" term over
all tasks (artifact of the proof by contradiction). *)
assert (SUM: \sum_((tsk_k, R_k) <- hp_bounds)
minn (x tsk_k) (R - task_cost tsk + 1) >
total_interference_bound_jlfp task_cost task_period tsk hp_bounds R).
Print interference_bound_edf.
assert (SUM: \sum_(k <- rt_bounds | is_interfering_task_jlfp tsk (fst k))
(minn
(interference_bound_edf task_cost task_period task_deadline
tsk R k )
(minn (x (fst k)) ((snd k) - task_cost tsk + 1)))
>
workload_bound (tsk, R)).
{
apply leq_trans with (n := \sum_(tsk_k <- ts) minn (x tsk_k) (R - task_cost tsk + 1));
last first.
{
rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
last by ins; destruct i.
apply leq_trans with (n := \sum_(tsk_k <- ts | interferes_with_tsk tsk_k) minn (x tsk_k) (R - task_cost tsk + 1)).
{ apply leq_trans with (n := \sum_(i<- rt_bounds | is_interfering_task_jlfp tsk (fst i))
(minn (x (fst i)) ((snd(i) - task_cost tsk + 1))));
last first.
{
rewrite [\sum_(_ <- _ | interferes_with_tsk _)_]big_mkcond eq_leq //.
apply leq_sum.
intros i _.
destruct i as [i R_i].
rewrite leq_min; apply/andP; split; last by done.
{
apply leq_trans with (n := x i);
first by apply geq_minl.
admit.
}
}
rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1))).
admit.
admit.
}
admit.
}
admit.
(* last by ins; destruct i.
apply leq_trans with (n := \sum_(tsk_k <- ts | is_interfering_task_jlfp tsk tsk_k) minn (x tsk_k) (R - task_cost tsk + 1)).
{
rewrite [\sum_(_ <- _ | is_interfering_task_jlfp tsk _)_]big_mkcond eq_leq //.
apply eq_bigr; intros i _; unfold x.
by destruct (interferes_with_tsk i); rewrite ?andbT ?andbF ?min0n.
by destruct (is_interfering_task_jlfp tsk i); rewrite ?andbT ?andbF ?min0n.
}
have MAP := big_map (fun x => fst x) (fun i => true) (fun i => minn (x i) (R - task_cost tsk + 1)).
by unfold unzip1 in *; rewrite -MAP -FST -big_filter.
unfold unzip1 in *. rewrite -MAP. -FST -big_filter.
}
apply ltn_div_trunc with (d := num_cpus);
first by apply H_at_least_one_cpu.
......@@ -540,17 +573,17 @@ Module ResponseTimeAnalysisEDF.
apply MINSERV.
apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
by rewrite leq_mul2r; apply/orP; right; apply INTERF.
}
}*)
(* 5) This implies that there exists a tuple (tsk_k, R_k) such that
min (x_k, R - e_i + 1) > min (W_k, R - e_i + 1). *)
assert (EX: has (fun tup : task_with_response_time =>
(* assert (EX: has (fun tup : task_with_response_time =>
let (tsk_k, R_k) := tup in
(tsk_k \in ts) &&
interferes_with_tsk tsk_k &&
is_interfering_task_jlfp tsk tsk_k &&
(minn (x tsk_k) (R - task_cost tsk + 1) >
minn (workload_bound (tsk_k, snd tup)) (R - task_cost tsk + 1)))
hp_bounds).
unfold rt_bounds).
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
......@@ -580,8 +613,13 @@ Module ResponseTimeAnalysisEDF.
specialize (WORKLOAD tsk_k INTERFk R_k HPk).
apply leq_ltn_trans with (p := x tsk_k) in WORKLOAD; first by rewrite ltnn in WORKLOAD.
by unfold workload_bound; rewrite INTERFk'; apply BUG.
*)
Qed.
*)
Qed.
End ResponseTimeBound.
......
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