Commit 8a48db8d authored by jonathan julou's avatar jonathan julou

fuuuuuuuuuuuuuuuuuu

parent 4cc95ad9
Pipeline #19242 failed with stages
in 26 seconds
......@@ -4,6 +4,7 @@ From rt.restructuring.model Require Export preemptive.
From rt.restructuring.model Require Export work_conserving.
From rt.restructuring.analysis Require Export schedulability_up_to_t.
(*From rt.restructuring.implementation Require Export prefix.*)
Set Bullet Behavior "Strict Subproofs".
......@@ -217,12 +218,10 @@ Section Transformation.
Definition arr_seq_prefixed time:=
if ( time <= t ) then ( arr_seq time ) else ( nil ).
(*
Fixpoint schedule_prefix time:=
if ( time <= t ) then ( sched time ) else ( ??? ).
Definition complete_schedule : schedule State :=
fun t => complete_schedule_helper (t - t_start) t.
*)
Lemma valid_arrival_sequence_completion :
valid_arrival_sequence_up_to_t arr_seq t ->
valid_arrival_sequence arr_seq_prefixed.
......@@ -272,6 +271,41 @@ Section Transformation.
+ discriminate.
Qed.
(*Lemma from facts/service.v rewritten up to t.
It is useful for the next lemma*)
Lemma positive_service_implies_scheduled_since_arrival_up_to_t tps:
forall j t', t' <= tps ->
jobs_must_arrive_to_execute_up_to_t State sched tps->
service sched j t' > 0 ->
exists t'', (job_arrival j <= t'' < t' /\ scheduled_at sched j t'').
Proof.
move=> j t' UTT JMATE SERVICE.
have EX_SCHED := positive_service_implies_scheduled_before sched j t' SERVICE.
inversion EX_SCHED as [t'' [TIMES SCHED_AT]].
exists t''; split; last by assumption.
rewrite /(_ && _) ifT //.
move: JMATE. rewrite /jobs_must_arrive_to_execute_up_to_t /has_arrived => ARR.
apply: ARR. ssromega. easy.
Qed.
(* Lemma from facts/completion.v. we prove that the job with a
positive cost must be scheduled to be completed before a given time. *)
Lemma completed_implies_scheduled_before_up_to_t tps:
forall j t', t' <= tps ->
jobs_must_arrive_to_execute_up_to_t State sched tps->
completed_by sched j t' ->
exists t'',
job_arrival j <= t'' < t'
/\ scheduled_at sched j t''.
Proof.
rewrite /completed_by.
move=> j t' UTT JMATE COMPLETE.
have POSITIVE_SERVICE: 0 < service sched j t'.
apply leq_trans with (n := job_cost j); auto.
apply positive_service_implies_scheduled_since_arrival_up_to_t with tps;
easy.
Qed.
Lemma valid_schedule_completion :
valid_arrival_sequence_up_to_t arr_seq t ->
valid_schedule_up_to_t State sched arr_seq t ->
......@@ -288,10 +322,16 @@ Section Transformation.
unfold jobs_come_from_arrival_sequence_up_to_t in JCFAS.
unfold arrives_in in JCFAS. unfold jobs_arriving_at in JCFAS.
destruct (n <= t) eqn: E.
+ apply JCFAS with (j:=j) in E. destruct E as [t' E].
admit. admit.
+ assert (J: n<=t) by apply E. apply JCFAS with (j:=j) in E.
destruct E as [t' E]. exists n. rewrite J. admit. admit.
+ admit.
- admit.
- unfold jobs_must_arrive_to_execute.
intros j n scheduled. destruct (n <= t) eqn:E.
+ unfold has_arrived.
unfold jobs_must_arrive_to_execute_up_to_t in JMATE.
unfold has_arrived in JMATE. apply JMATE; auto.
+ unfold scheduled_at in scheduled. admit.
- admit.
Admitted.
......@@ -335,6 +375,8 @@ Section Transformation.
apply upper_bound_forall_t_to_infinity. exact prefixed.
Qed.
Lemma response_time_analysis :
valid_arrival_sequence_up_to_t arr_seq t ->
all_jobs_from_taskset_up_to_t arr_seq ts t ->
......@@ -346,24 +388,37 @@ Section Transformation.
assert (prefixed: task_response_time_upper_bound_until_t sched arr_seq_prefixed t R tsk) by
apply (finite_analysis_prefixed VAS AJFT VS).
assert (M: valid_schedule sched arr_seq_prefixed).
apply valid_schedule_completion; auto.
unfold valid_schedule in M. destruct M as [P1 M]; destruct M as [P2 P3].
unfold task_response_time_upper_bound_until_t in prefixed.
unfold task_response_time_upper_bound_until_t.
intros j in_arr_seq in_task. split.
- intro CBS. apply prefixed. 3: exact CBS. 2: exact in_task.
unfold arrives_in. unfold arrives_in in in_arr_seq.
destruct in_arr_seq as [n P].
unfold jobs_arriving_at. unfold jobs_arriving_at in P.
unfold arr_seq_prefixed. exists n. destruct (n <= t) eqn: E.
+ exact P.
+ admit.
assert (K: exists t', job_arrival j <= t' < t /\ scheduled_at sched j t').
apply completed_implies_scheduled_before_up_to_t with t. apply leqnn.
unfold valid_schedule_up_to_t in VS.
destruct VS as [A B]. destruct B as [B C].
apply B. exact CBS. destruct K as [y K]. destruct K as [arr_bound scheduled].
unfold jobs_come_from_arrival_sequence in P1. apply P1 with y.
exact scheduled.
- intro pend. apply prefixed. 3: exact pend. 2: exact in_task.
unfold arrives_in. unfold arrives_in in in_arr_seq.
destruct in_arr_seq as [n P].
unfold jobs_arriving_at. unfold jobs_arriving_at in P.
unfold arr_seq_prefixed. exists n. destruct (n <= t) eqn: E.
+ exact P.
+ admit.
unfold pending in pend.
unfold has_arrived in pend.
unfold arrives_in. exists (job_arrival j).
unfold arr_seq_prefixed. unfold jobs_arriving_at.
apply tactics.vlib__andb_split in pend.
destruct pend as [arr_bound incompletion].
rewrite arr_bound.
unfold arrives_in in in_arr_seq. destruct in_arr_seq as [y P].
unfold valid_arrival_sequence_up_to_t in VAS. destruct VAS as [CAT ASU].
unfold consistent_arrival_times_up_to_t in CAT. unfold arrives_at in CAT.
assert (copyP: j \in arr_seq y). unfold jobs_arriving_at in P. exact P.
apply CAT in P. rewrite P. exact copyP. admit.
Admitted.
......
From rt.restructuring.behavior Require Export arrival_sequence.
From rt.util Require Import all.
(*
(* In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix.
......@@ -11,17 +11,6 @@ Section ArrivalSequencePrefix.
(* Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
(* By concatenation, we construct the list of jobs that arrived in the
interval [t1, t2). *)
Definition jobs_arrived_between (t1 t2 : instant) :=
\cat_(t1 <= t < t2) jobs_arriving_at arr_seq t.
(* Based on that, we define the list of jobs that arrived up to time t, ...*)
Definition jobs_arrived_up_to (t : instant) := jobs_arrived_between 0 t.+1.
(* ...and the list of jobs that arrived strictly before time t. *)
Definition jobs_arrived_before (t : instant) := jobs_arrived_between 0 t.
(* In this section, we prove some lemmas about arrival sequence prefixes. *)
Section Lemmas.
......@@ -30,42 +19,42 @@ Section ArrivalSequencePrefix.
(* First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma job_arrived_between_cat:
Lemma arrivals_between_cat:
forall t1 t t2,
t1 <= t ->
t <= t2 ->
jobs_arrived_between t1 t2 = jobs_arrived_between t1 t ++ jobs_arrived_between t t2.
arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
Proof.
unfold jobs_arrived_between; intros t1 t t2 GE LE.
unfold arrivals_between; intros t1 t t2 GE LE.
by rewrite (@big_cat_nat _ _ _ t).
Qed.
(* Second, the same observation applies to membership in the set of
arrived jobs. *)
Lemma jobs_arrived_between_mem_cat:
Lemma arrivals_between_mem_cat:
forall j t1 t t2,
t1 <= t ->
t <= t2 ->
j \in jobs_arrived_between t1 t2 =
(j \in jobs_arrived_between t1 t ++ jobs_arrived_between t t2).
j \in arrivals_between arr_seq t1 t2 =
(j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
Proof.
by intros j t1 t t2 GE LE; rewrite (job_arrived_between_cat _ t).
by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
Qed.
(* Third, we observe that we can grow the considered interval without
"losing" any arrived jobs, i.e., membership in the set of arrived jobs
is monotonic. *)
Lemma jobs_arrived_between_sub:
Lemma arrivals_between_sub:
forall j t1 t1' t2 t2',
t1' <= t1 ->
t2 <= t2' ->
j \in jobs_arrived_between t1 t2 ->
j \in jobs_arrived_between t1' t2'.
j \in arrivals_between arr_seq t1 t2 ->
j \in arrivals_between arr_seq t1' t2'.
Proof.
intros j t1 t1' t2 t2' GE1 LE2 IN.
move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
last by rewrite /jobs_arrived_between big_geq // in IN.
rewrite /jobs_arrived_between.
last by rewrite /arrivals_between big_geq // in IN.
rewrite /arrivals_between.
rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
rewrite mem_cat; apply/orP; right.
rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done].
......@@ -85,8 +74,8 @@ Section ArrivalSequencePrefix.
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
Lemma in_arrivals_implies_arrived:
forall j t1 t2,
j \in jobs_arrived_between t1 t2 ->
arrives_in arr_seq j.
j \in arrivals_between arr_seq t1 t2 ->
arrives_in arr_seq j.
Proof.
rename H_consistent_arrival_times into CONS.
intros j t1 t2 IN.
......@@ -100,7 +89,7 @@ Section ArrivalSequencePrefix.
t2. *)
Lemma in_arrivals_implies_arrived_between:
forall j t1 t2,
j \in jobs_arrived_between t1 t2 ->
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2.
Proof.
rename H_consistent_arrival_times into CONS.
......@@ -114,11 +103,10 @@ Section ArrivalSequencePrefix.
then it indeed arrives before time t. *)
Lemma in_arrivals_implies_arrived_before:
forall j t,
j \in jobs_arrived_before t ->
j \in arrivals_before arr_seq t ->
arrived_before j t.
Proof.
intros j t IN.
Fail suff: arrived_between j 0 t by rewrite /arrived_between /=.
have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
by rewrite /arrived_between /=.
Qed.
......@@ -129,7 +117,7 @@ Section ArrivalSequencePrefix.
forall j t1 t2,
arrives_in arr_seq j ->
arrived_between j t1 t2 ->
j \in jobs_arrived_between t1 t2.
j \in arrivals_between arr_seq t1 t2.
Proof.
rename H_consistent_arrival_times into CONS.
move => j t1 t2 [a_j ARRj] BEFORE.
......@@ -141,10 +129,10 @@ Section ArrivalSequencePrefix.
jobs, the same applies for any of its prefixes. *)
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq ->
forall t1 t2, uniq (jobs_arrived_between t1 t2).
forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
Proof.
rename H_consistent_arrival_times into CONS.
unfold jobs_arrived_up_to; intros SET t1 t2.
unfold arrivals_up_to; intros SET t1 t2.
apply bigcat_nat_uniq; first by done.
intros x t t' IN1 IN2.
by apply CONS in IN1; apply CONS in IN2; subst.
......@@ -155,3 +143,4 @@ Section ArrivalSequencePrefix.
End Lemmas.
End ArrivalSequencePrefix.
*)
\ No newline at end of file
From rt.restructuring.behavior Require Export schedule facts.arrivals facts.completion.
From rt.util Require Import bigcat.
From mathcomp Require Import seq.
From rt.restructuring.behavior Require Export arrival_sequence.
Section Schedule.
Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
Context {State : Type} `{ProcessorState Job State}.
Variable (arr_seq : arrival_sequence Job).
(* [next_state t candidate_jobs] should return the schedule state at time t given the list of pending jobs and their remaining cost *)
Variable next_state : instant -> seq (Job * duration) -> State.
Definition candidate_jobs (sched : schedule State) (t : instant) : seq (Job * nat):=
[seq (j, remaining_cost sched j t)
| j <- [seq j <- arrivals_before arr_seq t.+1
| ~~ completed_by sched j t]].
Hypothesis next_state_correct : forall t jobs j,
scheduled_in j (next_state t jobs) -> j \in map fst jobs.
Hypothesis next_state_service : forall t jobs j c,
(j, c) \in jobs -> service_in j (next_state t jobs) <= c.
Lemma next_state_remaining_cost sched j t :
service_in j (next_state t (candidate_jobs sched t)) <= remaining_cost sched j t.
Proof.
case:(boolP (scheduled_in j (next_state t (candidate_jobs sched t)))).
{ move=>/next_state_correct.
rewrite -map_comp map_id=>Hj.
apply: next_state_service.
by rewrite mem_map=>[|j1 j2 []->//]. }
{ move=>/negbTE Hj.
by rewrite service_implies_scheduled. }
Qed.
Hypothesis Harr_seq : valid_arrival_sequence arr_seq.
Lemma candidate_jobsP sched j t :
reflect (arrives_in arr_seq j /\ pending sched j t) (j \in map fst (candidate_jobs sched t)).
Proof.
rewrite -map_comp/=map_id.
rewrite mem_filter.
apply:(iffP idP)=>[/andP[Hnot_comp Harrj]|[[tj Htj] /andP[Harrivalj ->/=]]].
{ split; first (apply: in_arrivals_implies_arrived; exact: Harrj).
rewrite /pending /has_arrived Hnot_comp andbT.
rewrite -ltnS.
apply: in_arrivals_implies_arrived_before; [|exact: Harrj].
by move:Harr_seq=>[]. }
{ apply: mem_bigcat_nat.
- rewrite /= ltnS.
exact: Harrivalj.
- by move: Harr_seq=>[/(_ j tj) ->]. }
Qed.
Section ScheduleCompletion.
Variable sched : schedule State.
Variable t_start : instant.
(* Given [sched] which is valid before [t_start], [complete_schedule_helper sched t_start d] is valid up to [t_start + d] *)
Fixpoint complete_schedule_helper (d : duration)
: schedule State :=
let sched' := if d is d.+1 then complete_schedule_helper d else sched in
fun t => if t == t_start + d then
next_state t (candidate_jobs sched' t)
else
sched' t.
Lemma complete_schedule_helper_prefix d t :
t < t_start ->
complete_schedule_helper d t = sched t.
Proof.
move=> Ht.
have{Ht} ineq: forall x, t == t_start + x = false
by move=>x; apply/negbTE; rewrite neq_ltn (leq_trans Ht) ?leq_addr.
elim: d=>[|d IH]; by rewrite /complete_schedule_helper ?IH ineq.
Qed.
Lemma complete_schedule_helper_preserves_prefix d t :
t - t_start <= d ->
complete_schedule_helper d t = complete_schedule_helper (t - t_start) t.
Proof.
elim: d=>[|d IH]; first by rewrite leqn0=>/eqP->.
rewrite leq_eqVlt ltnS =>/orP[/eqP->//|ineq].
rewrite -(IH ineq)/=.
suff/negbTE->: t != t_start + d.+1 by [].
by rewrite neq_ltn addnC addSn ltnS addnC -leq_subLR ineq.
Qed.
Definition complete_schedule : schedule State :=
fun t => complete_schedule_helper (t - t_start) t.
Lemma complete_schedule_prefix t :
t < t_start ->
complete_schedule t = sched t.
Proof.
exact: complete_schedule_helper_prefix.
Qed.
Lemma complete_schedule_prefix_service j :
service sched j t_start = service complete_schedule j t_start.
Proof.
apply: eq_big_nat=>t/= Ht.
by rewrite /service_at complete_schedule_prefix.
Qed.
Lemma complete_schedule_construction t :
t_start <= t ->
complete_schedule t =
next_state t (candidate_jobs complete_schedule t).
Proof.
move=>/subnK<-.
elim: (t - t_start) =>[|d IH]{t}/=.
{ rewrite add0n {1}/complete_schedule subnn/= addn0 eqxx.
f_equal.
rewrite /candidate_jobs.
set s1 := filter _ _.
set s2 := filter _ _.
have->: s1 = s2
by apply: eq_filter=>j; rewrite /completed_by complete_schedule_prefix_service.
apply: eq_map=>j.
by rewrite /remaining_cost complete_schedule_prefix_service. }
{ rewrite {1}/complete_schedule addnK/= addnC eqxx.
f_equal.
rewrite /candidate_jobs.
set s1 := filter _ _.
set s2 := filter _ _.
have->: s1 = s2.
{ apply: eq_filter=>j.
rewrite /completed_by.
do 2!f_equal.
rewrite addnC addSn.
apply: eq_big_nat=>t/=.
by rewrite ltnS/service_at addnC -leq_subLR=>/complete_schedule_helper_preserves_prefix->. }
apply: eq_map=>j.
rewrite /remaining_cost.
do 2!f_equal.
rewrite addnC addSn.
apply: eq_big_nat=>t/=.
by rewrite ltnS/service_at addnC -leq_subLR=>/complete_schedule_helper_preserves_prefix->. }
Qed.
Section Lemmas.
Hypothesis Hsched1 : forall j t, t < t_start -> scheduled_at sched j t -> arrives_in arr_seq j.
Hypothesis Hsched2 : forall j t, t < t_start -> scheduled_at sched j t -> has_arrived j t.
Hypothesis Hsched3 : forall j t, t <= t_start -> service sched j t <= job_cost j.
Lemma complete_schedule_valid : valid_schedule complete_schedule arr_seq.
Proof.
repeat split.
{ move=> j t.
rewrite /scheduled_at.
case: (ltnP t t_start)=> Ht.
- by move:(Ht)=>/complete_schedule_prefix->/(Hsched1 _ _ Ht).
- by rewrite complete_schedule_construction// =>/next_state_correct/candidate_jobsP[]. }
{ move=> j t.
rewrite /scheduled_at.
case: (ltnP t t_start)=> Ht; first by move: (Ht)=>/complete_schedule_prefix->/(Hsched2 _ _ Ht).
by rewrite complete_schedule_construction// =>
/next_state_correct/candidate_jobsP[_[/andP[]]]. }
{ move=> j.
elim=>[|t IH]; first by rewrite service0.
case: (ltnP t t_start)=> Ht.
- apply: leq_trans; last exact: (Hsched3 j t.+1).
apply: sum.leq_sum_nat => t0/= Ht0 _.
by rewrite /service_at complete_schedule_prefix// (leq_trans Ht0 Ht).
- rewrite -service_last_plus_before/service_at complete_schedule_construction//.
move/subnK in IH.
rewrite -IH addnC leq_add//.
exact: next_state_remaining_cost. }
Qed.
End Lemmas.
End ScheduleCompletion.
Variable default_state : State.
Definition build_schedule : schedule State := complete_schedule (fun t => default_state) 0.
Lemma build_schedule_valid : valid_schedule build_schedule arr_seq.
Proof.
apply: complete_schedule_valid=>// j t.
rewrite leqn0=>/eqP->.
by rewrite service0.
Qed.
End Schedule.
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