Commit 37bb2c69 authored by jonathan julou's avatar jonathan julou

still more comments

parent 0e3e8b4a
Pipeline #19272 failed with stages
in 3 minutes and 48 seconds
......@@ -97,7 +97,7 @@ Section CPA_temp_step.
(*at all time, for every task, it is possible to perform an analysis of
a system with correct arrival models to certify that
the BCRTs and WCRTs are correct up to that instant.*)
WCRTs are correct up to that instant.*)
Hypothesis response_time_analysis :
forall t tsk, tsk \in ts ->
all_task_models_correct_until_t t ->
......@@ -147,7 +147,7 @@ Section CPA_temp_step.
- apply H_input_model_known. exact belong. exact E.
Qed.
(*the initialization of the induction in the proof below*)
Lemma induction_first_step : forall tsk, tsk \in ts ->
task_response_time_upper_bound_until_t sched arr_seq 0 (task_WCRT tsk) tsk /\
all_task_models_correct_until_t 0.
......
......@@ -113,9 +113,9 @@ Section CPA_temp_step.
Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
(*at all time, for every task, it is possible to perform an analysis of
a system with correct arrival models to certify that
the BCRTs and WCRTs are correct up to that instant.*)
(*for every task, it is possible to perform an analysis of
a system with correct infinite arrival models to certify that
WCRTs are correct.*)
Hypothesis response_time_analysis :
forall tsk, tsk \in ts ->
all_task_models_correct ->
......
......@@ -117,9 +117,7 @@ Section ScheduleDefs.
Variable ts : seq Tasks.
(* DONE : all_jobs_from_taskset in model.task? + up_to_t + equiv *)
(*Definition all_jobs_from_taskset := valid_arrival_sequence arr_seq /\ ts = nil.*)
(*defining what it means for all jobs to come from the taskset*)
Definition all_jobs_from_taskset := forall (j : Jobs), arrives_in arr_seq j -> job_task j \in ts.
Definition all_jobs_from_taskset_up_to_t (t : instant) := forall (j : Jobs),
......@@ -139,8 +137,7 @@ Section ScheduleDefs.
Qed.
(* DONE : respects_preemptive_priorities_up_to_t + equiv *)
(*redefinition of respecting the preemptive priority schedule up to t*)
Context `{JLDP_policy Jobs}.
Definition respects_preemptive_priorities_up_to_t (t : instant) :=
......@@ -234,6 +231,7 @@ Section Transformation.
Check sched_prefixed.
(*if the arr_seq is valid up to t, the completed arr_seq is always valid*)
Lemma valid_arrival_sequence_completion :
valid_arrival_sequence_up_to_t arr_seq t ->
valid_arrival_sequence arr_seq_prefixed.
......@@ -258,7 +256,8 @@ Section Transformation.
+ trivial.
Qed.
(*if all jobs come from taskset up to t in arr_seq, they do indefinitely in
the completed arrival sequence *)
Lemma all_jobs_from_taskset_completion :
valid_arrival_sequence_up_to_t arr_seq t ->
all_jobs_from_taskset_up_to_t arr_seq ts t ->
......@@ -318,6 +317,7 @@ Section Transformation.
easy.
Qed.
(*USELESS, REPLACE WITH THE PROOF IN PREFIX.V*)
Lemma valid_schedule_completion :
valid_arrival_sequence_up_to_t arr_seq t ->
valid_schedule_up_to_t State sched arr_seq t ->
......@@ -347,7 +347,8 @@ Section Transformation.
- admit.
Admitted.
(*if all properties are verified up to t, the response time is
bound indefinitely in the completed trace *)
Lemma response_time_analysis_prefixed :
valid_arrival_sequence_up_to_t arr_seq t ->
all_jobs_from_taskset_up_to_t arr_seq ts t ->
......@@ -362,6 +363,7 @@ Section Transformation.
apply valid_schedule_completion. exact VAS. exact VS.
Qed.
(*if a job finishes at t, it must have arrived before t*)
Lemma arr_bound : forall (j:Jobs) sch, jobs_must_arrive_to_execute sch ->
completed_by sch j t -> job_arrival j <= t.
Proof.
......@@ -374,6 +376,8 @@ Section Transformation.
- ssromega.
Qed.
(*if all properties are verified up to t, the response time is
bound up to t in the completed trace *)
Lemma finite_analysis_prefixed :
valid_arrival_sequence_up_to_t arr_seq t ->
all_jobs_from_taskset_up_to_t arr_seq ts t ->
......@@ -388,7 +392,11 @@ Section Transformation.
Qed.
(*attempt to prove the response time analysis up to t in the
original trace.
wrong since it uses the wrong schedule in the completed trace,
but some parts might be useful maybe*)
Lemma response_time_analysis :
valid_arrival_sequence_up_to_t arr_seq t ->
all_jobs_from_taskset_up_to_t arr_seq ts t ->
......
......@@ -44,6 +44,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):=
respects_periodic_jitter_task_model (task_period tsk) (task_jitter tsk)
arr_seq tsk off.
......@@ -69,7 +70,9 @@ Section Periojitt_same_law.
Hypothesis correct_period: valid_period (task_period tsk1).
(*strange necessary hypothesis that the trace be annotated
with theoretical arrivals must verify a dependency between the
theoretical arrivals of j and of the preceding job.*)
Hypothesis hyp_arrival_suiv_expr: forall (j pred_j : Job) (offset : nat),
arrives_in arr_seq j ->
arrives_in arr_seq pred_j ->
......@@ -87,6 +90,7 @@ Section Periojitt_same_law.
(* --- IV --- BOUNDING LEMMAS --- IV --- *)
(*========================================================================*)
(*it rewrites the definition of BCRT in a practical and intuitive way*)
Lemma dependency_arrival_bound_BCRT: forall (j pred_j : Job),
arrives_in arr_seq j ->
arrives_in arr_seq pred_j ->
......@@ -127,7 +131,7 @@ Section Periojitt_same_law.
exact Q.
Qed.
(*it rewrites the definition of WCRT in a practical and intuitive way*)
Lemma dependency_arrival_bound_WCRT: forall (j pred_j : Job),
arrives_in arr_seq j ->
arrives_in arr_seq pred_j ->
......@@ -299,6 +303,7 @@ Section Periojitt_same_law.
(* --- VII --- SOME LEMMAS TO SOOTHE THE PIPELINE --- VII --- *)
(*========================================================================*)
(*technical lemma used in the next proof*)
Local Lemma absurd_case: forall offset j pred_j,
task_dependency tsk1 tsk2 ->
is_indeed_the_offset tsk1 offset ->
......@@ -349,7 +354,7 @@ Section Periojitt_same_law.
Qed.
(*proof of the first hypothesis of the periodic jitter model*)
Local Lemma correction_lemma: forall offset j,
task_dependency tsk1 tsk2 ->
is_indeed_the_offset tsk1 offset ->
......@@ -403,8 +408,8 @@ Section Periojitt_same_law.
Qed.
Local Lemma induction_lemma: forall offset j j',
(*proof of the second hypothesis of the periodic jitter model*)
Local Lemma injection_lemma: forall offset j j',
task_dependency tsk1 tsk2 ->
is_indeed_the_offset tsk1 offset ->
arrives_in arr_seq j ->
......@@ -457,7 +462,7 @@ Section Periojitt_same_law.
Qed.
(*proof of the third hypothesis of the periodic jitter model*)
Lemma surjection_lemma: forall offset n : nat,
task_dependency tsk1 tsk2 ->
is_indeed_the_offset tsk1 offset ->
......@@ -564,7 +569,7 @@ Section Periojitt_same_law.
intros ja jb.
intros in_arr_seq_ja in_arr_seq_jb.
intros in_task_two_ja in_task_two_jb.
apply (induction_lemma offset ja jb dependency RPJTM
apply (injection_lemma offset ja jb dependency RPJTM
in_arr_seq_ja in_arr_seq_jb
in_task_two_ja in_task_two_jb).
......
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