Commit 1dfedb3b authored by jonathan julou's avatar jonathan julou

just to remember

parent 03ce6180
......@@ -131,8 +131,8 @@ Section Periojitt_same_law.
(job_arrival pred_j) + BCRT <= job_arrival j.
Proof.
intros j pred_j temporal_bound in_arr_seq_j in_arr_seq_pred_j in_task_2 in_task_1 dependency.
intros j pred_j temporal_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.
unfold respects_job_dependency in correct_schedule.
......@@ -140,7 +140,7 @@ Section Periojitt_same_law.
unfold completes_at in dependency.
assert (UwU: job_cost pred_j <= service sched pred_j (job_arrival j)) by ssromega.
destruct (completed_by sched pred_j (t + BCRT)) eqn:E.
destruct (completed_by sched pred_j t) eqn:E.
unfold task_response_time_lower_bound_until_t in BCRT_correct.
apply BCRT_correct in in_arr_seq_pred_j.
......@@ -164,17 +164,23 @@ Section Periojitt_same_law.
exact Q. exact E.
(*----------------------------------------------------------------*)
assert (link: completes_at sched pred_j (job_arrival j)). { apply correct_schedule. exact dep. }
unfold completed_by in E. assert (ganon: job_cost pred_j > service sched pred_j (t + BCRT)) by ssromega.
unfold completed_by in E. assert (E': job_cost pred_j > service sched pred_j t) by ssromega.
unfold completes_at in link.
assert (zora: t + BCRT <= job_arrival j).
{
unfold service in link. unfold service in ganon.
apply leq_trans with (n:= job_cost pred_j) (p:= service_during sched pred_j 0 (job_arrival j)) in ganon.
apply jonathan.sum_to_args_leq with (F := service_at sched pred_j )in ganon. exact ganon.
ssromega.
}
ssromega.
destruct (completed_by sched pred_j (t+BCRT)) eqn:K.
+ exfalso.
+ unfold completed_by in K. assert (ganon: job_cost pred_j > service sched pred_j (t + BCRT)) by ssromega.
unfold completes_at in link.
assert (zora: t + BCRT <= job_arrival j).
{
unfold service in link. unfold service in ganon.
apply leq_trans with (n:= job_cost pred_j) (p:= service_during sched pred_j 0 (job_arrival j)) in ganon.
apply jonathan.sum_to_args_leq with (F := service_at sched pred_j )in ganon. exact ganon.
ssromega.
}
ssromega.
Qed.
......
......@@ -33,9 +33,9 @@ Section Tasks.
arrives_in arr_seq j ->
job_task j = tsk ->
(
completed_by sched j (t+R) ->
completed_by sched j t ->
~ job_response_time_bound sched j R
).
)
(*for all job, if it completed before t, then it completed before its WCRT.
If it didn't finish before t, then it arrived after t-WCRT *)
......@@ -44,13 +44,13 @@ Section Tasks.
arrives_in arr_seq j ->
job_task j = tsk ->
(
completed_by sched j (t+R)->
completed_by sched j t->
job_response_time_bound sched j R
)
/\
(
pending sched j (t+R) ->
job_arrival j > t
pending sched j t ->
job_arrival j >= t-R
).
End Tasks.
......@@ -89,7 +89,7 @@ Section Proofs.
unfold task_response_time_lower_bound_until_t in P.
destruct (completed_by sched j (job_arrival j + BCRT)) eqn:Q.
+ rewrite <- Q.
apply P with (t := job_arrival j). exact in_arr_seq.
apply P with (t := job_arrival j + BCRT). exact in_arr_seq.
exact in_task. exact Q.
+ trivial.
......@@ -114,12 +114,12 @@ Section Proofs.
destruct (completed_by sched j (job_arrival j + WCRT)) eqn:Q.
+ trivial.
+ destruct (completed_by sched j (job_arrival j + WCRT).+1) eqn:E.
* apply P with (t:= (job_arrival j).+1). exact in_arr_seq.
* apply P with (t:= (job_arrival j + WCRT).+1). exact in_arr_seq.
exact in_task. exact E.
* assert (R: (job_arrival j).+1 < job_arrival j).
apply P with (t := (job_arrival j).+1).
* assert (R: (job_arrival j + WCRT).+1 - WCRT <= job_arrival j).
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).+1 + WCRT) eqn: J.
unfold has_arrived. destruct (job_arrival j <= (job_arrival j + WCRT).+1) eqn: J.
-- simpl. apply/eqP. move/eqP in E. exact E.
-- exfalso; ssromega.
-- exfalso; ssromega.
......@@ -134,14 +134,14 @@ Section Proofs.
destruct PS as [arrjt cpltjt].
unfold has_arrived in arrjt. unfold completed_by in cpltjt.
unfold completed_by in Q.
assert (cpltjt_rewritten: job_cost j > service sched j (t+WCRT)). ssromega.
assert (R: service sched j (t+WCRT) < service sched j (job_arrival j + WCRT)).
assert (cpltjt_rewritten: job_cost j > service sched j t). ssromega.
assert (R: service sched j t < service sched j (job_arrival j + WCRT)).
{ 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).
apply jonathan.sum_to_args_lt with (F := service_at sched j) in R.
ssromega. exact W.
assert (W: t <= job_arrival j + WCRT).
apply jonathan.sum_to_args_leq with (F := service_at sched j).
exact R. ssromega.
Qed.
End Proofs.
\ No newline at end of file
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