Commit 5f4d4e8f authored by jonathan julou's avatar jonathan julou

reduced a proof in CPA_temporal step

parent 5357fe40
Pipeline #18907 failed with stages
in 42 seconds
......@@ -6,7 +6,7 @@ From rt.util Require Export list.
From rt.util Require Import ssromega.
From rt.util Require Import bigcat.
From rt.restructuring.analysis.frame_by_frame Require Export schedulability_up_to_t.
From rt.restructuring.analysis.analysis_up_to_t Require Export schedulability_up_to_t.
Set Bullet Behavior "Strict Subproofs".
......@@ -140,6 +140,28 @@ Section CPA_temp_step.
Qed.
Lemma induction_first_step : forall tsk, tsk \in ts ->
task_response_time_upper_bound_until_t sched arr_seq 0 (task_WCRT tsk) tsk /\
task_response_time_lower_bound_until_t sched arr_seq 0 (task_BCRT tsk) tsk /\
all_task_models_correct_until_t 0.
Proof.
intros tsk belong.
split. 2:split.
- unfold task_response_time_upper_bound_until_t.
intros j P1 P2. split.
intro Q. apply completed_implies_scheduled_before in Q.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive. intro Q. ssromega.
- unfold task_response_time_lower_bound_until_t.
intros j P1 P2.
intro Q. apply completed_implies_scheduled_before in Q.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive.
- unfold all_task_models_correct_until_t.
intros tsssk Q. apply models_correct_on_init. exact Q.
Qed.
(*final lemma: all WCRT correct for infinite traces.
It should be unnecessary to verify BCRTs at this step,
but should be easy by extracting it alongside the WCRT
......@@ -148,7 +170,7 @@ Section CPA_temp_step.
task_response_time_upper_bound arr_seq sched tsk (task_WCRT tsk).
Proof.
intros tsk belong IFS.
intros tsk belong.
apply upper_bound_forall_t_to_infinity. apply H_all_jobs_complete.
assert (P:
......@@ -160,22 +182,9 @@ Section CPA_temp_step.
{ intros P t. apply P. }
apply P.
induction t as [| t IHt].
{ (*INITIALISATION*)
split. 2:split.
- unfold task_response_time_upper_bound_until_t.
intros j P1 P2. split.
intro Q. apply completed_implies_scheduled_before in Q.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive. intro Q. ssromega.
- unfold task_response_time_lower_bound_until_t.
intros j P1 P2.
intro Q. apply completed_implies_scheduled_before in Q.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive.
- unfold all_task_models_correct_until_t.
intros tsssk Q. apply models_correct_on_init. exact Q.
apply induction_first_step. exact belong.
}
{ (*HEREDITY*)
destruct IHt as [W IHt].
......
......@@ -10,3 +10,7 @@ ANALYSIS
modification de tous les autres fichiers sauf schedulability
et latency_backup (squelette fait par Maxime qui ne devrait plus servir)
/!\ hors de restructuring, le script python proofloc.py est aussi modifié /!\
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