Commit 76345509 authored by jonathan julou's avatar jonathan julou

removed WCRT analysis for now

parent dfb60a45
Pipeline #18945 passed with stages
in 3 minutes and 35 seconds
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
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