Commit 89bef524 authored by jonathan julou's avatar jonathan julou

petit commit qui marchera pas

parent 839bdc2e
Pipeline #18905 failed with stages
in 1 minute and 18 seconds
......@@ -101,8 +101,8 @@ Section CPA_temp_step.
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk ).
(*necessary for the base case of the induction in the final lemma*)
(*should be easy to verify from a trace, since only the first task can
have a job at t=0. For the other tasks, it is sufficient to verify
(*should be easy to verify from an actual trace, since only the first task
can have a job at t=0. For the other tasks, it is sufficient to verify
that their model allows them to not have a job at t=0.*)
Hypothesis models_correct_on_init : all_task_models_correct_until_t 0.
......
From rt.restructuring.model Require Export dependency.
From rt.restructuring.model.arrival Require Export periodic_jitter.
From rt.restructuring.analysis Require Export schedulability.
From rt.restructuring.behavior Require Export schedule.
From rt.util Require Import ssromega.
From rt.restructuring.analysis Require Export verify_up_to_t.
From rt.restructuring.analysis Require Export schedulability_up_to_t.
From rt.restructuring.analysis Require Export periodic_jitter_propagation_up_to_t.
From rt.restructuring.model Require Export task_cost.
Set Bullet Behavior "Strict Subproofs".
Section Analysis.
(*========================================================================*)
(* --- I --- CONTEXT AND VARIABLES --- I --- *)
(*========================================================================*)
Context {PState : Type}.
Context (sched : schedule PState).
Context (Task: TaskType)
`{PeriodicJitterModel Task}
`{TaskDependency Task}
`{TaskCost Task}.
Context {Job : JobType}
`{JobTask Job Task}
`{JobArrival Job}
`{JobJitter Job}
`{JobCost Job}
`{ProcessorState Job PState}
`{JobDependency Job}.
Context (arr_seq : arrival_sequence Job).
Variable ts : {set Task}.
Variable t : instant.
Variable task_WCRT : Task -> duration.
Variable task_BCRT : Task -> duration.
(*we get need more information on the base system*)
Variable task_BCET: Task -> duration.
Variable task_resource: Task -> nat.
Variable task_priority: Task -> nat.
Let task_WCET := task_cost.
(*========================================================================*)
(* --- II --- DEFINITIONS --- II --- *)
(*========================================================================*)
Definition task_higher_priority tsk1 tsk2 :=
(task_resource tsk1 == task_resource tsk2) &&
(task_priority tsk1 > task_priority tsk2).
Definition WCRT_lower_bound (t: instant) (tsk: Task):=
(forall tsk', tsk' \in ts -> task_higher_priority tsk' tsk ->
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk') tsk') ->
task_WCRT tsk >= task_WCET tsk
+ \sum_(tsk' <- ts| task_higher_priority tsk' tsk )
((1 + Nat.div(task_jitter tsk')(task_period tsk')
+ Nat.div(task_WCRT tsk)(task_period tsk'))
* task_WCRT tsk').
Definition BCRT_upper_bound (t: instant) (tsk: Task) :=
task_BCRT tsk <= task_BCET tsk.
(*========================================================================*)
(* --- III --- HYPOTHESIS --- III --- *)
(*========================================================================*)
Hypothesis priority_injective : forall tsk1 tsk2,
task_resource tsk1 = task_resource tsk2 ->
task_priority tsk1 = task_priority tsk2 ->
tsk1 = tsk2.
Hypothesis BCET_is_a_BCRT : forall tsk,
task_response_time_lower_bound_until_t sched arr_seq t (task_BCET tsk) tsk.
Hypothesis well_bounded_WCRTs: forall tsk, WCRT_lower_bound t tsk.
Hypothesis well_bounded_BCRTs: forall tsk, BCRT_upper_bound t tsk.
(*========================================================================*)
(* --- III --- LEMMAS --- III --- *)
(*========================================================================*)
Lemma WCRT_lower_bound_correct: forall tsk, tsk \in ts ->
WCRT_lower_bound t tsk ->
all_task_models_correct_until_t arr_seq ts (task_input_PJM sched Task) t->
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk.
Proof.
Admitted.
Lemma BCRT_upper_bound_correct: forall tsk, tsk \in ts ->
BCRT_upper_bound t tsk ->
all_task_models_correct_until_t arr_seq ts (task_input_PJM sched Task) t->
task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk) tsk.
Proof.
intros tsk in_ts Bub ATMC.
Qed.
Lemma response_time_analysis :
forall tsk, tsk \in ts ->
all_task_models_correct_until_t arr_seq ts (task_input_PJM sched Task) t->
(task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk) tsk
/\
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk ).
Proof.
intros tsk in_ts ATMC. split.
- apply BCRT_upper_bound_correct.
exact in_ts. apply well_bounded_BCRTs. exact ATMC.
- apply WCRT_lower_bound_correct.
exact in_ts. apply well_bounded_WCRTs. exact ATMC.
Qed.
End Analysis.
\ No newline at end of file
......@@ -59,11 +59,10 @@ Section Periojitt_same_law.
(* --- III --- HYPOTHESIS --- III --- *)
(*========================================================================*)
(*the response time of the task tsk1 is always comprised between BCRT and WCRT*)
Hypothesis WCRT_correct: task_response_time_upper_bound_until_t sched arr_seq t (WCRT) tsk1.
Hypothesis BCRT_correct: task_response_time_lower_bound_until_t sched arr_seq t (BCRT) tsk1.
Hypothesis correct_dependancy: this_needs_a_name Task Job arr_seq task_dependency.
Hypothesis valid_arr_seq: valid_arrival_sequence arr_seq.
......@@ -72,7 +71,10 @@ Section Periojitt_same_law.
Hypothesis correct_period: valid_period (task_period tsk1).
(*we impose a hard link between the theoretical arrival of the previous job
and that of the next job, by saying the theoretical arrivals sould be periodic,
of period the best case response time.
It is necessary to caracterize the jitter of said next job.*)
Hypothesis hyp_arrival_suiv_expr: forall (j pred_j : Job) (offset : nat),
arrives_in arr_seq j ->
arrives_in arr_seq pred_j ->
......@@ -1115,7 +1117,8 @@ Section Propagatability.
(* --- >_< --- HYPOTHESIS --- >_< --- *)
(*========================================================================*)
(*we reformulate the lemma periodic_jitter_same_law_up_to_t proved above to
match the definition of the general propagagability. *)
Lemma all_models_propagatable_PJM:
forall (t:instant) (tsk1 tsk2:Task),
tsk1 \in ts -> propagatable sched arr_seq task_WCRT task_BCRT task_input_PJM tsk1 tsk2 t.
......@@ -1139,9 +1142,8 @@ Section Propagatability.
exact model_verified_by_tsk1. exact dependency. exact dependency.
Qed.
(*assuming the hypothesis, all WCRTs are respected.*)
Lemma final_result_PJM: forall tsk, tsk \in ts ->
task_response_time_upper_bound arr_seq sched tsk (task_WCRT tsk).
Proof.
intros tsk P.
......
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