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

Fix RT-bound def and try to prove R >= cost

parent f60c704e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
ResponseTimeDefs.v
+ 66
− 149
View file @ 69714df7
......@@ -8,8 +8,7 @@ Module ResponseTime.
Section ResponseTimeBound.
Context {Job: eqType}.
Variable job_arrival: Job -> nat.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
Variable num_cpus: nat.
......@@ -18,24 +17,29 @@ Module ResponseTime.
Variable tsk: sporadic_task.
Definition job_has_completed_by (sched: schedule Job) :=
Definition job_has_completed_by (job_cost: Job -> nat) (sched: schedule Job) :=
completed job_cost num_cpus rate sched.
Definition response_time_ub_task (response_time_bound: time) :=
forall (sched: schedule Job) (j: Job),
forall (job_arrival: Job -> nat)
(job_cost: Job -> nat)
(sched: schedule Job) (j: Job),
job_task j == tsk ->
schedule_of_platform sched ->
job_has_completed_by sched j (job_arrival j + response_time_bound).
(* job_arrival and job_cost are valid -> *)
job_has_completed_by job_cost sched j (job_arrival j + response_time_bound).
Section BasicLemmas.
Variable sched: schedule Job.
Hypothesis platform: schedule_of_platform sched.
Variable response_time_bound: time.
Hypothesis is_response_time_bound:
response_time_ub_task response_time_bound.
Variable job_arrival: Job -> nat.
Variable job_cost: Job -> nat.
Variable sched: schedule Job.
Hypothesis platform: schedule_of_platform sched.
Variable j: Job.
Hypothesis job_of_task: job_task j == tsk.
......@@ -48,9 +52,9 @@ Module ResponseTime.
Proof.
rename response_time_bound into R, is_response_time_bound into RT,
comp_jobs_dont_exec into EXEC; ins.
unfold response_time_ub_task, job_has_completed_by, completed,
unfold response_time_ub_task, completed,
completed_job_doesnt_exec in *.
specialize (RT sched j job_of_task platform).
specialize (RT job_arrival job_cost sched j job_of_task platform).
apply/eqP; rewrite -leqn0.
rewrite <- leq_add2l with (p := job_cost j).
move: RT => /eqP RT; rewrite -{1}RT addn0.
......@@ -72,147 +76,60 @@ Module ResponseTime.
Qed.
End BasicLemmas.
Section LowerBoundOfResponseTimeBound.
End ResponseTimeBound.
End ResponseTime.
(*Variable plat: processor_platform.
Variable ts: sporadic_taskset.
Variable tsk: sporadic_task.
Definition response_time_ub (R: time) :=
forall (sched: schedule) (PLAT: plat sched)
j (JOBof: job_task j == tsk)
t_a (ARRj: arrives_at sched j t_a),
completed sched j (t_a + R).
Import SporadicTaskJob SporadicTaskset Platform.
Definition my_service_at (my_j j: job) (t: time) :=
if my_j == j then
(if t < task_cost (job_task j) then 1 else 0)
else 0.
Definition my_arr_seq (my_j: job) (t: nat) :=
if (t == 0) then [::my_j] else [::].
Section ResponseTimeGEQCost.
Variable ts: sporadic_taskset.
Variable tsk: sporadic_task.
Hypothesis in_ts: tsk \in ts.
Import Job.
Variable response_time_bound: time.
Hypothesis is_response_time_bound:
response_time_ub_task response_time_bound.
Hypothesis set_of_jobs_nonempty:
exists j: Job, job_task j == tsk.
Variable R_tsk: time.
Variable platform: processor_platform.
Hypothesis rt_bound: response_time_ub platform tsk R_tsk.
(*Hypothesis exists_sched:
forall arr_seq, exists (sched: schedule), arr_list sched = arr_seq /\ platform sched.*)
Hypothesis rate_at_most_one:
forall (j: Job) (cpu: processor), rate j cpu <= 1.
Hypothesis service_lt_one :
forall (sched: schedule) (PLAT: platform sched), max_service_one sched.
Lemma response_time_ub_ge_cost: response_time_bound >= task_cost tsk.
Proof.
unfold response_time_ub_task, valid_sporadic_task,
job_has_completed_by, completed in *;
rename set_of_jobs_nonempty into EX, is_response_time_bound into BOUND,
response_time_bound into R; des.
set myarr := fun (j: Job) => 0.
set mysched := fun (cpu: processor) (t: time) =>
if cpu == 0 then
(if t < task_cost (job_task j) then Some j else None)
else None.
assert (PLAT: schedule_of_platform mysched). admit.
set mycost := fun (j: Job) => task_cost (job_task j).
specialize (BOUND myarr mycost mysched j EX PLAT).
move: EX => /eqP EX.
move: BOUND; rewrite eqn_leq; move => /andP [_ LE].
apply leq_trans with (n := service num_cpus rate mysched j (myarr j + R));
first by unfold mycost in LE; rewrite EX in LE.
unfold service, service_at, myarr, mysched.
rewrite exchange_big_nat /=.
destruct num_cpus; first by rewrite big_geq //.
rewrite big_nat_recl // /=.
rewrite -> eq_big_nat with (n := n) (F2 := fun i => 0);
last by ins; rewrite -> eq_big_nat with (F2 := fun i => 0);
by ins; rewrite big_const_nat iter_addn mul0n addn0.
rewrite big_const_nat iter_addn mul0n 2!addn0.
apply leq_trans with (n := \sum_(0 <= i < 0 + R) 1);
last by rewrite big_const_nat iter_addn subn0 add0n mul1n addn0 leqnn.
apply leq_sum; ins.
rewrite -[1]muln1; apply leq_mul; [by apply leq_b1 | by apply rate_at_most_one].
Qed.
Lemma rt_geq_wcet_identmp : R_tsk >= task_cost tsk.
Proof.
rename rt_bound into RESP.
unfold response_time_ub in *; ins; des.
End LowerBoundOfResponseTimeBound.
End ResponseTimeBound.
(*have PROP := task_properties tsk; des.*)
(* assert (VALIDj: << X1: 0 < task_cost tsk >> /\
<< X2: task_cost tsk <= task_deadline tsk >> /\
<< X3: 0 < task_deadline tsk >> /\
<< X4: task_cost tsk <= task_cost tsk >> /\
<< X5: task_deadline tsk = task_deadline tsk >> ).
by repeat split; ins; try apply leqnn; clear tmp_job; rename x0 into j.*)
set j := Build_job 0 (task_cost tsk) (task_deadline tsk) tsk VALIDj.
assert (VALIDarr: << NOMULT: forall (j0 : job_eqType) (t1 t2 : time),
j0 \in my_arr_seq j t1 -> j0 \in my_arr_seq j t2 -> t1 = t2 >> /\
<< ARR_PARAMS: forall (j0 : job_eqType) (t : time),
j0 \in my_arr_seq j t -> job_arrival j0 = t >> /\
<< UNIQ: forall t, uniq (my_arr_seq j t)>>).
{
repeat split; try red.
by intros j0 t1 t2 ARR1 ARR2; unfold my_arr_seq in *; destruct t1, t2; ins.
intros j0 t ARRj0; unfold my_arr_seq in *; destruct t; simpl in *.
by move: ARRj0; rewrite mem_seq1; move => /eqP ARRj0; subst.
by rewrite in_nil in ARRj0.
by intros t; unfold my_arr_seq; destruct (t == 0).
}
set arr := Build_arrival_sequence (my_arr_seq j) VALIDarr.
assert (VALIDsched: (<< VALID0: forall (j0 : job) (t : time),
scheduled {| service_at := my_service_at j; arr_list := arr |} j0 t ->
arrived {| service_at := my_service_at j; arr_list := arr |} j0 t >> /\
<< VALID1: forall (j0 : job) (t : nat) (t_comp : time),
completed {| service_at := my_service_at j; arr_list := arr |} j0 t_comp ->
t_comp <= t ->
~~ scheduled {| service_at := my_service_at j; arr_list := arr |} j0 t >> )).
{
repeat (split; try red).
{
intros j0 t SCHED.
unfold scheduled, arrived in *; apply/exists_inP_nat.
unfold service_at, my_service_at in SCHED.
destruct (j == j0) eqn:EQj_j0; last by move: SCHED => /eqP SCHED; intuition.
destruct (t < task_cost (job_task j0)) eqn:LE; last by move: SCHED => /eqP SCHED; intuition.
exists 0; split; first by apply ltn0Sn.
unfold arrives_at, arr_list, arr, my_arr_seq; simpl.
move: EQj_j0 => /eqP EQj_j0; subst.
by rewrite mem_seq1; apply/eqP.
}
{
unfold completed, service; intros j0 t t_comp COMPLETED LE.
unfold scheduled, service_at, my_service_at.
destruct (j == j0) eqn:EQj_j0; last by apply negbT; apply/eqP.
move: EQj_j0 => /eqP EQj_j0; subst j0.
apply negbT; apply/eqP.
have jPROP := job_properties j; des; simpl in *.
destruct (t < task_cost tsk) eqn:LEcost; last by trivial.
{
assert (LT: t_comp < task_cost tsk).
by apply leq_trans with (n := t.+1); [rewrite ltnS | ins].
move: COMPLETED => /eqP COMPLETED; rewrite <- COMPLETED in *.
assert (LTNN: t_comp < t_comp); last by rewrite ltnn in LTNN.
{
apply leq_trans with (n := \sum_(0 <= t0 < t_comp)
my_service_at j j t0); first by ins.
apply leq_trans with (n := \sum_(0 <= t0 < t_comp) 1);
last by rewrite big_const_nat iter_addn mul1n addn0 subn0.
apply leq_sum; ins; unfold my_service_at; rewrite eq_refl.
by destruct (i < task_cost (job_task j)); ins.
}
}
}
}
specialize (EX arr); des.
assert (ARRts: ts_arrival_sequence ts sched).
{
unfold ts_arrival_sequence; ins.
unfold arrives_at in ARR; rewrite EX /= in ARR.
unfold my_arr_seq in ARR; simpl in ARR.
destruct (t == 0); last by rewrite in_nil in ARR.
by move: ARR; rewrite mem_seq1; move => /eqP ARR; subst; ins.
}
unfold response_time_ub in RESP; des; specialize (RESP0 sched EX0 ARRts j).
exploit RESP0.
by apply/eqP.
by instantiate (1 := 0); unfold arrives_at; rewrite EX /=; unfold my_arr_seq, arrives_at in *;
rewrite mem_seq1; apply/eqP.
unfold completed, service; simpl; move => /eqP SUM; rewrite -SUM add0n.
apply leq_trans with (n := \sum_(0 <= t < R_tsk) 1);
last by rewrite sum_nat_const_nat muln1 subn0.
by apply leq_sum; intros t _; apply service_lt_one, EX0.
Qed.*)
\ No newline at end of file
End ResponseTime.
\ No newline at end of file
ScheduleDefs.v
+ 45
− 2
View file @ 69714df7
......@@ -218,6 +218,11 @@ Module Schedule.
Variable rate: Job -> processor -> nat.
Variable sched: schedule Job.
(* Whether job parallelism is disallowed *)
Definition jobs_dont_execute_in_parallel :=
forall j t cpu1 cpu2,
sched cpu1 t == Some j -> sched cpu2 t == Some j -> cpu1 = cpu2.
(* Whether a job can only be scheduled if it has arrived *)
Definition job_must_arrive_to_exec :=
forall j t, scheduled num_cpus sched j t -> has_arrived job_arrival j t.
......@@ -247,14 +252,52 @@ Module Schedule.
Lemma service_monotonic :
forall t t',
t <= t' ->
(service num_cpus rate sched j t <=
service num_cpus rate sched j t').
service num_cpus rate sched j t <= service num_cpus rate sched j t'.
Proof.
unfold service; ins; rewrite -> big_cat_nat with (p := t') (n := t);
by [apply leq_addr | by ins | by ins].
Qed.
End Basic.
Section MaxRate.
Variable max_rate: nat.
Hypothesis there_is_max_rate:
forall j cpu, rate j cpu <= max_rate.
Hypothesis no_parallelism:
jobs_dont_execute_in_parallel sched.
Lemma service_at_le_max_rate :
forall t, service_at num_cpus rate sched j t <= max_rate.
Proof.
unfold service_at, jobs_dont_execute_in_parallel in *; ins.
rewrite -> eq_bigr with (F2 := fun cpu => if sched cpu t == Some j then rate j cpu else 0);
last by ins; rewrite mulnbl.
rewrite -big_mkcond /=.
destruct (scheduled num_cpus sched j t) eqn:SCHED; unfold scheduled in SCHED.
{
move: SCHED => /(exists_inP_nat num_cpus (fun cpu => sched cpu t == Some j)) SCHED; des.
rewrite -big_filter.
rewrite (bigD1_seq x); [simpl | | by rewrite filter_uniq // iota_uniq];
last by rewrite mem_filter; apply/andP; split;
[by ins | by rewrite mem_iota; apply/andP; split; [by ins | by rewrite subn0 add0n]].
rewrite -big_filter -filter_predI big_filter.
rewrite -> eq_bigr with (F2 := fun cpu => 0);
first by rewrite big_const_seq iter_addn /= mul0n 2!addn0 there_is_max_rate.
intro i; move => /andP [/eqP NEQ SCHEDi].
apply no_parallelism with (cpu1 := x) in SCHEDi; [by subst | by ins].
}
{
apply negbT in SCHED; rewrite negb_exists_in in SCHED.
move: SCHED => /(forall_inP_nat num_cpus (fun cpu => sched cpu t != Some j)) SCHED.
rewrite big_nat_cond big_pred0 //; red; ins; apply/negP; move => /andP [LT EQ].
by specialize (SCHED x LT); move: EQ => /eqP EQ; rewrite EQ eq_refl in SCHED.
}
Qed.
End MaxRate.
Section Completion.
......
WorkloadDefs.v
+ 42
− 40
View file @ 69714df7
......@@ -70,7 +70,8 @@ Module Workload.
by rewrite -> eq_bigr with (F2 := fun i => 0);
[by rewrite big_const_seq iter_addn | by ins].
{
rename s into j; destruct (job_task j == tsk) eqn:EQtsk; try rewrite mul1n; try rewrite mul0n.
rename s into j; destruct (job_task j == tsk) eqn:EQtsk;
try rewrite mul1n; try rewrite mul0n.
{
rewrite -> bigD1_seq with (j := j); last by rewrite filter_undup undup_uniq.
{
......@@ -138,44 +139,30 @@ Module Workload.
Variable sched: schedule Job.
Hypothesis sched_of_platform: schedule_of_platform sched.
(* Assumption: used to eliminate jobs that arrive after t2. *)
(* Assumption: jobs only execute if they arrived.
This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)
Hypothesis jobs_must_arrive:
job_must_arrive_to_exec job_arrival num_cpus sched.
(* Assumption: used to eliminate jobs that complete before t1. *)
(* Assumption: jobs do not execute after they completed.
This is used to eliminate jobs that complete before the start of the interval t1. *)
Hypothesis completed_jobs:
completed_job_doesnt_exec job_cost num_cpus rate sched.
(* Assumptions:
Necessary to use interval lengths as a measure of service.
The second one is not necessary but I'll remove it later. *)
1) A job does not execute in parallel.
2) The service rate of the platform is at most 1.
This is required to use interval lengths as a measure of service. *)
Hypothesis no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis rate_at_most_one :
forall j cpu, rate j cpu <= 1.
Hypothesis max_service_one:
forall j t, service_at num_cpus rate sched j t <= 1.
Variable ts: sporadic_taskset.
(* Assumption: needed to conclude that jobs ordered by arrival times
are separated by 'period' times units. *)
(* 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 job_arrival job_task.
(* Assumption: we need valid task parameters such as
a) period > 0 (used in divisions)
b) deadline of the job = deadline of the task
c) cost <= period
(At some point I need to prove that the distance between
the first and the last 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_taskset ts.
(* Assumption: I used the restricted deadlines assumption when proving that
that n_k (max_jobs) from Bertogna and Cirinei's formula
accounts for at least the number of middle jobs
(i.e., number of jobs - 2 in the worst case). *)
Hypothesis restricted_deadlines: restricted_deadline_model ts.
(* Before starting the proof, let's give simpler names to the definitions. *)
Definition response_time_bound_of (tsk: sporadic_task) (R: time) :=
response_time_ub_task job_arrival job_cost job_task num_cpus rate
......@@ -188,8 +175,23 @@ Module Workload.
(* Now we define the theorem. Let tsk be any task in the taskset. *)
Variable tsk: sporadic_task.
Hypothesis in_ts: tsk \in ts.
(* Assumption: the task must have valid parameters:
a) period > 0 (used in divisions)
b) deadline of the jobs = deadline of the task
c) cost <= period
(used to prove that the distance between the first and last
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.
(* Assumption: the task must have a restricted deadline.
This is required to prove that n_k (max_jobs) from Bertogna
and Cirinei's formula accounts for at least the number of
middle jobs (i.e., number of jobs - 2 in the worst case). *)
Hypothesis restricted_deadline: task_deadline tsk <= task_period tsk.
(* Assume that a response-time bound R_tsk for that task in any
schedule of this processor platform is also given. *)
Variable R_tsk: time.
......@@ -320,7 +322,7 @@ Module Workload.
rewrite -[service_during _ _ _ _ _ _]addn0.
apply leq_add; last by ins.
apply leq_trans with (n := \sum_(t1 <= t < t2) 1).
by apply leq_sum; intros i _; apply max_service_one.
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.
}
}
......@@ -361,8 +363,8 @@ Module Workload.
}
(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
assert(BOUNDend: service_during num_cpus rate sched j_fst t1 t2 +
service_during num_cpus rate sched j_lst t1 t2 <=
assert (BOUNDend: service_during num_cpus rate sched j_fst t1 t2 +
service_during num_cpus rate sched j_lst t1 t2 <=
(job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst)).
{
apply leq_add; unfold service_during.
......@@ -370,7 +372,7 @@ Module Workload.
rewrite -[_ + _ - _]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
apply leq_trans with (n := \sum_(t1 <= t < job_arrival j_fst + R_tsk)
service_at num_cpus rate sched j_fst t);
last by apply leq_sum; ins; apply max_service_one.
last by apply leq_sum; ins; apply service_at_le_max_rate.
destruct (job_arrival j_fst + R_tsk <= t2) eqn:LEt2; last first.
{
unfold t2; apply negbT in LEt2; rewrite -ltnNge in LEt2.
......@@ -395,7 +397,7 @@ Module Workload.
service_at num_cpus rate sched j_lst t);
first by rewrite -> big_cat_nat with (m := job_arrival j_lst) (n := t1);
[by apply leq_addl | by ins | by apply leq_addr].
by apply leq_sum; ins; apply max_service_one.
by apply leq_sum; ins; apply service_at_le_max_rate.
}
{
apply negbT in LT; rewrite -ltnNge in LT.
......@@ -403,7 +405,7 @@ Module Workload.
rewrite /= -[\sum_(_ <= _ < _) 1]add0n; apply leq_add.
rewrite (sum_service_before_arrival job_arrival);
[by apply leqnn | by ins | by apply leqnn].
by apply leq_sum; ins; apply max_service_one.
by apply leq_sum; ins; apply service_at_le_max_rate.
}
}
}
......@@ -497,7 +499,7 @@ Module Workload.
rewrite -addn1 mulnDl mul1n leq_add2r.
apply leq_trans with (n := delta + R_tsk - task_cost tsk);
first by rewrite -addnBA //; apply leq_addr.
by apply ltnW, ltn_ceil; specialize (task_properties tsk in_ts); des.
by apply ltnW, ltn_ceil, task_properties0.
}
by apply leq_trans with (n.+1 * task_period tsk);
[by rewrite leq_mul2r; apply/orP; right | by apply DIST].
......@@ -511,7 +513,7 @@ Module Workload.
intros BEFOREt2; apply BEFOREt2'; clear BEFOREt2'.
apply leq_trans with (n := job_arrival j_fst + task_deadline tsk + delta);
last by apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta);
[by rewrite leq_add2r leq_add2l; apply restricted_deadlines | apply DISTmax].
[rewrite leq_add2r leq_add2l; apply restricted_deadline | apply DISTmax].
{
(* Show that j_fst doesn't execute d_k units after its arrival. *)
unfold t2; rewrite leq_add2r; rename completed_jobs into EXEC.
......@@ -524,7 +526,7 @@ Module Workload.
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_deadlines tsk in_ts).
by rewrite job_properties1 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.
......@@ -583,14 +585,14 @@ Module Workload.
{
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 specialize (task_properties tsk in_ts); des.
rewrite NK ltnW // -ltn_divLR; last by apply task_properties0.
by unfold n_k, max_jobs, div_floor.
}
{
rewrite -subnDA; apply leq_sub2l.
apply leq_trans with (n := n.+1 * task_period tsk); last by apply DIST.
rewrite -addn1 addnC mulnDl mul1n.
by rewrite leq_add2l; last by specialize (task_properties tsk in_ts); des.
rewrite leq_add2l; last by apply task_properties3.
}
}
Qed.
......
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