Skip to content
GitLab
Commit 13649d01 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Fix broken code after changes in spec

parent 96576ba4
Hide whitespace changes
Inline Side-by-side
BertognaResponseTimeDefsEDF.v
View file @ 13649d01
......@@ -196,7 +196,7 @@ Module ResponseTimeAnalysisEDF.
{
by intros tsk0 R0 IN0; rewrite [R0](FIX tsk0); first apply leq_addr.
}
(* First, rewrite the claim in terms of the *absolute* response-time bound (arrival + R) *)
remember (job_arrival j + R) as ctime.
......@@ -904,7 +904,8 @@ Module ResponseTimeAnalysisEDF.
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.
rewrite -big_mkcond -big_seq_cond -big_mkcond sum1_count.
by apply (INVARIANT tsk' j'); try (by done); apply (INts tsk' R').
by eapply cpus_busy_with_interfering_tasks;
[by apply INVARIANT | by apply JOBtsk | by apply BACK].
}
(* 3) Next, we prove the auxiliary lemma from the paper. *)
......@@ -1000,9 +1001,10 @@ Module ResponseTimeAnalysisEDF.
rewrite mul1n; move: HAS => /hasP HAS.
destruct HAS as [tsk_k INk H].
move: H => /andP [/andP [INTERFk LEk] SCHEDk].
exploit INVARIANT;
[by apply (INts tsk' R') | by apply JOBtsk | by apply BACK | intro COUNT].
generalize INVARIANT; intro COUNT.
apply cpus_busy_with_interfering_tasks with (job_task0 := job_task) (ts0 := ts) (j := j') (tsk := tsk') (t0 := t) in COUNT;
try by done.
unfold cardA.
set interfering_tasks_at_t :=
......
BertognaResponseTimeDefsJitter.v
View file @ 13649d01
......@@ -166,13 +166,7 @@ Module ResponseTimeAnalysisJitter.
the processors must be busy with jobs of equal or higher
priority. *)
Hypothesis H_global_scheduling_invariant:
forall (j: JobIn arr_seq) (t: time),
job_task j = tsk ->
backlogged job_cost rate sched j t ->
count
(fun tsk_other : sporadic_task_with_jitter =>
is_interfering_task_fp tsk higher_eq_priority tsk_other &&
task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_eq_priority.
(* Next, we define Bertogna and Cirinei's response-time bound recurrence *)
......@@ -218,7 +212,7 @@ Module ResponseTimeAnalysisJitter.
set x := fun hp_tsk =>
if (hp_tsk \in ts) && interferes_with_tsk hp_tsk then
task_interference job_cost job_task rate sched j
(job_arrival j) (job_arrival j + R) hp_tsk
hp_tsk (job_arrival j) (job_arrival j + R)
else 0.
set X := total_interference job_cost rate sched j (job_arrival j) (job_arrival j + R).
......@@ -346,7 +340,8 @@ Module ResponseTimeAnalysisJitter.
}
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));
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.
by apply (INVARIANT tsk j).
}
(* 3) Next, we prove the auxiliary lemma from the paper. *)
......@@ -443,8 +438,7 @@ Module ResponseTimeAnalysisJitter.
destruct HAS as [tsk_k INk H].
move: H => /andP [/andP [INTERFk LEk] SCHEDk].
exploit INVARIANT;
[by apply JOBtsk | by apply BACK | intro COUNT].
exploit (INVARIANT tsk j t); try (by done); intro COUNT.
unfold cardA.
set interfering_tasks_at_t :=
......@@ -469,8 +463,7 @@ Module ResponseTimeAnalysisJitter.
[by rewrite andbT | by rewrite andbF].
}
rewrite leq_subLR.
rewrite -count_predUI.
rewrite leq_subLR -count_predUI.
apply leq_trans with (n :=
count (predU (fun i : sporadic_task_with_jitter =>
interferes_with_tsk i &&
......
BertognaResponseTimeEDFComp.v
View file @ 13649d01
......@@ -137,9 +137,9 @@ Module ResponseTimeIterationEDF.
first by apply geq_minr.
unfold edf_specific_bound; simpl.
rewrite leq_add2l leq_min; apply/andP; split; first by apply geq_minl.
by apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
task_deadline tsk_other + R);
[by apply geq_minr | by rewrite leq_add2l].
apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
(task_deadline tsk_other - R));
[by apply geq_minr | by rewrite 2?leq_sub2l].
}
Qed.
......@@ -275,17 +275,17 @@ Module ResponseTimeIterationEDF.
(* ...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_no_intra_task_parallelism:
jobs_of_same_task_dont_execute_in_parallel job_task sched.
(* Assume that the schedule satisfies the global scheduling
invariant with EDF priority, i.e., if any job of tsk is
backlogged, every processor must be busy with jobs with
no greater absolute deadline. *)
Let higher_eq_priority :=
@EDF Job arr_seq job_deadline. (* TODO: implicit params seems broken *)
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_jlfp tsk tsk_other &&
task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus rate sched higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
......
BertognaResponseTimeFP.v
View file @ 13649d01
......@@ -375,7 +375,7 @@ Module ResponseTimeIterationFP.
uniq (rcons ts' tsk) ->
sorted higher_eq_priority (rcons ts' tsk) ->
R_list (rcons ts' tsk) = Some (rcons hp_bounds (tsk, R)) ->
[seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp tsk higher_eq_priority tsk_hp] =
[seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp higher_eq_priority tsk tsk_hp] =
unzip1 hp_bounds.
Proof.
intros ts tsk hp_bounds R TRANS.
......@@ -405,11 +405,11 @@ Module ResponseTimeIterationFP.
rewrite filter_rcons in IHts.
unfold is_interfering_task_fp in IHts.
rewrite eq_refl andbF in IHts.
assert (NOTHP: is_interfering_task_fp tsk higher_eq_priority tsk = false).
assert (NOTHP: is_interfering_task_fp higher_eq_priority tsk tsk = false).
{
by unfold is_interfering_task_fp; rewrite eq_refl andbF.
} rewrite filter_rcons NOTHP; clear NOTHP.
assert (HP: is_interfering_task_fp tsk higher_eq_priority tsk_lst).
assert (HP: is_interfering_task_fp higher_eq_priority tsk tsk_lst).
{
unfold is_interfering_task_fp; apply/andP; split.
{
......@@ -423,8 +423,8 @@ Module ResponseTimeIterationFP.
}
} rewrite filter_rcons HP; clear HP.
unfold unzip1; rewrite map_rcons /=; f_equal.
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]).
assert (SHIFT: [seq tsk_hp <- ts' | is_interfering_task_fp higher_eq_priority tsk tsk_hp] = [seq tsk_hp <- ts'
| is_interfering_task_fp higher_eq_priority tsk_lst tsk_hp]).
{
apply eq_in_filter; red.
unfold is_interfering_task_fp; intros x INx.
......@@ -524,14 +524,7 @@ Module ResponseTimeIterationFP.
(* 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.
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
......@@ -611,6 +604,7 @@ Module ResponseTimeIterationFP.
apply BOUND with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (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 rewrite mem_rcons in_cons eq_refl orTb.
by apply R_list_unzip1 with (R := R_lst).
{
intros hp_tsk R0 HP j0 JOB0.
......@@ -637,10 +631,6 @@ Module ResponseTimeIterationFP.
}
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.
......
BertognaResponseTimeFPJitter.v
View file @ 13649d01
Require Import Vbase JobDefs TaskDefs ScheduleDefs TaskArrivalDefs PriorityDefs WorkloadDefsJitter BertognaResponseTimeDefsJitter divround helper
Require Import Vbase JobDefs TaskDefs ScheduleDefs TaskArrivalDefs PriorityDefs WorkloadDefsJitter BertognaResponseTimeDefsJitter InterferenceDefs divround helper
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeIterationFPWithJitter.
Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisJitter.
Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisJitter Interference.
Section Analysis.
......@@ -378,7 +378,7 @@ Module ResponseTimeIterationFPWithJitter.
uniq (rcons ts' tsk) ->
sorted higher_eq_priority (rcons ts' tsk) ->
R_list (rcons ts' tsk) = Some (rcons hp_bounds (tsk, R)) ->
[seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp tsk higher_eq_priority tsk_hp] =
[seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp higher_eq_priority tsk tsk_hp] =
unzip1 hp_bounds.
Proof.
intros ts tsk hp_bounds R TRANS.
......@@ -408,11 +408,11 @@ Module ResponseTimeIterationFPWithJitter.
rewrite filter_rcons in IHts.
unfold is_interfering_task_fp in IHts.
rewrite eq_refl andbF in IHts.
assert (NOTHP: is_interfering_task_fp tsk higher_eq_priority tsk = false).
assert (NOTHP: is_interfering_task_fp higher_eq_priority tsk tsk = false).
{
by unfold is_interfering_task_fp; rewrite eq_refl andbF.
} rewrite filter_rcons NOTHP; clear NOTHP.
assert (HP: is_interfering_task_fp tsk higher_eq_priority tsk_lst).
assert (HP: is_interfering_task_fp higher_eq_priority tsk tsk_lst).
{
unfold is_interfering_task_fp; apply/andP; split.
{
......@@ -426,8 +426,8 @@ Module ResponseTimeIterationFPWithJitter.
}
} rewrite filter_rcons HP; clear HP.
unfold unzip1; rewrite map_rcons /=; f_equal.
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]).
assert (SHIFT: [seq tsk_hp <- ts' | is_interfering_task_fp higher_eq_priority tsk tsk_hp] = [seq tsk_hp <- ts'
| is_interfering_task_fp higher_eq_priority tsk_lst tsk_hp]).
{
apply eq_in_filter; red.
unfold is_interfering_task_fp; intros x INx.
......@@ -525,14 +525,7 @@ Module ResponseTimeIterationFPWithJitter.
(* Assume the platform satisfies the global scheduling invariant. *)
Hypothesis H_global_scheduling_invariant:
forall (tsk: sporadic_task_with_jitter) (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.
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task_with_jitter) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
......@@ -613,7 +606,8 @@ Module ResponseTimeIterationFPWithJitter.
apply BOUND with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (job_deadline := job_deadline) (job_task := job_task) (tsk := tsk_lst) (job_jitter := job_jitter)
(ts := rcons ts' tsk_lst) (hp_bounds := hp_bounds)
(higher_eq_priority := higher_eq_priority); clear BOUND; try (by ins).
apply R_list_unzip1 with (R := R_lst); try (by ins).
by rewrite mem_rcons in_cons eq_refl orTb.
by apply R_list_unzip1 with (R := R_lst); try (by ins).
{
intros hp_tsk R0 HP j0 JOB0.
apply IH with (rt_bounds := hp_bounds) (tsk := hp_tsk); try (by ins).
......@@ -639,10 +633,6 @@ Module ResponseTimeIterationFPWithJitter.
}
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 per_task_rta_fold.
apply per_task_rta_converges with (ts' := ts'); try (by ins).
......
GuanDefs.v
View file @ 13649d01
Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
PlatformDefs WorkloadDefs BertognaResponseTimeDefs SchedulabilityDefs PriorityDefs
PlatformDefs WorkloadDefs BertognaResponseTimeDefs SchedulabilityDefs PriorityDefs InterferenceDefs PlatformDefs
ResponseTimeDefs divround helper
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeAnalysisGuan.
Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival.
Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival Interference Platform.
Export Workload ResponseTimeAnalysis.
Section InterferenceBoundGuan.
......@@ -33,7 +33,7 @@ Module ResponseTimeAnalysisGuan.
(* Let's filter the list of task and response-times so that it only has interfering tasks. *)
Let interfering_tasks :=
[seq (tsk_other, R) <- R_prev | is_interfering_task_fp tsk higher_eq_priority tsk_other].
[seq (tsk_other, R) <- R_prev | is_interfering_task_fp higher_eq_priority tsk tsk_other].
(* After that, we list all possible pairs of subsets of that list:
[(subset0, subset1), (subset0, subset2), ...]*)
......@@ -141,7 +141,7 @@ Module ResponseTimeAnalysisGuan.
(* Assume there exists a fixed task priority. *)
Variable higher_eq_priority: fp_policy sporadic_task.
Let interferes_with_tsk := is_interfering_task_fp tsk higher_eq_priority.
Let interferes_with_tsk := is_interfering_task_fp higher_eq_priority tsk.
(* Assume that hp_bounds has exactly the tasks that interfere with tsk,... *)
Hypothesis H_hp_bounds_has_interfering_tasks:
......@@ -174,7 +174,7 @@ Module ResponseTimeAnalysisGuan.
backlogged job_cost rate sched j t ->
count
(fun tsk_other : sporadic_task =>
is_interfering_task_fp tsk higher_eq_priority tsk_other &&
is_interfering_task_fp higher_eq_priority tsk tsk_other &&
task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
(* Next, we define Bertogna and Cirinei's response-time bound recurrence *)
......@@ -218,7 +218,7 @@ Module ResponseTimeAnalysisGuan.
set x := fun hp_tsk =>
if (hp_tsk \in ts) && interferes_with_tsk hp_tsk then
task_interference job_cost job_task rate sched j
(job_arrival j) (job_arrival j + R) hp_tsk
hp_tsk (job_arrival j) (job_arrival j + R)
else 0.
set X := total_interference job_cost rate sched j (job_arrival j) (job_arrival j + R).
......
GuanFP.v
View file @ 13649d01
......@@ -314,7 +314,7 @@ Module ResponseTimeIterationFPGuan.
unfold time in *.
set interfering_tasks :=
[seq i <- rt_bounds | let '(tsk_other, _) := i in
is_interfering_task_fp tsk higher_eq_priority tsk_other].
is_interfering_task_fp higher_eq_priority tsk tsk_other].
fold interfering_tasks in IN_CI, IN_NC.
apply mem_powerset with (x := interfering_tasks) in IN_CI.
apply mem_powerset with (x := interfering_tasks) in IN_NC.
......@@ -416,7 +416,7 @@ Module ResponseTimeIterationFPGuan.
uniq (rcons ts' tsk) ->
sorted higher_eq_priority (rcons ts' tsk) ->
R_list (rcons ts' tsk) = Some (rcons hp_bounds (tsk, R)) ->
[seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp tsk higher_eq_priority tsk_hp] =
[seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp higher_eq_priority tsk tsk_hp] =
unzip1 hp_bounds.
Proof.
intros ts tsk hp_bounds R TRANS.
......@@ -446,11 +446,11 @@ Module ResponseTimeIterationFPGuan.
rewrite filter_rcons in IHts.
unfold is_interfering_task_fp in IHts.
rewrite eq_refl andbF in IHts.
assert (NOTHP: is_interfering_task_fp tsk higher_eq_priority tsk = false).
assert (NOTHP: is_interfering_task_fp higher_eq_priority tsk tsk = false).
{
by unfold is_interfering_task_fp; rewrite eq_refl andbF.
} rewrite filter_rcons NOTHP; clear NOTHP.
assert (HP: is_interfering_task_fp tsk higher_eq_priority tsk_lst).
assert (HP: is_interfering_task_fp higher_eq_priority tsk tsk_lst).
{
unfold is_interfering_task_fp; apply/andP; split.
{
......@@ -464,8 +464,8 @@ Module ResponseTimeIterationFPGuan.
}
} rewrite filter_rcons HP; clear HP.
unfold unzip1; rewrite map_rcons /=; f_equal.
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]).
assert (SHIFT: [seq tsk_hp <- ts' | is_interfering_task_fp higher_eq_priority tsk tsk_hp] = [seq tsk_hp <- ts'
| is_interfering_task_fp higher_eq_priority tsk_lst tsk_hp]).
{
apply eq_in_filter; red.
unfold is_interfering_task_fp; intros x INx.
......@@ -563,14 +563,7 @@ Module ResponseTimeIterationFPGuan.
(* 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.
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
......
PlatformDefs.v
View file @ 13649d01
......@@ -114,7 +114,10 @@ Module Platform.
task_is_scheduled job_task sched j t)
ts = num_cpus.
Proof.
admit.
intros j tsk t JOBtsk BACK.
move: H_invariant_holds => bla.
apply/eqP; rewrite eqn_leq; apply/andP; split.
admit. admit.
Qed.
End BasicLemmas.
......
Supports Markdown
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