Commit c8dafa7c authored by jonathan julou's avatar jonathan julou

ca avance

parent 1b75cc38
Pipeline #19282 failed with stages
in 3 minutes and 59 seconds
......@@ -174,7 +174,10 @@ and further development suggestions</h1>
<h3>/restructuring/analysis/analysis_up_to_t/up_to_t_definitions.v</h3>
some definitions of properties that were defined indefinitely that now
have an equivalent up to t.
have an equivalent up to t in the first half of the file.
In the second half, a transformation of an analysis on a full trace to
a prefix and back is being explored.
<h2>III) Suggestions</h2>
......@@ -190,19 +193,6 @@ and further development suggestions</h1>
What has to be done is to remove the 3rd hypothesis, and then rerun the proofs in
periodic_jitter_propagation.v removing all things surjectivity.
<h3>/restructuring/analysis/latency.v</h3>
All the mess with the reparticularization of the main_lemma and the local/general
hypothesis could be cleaned up.
It was necessary to have the particular view to understand how the path worked and
a general point of view was mandatory in order to actually do the induction,
however both ended up staying in the finished file.
The particularisation is absolutely useless.
The only potential problem is that it would become necessary to read
the dirty general lemmas rather than have the things spread out in the context.
<h3>/restructuring/analysis/analysis_up_to_t/cpa_temporal_step</h3>
......@@ -214,4 +204,22 @@ and further development suggestions</h1>
I tried to modify the proof in cpa_temporal_step_experimental.v to account for that,
nevertheless, it appears the new response_time_analysis would be impossible
because we don't have an output model at the end to verify the WCRT.
<h3>/restructuring/analysis/analysis_up_to_t/up_to_t_definitions.v</h3>
It would be necessary to prove the last lemma, response_time_analysis,
in order to tie everything together.
If the proof of valid_schedule_completion, which wires our hypothesis with
Maxime's proof, isn't finished, it would have to be done too.
A un moment je dois prouver une contradiction en utilisant le fait qu'un
job soit dans la sequence d'arrivée au delà de la frontière ou on sait des
choses sur elle. Je m'y suis peut être mal pris.
Si quoi que ce soit n'est pas clair, n'hesitez pas à me contacter par mail à
jonathan.julou@grenoble-inp.org
......@@ -219,7 +219,7 @@ Section Transformation.
(* [next_state t candidate_jobs] should return the schedule state at time t given the list of pending jobs and their remaining cost *)
Variable next_state : instant -> seq (Jobs * duration) -> State.
Variable t_start : instant.
(*Variable t_start : instant. <-- it should be my t *)
Hypothesis next_state_correct : forall t jobs j,
scheduled_in j (next_state t jobs) -> j \in map fst jobs.
......@@ -227,7 +227,7 @@ Section Transformation.
Hypothesis next_state_service : forall t jobs j c,
(j, c) \in jobs -> service_in j (next_state t jobs) <= c.
Definition sched_prefixed := complete_schedule arr_seq next_state sched t.
Definition sched_prefixed := complete_schedule arr_seq_prefixed next_state sched t.
Check sched_prefixed.
......@@ -317,36 +317,53 @@ 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 ->
(*
Hypothesis Hsched1 : forall j t', t' < t -> scheduled_at sched j t' -> arrives_in arr_seq_prefixed j.
Hypothesis Hsched2 : forall j t', t' < t -> scheduled_at sched j t' -> has_arrived j t'.
Hypothesis Hsched3 : forall j t', t' <= t -> service sched j t' <= job_cost j.
*)
(*if the base schedule is valid up to t, the completed_schedule
is always valid with the completed arrival_sequence*)
Lemma valid_schedule_to_prefixed_sched :
(*valid_arrival_sequence_up_to_t arr_seq t ->*)
valid_schedule_up_to_t State sched arr_seq t ->
valid_schedule sched arr_seq_prefixed.
valid_schedule_up_to_t State sched arr_seq_prefixed t.
Proof.
intros VAS VS.
unfold valid_schedule. unfold valid_schedule_up_to_t in VS.
destruct VS as [JCFAS VS]. destruct VS as [JMATE CJDE].
unfold valid_arrival_sequence_up_to_t in VAS.
destruct VAS as [CAT ASU].
split. 2: split.
- unfold jobs_come_from_arrival_sequence. intros j n P.
unfold arrives_in. unfold arrivals_at. unfold arr_seq_prefixed.
unfold jobs_come_from_arrival_sequence_up_to_t in JCFAS.
unfold arrives_in in JCFAS. unfold arrivals_at in JCFAS.
destruct (n <= t) eqn: E.
+ assert (J: n<=t) by apply E. apply JCFAS with (j:=j) in E.
destruct E as [t' E]. exists n. rewrite J. admit. admit.
+ admit.
- unfold jobs_must_arrive_to_execute.
intros j n scheduled. destruct (n <= t) eqn:E.
+ unfold has_arrived.
unfold jobs_must_arrive_to_execute_up_to_t in JMATE.
unfold has_arrived in JMATE. apply JMATE; auto.
+ unfold scheduled_at in scheduled. admit.
intros VS.
unfold valid_schedule_up_to_t in VS. destruct VS as [A B]. destruct B as [B C].
unfold valid_schedule_up_to_t. split. 2: split.
- unfold jobs_come_from_arrival_sequence_up_to_t in A.
unfold jobs_come_from_arrival_sequence_up_to_t.
intros t' j less schedat. unfold arrives_in in A. unfold arrives_in.
assert (D: exists t : instant, j \in arrivals_at arr_seq t). apply A with t'; auto.
destruct D as [y P].
unfold arrivals_at. unfold arr_seq_prefixed.
exists y. destruct (y<=t) eqn:E. unfold arrivals_at in P. exact P.
admit.
- admit.
- admit.
Admitted.
(*if the base schedule is valid up to t, the completed_schedule
is always valid with the completed arrival_sequence*)
Lemma valid_schedule_completion :
valid_arrival_sequence_up_to_t arr_seq t ->
valid_schedule_up_to_t State sched arr_seq t ->
valid_schedule sched_prefixed arr_seq_prefixed.
Proof.
intros VAS VS0.
assert (VS : valid_schedule_up_to_t State sched arr_seq_prefixed t).
apply valid_schedule_to_prefixed_sched. exact VS0.
unfold valid_schedule_up_to_t in VS. destruct VS as [A B]. destruct B as [B C].
apply complete_schedule_valid; auto.
- apply valid_arrival_sequence_completion. exact VAS.
- intros j t' less schedat.
unfold jobs_come_from_arrival_sequence_up_to_t in A.
apply A with t'. ssromega. exact schedat.
Qed.
(*if all properties are verified up to t, the response time is
bound indefinitely in the completed trace *)
Lemma response_time_analysis_prefixed :
......@@ -354,7 +371,7 @@ Section Transformation.
all_jobs_from_taskset_up_to_t arr_seq ts t ->
valid_schedule_up_to_t State sched arr_seq t ->
task_response_time_upper_bound arr_seq_prefixed sched tsk R.
task_response_time_upper_bound arr_seq_prefixed sched_prefixed tsk R.
Proof.
intros VAS AJFT VS.
apply H_analysis_correct.
......@@ -383,10 +400,10 @@ Section Transformation.
all_jobs_from_taskset_up_to_t arr_seq ts t ->
valid_schedule_up_to_t State sched arr_seq t ->
task_response_time_upper_bound_until_t sched arr_seq_prefixed t R tsk.
task_response_time_upper_bound_until_t sched_prefixed arr_seq_prefixed t R tsk.
Proof.
intros VAS AJFT VS.
assert (prefixed: task_response_time_upper_bound arr_seq_prefixed sched tsk R) by
assert (prefixed: task_response_time_upper_bound arr_seq_prefixed sched_prefixed tsk R) by
apply (response_time_analysis_prefixed VAS AJFT VS).
apply upper_bound_forall_t_to_infinity. exact prefixed.
Qed.
......@@ -405,10 +422,10 @@ Section Transformation.
task_response_time_upper_bound_until_t sched arr_seq t R tsk.
Proof.
intros VAS AJFT VS.
assert (prefixed: task_response_time_upper_bound_until_t sched arr_seq_prefixed t R tsk) by
assert (prefixed: task_response_time_upper_bound_until_t sched_prefixed arr_seq_prefixed t R tsk) by
apply (finite_analysis_prefixed VAS AJFT VS).
assert (M: valid_schedule sched arr_seq_prefixed).
assert (M: valid_schedule sched_prefixed arr_seq_prefixed).
apply valid_schedule_completion; auto.
unfold valid_schedule in M. destruct M as [P1 M]; destruct M as [P2 P3].
......@@ -416,6 +433,7 @@ Section Transformation.
unfold task_response_time_upper_bound_until_t.
intros j in_arr_seq in_task. split.
(*
- intro CBS. apply prefixed. 3: exact CBS. 2: exact in_task.
assert (K: exists t', job_arrival j <= t' < t /\ scheduled_at sched j t').
apply completed_implies_scheduled_before_up_to_t with t. apply leqnn.
......@@ -438,7 +456,7 @@ Section Transformation.
unfold consistent_arrival_times_up_to_t in CAT. unfold arrives_at in CAT.
assert (copyP: j \in arr_seq y). unfold arrivals_at in P. exact P.
apply CAT in P. rewrite P. exact copyP.
*)
Admitted.
......
......@@ -38,6 +38,7 @@ Section Prefixverif.
(* --- II --- DEFINITIONS --- II --- *)
(*========================================================================*)
(*first hypothesis of the model*)
Local Definition correction_t tsk j t off:=
job_arrival j <= t->
arrives_in arr_seq j ->
......@@ -46,7 +47,7 @@ Section Prefixverif.
theoretical_arrival j - off %| period /\
job_jitter j <= jitter.
(*second hypothesis of the model*)
Local Definition injection_t tsk j j' t:=
job_arrival j <= t ->
job_arrival j' <= t ->
......@@ -56,7 +57,7 @@ Section Prefixverif.
job_task j' = tsk->
theoretical_arrival j = theoretical_arrival j' -> j = j'.
(*third hypothesis of the model*)
Local Definition surjection_t tsk n t :=
offset + n * period + jitter <= t ->
exists j,
......@@ -64,14 +65,14 @@ Section Prefixverif.
job_task j = tsk /\
theoretical_arrival j = offset + n * period.
(*the model with the 3 properties*)
Definition respects_periodic_jitter_task_model_up_to_t
(tsk : Task) (t : instant) :=
(forall j, correction_t tsk j t offset)/\
(forall j j', injection_t tsk j j' t )/\
(forall n, surjection_t tsk n t ).
(*the same but with an unknown offset*)
Definition respects_periodic_jitter_task_model_up_to_t_offset_unknown
(tsk : Task) (t : instant) :=
exists off,
......@@ -90,6 +91,7 @@ Section Prefixverif.
(forall j, correction_t tsk j t offset)/\
(forall j j', injection_t tsk j j' t ).
(*the same as above, but with an unknown offset*)
Definition respects_periodic_jitter_task_model_up_to_t_offset_unknown_without_surjectivity
(tsk : Task) (t : instant) :=
exists off,
......@@ -118,84 +120,57 @@ 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.
intros j j' t t' Q R.
assert (U: maxn t t' >= t). destruct (t <= t') eqn:E.
assert (V: maxn t t' = t'). apply/maxn_idPr. exact E.
rewrite V. exact E. assert (U': t >= t'). ssromega.
assert (V: maxn t t' = t). apply/maxn_idPl. exact U'.
rewrite V. apply leqnn.
unfold completed_by. unfold service.
unfold completes_at in Q. unfold service in Q.
assert (J: service_during sched j 0 t <= service_during sched j 0 (maxn t t')).
unfold service_during.
unfold service_during in Q.
apply sum.extend_sum. apply leqnn. exact U.
apply leq_trans with (service_during sched j 0 t). ssromega.
exact J.
Qed.
*)
(*prooves the equivalence of this model for all t and the former infinite one*)
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).
Proof.
intros tsk P.
unfold respects_periodic_jitter_task_model_up_to_t in P.
unfold respects_periodic_jitter_task_model.
split. 2:split.
- intros j.
assert (P1: job_arrival j <= job_arrival j ->
intros tsk. split.
- intro P.
unfold respects_periodic_jitter_task_model_up_to_t in P.
unfold respects_periodic_jitter_task_model.
split. 2:split.
+ intros j.
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. apply/eqP. apply subnn.
- intros j j'.
assert (P2: job_arrival j <= (maxn (job_arrival j) (job_arrival j')) ->
by (apply P).
apply P1. apply/eqP. apply subnn.
+ intros j j'.
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; repeat (apply/eqP; rewrite maxnE; ssromega).
- intro n.
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.
Lemma periodic_jitter_finite: forall (tsk:Task),
( respects_periodic_jitter_task_model period jitter arr_seq tsk offset)
->
( forall t, respects_periodic_jitter_task_model_up_to_t tsk t ).
Proof.
intros tsk P t.
unfold respects_periodic_jitter_task_model_up_to_t.
unfold respects_periodic_jitter_task_model in P.
destruct P as [P1 P].
destruct P as [P2 P3].
split. 2:split.
- intros j inutile. apply P1.
- intros j j' inutile_1 inutile_2. apply P2.
- intros n inutile. apply P3.
by (apply P).
apply P2; repeat (apply/eqP; rewrite maxnE; ssromega).
+ intro n.
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.
- intros P t.
unfold respects_periodic_jitter_task_model_up_to_t.
unfold respects_periodic_jitter_task_model in P.
destruct P as [P1 P].
destruct P as [P2 P3].
split. 2:split.
+ intros j inutile. apply P1.
+ intros j j' inutile_1 inutile_2. apply P2.
+ intros n inutile. apply P3.
Qed.
......
......@@ -3,6 +3,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop p
From rt.util Require Import ssromega.
From rt.util Require Import sum.
(*mostly boolean utility lemmas for now*)
Lemma leq_plusplus: forall a b:nat, a<=b -> a.+1 <= b.+1.
Proof.
......@@ -123,6 +124,9 @@ From rt.util Require Import sum.
intros. ssromega.
Qed.
(*interesting property on sums that converts a strict inequality of the sums
to an inequality on the bounds of the sum variable*)
Local Lemma sum_to_args_leq: forall (a b:nat) (F:nat->nat),
\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t
-> a <= b.
......@@ -157,7 +161,8 @@ From rt.util Require Import sum.
exact P.
Qed.
(*interesting property on sums that converts a strict inequality of the sums
to a strict inequality on the bounds of the sum variable*)
Local Lemma sum_to_args_lt: forall (a b:nat) (F:nat->nat),
\sum_(0 <= t < a) F t < \sum_(0 <= t < b) F t
-> a < b.
......
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