Commit aaf460d7 authored by jonathan julou's avatar jonathan julou

deblokage

parent 2b450c38
Pipeline #19082 failed with stages
in 33 seconds
......@@ -159,7 +159,16 @@ Section CPA_temp_step.
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.
apply H_jobs_must_arrive. intro Q. destruct (task_WCRT tsk == 0) eqn: E.
+ move/eqP in E. rewrite E. destruct (job_arrival j == 0) eqn: F.
* move/eqP in F. assert (job_cost j = 0).
{
} assert (job_cost j > 0). apply H_positive_cost.
exfalso. ssromega.
* ssromega.
+ ssromega.
- unfold task_response_time_lower_bound_until_t.
intros j P1 P2.
intro Q. apply completed_implies_scheduled_before in Q.
......
......@@ -128,8 +128,54 @@ Section Periojitt_same_law.
Qed.
Local Lemma arrival_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
job_task j = tsk2 -> job_task pred_j = tsk1 ->
job_dependency pred_j j ->
job_arrival j > (job_arrival pred_j).
Proof.
intros j pred_j ias2 ias1 jt2 jt1 dep.
assert (link: completes_at sched pred_j (job_arrival j)). apply correct_schedule; auto.
unfold completes_at in link.
destruct (job_arrival pred_j < job_arrival j) eqn:E.
- trivial.
- assert (A: job_arrival pred_j >= job_arrival j) by ssromega.
unfold service in link.
assert (B: service_during sched pred_j 0 (job_arrival j) = 0).
apply cumulative_service_before_job_arrival_zero with job_arrival; auto.
assert (C: job_cost pred_j = 0). ssromega.
ssromega.
Qed.
Local Lemma arrival_bound_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
job_task j = tsk2 -> job_task pred_j = tsk1 ->
job_dependency pred_j j ->
job_arrival j <= t.+1 -> job_arrival pred_j <= t.
Proof.
intros j pred_j in_arr_seq_2 in_arr_seq_1 in_task_2 in_task_1
dependency hypo.
assert (Q: completed_by sched pred_j t.+1). apply dependency_bound with j; auto.
unfold completed_by in Q.
destruct (job_arrival pred_j <= t) eqn:E.
trivial.
exfalso. assert (T: job_arrival pred_j >= t.+1). ssromega.
assert (V:job_cost pred_j <= 0). unfold service in Q.
assert (W:service_during sched pred_j 0 t.+1 = 0).
apply cumulative_service_before_job_arrival_zero with job_arrival.
exact H_jobs_must_arrive. exact T.
ssromega. assert (contra: 0 < job_cost pred_j) by apply H_positive_cost.
ssromega.
Qed.
Lemma dependency_arrival_bound_WCRT: forall (j pred_j : Job),
job_arrival pred_j <= t ->
job_arrival j <= t.+1 ->
arrives_in arr_seq j ->
arrives_in arr_seq pred_j ->
job_task j = tsk2 ->
......@@ -139,10 +185,12 @@ Section Periojitt_same_law.
(job_arrival j) <= (job_arrival pred_j) + WCRT.
Proof.
intros j pred_j arrival_bound in_arr_seq_j in_arr_seq_pred_j in_task_2 in_task_1 dependency.
intros j pred_j end_bound in_arr_seq_j in_arr_seq_pred_j in_task_2 in_task_1 dependency.
assert (dep: job_dependency pred_j j). exact dependency.
assert (arrival_bound: job_arrival pred_j <= t). apply arrival_bound_propagation with j; auto.
unfold respects_job_dependency in correct_schedule.
apply correct_schedule in dependency.
unfold completes_at in dependency.
......@@ -175,19 +223,13 @@ Section Periojitt_same_law.
- assert (link: completes_at sched pred_j (job_arrival j)).
{ apply correct_schedule. exact dep. }
assert (hourra: job_arrival pred_j >= t-WCRT).
{ unfold task_response_time_upper_bound in WCRT_correct.
unfold task_response_time_upper_bound in WCRT_correct.
apply WCRT_correct in in_arr_seq_pred_j.
apply in_arr_seq_pred_j; auto. unfold pending. unfold has_arrived.
assert (Z: t < job_arrival pred_j + WCRT). apply in_arr_seq_pred_j; auto. unfold pending. unfold has_arrived.
assert (U: ~~ completed_by sched pred_j t).
apply/eqP. move/eqP in E. exact E.
destruct (~~ completed_by sched pred_j t), (job_arrival pred_j <= t); auto. }
Admitted.
destruct (~~ completed_by sched pred_j t), (job_arrival pred_j <= t); auto. ssromega.
Qed.
......@@ -319,51 +361,6 @@ Local Ltac init_pipeline_lemma offset:=
Local Lemma arrival_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
job_task j = tsk2 -> job_task pred_j = tsk1 ->
job_dependency pred_j j ->
job_arrival j > (job_arrival pred_j).
Proof.
intros j pred_j ias2 ias1 jt2 jt1 dep.
assert (link: completes_at sched pred_j (job_arrival j)). apply correct_schedule; auto.
unfold completes_at in link.
destruct (job_arrival pred_j < job_arrival j) eqn:E.
- trivial.
- assert (A: job_arrival pred_j >= job_arrival j) by ssromega.
unfold service in link.
assert (B: service_during sched pred_j 0 (job_arrival j) = 0).
apply cumulative_service_before_job_arrival_zero with job_arrival; auto.
assert (C: job_cost pred_j = 0). ssromega.
ssromega.
Qed.
Local Lemma arrival_bound_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
job_task j = tsk2 -> job_task pred_j = tsk1 ->
job_dependency pred_j j ->
job_arrival j <= t.+1 -> job_arrival pred_j <= t.
Proof.
intros j pred_j in_arr_seq_2 in_arr_seq_1 in_task_2 in_task_1
dependency hypo.
assert (Q: completed_by sched pred_j t.+1). apply dependency_bound with j; auto.
unfold completed_by in Q.
destruct (job_arrival pred_j <= t) eqn:E.
trivial.
exfalso. assert (T: job_arrival pred_j >= t.+1). ssromega.
assert (V:job_cost pred_j <= 0). unfold service in Q.
assert (W:service_during sched pred_j 0 t.+1 = 0).
apply cumulative_service_before_job_arrival_zero with job_arrival.
exact H_jobs_must_arrive. exact T.
ssromega. assert (contra: 0 < job_cost pred_j) by apply H_positive_cost.
ssromega.
Qed.
Local Lemma end_bound_propagation: forall (j pred_j : Job),
arrives_in arr_seq j -> arrives_in arr_seq pred_j ->
......@@ -469,6 +466,8 @@ Local Ltac init_pipeline_lemma offset:=
init_pipeline_lemma offset.
intros in_task_two in_arr_seq_two arr_bound.
assert (end_bound: job_arrival j <= t.+1) by (apply arr_bound).
previous_job_init j in_arr_seq_two in_task_two dependency.
apply arrival_bound_propagation with (pred_j := pred_j) in arr_bound.
correction_init j offset pred_j correction in_arr_seq_one in_task_one arr_bound.
......@@ -513,7 +512,7 @@ Local Ltac init_pipeline_lemma offset:=
- apply arrival_bound_propagation with (pred_j := pred_j) in arr_bound; auto.
-exact in_arr_seq_one. -exact in_task_two.
-exact in_task_one. -exact j_predj_dependency.
Admitted.
Qed.
......
......@@ -50,7 +50,7 @@ Section Tasks.
/\
(
pending sched j t ->
job_arrival j >= t-R
job_arrival j + R > t
).
End Tasks.
......@@ -116,7 +116,7 @@ Section Proofs.
+ destruct (completed_by sched j (job_arrival j + WCRT).+1) eqn:E.
* apply P with (t:= (job_arrival j + WCRT).+1). exact in_arr_seq.
exact in_task. exact E.
* assert (R: (job_arrival j + WCRT).+1 - WCRT <= job_arrival j).
* assert (R: (job_arrival j + WCRT).+1 < job_arrival j + WCRT).
apply P with (t := (job_arrival j + WCRT).+1).
exact in_arr_seq. exact in_task. unfold pending.
unfold has_arrived. destruct (job_arrival j <= (job_arrival j + WCRT).+1) eqn: J.
......@@ -139,9 +139,10 @@ Section Proofs.
{ apply leq_trans with (job_cost j). exact cpltjt_rewritten.
apply Q. exact in_arr_seq. exact in_task. }
unfold service in R. unfold service_during in R.
assert (W: t <= job_arrival j + WCRT).
apply jonathan.sum_to_args_leq with (F := service_at sched j).
exact R. ssromega.
assert (W: t < job_arrival j + WCRT).
apply jonathan.sum_to_args_lt with (F := service_at sched j).
exact R. exact W.
Qed.
End Proofs.
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