Skip to content
Snippets Groups Projects
Commit 724884f9 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Prove workload bound with jitter

parent 60232a68
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
BertognaResponseTimeDefs.v
+ 37
− 22
View file @ 724884f9
......@@ -9,10 +9,12 @@ Module ResponseTimeAnalysis.
Section Interference.
(* Assume any job arrival sequence...*)
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence...*)
Context {arr_seq: arrival_sequence Job}.
(* ... and any platform. *)
......@@ -169,10 +171,15 @@ Module ResponseTimeAnalysis.
Section InterferenceBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
Definition task_with_response_time := (sporadic_task * time)%type.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
......@@ -189,14 +196,14 @@ Module ResponseTimeAnalysis.
(* Based on the workload bound, Bertogna and Cirinei define the
following interference bound for a task. *)
Definition interference_bound :=
minn (W tsk_other R_other delta) (delta - (task_cost tsk) + 1).
minn (W task_cost task_period tsk_other R_other delta) (delta - (task_cost tsk) + 1).
End PerTask.
Section FP.
(* Assume an FP policy. *)
Variable higher_eq_priority: fp_policy.
Variable higher_eq_priority: fp_policy sporadic_task.
Definition is_interfering_task_fp (tsk_other: sporadic_task) :=
higher_eq_priority tsk_other tsk && (tsk_other != tsk).
......@@ -224,18 +231,25 @@ Module ResponseTimeAnalysis.
Section ResponseTimeBound.
(* Assume any job arrival sequence... *)
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks: sporadic_task_model arr_seq job_task.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
(valid_sporadic_job job_cost job_deadline job_task) j.
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Consider any schedule such that...*)
Variable num_cpus: nat.
......@@ -260,8 +274,9 @@ Module ResponseTimeAnalysis.
(* Assume that we have a task set where all tasks have valid
parameters and restricted deadlines. *)
Variable ts: sporadic_taskset.
Hypothesis H_valid_task_parameters: valid_sporadic_taskset ts.
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
......@@ -275,6 +290,7 @@ Module ResponseTimeAnalysis.
is_response_time_bound_of_task job_cost job_task tsk rate sched.
(* Assume a known response-time bound for any interfering task *)
Let task_with_response_time := (sporadic_task * time)%type.
Variable hp_bounds: seq task_with_response_time.
(* We derive the response-time bounds for FP and EDF scheduling
......@@ -282,7 +298,7 @@ Module ResponseTimeAnalysis.
Section UnderFPScheduling.
(* For FP scheduling, assume there exists a fixed task priority. *)
Variable higher_eq_priority: fp_policy.
Variable higher_eq_priority: fp_policy sporadic_task.
Let interferes_with_tsk := is_interfering_task_fp tsk higher_eq_priority.
......@@ -343,7 +359,7 @@ Module ResponseTimeAnalysis.
Hypothesis H_response_time_recurrence_holds :
R = task_cost tsk +
div_floor
(total_interference_bound_fp tsk hp_bounds R higher_eq_priority)
(total_interference_bound_fp task_cost task_period tsk hp_bounds R higher_eq_priority)
num_cpus.
(*..., and R is no larger than the deadline of tsk, ...*)
......@@ -384,7 +400,7 @@ Module ResponseTimeAnalysis.
set workload_bound := fun (tup: task_with_response_time) =>
let (tsk_k, R_k) := tup in
if interferes_with_tsk tsk_k then
W tsk_k R_k R
W task_cost task_period tsk_k R_k R
else 0.
(* Now we start the proof. Assume by contradiction that job j
......@@ -429,8 +445,7 @@ Module ResponseTimeAnalysis.
by destruct (sched cpu t);[by rewrite HAScpu mul1n RATE|by ins].
}
{
apply workload_bounded_by_W with
(job_cost := job_cost) (job_deadline := job_deadline); ins;
apply workload_bounded_by_W with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline); ins;
[ by rewrite RATE
| by apply TASK_PARAMS
| by apply RESTR
......@@ -504,10 +519,10 @@ Module ResponseTimeAnalysis.
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;
rewrite IN; [by rewrite andTb | by rewrite andFb].
[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));
last by ins; destruct (i \in ts) eqn:IN; rewrite IN ?andTb ?andFb.
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).
}
......@@ -576,7 +591,7 @@ Module ResponseTimeAnalysis.
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;
rewrite INTERFa; last by ins.
last by ins.
move: INTERFa => /andP INTERFa; des.
apply leq_sum; ins.
destruct (backlogged job_cost rate sched j i);
......@@ -664,7 +679,7 @@ Module ResponseTimeAnalysis.
task_is_scheduled job_task sched i t));
last first.
{
ins; destruct ((i \in ts) && interferes_with_tsk i) eqn:INTERi; rewrite INTERi;
ins; destruct ((i \in ts) && interferes_with_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].
......@@ -693,7 +708,7 @@ Module ResponseTimeAnalysis.
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_fp tsk hp_bounds
total_interference_bound_fp task_cost task_period tsk hp_bounds
R higher_eq_priority).
{
apply leq_trans with (n := \sum_(tsk_k <- ts) minn (x tsk_k) (R - task_cost tsk + 1));
......@@ -743,8 +758,8 @@ Module ResponseTimeAnalysis.
unfold interference_bound, workload_bound, x in *.
fold (interferes_with_tsk); destruct (interferes_with_tsk tsk_k) eqn:INTERFk;
[rewrite andbT in ALL; rewrite andbT | by rewrite andbF min0n].
destruct (tsk_k \in ts) eqn:INk; rewrite INk; last by rewrite min0n.
by rewrite INk andTb -leqNgt in ALL.
destruct (tsk_k \in ts) eqn:INk; last by rewrite min0n.
by rewrite andTb -leqNgt in ALL.
}
(* For this particular task, we show that x_k > W_k.
......@@ -753,7 +768,7 @@ Module ResponseTimeAnalysis.
destruct tup_k as [tsk_k R_k]; simpl in LTmin.
move: LTmin => /andP [INTERFk LTmin]; move: (INTERFk) => /andP [INk INTERFk'].
rewrite INTERFk' in LTmin; unfold minn at 1 in LTmin.
destruct (W tsk_k R_k R < R - task_cost tsk + 1); rewrite leq_min in LTmin;
destruct (W task_cost task_period tsk_k R_k R < R - task_cost tsk + 1); rewrite leq_min in LTmin;
last by move: LTmin => /andP [_ BUG]; rewrite ltnn in BUG.
move: LTmin => /andP [BUG _]; des.
specialize (WORKLOAD tsk_k INTERFk R_k HPk).
......
BertognaResponseTimeFP.v
+ 39
− 27
View file @ 724884f9
......@@ -4,14 +4,23 @@ Require Import Vbase ScheduleDefs BertognaResponseTimeDefs divround helper
Module ResponseTimeIterationFP.
Import Schedule ResponseTimeAnalysis.
Section Analysis.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
Let task_with_response_time := (sporadic_task * nat)%type.
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.
Variable higher_eq_priority: fp_policy sporadic_task.
Hypothesis H_valid_policy: valid_fp_policy higher_eq_priority.
(* Next we define the fixed-point iteration for computing
......@@ -30,8 +39,8 @@ Module ResponseTimeIterationFP.
iter step
(fun t => task_cost tsk +
div_floor
(total_interference_bound_fp
tsk R_prev t higher_eq_priority)
(total_interference_bound_fp task_cost task_period tsk
R_prev t higher_eq_priority)
num_cpus)
(task_cost tsk).
......@@ -59,12 +68,12 @@ Module ResponseTimeIterationFP.
(* To return the complete list of response-time bounds for any task set,
we just apply foldl (reduce) using the function above. *)
Definition R_list (ts: sporadic_taskset) : option (seq task_with_response_time) :=
Definition R_list (ts: taskset_of sporadic_task) : option (seq task_with_response_time) :=
foldl R_list_helper (Some [::]) ts.
(* The schedulability test simply checks if we got a list of
response-time bounds (i.e., if the computation did not fail). *)
Definition fp_schedulable (ts: sporadic_taskset) :=
Definition fp_schedulable (ts: taskset_of sporadic_task) :=
R_list ts != None.
Section AuxiliaryLemmas.
......@@ -268,19 +277,18 @@ Module ResponseTimeIterationFP.
}
Qed.
(* To prove convergence of R, we first show convergence of rt_rec. *)
Lemma per_task_rta_converges:
(* To prove convergence of R, we first show convergence of rt_rec. *) Lemma per_task_rta_converges:
forall ts' tsk rt_bounds,
valid_sporadic_taskset ts' ->
valid_sporadic_taskset task_cost task_period task_deadline ts' ->
R_list ts' = Some rt_bounds ->
per_task_rta tsk rt_bounds (max_steps tsk) <= task_deadline tsk ->
per_task_rta tsk rt_bounds (max_steps tsk) =
per_task_rta tsk rt_bounds (max_steps tsk).+1.
Proof.
unfold valid_sporadic_taskset, valid_sporadic_task in *.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
(* To simplify, let's call the function f.*)
intros ts tsk rt_bounds VALID SOME LE;
intros ts' tsk rt_bounds VALID SOME LE;
set (f := per_task_rta tsk rt_bounds); fold f in LE.
(* First prove that f is monotonic.*)
......@@ -298,13 +306,13 @@ Module ResponseTimeIterationFP.
intros i; destruct (i \in rt_bounds) eqn:HP;
last by rewrite andFb.
destruct i as [i R]; intros _.
have GE_COST := (R_list_ge_cost ts rt_bounds i R).
have INts := (R_list_non_empty ts rt_bounds i SOME).
have GE_COST := (R_list_ge_cost ts' rt_bounds i R).
have INts := (R_list_non_empty ts' rt_bounds i SOME).
destruct INts as [_ EX]; exploit EX; [by exists R | intro IN].
unfold interference_bound; simpl.
rewrite leq_min; apply/andP; split.
{
apply leq_trans with (n := W i R x1);
apply leq_trans with (n := W task_cost task_period i R x1);
first by apply geq_minl.
specialize (VALID i IN); des.
by apply W_monotonic; try (by ins); apply GE_COST.
......@@ -349,11 +357,11 @@ Module ResponseTimeIterationFP.
by apply leq_ltn_trans with (m := f (task_deadline tsk).+1) in BY1;
[by rewrite ltnn in BY1 | by ins].
Qed.
Lemma per_task_rta_fold :
forall tsk rt_bounds,
task_cost tsk +
div_floor (total_interference_bound_fp tsk rt_bounds
div_floor (total_interference_bound_fp task_cost task_period 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.
......@@ -452,7 +460,7 @@ Module ResponseTimeIterationFP.
Section Proof.
(* Consider a task set ts. *)
Variable ts: sporadic_taskset.
Variable ts: taskset_of sporadic_task.
(* Assume that higher_eq_priority is a total order.
Actually, it just needs to be total over the task set,
......@@ -467,7 +475,8 @@ Module ResponseTimeIterationFP.
Hypothesis H_ts_is_a_set: uniq ts.
(* ...all tasks have valid parameters, ... *)
Hypothesis H_valid_task_parameters: valid_sporadic_taskset ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
......@@ -486,10 +495,11 @@ Module ResponseTimeIterationFP.
(* ...they have valid parameters,...*)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_sporadic_job job_cost job_deadline job_task j.
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* ... and satisfy the sporadic task model.*)
Hypothesis H_sporadic_tasks: sporadic_task_model arr_seq job_task.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* Then, consider any platform with at least one CPU and unit
unit execution rate, where...*)
......@@ -554,7 +564,7 @@ Module ResponseTimeIterationFP.
clear ALLJOBS.
unfold fp_schedulable, R_list in *.
induction ts as [| ts' tsk_i] using last_ind.
induction ts as [| ts' tsk_i IH] using last_ind.
{
intros rt_bounds tsk R SOME IN.
by inversion SOME; subst; rewrite in_nil in IN.
......@@ -566,7 +576,7 @@ Module ResponseTimeIterationFP.
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).
apply IH 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.
......@@ -597,13 +607,13 @@ Module ResponseTimeIterationFP.
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)
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 apply R_list_unzip1 with (R := R_lst).
{
intros hp_tsk R0 HP j0 JOB0.
apply IHs with (rt_bounds := hp_bounds) (tsk := hp_tsk); try (by ins).
apply IH 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.
......@@ -688,7 +698,7 @@ Module ResponseTimeIterationFP.
rewrite eqn_leq; apply/andP; split; first by apply service_interval_le_cost.
apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, valid_sporadic_task in *.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
apply service_monotonic; rewrite leq_add2l.
specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
......@@ -736,4 +746,6 @@ Module ResponseTimeIterationFP.
End Proof.
End ResponseTimeIterationFP.
\ No newline at end of file
End Analysis.
End ResponseTimeIterationFP.
\ No newline at end of file
PriorityDefs.v
+ 22
− 24
View file @ 724884f9
......@@ -8,9 +8,7 @@ Module Priority.
Section PriorityDefs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable num_cpus: nat.
Variable arr_seq: arrival_sequence Job.
(* All the priority relations are non-strict, i.e., they specify that
......@@ -25,6 +23,7 @@ Module Priority.
(* FP policy is simply a relation between tasks.
Because our model of processor platform is based on a generic JLDP policy,
we generate a JLDP policy from an FP policy whenever required. *)
Variable sporadic_task: eqType.
Definition fp_policy := sporadic_task -> sporadic_task -> bool.
Section ValidJLFPPolicy.
......@@ -41,9 +40,7 @@ Module Priority.
(* A policy is total, since it must know the priority of any two jobs at any time. *)
Definition jlfp_is_total :=
forall (sched: schedule num_cpus arr_seq)
(j1 j2: JobIn arr_seq) t,
is_higher_priority sched t j1 j2 \/ is_higher_priority sched t j2 j1.
forall t, total (is_higher_priority t).
(* A JLDP policy is valid iff it satisfies the three properties.
Note that, for generality, we don't enforce antisymmetry and allow multiple
......@@ -61,9 +58,7 @@ Module Priority.
Definition fp_is_transitive := transitive is_higher_priority.
Definition fp_is_total :=
forall tsk1 tsk2,
is_higher_priority tsk1 tsk2 \/ is_higher_priority tsk2 tsk1.
Definition fp_is_total := total is_higher_priority.
(* We enforce the same restrictions for FP policy: reflexive, transitive, total. *)
Definition valid_fp_policy :=
......@@ -75,6 +70,10 @@ Module Priority.
Section RateDeadlineMonotonic.
Context {sporadic_task: eqType}.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
(* Rate-Monotonic and Deadline-Monotonic priority order *)
Definition RM (tsk1 tsk2: sporadic_task) := task_period tsk1 <= task_period tsk2.
......@@ -85,7 +84,7 @@ Module Priority.
unfold valid_fp_policy, fp_is_reflexive, fp_is_transitive, RM;
repeat (split; try red); first by ins.
by intros x y z XY YZ; apply leq_trans with (n := task_period x).
by intros tsk1 tsk2; destruct (leqP (task_period tsk1) (task_period tsk2));
by red; intros tsk1 tsk2; apply/orP; destruct (leqP (task_period tsk1) (task_period tsk2));
[by left | by right; apply ltnW].
Qed.
......@@ -94,7 +93,7 @@ Module Priority.
unfold valid_fp_policy, fp_is_reflexive, fp_is_transitive, DM;
repeat (split; try red); first by ins.
by intros x y z; apply leq_trans.
by intros tsk1 tsk2; destruct (leqP (task_deadline tsk1) (task_deadline tsk2));
by red; intros tsk1 tsk2; apply/orP; destruct (leqP (task_deadline tsk1) (task_deadline tsk2));
[by left | by right; apply ltnW].
Qed.
......@@ -102,13 +101,14 @@ Module Priority.
Section GeneralizeFP.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job -> sporadic_task.
Variable arr_seq: arrival_sequence Job.
Variable num_cpus: nat.
Definition fp_to_jldp (task_hp: fp_policy) : jldp_policy num_cpus arr_seq :=
fun (sched: schedule num_cpus arr_seq) (t: time) (jhigh jlow: JobIn arr_seq) =>
Definition fp_to_jldp (task_hp: fp_policy sporadic_task) : jldp_policy arr_seq :=
fun (t: time) (jhigh jlow: JobIn arr_seq) =>
task_hp (job_task jhigh) (job_task jlow).
Lemma valid_fp_is_valid_jldp :
......@@ -127,16 +127,17 @@ Module Priority.
Section JLFPDefs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Context {num_cpus: nat}.
Context {arr_seq: arrival_sequence Job}.
Variable is_higher_priority: jldp_policy num_cpus arr_seq.
Variable is_higher_priority: jldp_policy arr_seq.
(* JLFP policy is a JLDP policy where the priorities do not vary with time. *)
Definition is_jlfp_policy (is_higher_priority: jldp_policy num_cpus arr_seq) :=
forall sched j1 j2 t t',
is_higher_priority sched t j1 j2 -> is_higher_priority sched t' j1 j2.
Definition is_jlfp_policy (is_higher_priority: jldp_policy arr_seq) :=
forall j1 j2 t t',
is_higher_priority t j1 j2 -> is_higher_priority t' j1 j2.
(* Lemma: every FP policy is a JLFP policy. *)
Variable job_task: Job -> sporadic_task.
......@@ -156,7 +157,7 @@ Module Priority.
Context {arr_seq: arrival_sequence Job}.
Variable job_deadline: Job -> nat.
Definition EDF (sched: schedule num_cpus arr_seq) (t: time) (j1 j2: JobIn arr_seq) :=
Definition EDF (t: time) (j1 j2: JobIn arr_seq) :=
job_arrival j1 + job_deadline j1 <= job_arrival j2 + job_deadline j2.
(* Lemma: EDF is a JLFP policy. *)
......@@ -171,14 +172,14 @@ Module Priority.
repeat (split; try red).
by ins; apply leqnn.
by intros sched t y x z; apply leq_trans.
by intros sched j1 j2 t;
by intros _; red; intros j1 j2; apply/orP;
destruct (leqP (job_arrival j1 + job_deadline j1) (job_arrival j2 + job_deadline j2));
[by left | by right; apply ltnW].
Qed.
End EDFDefs.
Section ScheduleIndependent.
(*Section ScheduleIndependent.
Context {Job: eqType}.
Context {num_cpus: nat}.
......@@ -203,7 +204,7 @@ Module Priority.
by unfold schedule_independent, fp_to_jldp.
Qed.
End ScheduleIndependent.
End ScheduleIndependent.*)
End Priority.
......@@ -229,7 +230,4 @@ Definition interferes_with (jlow jhigh: job) :=
Definition num_interfering_jobs (jlow: job) :=
count (interferes_with jlow) (all_arrivals sched t).
End BasicDefinitions.*)
\ No newline at end of file
End BasicDefinitions.*)
\ No newline at end of file
ResponseTimeDefs.v
+ 7
− 2
View file @ 724884f9
......@@ -7,7 +7,8 @@ Module ResponseTime.
Import Schedule SporadicTaskset SporadicTaskArrival.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Context {arr_seq: arrival_sequence Job}.
Variable job_cost: Job -> nat.
......@@ -38,6 +39,7 @@ Module ResponseTime.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
......@@ -130,6 +132,9 @@ Module ResponseTime.
Section LowerBoundOfResponseTimeBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
......@@ -164,7 +169,7 @@ Module ResponseTime.
Lemma response_time_ub_ge_task_cost:
R >= task_cost tsk.
Proof.
unfold valid_sporadic_task, job_has_completed_by, completed in *.
unfold job_has_completed_by, completed in *.
rename job_of_tsk_exists into EX; des.
set new_cost := fun (j': Job) => task_cost (job_task j').
apply leq_trans with (n := new_cost j);
......
SchedulabilityDefs.v
+ 6
− 5
View file @ 724884f9
......@@ -12,7 +12,7 @@ Module Schedulability.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Section SingleSchedule.
Section ScheduleOfJobs.
Context {num_cpus: nat}.
Variable rate: Job -> processor num_cpus -> nat.
......@@ -23,17 +23,18 @@ Module Schedulability.
Definition job_misses_no_deadline :=
completed job_cost rate sched j (job_arrival j + job_deadline j).
End SingleSchedule.
End ScheduleOfJobs.
Section SingleScheduleTasks.
Section ScheduleOfTasks.
Context {sporadic_task: eqType}.
Variable job_task: Job -> sporadic_task.
Context {num_cpus: nat}.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
Variable ts: sporadic_taskset.
Variable ts: taskset_of sporadic_task.
Variable tsk: sporadic_task.
Definition task_misses_no_deadline :=
......@@ -47,7 +48,7 @@ Module Schedulability.
job_arrival j + job_deadline j <= t' ->
job_misses_no_deadline rate sched j.
End SingleScheduleTasks.
End ScheduleOfTasks.
End SchedulableDefs.
......
ScheduleDefs.v
+ 15
− 0
View file @ 724884f9
......@@ -392,6 +392,21 @@ Module ScheduleOfTaskWithJitter.
forall j t,
scheduled sched j t ->
job_arrival j + job_jitter j <= t.
Section BasicLemmas.
Lemma arrival_before_jitter :
jobs_execute_after_jitter ->
jobs_must_arrive_to_execute sched.
Proof.
unfold jobs_execute_after_jitter, jobs_must_arrive_to_execute.
intros ARRIVE j t SCHED; unfold has_arrived.
rewrite -(leq_add2r (job_jitter j)).
by apply leq_trans with (n := t);
[by apply ARRIVE | by apply leq_addr].
Qed.
End BasicLemmas.
End ArrivalAfterJitter.
......
TaskDefs.v
+ 23
− 19
View file @ 724884f9
......@@ -45,33 +45,37 @@ End SporadicTask.
Module SporadicTaskset.
Export SporadicTask.
(* Define task set as a sequence of sporadic tasks. *)
Variable Task: eqType.
Definition sporadic_taskset := seq Task.
Section TasksetDefs.
(* Define task set as a sequence of sporadic tasks. *)
Definition taskset_of (T: eqType) := seq T.
Section TasksetProperties.
Section TasksetProperties.
Variable task_cost: Task -> nat.
Variable task_period: Task -> nat.
Variable task_deadline: Task -> nat.
Context {Task: eqType}.
Variable task_cost: Task -> nat.
Variable task_period: Task -> nat.
Variable task_deadline: Task -> nat.
Variable ts: taskset_of Task.
Variable ts: sporadic_taskset.
Let is_valid_task :=
is_valid_sporadic_task task_cost task_period task_deadline.
Let is_valid_task :=
is_valid_sporadic_task task_cost task_period task_deadline.
Definition valid_sporadic_taskset :=
forall tsk (IN: tsk \in ts), is_valid_task tsk.
Definition valid_sporadic_taskset :=
forall tsk (IN: tsk \in ts), is_valid_task tsk.
(* Deadline models: implicit, restricted or arbitrary *)
Definition implicit_deadline_model :=
forall tsk (IN: tsk \in ts), task_deadline tsk = task_period tsk.
(* Deadline models: implicit, restricted or arbitrary *)
Definition implicit_deadline_model :=
forall tsk (IN: tsk \in ts), task_deadline tsk = task_period tsk.
Definition restricted_deadline_model :=
forall tsk (IN: tsk \in ts), task_deadline tsk <= task_period tsk.
Definition restricted_deadline_model :=
forall tsk (IN: tsk \in ts), task_deadline tsk <= task_period tsk.
Definition arbitrary_deadline_model := True.
Definition arbitrary_deadline_model := True.
End TasksetProperties.
End TasksetProperties.
End TasksetDefs.
End SporadicTaskset.
\ No newline at end of file
WorkloadDefs.v
+ 39
− 18
View file @ 724884f9
......@@ -7,7 +7,8 @@ Module Workload.
Import Job SporadicTaskset Schedule SporadicTaskArrival ResponseTime Schedulability.
Section WorkloadDef.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job -> sporadic_task.
Context {arr_seq: arrival_sequence Job}.
......@@ -99,6 +100,10 @@ Module Workload.
Section WorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable tsk: sporadic_task.
Variable R_tsk: time. (* Known response-time bound for the task *)
Variable delta: time. (* Length of the interval *)
......@@ -110,7 +115,6 @@ Module Workload.
(* Bertogna and Cirinei's bound on the workload of a task in an interval of length delta *)
Definition W :=
let e_k := (task_cost tsk) in
let d_k := (task_deadline tsk) in
let p_k := (task_period tsk) in
minn e_k (delta + R_tsk - e_k - max_jobs * p_k) + max_jobs * e_k.
......@@ -118,18 +122,26 @@ Module Workload.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable tsk: sporadic_task.
Hypothesis period_positive: task_period tsk > 0.
Variable R: time.
Hypothesis R_lower_bound: R >= task_cost tsk.
Lemma W_monotonic :
forall t1 t2, t1 <= t2 -> W tsk R t1 <= W tsk R t2.
Proof.
intros t1 t2 LEt.
unfold W, max_jobs, div_floor; rewrite 2!subndiv_eq_mod.
set e := task_cost tsk; set p := task_period tsk.
Let workload_bound := W task_cost task_period tsk R.
Lemma W_monotonic :
forall t1 t2,
t1 <= t2 ->
workload_bound t1 <= workload_bound t2.
Proof.
intros t1 t2 LEt.
unfold workload_bound, W, max_jobs, div_floor; rewrite 2!subndiv_eq_mod.
set e := task_cost tsk; set p := task_period tsk.
generalize dependent t2; rewrite leq_as_delta.
induction delta;
......@@ -182,8 +194,13 @@ Module Workload.
End BasicLemmas.
Section ProofWorkloadBound.
Variable Job: eqType.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
Variable job_deadline: Job -> nat.
......@@ -193,7 +210,7 @@ Module Workload.
(* Assume that all jobs have valid parameters *)
Hypothesis jobs_have_valid_parameters :
forall (j: JobIn arr_seq),
valid_sporadic_job job_cost job_deadline job_task j.
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
......@@ -225,7 +242,7 @@ Module Workload.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
are separated by at least 'period' times units. *)
Hypothesis sporadic_tasks: sporadic_task_model arr_seq job_task.
Hypothesis sporadic_tasks: sporadic_task_model task_period arr_seq job_task.
(* Before starting the proof, let's give simpler names to the definitions. *)
Definition response_time_bound_of (tsk: sporadic_task) (R: time) :=
......@@ -248,7 +265,8 @@ Module Workload.
jobs is at least (cost + n*period), where n is the number
of middle jobs. If cost >> period, the claim does not hold
for every task set. *)
Hypothesis valid_task_parameters: valid_sporadic_task tsk.
Hypothesis valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
(* Assumption: the task must have a restricted deadline.
This is required to prove that n_k (max_jobs) from Bertogna
......@@ -268,19 +286,22 @@ Module Workload.
Hypothesis no_deadline_misses_during_interval: no_deadline_misses_by tsk (t1 + delta).
(* Then the workload of the task in the interval is bounded by W. *)
Let workload_bound := W task_cost task_period.
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) <= W tsk R_tsk delta.
workload_of tsk t1 (t1 + delta) <= workload_bound tsk R_tsk delta.
Proof.
rename jobs_have_valid_parameters into job_properties,
no_deadline_misses_during_interval into no_dl_misses,
valid_task_parameters into task_properties.
unfold valid_sporadic_job, valid_realtime_job, restricted_deadline_model,
valid_sporadic_taskset, valid_sporadic_task, sporadic_task_model,
workload_of, response_time_bound_of, no_deadline_misses_by, W in *; ins; des.
valid_sporadic_taskset, is_valid_sporadic_task, sporadic_task_model,
workload_of, response_time_bound_of, no_deadline_misses_by, workload_bound, W in *; ins; des.
(* Simplify names *)
set t2 := t1 + delta.
set n_k := max_jobs tsk R_tsk delta.
set n_k := max_jobs task_cost task_period tsk R_tsk delta.
(* Use the definition of workload based on list of jobs. *)
rewrite workload_eq_workload_joblist; unfold workload_joblist.
......
WorkloadDefsJitter.v
+ 68
− 41
View file @ 724884f9
......@@ -4,11 +4,16 @@ Require Import Vbase JobDefs TaskDefs ScheduleDefs TaskArrivalDefs ResponseTimeD
Module WorkloadWithJitter.
Import Job SporadicTasksetWithJitter ScheduleOfTaskWithJitter
Import Job SporadicTaskset ScheduleOfTaskWithJitter
SporadicTaskArrival ResponseTime Schedulability Workload.
Section WorkloadBoundWithJitter.
Context {sporadic_task_with_jitter: eqType}.
Variable task_cost: sporadic_task_with_jitter -> nat.
Variable task_period: sporadic_task_with_jitter -> nat.
Variable task_jitter: sporadic_task_with_jitter -> nat.
Context {Job: eqType}.
Variable job_task: Job -> sporadic_task_with_jitter.
Context {arr_seq: arrival_sequence Job}.
......@@ -29,7 +34,6 @@ Module WorkloadWithJitter.
(* Bertogna and Cirinei's bound on the workload of a task in an interval of length delta *)
Definition W_jitter :=
let e_k := (task_cost tsk) in
let d_k := (task_deadline tsk) in
let p_k := (task_period tsk) in
let j_k := (task_jitter tsk) in
minn e_k (delta + j_k + R_tsk - e_k - max_jobs_jitter * p_k) + max_jobs_jitter * e_k.
......@@ -38,19 +42,26 @@ Module WorkloadWithJitter.
Section BasicLemmas.
Context {sporadic_task_with_jitter: eqType}.
Variable task_cost: sporadic_task_with_jitter -> nat.
Variable task_period: sporadic_task_with_jitter -> nat.
Variable task_jitter: sporadic_task_with_jitter -> nat.
Variable tsk: sporadic_task_with_jitter.
Hypothesis period_positive: task_period tsk > 0.
Variable R: time.
Hypothesis R_lower_bound: R >= task_cost tsk.
Lemma W_monotonic :
Let workload_bound := W_jitter task_cost task_period task_jitter tsk R.
Lemma W_jitter_monotonic :
forall t1 t2,
t1 <= t2 ->
W_jitter tsk R t1 <= W_jitter tsk R t2.
workload_bound t1 <= workload_bound t2.
Proof.
intros t1 t2 LEt.
unfold W_jitter, max_jobs_jitter, div_floor; rewrite 2!subndiv_eq_mod.
unfold workload_bound, W_jitter, max_jobs_jitter, div_floor; rewrite 2!subndiv_eq_mod.
set e := task_cost tsk; set p := task_period tsk; set j := task_jitter tsk.
generalize dependent t2; rewrite leq_as_delta.
......@@ -104,8 +115,14 @@ Module WorkloadWithJitter.
End BasicLemmas.
Section ProofWorkloadBoundJitter.
Variable Job: eqType.
Context {sporadic_task_with_jitter: eqType}.
Variable task_cost: sporadic_task_with_jitter -> nat.
Variable task_period: sporadic_task_with_jitter -> nat.
Variable task_deadline: sporadic_task_with_jitter -> nat.
Variable task_jitter: sporadic_task_with_jitter -> nat.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task_with_jitter.
Variable job_deadline: Job -> nat.
......@@ -116,7 +133,7 @@ Module WorkloadWithJitter.
(* Assume that all jobs have valid parameters *)
Hypothesis jobs_have_valid_parameters :
forall (j: JobIn arr_seq),
valid_sporadic_job_with_jitter job_cost job_deadline job_task job_jitter j.
valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
......@@ -148,7 +165,8 @@ Module WorkloadWithJitter.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
are separated by at least 'period' times units. *)
Hypothesis sporadic_tasks: sporadic_task_model arr_seq job_task.
Hypothesis sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* Before starting the proof, let's give simpler names to the definitions. *)
Section CleanerDefinitions.
......@@ -173,7 +191,8 @@ Module WorkloadWithJitter.
jobs is at least (cost + n*period), where n is the number
of middle jobs. If cost >> period, the claim does not hold
for every task set. *)
Hypothesis valid_task_parameters: valid_sporadic_task tsk.
Hypothesis valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
(* Assumption: the task must have a restricted deadline.
This is required to prove that n_k (max_jobs) from Bertogna
......@@ -192,20 +211,23 @@ Module WorkloadWithJitter.
Variable t1 delta: time.
Hypothesis no_deadline_misses_during_interval: no_deadline_misses_by tsk (t1 + delta).
(* Then the workload of the task in the interval is bounded by W. *)
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) <= W_jitter tsk R_tsk delta.
(* Then the workload of the task in the interval is bounded by W_jitter. *)
Let workload_bound := W_jitter task_cost task_period task_jitter.
Theorem workload_bounded_by_W_jitter :
workload_of tsk t1 (t1 + delta) <= workload_bound tsk R_tsk delta.
Proof.
rename jobs_have_valid_parameters into job_properties,
no_deadline_misses_during_interval into no_dl_misses,
valid_task_parameters into task_properties.
unfold valid_sporadic_job, valid_realtime_job, restricted_deadline_model,
valid_sporadic_taskset, valid_sporadic_task, sporadic_task_model,
workload_of, response_time_bound_of, no_deadline_misses_by, W in *; ins; des.
valid_task_parameters into task_properties,
H_jobs_must_arrive_after_jitter into ARRIVE.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job, valid_realtime_job, restricted_deadline_model, jobs_execute_after_jitter,
valid_sporadic_taskset, is_valid_sporadic_task, sporadic_task_model,
workload_of, response_time_bound_of, no_deadline_misses_by, workload_bound, W_jitter in *; ins; des.
(* Simplify names *)
set t2 := t1 + delta.
set n_k := max_jobs_jitter tsk R_tsk delta.
set n_k := max_jobs_jitter task_cost task_period task_jitter tsk R_tsk delta.
(* Use the definition of workload based on list of jobs. *)
rewrite workload_eq_workload_joblist; unfold workload_joblist.
......@@ -227,11 +249,7 @@ Module WorkloadWithJitter.
rewrite (eq_bigr (fun x => 0)); last by move => j_i /andP JOBi; des; apply /eqP.
rewrite big_const_seq iter_addn mul0n add0n add0n.
by rewrite big_filter.
}
Set Printing All. idtac.
simpl
rewrite SIMPL. rewrite SIMPL; clear SIMPL.
} rewrite SIMPL; clear SIMPL.
(* Remember that for any job of tsk, service <= task_cost tsk *)
assert (LTserv: forall j_i (INi: j_i \in interfering_jobs),
......@@ -326,7 +344,7 @@ Module WorkloadWithJitter.
apply leq_add; last by ins.
apply leq_trans with (n := \sum_(t1 <= t < t2) 1).
by apply leq_sum; ins; apply service_at_le_max_rate.
by unfold t2; rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA // subnn addn0.
by unfold t2; rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA // subnn addn0 leq_addr.
}
}
} rewrite [nth]lock /= -lock in ALL.
......@@ -360,13 +378,14 @@ Module WorkloadWithJitter.
move: LTsize => /andP [LTsize _]; des.
move: LTsize => /andP [_ SERV].
move: SERV => /eqP SERV; apply SERV.
by unfold service_during; rewrite sum_service_before_arrival.
unfold service_during; rewrite sum_service_before_arrival; try (by ins).
by apply arrival_before_jitter with (job_jitter0 := job_jitter).
}
(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
assert (BOUNDend: service_during rate sched j_fst t1 t2 +
service_during rate sched j_lst t1 t2 <=
(job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst)).
(job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst)).
{
apply leq_add; unfold service_during.
{
......@@ -402,7 +421,10 @@ Module WorkloadWithJitter.
apply negbT in LT; rewrite -ltnNge in LT.
rewrite -> big_cat_nat with (n := job_arrival j_lst); [|by apply ltnW| by apply ltnW].
rewrite /= -[\sum_(_ <= _ < _) 1]add0n; apply leq_add.
rewrite sum_service_before_arrival; [by apply leqnn | by ins | by apply leqnn].
{
rewrite sum_service_before_arrival; [by ins| |by apply leqnn].
by apply arrival_before_jitter with (job_jitter0 := job_jitter).
}
by apply leq_sum; ins; apply service_at_le_max_rate.
}
}
......@@ -495,8 +517,8 @@ Module WorkloadWithJitter.
apply leq_trans with (n := n_k.+2 * task_period tsk).
{
rewrite -addn1 mulnDl mul1n leq_add2r.
apply leq_trans with (n := delta + R_tsk - task_cost tsk);
first by rewrite -addnBA //; apply leq_addr.
apply leq_trans with (n := delta + task_jitter tsk + R_tsk - task_cost tsk);
first by rewrite -addnBA // -addnA; apply leq_addr.
by apply ltnW, ltn_ceil, task_properties0.
}
by apply leq_trans with (n.+1 * task_period tsk);
......@@ -524,7 +546,7 @@ Module WorkloadWithJitter.
rewrite -addnA leq_add2l -[job_deadline _]addn0.
apply leq_add; last by ins.
specialize (job_properties j_fst); des.
by rewrite job_properties1 FSTtask restricted_deadline.
by rewrite job_properties2 FSTtask restricted_deadline.
}
rewrite leqNgt; apply/negP; unfold not; intro LTt1.
(* Now we assume that (job_arrival j_fst + d_k < t1) and reach a contradiction.
......@@ -541,11 +563,10 @@ Module WorkloadWithJitter.
unfold service; rewrite -> big_cat_nat with (m := 0) (p := t2) (n := t1);
[rewrite leq_add2r /= | by ins | by apply leq_addr].
rewrite -> big_cat_nat with (p := t1) (n := job_arrival j_fst + job_deadline j_fst);
[| by ins | by apply ltnW; specialize (job_properties j_fst); des;
rewrite job_properties1 FSTtask].
[| by ins | by apply ltnW; specialize (job_properties j_fst); des; rewrite job_properties2 FSTtask].
by rewrite /= -{1}[\sum_(_ <= _ < _) _]addn0 leq_add2l.
}
}
}
}
(* With the facts that we derived, we can now prove the workload bound.
......@@ -563,28 +584,35 @@ Module WorkloadWithJitter.
{
rewrite subnAC subnK; last first.
{
assert (TMP: delta + R_tsk = task_cost tsk + (delta + R_tsk - task_cost tsk));
assert (TMP: delta + task_jitter tsk + R_tsk = task_cost tsk + (delta + task_jitter tsk + R_tsk - task_cost tsk));
first by rewrite subnKC; [by ins | by rewrite -[task_cost _]add0n; apply leq_add].
rewrite TMP; clear TMP.
rewrite -{1}[task_cost _]addn0 -addnBA NK; [by apply leq_add | by apply leq_trunc_div].
}
apply leq_trans with (delta + R_tsk - (job_arrival j_lst - job_arrival j_fst));
first by rewrite addnC; apply BOUNDend.
by apply leq_sub2l, DIST.
apply leq_trans with (delta + R_tsk - n.+1 * task_period tsk);
first by apply leq_sub2l, DIST.
by rewrite leq_sub2r // leq_add2r leq_addr.
}
}
{
(* Case 2: n_k = n, where n is the number of middle jobs. *)
move: NK => /eqP NK; rewrite -NK.
apply leq_add; [clear BOUNDmid | by apply BOUNDmid].
apply leq_trans with (delta + R_tsk - (job_arrival j_lst - job_arrival j_fst));
first by rewrite addnC; apply BOUNDend.
apply leq_trans with (delta + task_jitter tsk + R_tsk - (job_arrival j_lst - job_arrival j_fst)).
{
apply leq_trans with (delta + R_tsk - (job_arrival j_lst - job_arrival j_fst));
first by rewrite addnC BOUNDend.
by rewrite leq_sub2r // leq_add2r leq_addr.
}
rewrite leq_min; apply/andP; split.
{
rewrite leq_subLR [_ + task_cost _]addnC -leq_subLR.
apply leq_trans with (n.+1 * task_period tsk); last by apply DIST.
rewrite NK ltnW // -ltn_divLR; last by apply task_properties0.
by unfold n_k, max_jobs, div_floor.
by unfold n_k, max_jobs_jitter, div_floor.
}
{
rewrite -subnDA; apply leq_sub2l.
......@@ -592,8 +620,7 @@ Module WorkloadWithJitter.
rewrite -addn1 addnC mulnDl mul1n.
rewrite leq_add2l; last by apply task_properties3.
}
}*)
admit.
}
Qed.
End ProofWorkloadBoundJitter.
......
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