Commit b222b4d0 authored by jonathan julou's avatar jonathan julou

honk

parent 2a6fb55f
Pipeline #18957 failed with stages
in 44 seconds
......@@ -81,9 +81,6 @@ Section CPA_temp_step.
forall (t:instant) (tsk1 tsk2:Task),
tsk1 \in ts -> tsk2 \in ts -> propagatable tsk1 tsk2 t.
(*every single job eventually completes.*)
Hypothesis H_all_jobs_complete: forall j, exists t, completes_at sched j t.
(*we know that the arrival model for tasks without predecessors
(the 'inputs' of the task chain), the model is correct, since we have
a trace for it.*)
......@@ -110,7 +107,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.*)
the schedule property is correct up to that instant.*)
Hypothesis schedule_property_analysis :
forall t tsk, tsk \in ts ->
all_task_models_correct_until_t t ->
......@@ -182,7 +179,7 @@ Section CPA_temp_step.
Proof.
intros tsk belong.
apply upper_bound_forall_t_to_infinity. apply H_all_jobs_complete.
apply upper_bound_forall_t_to_infinity.
assert (P:
(forall t : instant, task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk
......
......@@ -50,8 +50,7 @@ Section Periojitt_same_law.
Definition is_indeed_the_offset (tsk : Task) (off : nat) time:=
respects_periodic_jitter_task_model_up_to_t_without_surjectivity
sched arr_seq
(task_jitter tsk) (task_period tsk)
arr_seq (task_jitter tsk) (task_period tsk)
off tsk time.
......@@ -94,8 +93,6 @@ Section Periojitt_same_law.
(*il faudra alors aussi retirer la 3e hypothese du modele*)
*)
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.
......@@ -914,8 +911,6 @@ Section Propagatability.
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 positive_cost: forall j, job_cost j > 0.
Hypothesis jobs_must_arrive: jobs_must_arrive_to_execute sched.
......@@ -982,7 +977,6 @@ Section Propagatability.
- intros t t1 t2 B W. unfold cpa_temporal_step.task_model_correct_until_t.
apply all_models_propagatable_PJM. exact B.
- exact all_jobs_complete.
- exact input_model_known.
- exact positive_cost.
- exact jobs_must_arrive.
......
......@@ -72,7 +72,7 @@ Section Proofs.
Context (arr_seq : arrival_sequence Job).
Hypothesis all_jobs_complete: forall j, exists t, completes_at sched j t.
(*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
......@@ -84,14 +84,14 @@ Section Proofs.
intros tsk BCRT.
split.
- intro P. unfold task_response_time_lower_bound.
- intro P. unfold task_response_time_lower_bound. unfold job_response_time_bound.
intros j in_arr_seq in_task.
unfold task_response_time_lower_bound_until_t in P.
assert (finition: exists t, completes_at sched j t)
by apply all_jobs_complete. destruct finition as [t finition].
apply P with (t := t). exact in_arr_seq. exact in_task.
unfold completes_at in finition.
unfold completed_by. ssromega.
destruct (completed_by sched j (job_arrival j + BCRT)) eqn:Q.
+ rewrite <- Q.
apply P with (t := job_arrival j + BCRT). exact in_arr_seq.
exact in_task. exact Q.
+ trivial.
- intro Q. unfold task_response_time_lower_bound_until_t.
intros t j in_arr_seq in_task CBS.
......@@ -111,11 +111,18 @@ Section Proofs.
- intro P. unfold task_response_time_upper_bound.
intros j in_arr_seq in_task.
unfold task_response_time_upper_bound_until_t in P.
assert (finition: exists t, completes_at sched j t)
by apply all_jobs_complete. destruct finition as [t finition].
apply P with (t := t). exact in_arr_seq. exact in_task.
unfold completes_at in finition.
unfold completed_by. ssromega.
destruct (completed_by sched j (job_arrival j + WCRT)) eqn:Q.
+ trivial.
+ destruct (completed_by sched j (job_arrival j + WCRT).+1) eqn:E.
* apply P with (t:= (job_arrival j + WCRT).+1). exact in_arr_seq.
exact in_task. exact E.
* assert (R: (job_arrival j + WCRT).+1 - WCRT <= job_arrival j).
apply P with (t := (job_arrival j + WCRT).+1).
exact in_arr_seq. exact in_task. unfold pending.
unfold has_arrived. destruct (job_arrival j <= (job_arrival j + WCRT).+1) eqn: J.
-- simpl. apply/eqP. move/eqP in E. exact E.
-- exfalso; ssromega.
-- exfalso; ssromega.
- intro Q. unfold task_response_time_upper_bound_until_t.
intros t j in_arr_seq in_task. split.
......
......@@ -39,7 +39,7 @@ Section Prefixverif.
(*========================================================================*)
Local Definition correction_t tsk j t off:=
completed_by sched j t ->
job_arrival j <= t->
arrives_in arr_seq j ->
job_task j = tsk ->
off <= theoretical_arrival j /\
......@@ -48,8 +48,8 @@ Section Prefixverif.
Local Definition injection_t tsk j j' t:=
completed_by sched j t ->
completed_by sched j' t ->
job_arrival j <= t ->
job_arrival j' <= t ->
arrives_in arr_seq j ->
arrives_in arr_seq j'->
job_task j = tsk ->
......@@ -123,7 +123,7 @@ Section Prefixverif.
(*========================================================================*)
(* --- IV --- LEMMAS --- IV --- *)
(*========================================================================*)
(*
Local Lemma utilitaire: forall j j' t t',
completes_at sched j t -> completes_at sched j' t' -> completed_by sched j (maxn t t').
Proof.
......@@ -145,8 +145,9 @@ Section Prefixverif.
apply leq_trans with (service_during sched j 0 t). ssromega.
exact J.
Qed.
*)
Lemma periodic_jitter_infinite: forall (tsk:Task),
Lemma periodic_jitter_infinite: forall (tsk:Task),
( forall t, respects_periodic_jitter_task_model_up_to_t tsk t )
->
( respects_periodic_jitter_task_model period jitter arr_seq tsk offset).
......@@ -156,25 +157,30 @@ Section Prefixverif.
unfold respects_periodic_jitter_task_model.
split. 2:split.
- 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) offset)
assert (P1: job_arrival j <= job_arrival j ->
arrives_in arr_seq j ->
job_task j = tsk ->
offset <= theoretical_arrival j /\
theoretical_arrival j - offset %| period /\
job_jitter j <= jitter)
by (apply P).
apply P1. unfold completes_at in Q. unfold completed_by. ssromega.
apply P1. apply/eqP. apply subnn.
- intros j j'.
assert (Q: exists t, completes_at sched j t). apply all_jobs_complete.
destruct Q as [t Q].
assert (R: exists t', completes_at sched j' t'). apply all_jobs_complete.
destruct R as [t' R].
assert (P2: injection_t tsk j j' (maxn t t'))
assert (P2: job_arrival j <= (maxn (job_arrival j) (job_arrival j')) ->
job_arrival j'<= (maxn (job_arrival j) (job_arrival j')) ->
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')
by (apply P).
apply P2.
+ apply utilitaire with j'. exact Q. exact R.
+ rewrite maxnC. apply utilitaire with j. exact R. exact Q.
apply P2; repeat (apply/eqP; rewrite maxnE; ssromega).
- intro n.
assert (P3: surjection_t tsk n (offset + n * period +jitter) )
assert (P3: offset + n * period + jitter <= offset + n * period +jitter->
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
theoretical_arrival j = offset + n * period)
by (apply P).
apply P3. apply leqnn.
Qed.
......@@ -198,5 +204,4 @@ Section Prefixverif.
Qed.
End Prefixverif.
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