Commit 807901f6 authored by jonathan julou's avatar jonathan julou

message

parent 1875675d
Pipeline #19247 failed with stages
in 3 minutes and 38 seconds
......@@ -110,8 +110,10 @@ Section Periojitt_same_law.
intros tps j pred_j dep. split.
- intro temporal_bound.
assert (J: completes_at sched pred_j (job_arrival j)). apply correct_schedule. exact dep.
unfold completes_at in J. unfold service in J.
assert (J: dependency.completes_at sched pred_j (job_arrival j)).
unfold respects_job_dependency in correct_schedule.
apply correct_schedule. exact dep.
unfold dependency.completes_at in J. unfold service in J.
unfold completed_by in temporal_bound. unfold service in temporal_bound.
assert (K: service_during sched pred_j 0 (job_arrival j).-1 < service_during sched pred_j 0 tps).
{ apply leq_trans with (n := job_cost pred_j). ssromega. ssromega. }
......@@ -119,9 +121,9 @@ Section Periojitt_same_law.
apply jonathan.sum_to_args_lt in K. ssromega.
- intro hypo.
assert (P: completes_at sched pred_j (job_arrival j)).
assert (P: dependency.completes_at sched pred_j (job_arrival j)).
apply correct_schedule. exact dep.
unfold completes_at in P. unfold completed_by.
unfold dependency.completes_at in P. unfold completed_by.
apply leq_trans with (n:=service sched pred_j (job_arrival j)).
ssromega. unfold service. unfold service_during.
apply sum.extend_sum. apply leqnn. exact hypo.
......@@ -136,9 +138,9 @@ Section Periojitt_same_law.
Proof.
intros j pred_j ias2 ias1 jt2 jt1 dep.
assert (link: completes_at sched pred_j (job_arrival j)). apply correct_schedule; auto.
assert (link: dependency.completes_at sched pred_j (job_arrival j)). apply correct_schedule; auto.
unfold completes_at in link.
unfold dependency.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.
......@@ -193,7 +195,7 @@ Section Periojitt_same_law.
unfold respects_job_dependency in correct_schedule.
apply correct_schedule in dependency.
unfold completes_at in dependency.
unfold dependency.completes_at in dependency.
assert (UwU: service sched pred_j (job_arrival j).-1 < job_cost pred_j) by ssromega.
destruct (completed_by sched pred_j t) eqn:E.
......@@ -220,7 +222,7 @@ Section Periojitt_same_law.
}
ssromega.
- assert (link: completes_at sched pred_j (job_arrival j)).
- assert (link: dependency.completes_at sched pred_j (job_arrival j)).
{ apply correct_schedule. exact dep. }
unfold task_response_time_upper_bound in WCRT_correct.
......@@ -389,10 +391,10 @@ Local Ltac init_pipeline_lemma offset:=
ssromega.
}
assert (Q: completes_at sched pred_j (job_arrival j)).
assert (Q: dependency.completes_at sched pred_j (job_arrival j)).
apply correct_schedule. exact dependency.
unfold completed_by. unfold completes_at in Q.
unfold completed_by. unfold dependency.completes_at in Q.
unfold service. unfold service in Q.
apply leq_trans with (service_during sched pred_j 0 (job_arrival j)).
......
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