Commit a046f668 authored by jonathan julou's avatar jonathan julou

defined abstracted arrival model

parent fb7f6470
Pipeline #18885 passed with stages
in 3 minutes and 53 seconds
From rt.restructuring.model Require Export dependency.
From rt.restructuring.analysis Require Export schedulability.
From rt.restructuring.model Require Export simple_abstracted_propagatable.
From rt.restructuring.model Require Export simple_abstracted.
From mathcomp Require Export bigop path.
From rt.util Require Export list.
From rt.util Require Import ssromega.
......@@ -28,38 +28,22 @@ Section CPA_temp_step.
Context `{JobCost Job} `{JobArrival Job} `{JobTask Job Task}.
Context (arr_seq : arrival_sequence Job).
Variable ts : {set Task}.
Variable arr_seq: arrival_sequence Job.
(* for each task we get its BCRT et WCRT, as given by the CPA,
but without any bounding properties until the analysis gives them*)
Variable task_WCRT : Task -> duration.
Variable task_BCRT : Task -> duration.
(*========================================================================*)
(* --- II --- HYPOTHESIS, 1st round --- II --- *)
(*========================================================================*)
Hypothesis all_jobs_complete: forall j, exists t, completes_at sched j t.
(*========================================================================*)
(* --- V --- ARRIVAL MODEL ABSTRACTION --- V --- *)
(* --- II --- ARRIVAL MODEL PROPERTIES --- II --- *)
(*========================================================================*)
(*We define an arrival model*)
Class FiniteModel := 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)
comme ils seront constants durant la récurrence*)
Check @FiniteModel.
(*for all task, we get a hold of the input model calculated by CPA*)
Class TaskInputModel := task_input_model : Task -> FiniteModel.
Context {task_input_model : TaskInputModel}.
Variable task_input_model : Task -> @FiniteModel Job Task.
Definition task_correct_temporal_step (tsk : Task) (t:instant):=
......@@ -67,49 +51,47 @@ Section CPA_temp_step.
Definition propagatable tsk1 tsk2 t:=
task_dependency tsk1 tsk2 ->
task_response_time_lower_bound_until_t arr_seq sched t (task_BCRT tsk1) tsk1 ->
task_response_time_upper_bound_until_t arr_seq sched t (task_WCRT tsk1) tsk1 ->
task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk1) tsk1 ->
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk1) tsk1 ->
task_correct_temporal_step tsk1 t ->
task_correct_temporal_step tsk2 (t.+1).
Hypothesis all_models_propagatable :
forall (t:instant) (tsk1 tsk2:Task),
tsk1 \in ts -> tsk2 \in ts -> propagatable tsk1 tsk2 t.
Definition complete_consistency_until_t t :=
forall tsk, tsk \in ts -> task_correct_temporal_step tsk t.
(*========================================================================*)
(* --- VI --- ANALYSER --- VI --- *)
(* --- III --- HYPOTHESIS --- III --- *)
(*========================================================================*)
Hypothesis response_time_analysis :
forall t tsk, tsk \in ts ->
complete_consistency_until_t t ->
(task_response_time_lower_bound_until_t arr_seq sched t (task_BCRT tsk) tsk
/\
task_response_time_upper_bound_until_t arr_seq sched t (task_WCRT tsk) tsk ).
Hypothesis H_all_models_propagatable :
forall (t:instant) (tsk1 tsk2:Task),
tsk1 \in ts -> tsk2 \in ts -> propagatable tsk1 tsk2 t.
(*========================================================================*)
(* --- VII --- HYPOTHESIS, 2nd round --- VII --- *)
(*========================================================================*)
Hypothesis H_all_jobs_complete: forall j, exists t, completes_at sched j t.
Hypothesis input_model_known :
Hypothesis H_input_model_known :
forall tsk, tsk \in ts -> prev_task tsk ts = None ->
(forall t, task_correct_temporal_step tsk t).
Hypothesis H_positive_cost: forall j, job_cost j > 0.
Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
Hypothesis response_time_analysis :
forall t tsk, tsk \in ts ->
complete_consistency_until_t t ->
(task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk) tsk
/\
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk ).
(*========================================================================*)
(* --- VIII --- MAIN LEMMAS --- VIII --- *)
(* --- IV --- MAIN LEMMAS --- VI --- *)
(*========================================================================*)
(*at an instant t, if the arrival models, WCRT and BCRT
were correct until t, then the models are correct until t+1*)
Lemma time_step: forall t,
......@@ -125,56 +107,62 @@ Section CPA_temp_step.
{ unfold complete_consistency_until_t in CC. apply CC.
apply prev_task_in_task_set with tsk. exact E. }
assert (Q: task_response_time_lower_bound_until_t arr_seq sched t (task_BCRT s) s
/\ task_response_time_upper_bound_until_t arr_seq sched t (task_WCRT s) s).
assert (Q: task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT s) s
/\ task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT s) s).
{ apply response_time_analysis. apply prev_task_in_task_set with tsk.
exact E. exact CC. }
destruct Q as [RTA_BCRT RTA_WCRT].
apply all_models_propagatable with s. apply prev_task_in_task_set with tsk. exact E. exact belong.
apply H_all_models_propagatable with s. apply prev_task_in_task_set with tsk. exact E. exact belong.
apply prev_task_dependency with ts. exact belong. exact E.
exact RTA_BCRT. exact RTA_WCRT.
exact P.
- apply input_model_known. exact belong. exact E.
- apply H_input_model_known. exact belong. exact E.
Qed.
(*the base case of the induction in the next lemma*)
Definition induction_first_step tsk :=
task_response_time_upper_bound_until_t arr_seq sched 0
(task_WCRT tsk) tsk /\
task_response_time_lower_bound_until_t arr_seq sched 0
(task_BCRT tsk) tsk /\ complete_consistency_until_t 0.
Hypothesis models_correct_on_init : forall tsk,
task_correct_temporal_step tsk 0.
(*final lemma: all WCRT correct for infinite traces.
It should be unnecessary to verify BCRTs at this step,
but should be easy by mimicking the WCRT proof*)
Lemma final_result: forall tsk,
tsk \in ts ->
induction_first_step tsk-> (*maybe as hypothesis if we suppose there is no job at t=0*)
Lemma final_result: forall tsk, tsk \in ts ->
task_response_time_upper_bound arr_seq sched tsk (task_WCRT tsk).
Proof.
intros tsk belong IFS.
apply upper_bound_forall_t_to_infinity. apply all_jobs_complete.
apply upper_bound_forall_t_to_infinity. apply H_all_jobs_complete.
assert (P:
(forall t : instant, task_response_time_upper_bound_until_t arr_seq sched t (task_WCRT tsk) tsk
/\ task_response_time_lower_bound_until_t arr_seq sched t (task_BCRT tsk) tsk
(forall t : instant, task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk
/\ task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk) tsk
/\ complete_consistency_until_t t)
->
(forall t : instant, task_response_time_upper_bound_until_t arr_seq sched t (task_WCRT tsk) tsk )).
(forall t : instant, task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk )).
{ intros P t. apply P. }
apply P.
induction t as [| t IHt].
{ (*INITIALISATION*)
exact IFS.
split. 2:split.
- unfold task_response_time_upper_bound_until_t.
intros j P1 P2. split.
intro Q. apply completed_implies_scheduled_before in Q.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive. intro Q. ssromega.
- unfold task_response_time_lower_bound_until_t.
intros j P1 P2.
intro Q. apply completed_implies_scheduled_before in Q.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive.
- unfold complete_consistency_until_t.
intros tsssk Q. apply models_correct_on_init.
}
{ (*HEREDITY*)
destruct IHt as [W IHt].
......@@ -183,10 +171,10 @@ Section CPA_temp_step.
{ apply time_step. exact CC. }
assert (next_RTA_destructable:
task_response_time_lower_bound_until_t arr_seq sched t.+1
task_response_time_lower_bound_until_t sched arr_seq t.+1
(task_BCRT tsk) tsk
/\
task_response_time_upper_bound_until_t arr_seq sched t.+1
task_response_time_upper_bound_until_t sched arr_seq t.+1
(task_WCRT tsk) tsk).
{ apply response_time_analysis. exact belong. exact next_CC. }
......
......@@ -39,9 +39,6 @@ Section Periojitt_same_law.
Variable WCRT: duration.
Variable BCRT: duration.
Variable t:instant.
......@@ -62,9 +59,9 @@ Section Periojitt_same_law.
(* --- III --- HYPOTHESIS --- III --- *)
(*========================================================================*)
Hypothesis WCRT_correct: task_response_time_upper_bound_until_t arr_seq sched t (WCRT) tsk1.
Hypothesis WCRT_correct: task_response_time_upper_bound_until_t sched arr_seq t (WCRT) tsk1.
Hypothesis BCRT_correct: task_response_time_lower_bound_until_t arr_seq sched t (BCRT) tsk1.
Hypothesis BCRT_correct: task_response_time_lower_bound_until_t sched arr_seq t (BCRT) tsk1.
Hypothesis correct_dependancy: this_needs_a_name Task Job arr_seq task_dependency.
......@@ -1020,16 +1017,13 @@ Local Ltac init_pipeline_lemma offset:=
*)
Qed.
(*Definition analyser: fct qui a tout tâche donne un WCRT avant t
si l'analyse est correcte en t*)
End Periojitt_same_law.
From rt.restructuring.analysis.frame_by_frame Require Export cpa_temporal_step.
Section propagatability.
Section Propagatability.
Context {PState : Type}.
Context (sched : schedule PState).
......@@ -1067,20 +1061,14 @@ Section propagatability.
Definition task_correct_temporal_step (tsk : Task) (t:instant):=
PJ_model arr_seq tsk t.
(*defines an arrival model where all tasks follow the PJM*)
Definition task_input_PJM (tsk : Task):= PJ_model.
Definition propagatable_PJM t1 t2 t:=
task_dependency t1 t2 ->
task_response_time_lower_bound_until_t arr_seq sched t (task_BCRT t1) t1 ->
task_response_time_upper_bound_until_t arr_seq sched t (task_WCRT t1) t1 ->
task_correct_temporal_step t1 t ->
task_correct_temporal_step t2 (t.+1).
(*========================================================================*)
(* --- >_< --- HYPOTHESIS --- >_< --- *)
(*========================================================================*)
Hypothesis correct_dependancy: this_needs_a_name Task Job arr_seq task_dependency.
Hypothesis valid_arr_seq: valid_arrival_sequence arr_seq.
......@@ -1116,11 +1104,12 @@ Section propagatability.
Hypothesis response_time_analysis :
forall t tsk, tsk \in ts ->
forall tsk, tsk \in ts -> task_correct_temporal_step tsk t ->
(task_response_time_lower_bound_until_t arr_seq sched t (task_BCRT tsk) tsk
(task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk) tsk
/\
task_response_time_upper_bound_until_t arr_seq sched t (task_WCRT tsk) tsk ).
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk ).
Hypothesis models_correct_on_init : forall tsk,
task_correct_temporal_step tsk 0.
(*========================================================================*)
(* --- >_< --- HYPOTHESIS --- >_< --- *)
(*========================================================================*)
......@@ -1128,14 +1117,15 @@ Section propagatability.
Lemma all_models_propagatable_PJM:
forall (t:instant) (tsk1 tsk2:Task),
tsk1 \in ts -> propagatable_PJM tsk1 tsk2 t.
tsk1 \in ts -> propagatable sched arr_seq task_WCRT task_BCRT task_input_PJM tsk1 tsk2 t.
Proof.
intros t tsk1 tsk2 ints1.
unfold propagatable_PJM.
unfold propagatable.
intros dependency B W model_verified_by_tsk1.
unfold task_correct_temporal_step. unfold PJ_model.
unfold task_correct_temporal_step in model_verified_by_tsk1.
unfold PJ_model in model_verified_by_tsk1.
unfold cpa_temporal_step.task_correct_temporal_step.
unfold task_input_PJM. unfold PJ_model.
unfold cpa_temporal_step.task_correct_temporal_step in model_verified_by_tsk1.
unfold task_input_PJM in model_verified_by_tsk1. unfold PJ_model in model_verified_by_tsk1.
rewrite -> H_period with (t1 :=tsk1).
rewrite -> H_jitter with (t1 :=tsk1).
......@@ -1149,35 +1139,28 @@ Section propagatability.
Qed.
Definition induction_first_step tsk :=
task_response_time_upper_bound_until_t arr_seq sched 0
(task_WCRT tsk) tsk /\
task_response_time_lower_bound_until_t arr_seq sched 0
(task_BCRT tsk) tsk /\ (forall tsk, tsk \in ts -> task_correct_temporal_step tsk 0).
Lemma final_result_PJM: forall tsk,
tsk \in ts ->
induction_first_step tsk-> (*maybe as hypothesis if we suppose there is no job at t=0*)
Lemma final_result_PJM: forall tsk, tsk \in ts ->
task_response_time_upper_bound arr_seq sched tsk (task_WCRT tsk).
Proof.
intros tsk P Q.
intros tsk P.
apply final_result with H0 ts task_BCRT task_input_PJM.
- exact all_jobs_complete.
- intros t t1 t2 B W. unfold cpa_temporal_step.task_correct_temporal_step.
apply all_models_propagatable_PJM. exact B.
- exact all_jobs_complete.
- exact input_model_known.
- exact H_positive_cost.
- exact H_jobs_must_arrive.
- unfold complete_consistency_until_t.
unfold cpa_temporal_step.task_correct_temporal_step.
unfold task_correct_temporal_step in response_time_analysis.
unfold task_input_PJM. intros t tsk0 L G.
apply response_time_analysis with tsk0. exact L. exact L.
apply G. exact L.
- exact input_model_known.
- exact models_correct_on_init.
- exact P.
- exact Q.
Qed.
End propagatability.
End Propagatability.
......@@ -12,18 +12,18 @@ Set Bullet Behavior "Strict Subproofs".
Section Tasks.
Context {PState : Type}.
Context (sched : schedule PState).
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule PState.
Context (arr_seq : arrival_sequence Job).
......@@ -58,25 +58,26 @@ End Tasks.
Section Proofs.
Context {PState : Type}.
Context (sched : schedule PState).
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Variable arr_seq: arrival_sequence Job.
Context (arr_seq : arrival_sequence Job).
Variable sched: schedule PState.
Hypothesis all_jobs_complete: forall j, exists t, completes_at sched j t.
Lemma lower_bound_forall_t_to_infinity: forall tsk R,
(forall t, task_response_time_lower_bound_until_t arr_seq sched t R tsk)
(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.
Proof.
intros tsk BCRT P.
......@@ -92,7 +93,7 @@ Section Proofs.
Qed.
Lemma upper_bound_forall_t_to_infinity: forall tsk R,
(forall t, task_response_time_upper_bound_until_t arr_seq sched t R tsk)
(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.
Proof.
intros tsk WCRT P.
......
......@@ -11,9 +11,6 @@ From rt.restructuring.model.arrival Require Export periodic_jitter.
Set Bullet Behavior "Strict Subproofs".
Section Prefixverif.
(*========================================================================*)
(* --- I --- CONTEXT AND VARIABLES --- I --- *)
(*========================================================================*)
......@@ -29,7 +26,9 @@ Section Prefixverif.
Context `{JobCost Job} `{JobArrival Job} `{JobTask Job Task}
`{JobJitter Job}.
Variable arr_seq : arrival_sequence Job.
Context (arr_seq : arrival_sequence Job).
Variable jitter : duration.
Variable period : duration.
Variable offset : duration.
......@@ -76,29 +75,15 @@ Section Prefixverif.
Definition respects_periodic_jitter_task_model_up_to_t_offset_unknown
(tsk : Task) (t : instant) :=
exists off,
(forall j,
completed_by sched j t ->
arrives_in arr_seq j ->
job_task j = tsk ->
off <= theoretical_arrival j /\
theoretical_arrival j - off %| period /\
job_jitter j <= jitter) /\
(forall j j',
completed_by sched j t ->
completed_by sched j' t ->
arrives_in arr_seq j ->
arrives_in arr_seq j'->
job_task j = tsk ->
job_task j' = tsk->
theoretical_arrival j = theoretical_arrival j' ->
j = j') /\
(forall n,
off + n * period + jitter <= t ->
exists j,
arrives_in arr_seq j /\
job_task j = tsk /\
theoretical_arrival j = off + n * period).
(forall j, correction_t tsk j t off)/\
(forall j j', injection_t tsk j j' t )/\
(forall n, surjection_t tsk n t ).
(* the version without surjectivity won't be linked to a infinite time model
however it would be trivial to do so, since it only requires to get rid of
the third hypothesis of the model everywhere.*)
Definition respects_periodic_jitter_task_model_up_to_t_without_surjectivity
(tsk : Task) (t : instant) :=
......
......@@ -3,56 +3,26 @@ From rt.restructuring.model Require Export task.
From mathcomp Require Export div.
(*
Section abstract.
Context {PState : Type}.
Section Model.
Context {Job: JobType} {Task: TaskType}.
Context `{JobCost Job} `{JobArrival Job} `{JobTask Job Task}.
Variable arr_seq: arrival_sequence Job.
Context (arr_seq : arrival_sequence Job).
(*We define an arrival model*)
Class ArrivalModel := arrival_model:
(arrival_sequence Job) -> Task -> Prop.
(*We define an arrival model verified until an instant t*)
Class FiniteModel := 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)
comme ils seront constants durant la récurrence*)
End Model.
(*for all task, we get a hold of the input model calculated by CPA*)
Class TaskInputModel := task_input_model : Task -> FiniteModel.
Context {task_input_model : TaskInputModel}.
Definition task_correct_temporal_step (tsk : Task) (t:instant):=
(task_input_model tsk) arr_seq tsk t.
From rt.restructuring.analysis Require Export schedulability_up_to_t.
From rt.restructuring.model Require Export dependency.
Context (sched : schedule PState).
Context `{JobDependency Job} `{TaskDependency Task}.
Context `{ProcessorState Job PState}.
Definition propagatable tsk1 tsk2 BCRT WCRT t:=
task_dependency tsk1 tsk2 ->
task_response_time_lower_bound_until_t arr_seq sched t BCRT tsk1 ->
task_response_time_upper_bound_until_t arr_seq sched t WCRT tsk1 ->
task_correct_temporal_step tsk1 t ->
task_correct_temporal_step tsk2 (t.+1).
Definition all_models_propagatable :=
forall (t:instant) (tsk1 tsk2:Task) (BCRT WCRT : duration),
propagatable tsk1 tsk2 BCRT WCRT t.
End abstract.
*)
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