Commit 2d0a420d authored by jonathan julou's avatar jonathan julou

il reste a generaliser cpa_temporal_step pour ne plus utiliser BCRT et WCRT

parent 76345509
Pipeline #18946 passed with stages
in 3 minutes and 34 seconds
From rt.restructuring.model Require Export dependency.
From rt.restructuring.analysis Require Export schedulability.
From rt.restructuring.model Require Export simple_abstracted.
From mathcomp Require Export bigop path.
From rt.util Require Export list.
......@@ -43,7 +42,7 @@ Section CPA_temp_step.
(*========================================================================*)
(*for all task, we get a hold of the input model calculated by CPA*)
Variable task_input_model : Task -> @FiniteModel Job Task.
Variable task_input_model : Task -> @ArrivalModelUpTo Job Task.
(*what it means for a task to respect its input model until t*)
......
......@@ -145,7 +145,7 @@ Section Periojitt_same_law.
unfold task_response_time_lower_bound in BCRT_correct.
apply BCRT_correct in in_arr_seq_pred_j.
unfold job_response_time_lower_bound in in_arr_seq_pred_j.
unfold job_response_time_bound in in_arr_seq_pred_j.
unfold completed_by in in_arr_seq_pred_j.
apply jonathan.not_leq_lt in in_arr_seq_pred_j.
......@@ -378,7 +378,7 @@ Local Ltac init_pipeline_lemma offset:=
unfold task_response_time_lower_bound in BCRT_correct.
apply BCRT_correct in in_arr_seq_1.
unfold job_response_time_lower_bound in in_arr_seq_1.
unfold job_response_time_bound in in_arr_seq_1.
unfold completed_by in in_arr_seq_1.
apply jonathan.not_leq_lt in in_arr_seq_1.
......
......@@ -27,19 +27,18 @@ Section Tasks.
Context (arr_seq : arrival_sequence Job).
(*tout job ayant fini avant t a fini avant son BCRT, sinon il est pending*)
(*tout job ayant fini ont fini avant WCRT et tout job pending n'a pas ete activé avant t-WCRT*)
(*for all job, if it completed before t, then it completed after its BCRT*)
Definition task_response_time_lower_bound_until_t t R tsk:=
forall j,
arrives_in arr_seq j ->
job_task j = tsk ->
(
completed_by sched j t ->
job_response_time_lower_bound sched j R
~ job_response_time_bound sched j R
).
(*for all job, if it completed before t, then it completed before its WCRT.
If it didn't finish before t, then it arrived after t-WCRT *)
Definition task_response_time_upper_bound_until_t t R tsk:=
forall j,
arrives_in arr_seq j ->
......@@ -76,7 +75,8 @@ Section Proofs.
Hypothesis all_jobs_complete: forall j, exists t, completes_at sched j t.
(*it is equivalent to say that R is a BCRT for the task tsk and that for
all instant t it is a BCRT until t *)
Lemma lower_bound_forall_t_to_infinity: forall tsk R,
(forall t, task_response_time_lower_bound_until_t sched arr_seq t R tsk)
<-> task_response_time_lower_bound arr_seq sched tsk R.
......@@ -99,6 +99,8 @@ Section Proofs.
apply Q. exact in_arr_seq. exact in_task.
Qed.
(*it is equivalent to say that R is a WCRT for the task tsk and that for
all instant t it is a WCRT until t *)
Lemma upper_bound_forall_t_to_infinity: forall tsk R,
(forall t, task_response_time_upper_bound_until_t sched arr_seq t R tsk)
<-> task_response_time_upper_bound arr_seq sched tsk R.
......
......@@ -107,7 +107,7 @@ Section Periojitt_same_law.
unfold task_response_time_lower_bound in BCRT_correct.
apply BCRT_correct in in_arr_seq_pred_j.
unfold job_response_time_lower_bound in in_arr_seq_pred_j.
unfold job_response_time_bound in in_arr_seq_pred_j.
unfold completed_by in in_arr_seq_pred_j.
apply jonathan.not_leq_lt in in_arr_seq_pred_j.
......
......@@ -35,15 +35,12 @@ Section Task.
(* We say that Rl is a response time lower bound of a job j
if j has not completed by Rl units after its arrival *)
(* put into schedule.v ? *)
Definition job_response_time_lower_bound (j : Job) (R : duration) :=
~ (completed_by sched j (job_arrival j + R)).
Definition task_response_time_lower_bound tsk R:=
forall j,
arrives_in arr_seq j ->
job_task j = tsk ->
job_response_time_lower_bound j R.
~ job_response_time_bound sched j R.
(* We say that a task is schedulable if all its jobs meet their deadline *)
Definition schedulable_task :=
......
......@@ -57,6 +57,7 @@ Section Schedule.
Definition job_response_time_bound (j : Job) (R : duration) :=
completed_by j (job_arrival j + R).
(* We say that a job meets its deadline if it completes by its absolute deadline *)
Definition job_meets_deadline (j : Job) :=
completed_by j (job_deadline j).
......
......@@ -13,7 +13,7 @@ Section Model.
(*We define an arrival model verified until an instant t*)
Class FiniteModel := finite_model:
Class ArrivalModelUpTo := finite_model:
(arrival_sequence Job) -> Task -> instant -> Prop.
(*pour periodic jitter on peut faire rentrer periode, jitter et offset
dans le modèle fini (sans 'il existe' pour l'offset)
......
Markdown is supported
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