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

commit the comments

parent 37bb2c69
Pipeline #19273 failed with stages
in 3 minutes and 40 seconds
......@@ -47,7 +47,7 @@ Section Periojitt_same_law.
(* --- II --- DEFINITIONS --- II --- *)
(*========================================================================*)
(*States that the given offset verifies the periodic jitter model *)
Definition is_indeed_the_offset (tsk : Task) (off : nat) time:=
respects_periodic_jitter_task_model_up_to_t_without_surjectivity
arr_seq (task_jitter tsk) (task_period tsk)
......@@ -86,13 +86,6 @@ Section Periojitt_same_law.
theoretical_arrival j = theoretical_arrival pred_j + BCRT.
(*
Hypothesis existence: exists j, (job_task j = tsk2) /\ (arrives_in arr_seq j).
(*^^^ necessaire pour prouver la troisieme hypothese du modele*)
(*posera probleme a l'initialisation de l'induction*)
(*il faudra alors aussi retirer la 3e hypothese du modele*)
*)
Hypothesis H_positive_cost: forall j, job_cost j > 0.
Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
......@@ -103,6 +96,7 @@ Section Periojitt_same_law.
(* --- VI --- BOUNDING LEMMAS --- VI --- *)
(*========================================================================*)
(*practical rewriting of correct_dependency*)
Lemma dependency_bound: forall tps (j pred_j : Job),
job_dependency pred_j j ->
completed_by sched pred_j tps <-> job_arrival j <= tps.
......@@ -129,7 +123,7 @@ Section Periojitt_same_law.
apply sum.extend_sum. apply leqnn. exact hypo.
Qed.
(* the next job arrives after its predecessor's arrival *)
Local Lemma arrival_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
job_task j = tsk2 -> job_task pred_j = tsk1 ->
......@@ -151,7 +145,7 @@ Section Periojitt_same_law.
ssromega.
Qed.
(*if a job arrives before t+1, its predecessor arrives before t*)
Local Lemma arrival_bound_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
job_task j = tsk2 -> job_task pred_j = tsk1 ->
......@@ -175,7 +169,7 @@ Section Periojitt_same_law.
ssromega.
Qed.
(*it rewrites the definition of WCRT in a practical and intuitive way*)
Lemma dependency_arrival_bound_WCRT: forall (j pred_j : Job),
job_arrival j <= t.+1 ->
arrives_in arr_seq j ->
......@@ -290,15 +284,11 @@ Section Periojitt_same_law.
Local Ltac init_pipeline_lemma offset:=
Local Ltac init_pipeline_lemma offset:=
intros dependency Q;
unfold respects_periodic_jitter_task_model in Q;
assert (RPJTM: is_indeed_the_offset tsk1 offset t) by (exact Q);
(*
destruct Q as [correction Q];
destruct Q as [injection surjection];
*)
destruct Q as [correction injection];
destruct correct_dependancy as [right_complete left_complete].
......@@ -363,7 +353,7 @@ Local Ltac init_pipeline_lemma offset:=
(*if a job completes before t+1, its predecessor completes before t*)
Local Lemma end_bound_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
job_task j = tsk2 -> job_task pred_j = tsk1 ->
......@@ -403,7 +393,7 @@ Local Ltac init_pipeline_lemma offset:=
apply sum.extend_sum. apply leqnn. exact P.
Qed.
(*technical lemma*)
Local Lemma absurd_case_UTT: forall offset j pred_j,
task_dependency tsk1 tsk2 ->
is_indeed_the_offset tsk1 offset t->
......@@ -454,6 +444,7 @@ Local Ltac init_pipeline_lemma offset:=
ssromega.
Qed.
(*technical lemma*)
Local Lemma correction_lemma_UTT: forall offset j,
task_dependency tsk1 tsk2 ->
is_indeed_the_offset tsk1 offset t->
......@@ -517,7 +508,7 @@ Local Ltac init_pipeline_lemma offset:=
Qed.
(*technical lemma*)
Local Lemma induction_lemma_UTT: forall offset j j',
task_dependency tsk1 tsk2 ->
is_indeed_the_offset tsk1 offset t->
......@@ -579,7 +570,7 @@ Local Ltac init_pipeline_lemma offset:=
Qed.
(*for all jobs, the job jitter is less than its task's jitter*)
Lemma jobjitter_bound: forall tsk j off,
job_task j = tsk -> arrives_in arr_seq j ->
(arrives_in arr_seq j ->
......@@ -746,6 +737,8 @@ Section Propagatability.
Hypothesis models_correct_on_init : forall tsk,
task_correct_temporal_step tsk 0.
(*we suppose we have the analysis on BCRT and WCRT
to propagate their correction*)
Hypothesis response_time_analysis :
forall t tsk, tsk \in ts ->
forall tsk, tsk \in ts -> task_correct_temporal_step tsk t ->
......
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