Commit 0e3e8b4a authored by jonathan julou's avatar jonathan julou

commented latency

parent 574dcc47
Pipeline #19266 failed with stages
in 3 minutes and 36 seconds
......@@ -429,7 +429,7 @@ Section Transformation.
unfold valid_arrival_sequence_up_to_t in VAS. destruct VAS as [CAT ASU].
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. admit.
apply CAT in P. rewrite P. exact copyP.
Admitted.
......
......@@ -42,17 +42,20 @@ Section PathResponseTime.
(* --- II --- DEFINITIONS --- II --- *)
(*========================================================================*)
(*in the task_path, each task is dependant of its predecessor*)
Definition valid_task_path (tsk : Task) (rest : seq Task) :=
path task_dependency tsk rest.
(*a functionnal chain is a job chain corresponding to a task chain
up to some point *)
Fixpoint functional_chain (j : Job) (tsk_chain : seq Task) :=
match (tsk_chain), (next_job j) with
| tsk :: tsk_chain', Some j' => j :: functional_chain j' tsk_chain'
| _ , _ => nil
end.
(* EQUIVALENT:
(* EQUIVALENT: what maxime wrote at first. It generates the same function
Fixpoint functional_chain (j : Job) (tsk_chain : seq Task) :=
match tsk_chain with
| nil => nil
......@@ -65,7 +68,11 @@ Section PathResponseTime.
end.
*)
(*the last job of the functionnal chain starting at j finishes before
job_arrival j + K
intuitively, it means it takes less than K for the job j to propagate
through the task_chain *)
Definition valid_functional_path_response_time_bound K :=
forall j,
job_task j = task_path_head ->
......@@ -73,12 +80,12 @@ Section PathResponseTime.
completed_by sched (last j (functional_chain j (task_path_head :: task_path_tail)))
(job_arrival j + K).
(*the sum of each task's WCRT *)
Definition PRT := \sum_(x <- WCRTs) x.
(*a generalization of H_WCRTs used in the induction near the end of the file*)
Definition generalized_H_WCRTs WCRT_list TPH TPT :=
forall i,
i <= size TPT ->
......@@ -119,6 +126,8 @@ Section PathResponseTime.
(* --- IV --- LIST LEMMAS : nth --- IV --- *)
(*========================================================================*)
(*the nth term of a list is the (n-1)th term of its tail
if it isn't the first term *)
Local Lemma nth_pred: forall {X:Type} (l:list X) (x y:X) (i:nat),
i <> 0 -> nth x (y :: l) i = nth x l i.-1.
Proof.
......@@ -142,7 +151,7 @@ Section PathResponseTime.
simpl. reflexivity.
Qed.
(*the (n+1)th term of a list is the nth term of its tail *)
Local Lemma nth_suiv: forall {X:Type} (l:list X) (x y:X) (i:nat),
nth x (y :: l) i.+1 = nth x l i.
Proof.
......@@ -160,7 +169,8 @@ Section PathResponseTime.
reflexivity.
Qed.
(*the first term of a list is the same as the first term of a list
containing only the first term *)
Local Lemma list_first_term_rewrite: forall {X:Type} (l:list X) (x:X),
nth x [:: x] 0 = nth x [:: x & l] 0.
Proof.
......@@ -178,6 +188,7 @@ Section PathResponseTime.
(* --- V --- LIST LEMMAS : size --- V --- *)
(*========================================================================*)
(*the size of a list is 1 + the size of its tail *)
Local Lemma size_app: forall {X:Type} (l : list X) (a : X),
size (a :: l) = (size l).+1.
Proof.
......@@ -187,7 +198,7 @@ Section PathResponseTime.
- intro a. reflexivity.
Qed.
(*if the nth term exists, the default answer of nth is interchangeable*)
Local Lemma nth_exchange_first_term: forall {X:Type} (l : list X) (a b : X) (i : nat),
i < size l -> nth a l i = nth b l i.
Proof.
......@@ -211,6 +222,7 @@ Section PathResponseTime.
(* --- VI --- OTHER LIST LEMMAS --- VI --- *)
(*========================================================================*)
(*if a list has no head, it is empty *)
Local Lemma empty_list: forall {X:Type} (l:list X),
List.hd_error l = None -> l = [::].
Proof.
......@@ -221,7 +233,8 @@ Section PathResponseTime.
discriminate.
Qed.
(*the last job of a functionnal chain starting one step further
is the same as the last job of the original chain *)
Local Lemma last_but_not_least: forall s v y l,
next_job s = Some v ->
last s (functional_chain s (y::l)) = last s (functional_chain v l).
......@@ -236,6 +249,7 @@ Section PathResponseTime.
(* --- VII --- SUM LEMMAS --- VII --- *)
(*========================================================================*)
(*the first term of a non-empty sum is less than the sum itself *)
Local Lemma sum_leq_first_term: forall (l: list nat) (n:nat),
n <= \sum_(x <- (n :: l)) x.
Proof.
......@@ -249,7 +263,7 @@ Section PathResponseTime.
rewrite P. ssromega.
Qed.
(* the sum of a list starting with n is n + the sum of the tail of said list*)
Local Lemma sum_hd_tl: forall l n,
List.hd_error l = Some n ->
\sum_(x <- l) x = \sum_(x <- List.tl l) x + n.
......@@ -279,6 +293,8 @@ Section PathResponseTime.
(* --- VIII --- FUNCTIONNAL CHAIN LEMMAS --- VIII --- *)
(*========================================================================*)
(*the functional chain associated with a task chain is longer than
the functionnal chain associated with the tail of the task chain*)
Lemma functional_app_bound : forall (l : list Task) (j : Job) (a : Task),
size (functional_chain j (a :: l)) >= size (functional_chain j l).
Proof.
......@@ -291,7 +307,9 @@ Section PathResponseTime.
+ easy.
Qed.
(*if the first job j of a functionnal chain has a next job j',
the length of the functionnal chain starting at j is
1 + the length of the chain starting at j' *)
Lemma functional_next_job: forall (l:list Task) (t:Task) (j j':Job) ,
next_job j = some j'->
size (functional_chain j (t :: l)) = (size (functional_chain j' l)).+1.
......@@ -303,7 +321,7 @@ Section PathResponseTime.
simpl. rewrite P. reflexivity.
Qed.
(*the first job of a functionnal chain starting at j is j *)
Lemma functional_first_job_identification:
forall (lt : list Task) (lj : list Job) (j s:Job) ,
functional_chain j lt = s :: lj -> j = s.
......@@ -323,6 +341,9 @@ Section PathResponseTime.
(* --- IX --- TRAINING DEPENDENCY LEMMA (unused) --- IX --- *)
(*========================================================================*)
(*unused lemma
it states that forall i, the i+1-th job of the functionnal chain
is indeed dependent of the i-th job *)
Lemma job_dependency_lemma: forall (l : list Task) (i : nat) (j : Job) ,
i < (size (functional_chain j l)).-1->
job_dependency (nth j (functional_chain j l) i)
......@@ -399,7 +420,8 @@ Section PathResponseTime.
+ ssromega.
Qed.
(* if the response time bounds are correct for a list,
it is correct for its tail *)
Lemma gen_H_WCRT_tail: forall WCRT_list l x y,
generalized_H_WCRTs WCRT_list x (y::l) ->
generalized_H_WCRTs (List.tl WCRT_list) y l.
......@@ -427,6 +449,8 @@ Section PathResponseTime.
(* --- XI --- TRIVIAL CASES LEMMAS --- XI --- *)
(*========================================================================*)
(*We show that a job j always finishes before the sum of WCRTs.
It is a different formulation for technical use *)
Lemma schedimentation_1:
forall (WCRT_list: list duration) gPRT (TPT: list Task) (TPH:Task) j,
arrives_in arr_seq j -> job_task j = TPH ->
......@@ -452,6 +476,9 @@ Section PathResponseTime.
+ apply sum_leq_first_term.
Qed.
(*We show that a job j always finishes before the sum of WCRTs,
but with a different hypothesis on WCRTs (actually the same
but written in a different way).*)
Lemma schedimentation_2:
forall (WCRT_list: list duration) gPRT (TPT l: list Task) (TPH y:Task) j,
arrives_in arr_seq j -> job_task j = TPH ->
......@@ -497,6 +524,8 @@ Section PathResponseTime.
(* --- XIII --- SOME LEMMAS TO SOOTHE THE PIPELINE --- XIII --- *)
(*========================================================================*)
(*shows that each job in the dependency chain of jobs is indeed
in the corresponding task in the task chain *)
Local Lemma in_task_2_lemma: forall s y l TPH (j:Job),
valid_task_path TPH (y :: l) ->
job_task j = TPH ->
......@@ -532,7 +561,7 @@ Section PathResponseTime.
Qed.
(*technical lemma used in the following induction *)
Local Lemma possible_case (WCRT_list:list duration) (d:duration)
l TPH y (j s v:Job):
List.hd_error WCRT_list = Some d ->
......@@ -594,7 +623,7 @@ Section PathResponseTime.
Qed.
(*technical lemma used in the following induction *)
Local Lemma absurd_case (WCRT_list:list duration)
l TPH y (j s:Job):
List.hd_error WCRT_list = None ->
......@@ -648,6 +677,8 @@ Section PathResponseTime.
(* --- XIV --- GENERAL MAIN RESULT --- XIV --- *)
(*========================================================================*)
(*lemma functionnal_path_valid_latency regeneralized to allow us to perform
an induction *)
Lemma generalized_main_lemma:
forall (TPT:list Task) (TPH:Task) (WCRT_list:list duration) (gPRT:duration) (j:Job),
arrives_in arr_seq j -> job_task j = TPH ->
......@@ -706,6 +737,8 @@ Section PathResponseTime.
(* --- XV --- PARTICULARISED MAIN RESULT --- XV --- *)
(*========================================================================*)
(*States that PRT is a response time bound of the propagation time of a
job through the task chain *)
Lemma functionnal_path_valid_latency : valid_functional_path_response_time_bound PRT.
Proof.
unfold valid_functional_path_response_time_bound.
......
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