Commit 1abfae4c authored by jonathan julou's avatar jonathan julou

periojit relié aux definitions et preuves generales

parent 21734291
Pipeline #18870 failed with stages
in 3 minutes and 36 seconds
......@@ -5,6 +5,7 @@ From rt.restructuring.behavior Require Export schedule.
From rt.util Require Import ssromega.
From rt.restructuring.analysis Require Export verify_up_to_t.
From rt.restructuring.analysis Require Export schedulability_up_to_t.
Set Bullet Behavior "Strict Subproofs".
......@@ -65,8 +66,6 @@ Section Periojitt_same_law.
Hypothesis BCRT_correct: task_response_time_lower_bound_until_t arr_seq sched t (BCRT) tsk1.
Hypothesis BCRT_inf_WCRT: BCRT <= WCRT.
Hypothesis correct_dependancy: this_needs_a_name Task Job arr_seq task_dependency.
......@@ -903,7 +902,7 @@ Local Ltac init_pipeline_lemma offset:=
assert (CPSj: completed_by sched j t.+1).
{
}
destruct G as [fj Pfj].
......@@ -1026,10 +1025,164 @@ 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.
Context {PState : Type}.
Context (sched : schedule PState).
Context (Task: TaskType)
`{PeriodicJitterModel Task}
`{TaskDependency Task}.
Context {Job : JobType}
`{JobTask Job Task}
`{JobArrival Job}
`{JobJitter Job}
`{JobCost Job}
`{ProcessorState Job PState}
`{JobDependency Job}.
Context (arr_seq : arrival_sequence Job).
Variable ts : {set Task}.
(* 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.
Definition PJ_model arrival_seq tsk t :=
respects_periodic_jitter_task_model_up_to_t_offset_unknown_without_surjectivity
sched arrival_seq
(task_jitter tsk)
(task_period tsk)
tsk t.
Definition task_correct_temporal_step (tsk : Task) (t:instant):=
PJ_model arr_seq tsk t.
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.
Hypothesis correct_schedule: respects_job_dependency sched.
Hypothesis correct_period: forall tsk, tsk \in ts -> valid_period (task_period tsk).
Hypothesis hyp_arrival_suiv_expr: forall (j pred_j : Job) (offset : nat) t,
arrives_in arr_seq j ->
arrives_in arr_seq pred_j ->
job_dependency pred_j j ->
is_indeed_the_offset sched Task arr_seq (job_task pred_j) offset t->
theoretical_arrival j = theoretical_arrival pred_j + task_BCRT (job_task pred_j).
Hypothesis all_jobs_complete: forall j, exists t, completes_at sched j t.
Hypothesis H_positive_cost: forall j, job_cost j > 0.
Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
Hypothesis H_period: forall t1 t2,
task_dependency t1 t2 -> task_period t2 = task_period t1.
Hypothesis H_jitter: forall t1 t2,
task_dependency t1 t2 -> task_jitter t2 = task_jitter t1 + (task_WCRT t1 - task_BCRT t1).
Hypothesis input_model_known :
forall tsk, tsk \in ts -> prev_task tsk ts = None ->
(forall t, task_correct_temporal_step tsk t).
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_upper_bound_until_t arr_seq sched t (task_WCRT tsk) tsk ).
(*========================================================================*)
(* --- >_< --- HYPOTHESIS --- >_< --- *)
(*========================================================================*)
Lemma all_models_propagatable_PJM:
forall (t:instant) (tsk1 tsk2:Task),
tsk1 \in ts -> propagatable_PJM tsk1 tsk2 t.
Proof.
intros t tsk1 tsk2 ints1.
unfold propagatable_PJM.
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.
rewrite -> H_period with (t1 :=tsk1).
rewrite -> H_jitter with (t1 :=tsk1).
apply periodic_jitter_same_law_up_to_t with H0 H6.
exact W. exact B. exact correct_dependancy. exact correct_schedule.
apply correct_period. exact ints1.
intros j pj offset P1 P2 P3 P4 P5 P6.
rewrite <- P4. apply hyp_arrival_suiv_expr with offset t. exact P1. exact P2. exact P5. exact P6.
exact H_positive_cost. exact H_jobs_must_arrive. exact dependency.
exact model_verified_by_tsk1. exact dependency. exact dependency.
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*)
task_response_time_upper_bound arr_seq sched tsk (task_WCRT tsk).
Proof.
intros tsk P Q.
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.
- 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 P.
- exact Q.
Qed.
End propagatability.
......@@ -39,12 +39,12 @@ Section Prefixverif.
(* --- II --- DEFINITIONS --- II --- *)
(*========================================================================*)
Local Definition correction_t tsk j t:=
Local Definition correction_t tsk j t off:=
completed_by sched j t ->
arrives_in arr_seq j ->
job_task j = tsk ->
offset <= theoretical_arrival j /\
theoretical_arrival j - offset %| period /\
off <= theoretical_arrival j /\
theoretical_arrival j - off %| period /\
job_jitter j <= jitter.
......@@ -68,7 +68,7 @@ Section Prefixverif.
Definition respects_periodic_jitter_task_model_up_to_t
(tsk : Task) (t : instant) :=
(forall j, correction_t tsk j t )/\
(forall j, correction_t tsk j t offset)/\
(forall j j', injection_t tsk j j' t )/\
(forall n, surjection_t tsk n t ).
......@@ -102,28 +102,14 @@ Section Prefixverif.
Definition respects_periodic_jitter_task_model_up_to_t_without_surjectivity
(tsk : Task) (t : instant) :=
(forall j, correction_t tsk j t )/\
(forall j, correction_t tsk j t offset)/\
(forall j j', injection_t tsk j j' t ).
Definition respects_periodic_jitter_task_model_up_to_t_offset_unknown_without_surjectivity
(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 j, correction_t tsk j t off)/\
(forall j j', injection_t tsk j j' t ).
(*========================================================================*)
......@@ -187,7 +173,7 @@ Section Prefixverif.
- intros j.
assert (Q: exists t, completes_at sched j t). apply all_jobs_complete.
destruct Q as [t Q].
assert (P1: correction_t tsk j (t))
assert (P1: correction_t tsk j (t) offset)
by (apply P).
apply P1. unfold completes_at in Q. unfold completed_by. ssromega.
......
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.restructuring.model Require Export task.
From mathcomp Require Export div.
(*
Section abstract.
Context {PState : Type}.
Context {Job: JobType} {Task: TaskType}.
Context `{JobCost Job} `{JobArrival Job} `{JobTask Job Task}.
Variable arr_seq: arrival_sequence Job.
(*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*)
(*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.
*)
......@@ -108,4 +108,142 @@ Section RespectsTaskDep.
forall t,
size (completed_jobs_before tsk1 t) = size (task_jobs_arrived_up_to tsk2 t).
End RespectsTaskDep.
\ No newline at end of file
End RespectsTaskDep.
Section navigation.
Context {PState : Type}.
Context (sched : schedule PState).
Context {Job: JobType} {Task: TaskType}.
Context `{JobDependency Job} `{TaskDependency Task}.
Context `{ProcessorState Job PState}.
Context `{JobCost Job} `{JobArrival Job} `{JobTask Job Task}.
Variable ts : {set Task}.
Variable arr_seq: arrival_sequence Job.
Fixpoint next_task (tsk : Task) (task_set : list Task) :=
match task_set with
|nil => None
|t :: l => if (task_dependency tsk t) then Some t else next_task tsk l
end.
Fixpoint prev_task (tsk : Task) (task_set : list Task) :=
match task_set with
|nil => None
|t :: l => if (task_dependency t tsk) then Some t else prev_task tsk l
end.
(*the previous task obtained by the above function is in the taskset*)
Lemma prev_task_in_task_set: forall (tsk_set: {set Task}) tsk prev_tsk,
prev_task tsk tsk_set = Some prev_tsk -> prev_tsk \in (_set_seq tsk_set).
Proof.
intro tsk_set.
induction (_set_seq tsk_set) as [| a l IHl].
intros tsk prev_tsk dependency. discriminate dependency.
intros tsk prev_tsk dependency.
destruct (prev_tsk == a) eqn:E.
- move/eqP in E. subst prev_tsk. apply mem_head.
- rewrite in_cons. rewrite E.
apply IHl with tsk.
unfold prev_task.
unfold prev_task in dependency.
destruct (task_dependency a tsk) eqn:F.
+ injection dependency. intro contradiction.
subst a. move/eqP in E. exfalso. apply E. reflexivity.
+ exact dependency.
Qed.
(*the next task obtained by the above function is in the taskset*)
Lemma next_task_in_task_set: forall (tsk_set: {set Task}) tsk suiv_tsk,
next_task tsk tsk_set = Some suiv_tsk -> suiv_tsk \in (_set_seq tsk_set).
Proof.
intro tsk_set.
induction (_set_seq tsk_set) as [| a l IHl].
intros tsk suiv_tsk dependency. discriminate dependency.
intros tsk suiv_tsk dependency.
destruct (suiv_tsk == a) eqn:E.
- move/eqP in E. subst suiv_tsk. apply mem_head.
- rewrite in_cons. rewrite E.
apply IHl with tsk.
unfold next_task.
unfold next_task in dependency.
destruct (task_dependency tsk a) eqn:F.
+ injection dependency. intro contradiction.
subst a. move/eqP in E. exfalso. apply E. reflexivity.
+ exact dependency.
Qed.
(*there is indeed a dependency between a task and its previous task
obtained by the above function*)
Lemma prev_task_dependency: forall (tsk_set: {set Task}) tsk prev_tsk,
tsk \in tsk_set -> prev_task tsk tsk_set = Some prev_tsk ->
task_dependency prev_tsk tsk.
Proof.
intros tsk_set.
induction (_set_seq tsk_set) as [| a l IHl].
intros tsk prev_tsk P Q. discriminate.
intros tsk prev_tsk P Q.
destruct (prev_tsk == a) eqn:E.
- move/eqP in E. subst prev_tsk.
unfold prev_task in Q.
destruct (task_dependency a tsk) eqn:F.
+ trivial.
+ fold prev_task in Q. rewrite <- F.
apply IHl. exact P. exact Q.
- apply IHl. exact P.
move/eqP in E. unfold prev_task. unfold prev_task in Q.
destruct (task_dependency a tsk) eqn:F.
+ injection Q. intro contradiction.
subst a. exfalso. apply E. reflexivity.
+ exact Q.
Qed.
(*there is indeed a dependency between a task and its next task
obtained by the above function*)
Lemma next_task_dependency: forall (tsk_set: {set Task}) tsk suiv_tsk,
tsk \in tsk_set -> next_task tsk tsk_set = Some suiv_tsk ->
task_dependency tsk suiv_tsk.
Proof.
intros tsk_set.
induction (_set_seq tsk_set) as [| a l IHl].
intros tsk next_tsk P Q. discriminate.
intros tsk next_tsk P Q.
destruct (next_tsk == a) eqn:E.
- move/eqP in E. subst next_tsk.
unfold next_task in Q.
destruct (task_dependency tsk a) eqn:F.
+ trivial.
+ fold next_task in Q. rewrite <- F.
apply IHl. exact P. exact Q.
- apply IHl. exact P.
move/eqP in E. unfold next_task. unfold next_task in Q.
destruct (task_dependency tsk a) eqn:F.
+ injection Q. intro contradiction.
subst a. exfalso. apply E. reflexivity.
+ exact Q.
Qed.
End navigation.
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