Commits (16)
......@@ -328,10 +328,10 @@ Section Sequential_Abstract_RTA.
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
/service_of_jobs.service_of_jobs_at/= scheduled_at_def.
rewrite !H_idle/=.
rewrite big1_eq addn0 add0n.
erewrite eq_bigr; last by move => i j' /=; rewrite service_at_def H_idle /=.
rewrite /= big1_eq add0n H_idle addn0.
case INT: (interference j t); last by done.
simpl; rewrite lt0b.
rewrite /= lt0b.
apply/hasP; exists j; last by done.
by rewrite mem_filter; apply/andP; split;
[rewrite H_job_of_tsk | eapply arrived_between_implies_in_arrivals; eassumption].
......@@ -360,18 +360,20 @@ Section Sequential_Abstract_RTA.
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
/task_scheduled_at /task_schedule.task_scheduled_at /service_of_jobs_at
/service_of_jobs.service_of_jobs_at scheduled_at_def/=.
have ARRs: arrives_in arr_seq j'; first by apply H_jobs_come_from_arrival_sequence with t; rewrite scheduled_at_def; apply/eqP.
rewrite H_sched H_not_job_of_tsk; simpl.
have ARRs: arrives_in arr_seq j';
first by apply H_jobs_come_from_arrival_sequence with t; rewrite scheduled_at_def; apply/eqP.
rewrite H_sched H_not_job_of_tsk /=.
rewrite (negbTE (option_inj_neq (neqprop_to_neqbool
(diseq (fun j => job_task j = tsk) _ _
(neqbool_to_neqprop H_not_job_of_tsk) H_job_of_tsk)))) addn0.
erewrite eq_bigr; last by move=> i _; rewrite service_at_def H_sched.
have ZERO: \sum_(i <- arrivals_between t1 (t1 + A + ε) | job_task i == tsk) (Some j' == Some i) = 0.
{ apply big1; move => j2 /eqP TSK2; apply/eqP; rewrite eqb0.
apply option_inj_neq, neqprop_to_neqbool, (diseq (fun j => job_task j = tsk) _ _
(neqbool_to_neqprop H_not_job_of_tsk) TSK2).
} rewrite ZERO ?addn0 add0n; simpl; clear ZERO.
} rewrite {}ZERO ?addn0 add0n /=.
case INT: (interference j t); last by done.
simpl; rewrite lt0b.
rewrite /= lt0b.
apply/hasP; exists j; last by done.
by rewrite mem_filter; apply/andP; split;
[rewrite H_job_of_tsk | eapply arrived_between_implies_in_arrivals; eassumption].
......@@ -413,7 +415,8 @@ Section Sequential_Abstract_RTA.
by rewrite H_sched [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) in CONTR.
}
rewrite big_mkcond; apply/sum_seq_gt0P; exists j'; split; last first.
{ by move: H_not_job_of_tsk => /eqP TSK; rewrite /job_of_task TSK eq_refl eq_refl. }
{ move: H_not_job_of_tsk => /eqP TSK.
by rewrite /job_of_task TSK eq_refl service_at_def H_sched eq_refl. }
{ intros. have ARR:= arrives_after_beginning_of_busy_interval j j' _ _ _ _ _ t1 t2 _ t.
feed_n 8 ARR; try (done || by move: H_t_in_interval => /andP [T1 T2]).
{ by move: H_not_job_of_tsk => /eqP TSK; rewrite TSK. }
......@@ -469,7 +472,8 @@ Section Sequential_Abstract_RTA.
feed ZIJT; first by rewrite scheduled_at_def H_sched; simpl.
move: ZIJT => /negP /eqP; rewrite eqb_negLR; simpl; move => /eqP ZIJT; rewrite ZIJT; simpl; rewrite add0n.
rewrite !eq_refl; simpl; rewrite big_mkcond //=; apply/sum_seq_gt0P.
by exists j; split; [apply j_is_in_arrivals_between | rewrite /job_of_task H_job_of_tsk H_sched !eq_refl].
exists j; split; first by apply j_is_in_arrivals_between.
by rewrite /job_of_task H_job_of_tsk service_at_def H_sched !eq_refl.
Qed.
End Case4.
......@@ -514,12 +518,12 @@ Section Sequential_Abstract_RTA.
/service_of_jobs exchange_big //=.
rewrite -(leq_add2r (\sum_(t1 <= t < (t1 + x)) service_at sched j t)).
rewrite [X in _ <= X]addnC addnA subnKC; last first.
{ rewrite exchange_big //= (big_rem j) //=; auto using j_is_in_arrivals_between.
by rewrite /job_of_task H_job_of_tsk eq_refl leq_addr. }
{ rewrite (exchange_big _ _ (arrivals_between _ _)) /= (big_rem j) //=.
by rewrite /job_of_task H_job_of_tsk eq_refl leq_addr. }
rewrite -big_split -big_split //=.
rewrite big_nat_cond [X in _ <= X]big_nat_cond leq_sum //; move => t /andP [NEQ _].
rewrite -scheduled_at_def.
by apply interference_plus_sched_le_serv_of_task_plus_task_interference.
rewrite {1}service_at_def -scheduled_at_def.
by apply interference_plus_sched_le_serv_of_task_plus_task_interference.
Qed.
(** On the other hand, the service terms in the inequality
......
......@@ -350,7 +350,7 @@ Section JLFPInstantiation.
{ ideal_proc_model_sched_case_analysis_eq sched x jo; first by done.
move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
destruct (another_hep_job jo j) eqn:PRIO; last by done.
rewrite (big_rem jo) //=; first by rewrite PRIO eq_refl.
rewrite (big_rem jo) /=; first by rewrite PRIO service_at_def EQ eq_refl.
apply arrived_between_implies_in_arrivals; try done.
- by apply H_jobs_come_from_arrival_sequence with x.
- rewrite /arrived_between; apply/andP; split.
......@@ -364,12 +364,14 @@ Section JLFPInstantiation.
eapply H_jobs_come_from_arrival_sequence; eauto.
+ by apply leq_ltn_trans with x; [apply H_jobs_must_arrive_to_execute | done].
}
{ ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
{ erewrite eq_bigr; last by move=> i _; rewrite service_at_def /=.
ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
destruct (another_hep_job jo j) eqn:PRIO.
- rewrite -EQ. have SCH := service_of_jobs_le_1 sched _ (arrivals_between t1 t) _ x.
eapply leq_trans; last by apply SCH; eauto using arrivals_uniq.
erewrite leq_sum; eauto 2.
move=> i _. by rewrite service_at_def.
- rewrite leqn0 big1 //; intros joo PRIO2.
apply/eqP; rewrite eqb0; apply/eqP; intros C.
inversion C; subst joo; clear C.
......@@ -391,7 +393,7 @@ Section JLFPInstantiation.
{ ideal_proc_model_sched_case_analysis_eq sched x jo; first by done.
move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
destruct (hep_job_from_another_task jo j) eqn:PRIO; last by done.
rewrite (big_rem jo) //=; first by rewrite PRIO eq_refl.
rewrite (big_rem jo) /=; first by rewrite PRIO service_at_def EQ eq_refl.
apply arrived_between_implies_in_arrivals; try done.
- by apply H_jobs_come_from_arrival_sequence with x.
- rewrite /arrived_between; apply/andP; split.
......@@ -402,15 +404,17 @@ Section JLFPInstantiation.
apply completed_implies_not_scheduled; eauto.
apply completion_monotonic with t1; try done.
apply H_quiet_time; try done.
eapply H_jobs_come_from_arrival_sequence; simpl; eauto.
by eapply H_jobs_come_from_arrival_sequence; eauto.
+ by apply leq_ltn_trans with x; [apply H_jobs_must_arrive_to_execute | done].
}
{ ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
{ erewrite eq_bigr; last by move=> i _; rewrite service_at_def /=.
ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
destruct (hep_job_from_another_task jo j) eqn:PRIO.
- rewrite -EQ. have SCH := service_of_jobs_le_1 sched _ (arrivals_between t1 t) _ x.
eapply leq_trans; last by apply SCH; eauto using arrivals_uniq.
erewrite leq_sum; eauto 2.
move=> i _. by rewrite service_at_def.
- rewrite leqn0 big1 //; intros joo PRIO2.
apply/eqP; rewrite eqb0; apply/eqP; intros C.
inversion C; subst joo; clear C.
......
......@@ -245,13 +245,28 @@ Section RelationToScheduled.
Variable j: Job.
(** We observe that a job that isn't scheduled cannot possibly receive service. *)
Lemma service_in_implies_scheduled_in : forall s,
~~ scheduled_in j s -> service_in j s = 0.
Proof.
move=> s /existsP Hsched.
rewrite /service_in.
apply/eqP.
rewrite sum_nat_eq0.
apply/forallP => c /=.
rewrite service_on_implies_scheduled_on => //.
apply/negP => Hsch.
apply: Hsched.
by exists c.
Qed.
(** In particular, it cannot receive service at any given time. *)
Lemma not_scheduled_implies_no_service:
forall t,
~~ scheduled_at sched j t -> service_at sched j t = 0.
Proof.
rewrite /service_at /scheduled_at.
move=> t NOT_SCHED.
rewrite service_implies_scheduled //.
by rewrite service_in_implies_scheduled_in.
Qed.
(** Conversely, if a job receives service, then it must be scheduled. *)
......@@ -261,7 +276,7 @@ Section RelationToScheduled.
Proof.
move=> t.
destruct (scheduled_at sched j t) eqn:SCHEDULED; first trivial.
rewrite not_scheduled_implies_no_service // negbT //.
by rewrite not_scheduled_implies_no_service // negbT.
Qed.
(** Thus, if the cumulative amount of service changes, then it must be
......@@ -272,7 +287,7 @@ Section RelationToScheduled.
Proof.
move => t.
rewrite -service_last_plus_before -{1}(addn0 (service sched j t)) ltn_add2l.
apply: service_at_implies_scheduled_at.
by apply: service_at_implies_scheduled_at.
Qed.
(** We observe that a job receives cumulative service during some interval iff
......@@ -299,7 +314,7 @@ Section RelationToScheduled.
rewrite andbT; move => /andP [GT LT].
specialize (ALL (Ordinal LT)); simpl in ALL.
rewrite GT andTb -eqn0Ngt in ALL.
apply /eqP => //.
by apply /eqP.
}
{
move=> [t [TT SERVICE]].
......@@ -356,9 +371,9 @@ Section RelationToScheduled.
Proof.
move=> t. rewrite /scheduled_at /service_at.
split => [NOT_SCHED | NO_SERVICE].
- by rewrite service_implies_scheduled //.
- by rewrite service_in_implies_scheduled_in.
- apply (contra (H_scheduled_implies_serviced j (sched t))).
by rewrite -eqn0Ngt; apply /eqP => //.
by rewrite -eqn0Ngt; apply /eqP.
Qed.
(** Then, if a job does not receive any service during an interval, it
......@@ -373,7 +388,7 @@ Section RelationToScheduled.
rewrite no_service_not_scheduled.
move: ZERO_SUM.
rewrite /service_during big_nat_eq0 => IS_ZERO.
by apply (IS_ZERO t); apply /andP; split => //.
by apply (IS_ZERO t); apply/andP.
Qed.
(** Conversely, if a job is not scheduled during an interval, then
......@@ -414,7 +429,7 @@ Section RelationToScheduled.
Proof.
move=> t [t' [TT SCHED]].
rewrite /service. apply scheduled_implies_cumulative_service.
exists t'; split => //.
by exists t'.
Qed.
End GuaranteedService.
......@@ -442,7 +457,7 @@ Section RelationToScheduled.
exists t''; split; last by assumption.
rewrite /(_ && _) ifT //.
move: H_jobs_must_arrive. rewrite /jobs_must_arrive_to_execute /has_arrived => ARR.
by apply: ARR; exact.
by apply: ARR.
Qed.
Lemma not_scheduled_before_arrival:
......@@ -450,7 +465,7 @@ Section RelationToScheduled.
Proof.
move=> t EARLY.
apply: (contra (H_jobs_must_arrive j t)).
rewrite /has_arrived -ltnNge //.
by rewrite /has_arrived -ltnNge.
Qed.
(** We show that job [j] does not receive service at any time [t] prior to its
......@@ -461,7 +476,7 @@ Section RelationToScheduled.
service_at sched j t = 0.
Proof.
move=> t NOT_ARR.
rewrite not_scheduled_implies_no_service // not_scheduled_before_arrival //.
by rewrite not_scheduled_implies_no_service // not_scheduled_before_arrival.
Qed.
(** Note that the same property applies to the cumulative service. *)
......@@ -477,7 +492,7 @@ Section RelationToScheduled.
rewrite big_nat_cond [in RHS]big_nat_cond.
apply: eq_bigr => i /andP [TIMES _]. move: TIMES => /andP [le_t1_i lt_i_t2].
apply (service_before_job_arrival_zero i).
by apply leq_trans with (n := t2); auto.
by apply leq_trans with (n := t2).
Qed.
(** Hence, one can ignore the service received by a job before its arrival
......@@ -491,7 +506,7 @@ Section RelationToScheduled.
move=> t1 t2 le_t1 le_t2.
rewrite -(service_during_cat sched j t1 (job_arrival j) t2).
rewrite cumulative_service_before_job_arrival_zero //.
by apply/andP; split; exact.
by apply/andP.
Qed.
(** ... which we can also state in terms of cumulative service. *)
......@@ -500,7 +515,7 @@ Section RelationToScheduled.
t <= job_arrival j -> service sched j t = 0.
Proof.
move=> t EARLY.
rewrite /service cumulative_service_before_job_arrival_zero //.
by rewrite /service cumulative_service_before_job_arrival_zero.
Qed.
End AfterArrival.
......@@ -525,7 +540,7 @@ Section RelationToScheduled.
Proof.
move: H_same_service.
rewrite -(service_cat sched j t1 t2) // -[service sched j t1 in LHS]addn0 => /eqP.
by rewrite eqn_add2l => /eqP //.
by rewrite eqn_add2l => /eqP.
Qed.
(** ...which of course implies that it does not receive service at any
......@@ -537,7 +552,8 @@ Section RelationToScheduled.
move=> t /andP [GE_t1 LT_t2].
move: constant_service_implies_no_service_during.
rewrite /service_during big_nat_eq0 => IS_ZERO.
apply IS_ZERO. apply /andP; split => //.
apply IS_ZERO.
by apply /andP.
Qed.
(** We show that job [j] receives service at some point [t < t1]
......@@ -585,7 +601,7 @@ Section RelationToScheduled.
- by apply service_at_implies_scheduled_at.
}
rewrite !CONV.
apply same_service_implies_serviced_at_earlier_times.
by apply same_service_implies_serviced_at_earlier_times.
Qed.
End TimesWithSameService.
......
......@@ -280,7 +280,8 @@ Section ExistsBusyIntervalJLFP.
move => t' /andP [_ NEQ]; rewrite mem_iota in NEQ.
rewrite big1_seq //.
move => jhp /andP [HP ARR].
apply/eqP; rewrite eqb0. rewrite -scheduled_at_def.
apply/eqP.
rewrite service_at_def eqb0 -scheduled_at_def.
apply (completed_implies_not_scheduled _ _ H_completed_jobs_dont_execute).
apply completion_monotonic with t1; [ move: NEQ => /andP [T1 _] | ]; try done.
apply H_quiet_time; try done.
......@@ -329,7 +330,7 @@ Section ExistsBusyIntervalJLFP.
apply/andP; split; first by done.
apply H_jobs_must_arrive_to_execute in Sched_jo.
by apply leq_ltn_trans with t'.
- by rewrite lt0b -scheduled_at_def.
- by rewrite service_at_def lt0b -scheduled_at_def.
}
}
Qed.
......@@ -479,16 +480,18 @@ Section ExistsBusyIntervalJLFP.
apply leq_sum_seq; move => t II _.
rewrite mem_index_iota in II; move: II => /andP [GEi LEt].
case SCHED: (sched t) => [j1 | ]; simpl; first last.
{ rewrite leqn0 big1_seq //. }
{ case PRIO1: (hep_job j1 j); simpl; first last.
- rewrite <- SCHED.
have SCH := service_of_jobs_le_1 sched _ _ _ t; eauto using arrivals_uniq.
{ rewrite leqn0 big1_seq // /service_at => i Hi.
by rewrite service_in_def SCHED. }
{ case PRIO1: (hep_job j1 j) => /=; first last.
- by have SCH := service_of_jobs_le_1 sched _ _ _ t; eauto using arrivals_uniq.
- rewrite leqn0 big1_seq; first by done.
move => j2 /andP [PRIO2 ARRj2].
case EQ: (j1 == j2).
+ by move: EQ => /eqP EQ; subst j2; rewrite PRIO1 in PRIO2.
+ apply/eqP; rewrite eqb0; apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
by inversion CONTR; clear CONTR; subst j2; rewrite PRIO1 in PRIO2. } } }
+ apply/eqP.
rewrite service_at_def eqb0.
apply/negP => /eqP CONTR. rewrite SCHED in CONTR.
by inversion CONTR; subst j2; rewrite PRIO1 in PRIO2. } } }
{ rewrite leq_add2r.
destruct (t1 + delta <= t_busy.+1) eqn:NEQ; [ | apply negbT in NEQ; rewrite -ltnNge in NEQ].
- apply leq_trans with (cumulative_priority_inversion sched j t1 t_busy.+1); last eauto 2.
......
......@@ -713,7 +713,8 @@ Section PriorityInversionIsBounded.
+ rewrite big_nat_cond [in X in _ <= X]big_nat_cond.
rewrite leq_sum //.
move => x /andP [HYP _].
by rewrite lt0b -scheduled_at_def; apply continuously_scheduled_between_preemption_points.
rewrite service_at_def lt0b -scheduled_at_def.
by apply continuously_scheduled_between_preemption_points.
} by done.
- case: (posnP fpt) => [ZERO|POS].
{ subst fpt.
......
......@@ -11,11 +11,11 @@ Require Import prosa.model.processor.ideal.
(** In this section we establish the classes to which an ideal schedule belongs. *)
Section ScheduleClass.
Local Transparent service_in scheduled_in scheduled_on.
Local Transparent scheduled_in scheduled_on.
(** Consider any job type and the ideal processor model. *)
Context {Job: JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobCost Job}.
(** We note that the ideal processor model is indeed a uni-processor
model. *)
......@@ -23,7 +23,21 @@ Section ScheduleClass.
uniprocessor_model (processor_state Job).
Proof.
move=> j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
by move: E1 E2=>->[].
by move: E1 E2 =>->[].
Qed.
(** As there is only one processor, the sum in the definition of [service_in]
collapses to only one term. *)
Lemma service_in_service_on (j : Job) s :
service_in j s = service_on j s tt.
Proof.
by rewrite /service_in /index_enum Finite.EnumDef.enumDef /= big_seq1.
Qed.
Lemma service_in_def (j : Job) (s : processor_state Job) :
service_in j s = (s == Some j).
Proof.
by rewrite service_in_service_on.
Qed.
(** We observe that the ideal processor model falls into the category
......@@ -32,8 +46,8 @@ Section ScheduleClass.
Lemma ideal_proc_model_ensures_ideal_progress:
ideal_progress_proc_model (processor_state Job).
Proof.
move=> j s /existsP[[]/eqP->]/=.
by rewrite eqxx.
move=> j s /existsP[[]/eqP->] /=.
by rewrite service_in_def /= eqxx /nat_of_bool.
Qed.
(** The ideal processor model is a unit-service model. *)
......@@ -41,7 +55,7 @@ Section ScheduleClass.
unit_service_proc_model (processor_state Job).
Proof.
move=> j s.
rewrite /service_in/=/nat_of_bool.
rewrite service_in_def /= /nat_of_bool.
by case:ifP.
Qed.
......@@ -51,7 +65,7 @@ Section ScheduleClass.
rewrite /scheduled_in/scheduled_on/=.
case: existsP=>[[_->]//|].
case: (s == Some j)=>//=[[]].
by exists.
by exists.
Qed.
Lemma scheduled_at_def sched (j : Job) t :
......@@ -63,7 +77,7 @@ Section ScheduleClass.
Lemma service_in_is_scheduled_in (j : Job) s :
service_in j s = scheduled_in j s.
Proof.
by rewrite /service_in scheduled_in_def/=.
by rewrite service_in_def scheduled_in_def.
Qed.
Lemma service_at_is_scheduled_at sched (j : Job) t :
......@@ -71,19 +85,31 @@ Section ScheduleClass.
Proof.
by rewrite /service_at service_in_is_scheduled_in.
Qed.
Lemma service_on_def (j : Job) (s : processor_state Job) c :
service_on j s c = (s == Some j).
Proof.
done.
Qed.
Lemma service_at_def sched (j : Job) t :
service_at sched j t = (sched t == Some j).
Proof.
by rewrite /service_at service_in_def.
Qed.
(** Next we prove a lemma which helps us to do a case analysis on
the state of an ideal schedule. *)
Lemma ideal_proc_model_sched_case_analysis:
forall (sched : schedule (ideal.processor_state Job)) (t : instant),
is_idle sched t \/ exists j, scheduled_at sched j t.
is_idle sched t \/ exists j, scheduled_at sched j t.
Proof.
intros.
unfold is_idle; simpl; destruct (sched t) eqn:EQ.
- by right; exists s; auto; rewrite scheduled_at_def EQ.
- by left; auto.
Qed.
End ScheduleClass.
(** * Incremental Service in Ideal Schedule *)
......@@ -100,7 +126,7 @@ Section IncrementalService.
Variable arr_seq : arrival_sequence Job.
(** ... and any ideal uni-processor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
Variable sched : schedule (ideal.processor_state Job).
(** As a base case, we prove that if a job j receives service in
some time interval <<[t1,t2)>>, then there exists a time instant t
......@@ -108,7 +134,7 @@ Section IncrementalService.
instant where j receives service. *)
Lemma positive_service_during:
forall j t1 t2,
0 < service_during sched j t1 t2 ->
0 < service_during sched j t1 t2 ->
exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0.
Proof.
intros j t1 t2 SERV.
......@@ -121,11 +147,12 @@ Section IncrementalService.
- apply/andP; split; first by done.
rewrite ltnNge; apply/negP; intros CONTR.
by move: SERV; rewrite/service_during big_geq.
- by rewrite /service_during big_geq.
}
- by rewrite /service_during big_geq.
}
{ apply negbT in SCHED.
move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [t [IN SCHEDt]].
rewrite lt0b in SCHEDt.
move: SERV.
rewrite /service_during => /sum_seq_gt0P [t [IN SCHEDt]].
rewrite service_at_def /= lt0b in SCHEDt.
rewrite mem_iota subnKC in IN; last by done.
move: IN => /andP [IN1 IN2].
move: (exists_first_intermediate_point
......@@ -134,13 +161,27 @@ Section IncrementalService.
move: A => [x [/andP [T1 T4] [T2 T3]]].
exists x; repeat split; try done.
- apply/andP; split; first by apply ltnW.
by apply leq_ltn_trans with t.
by apply leq_ltn_trans with t.
- apply/eqP; rewrite big_nat_cond big1 //.
move => y /andP [T5 _].
by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
apply/eqP.
rewrite service_at_def /= eqb0.
by specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
}
Qed.
Lemma service_during_ge :
forall j t1 t2 k,
service_during sched j t1 t2 > k ->
t1 < t2.
Proof.
move=> j t1 t2 k SERV.
rewrite leqNgt.
apply/negP => CONTR.
move: SERV.
by rewrite /service_during big_geq.
Qed.
(** Next, we prove that if in some time interval <<[t1,t2)>> a job j
receives k units of service, then there exists a time instant t ∈
[t1,t2) such that j is scheduled at time t and service of job j
......@@ -150,51 +191,51 @@ Section IncrementalService.
service_during sched j t1 t2 > k ->
exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.
Proof.
intros j t1 t2 k SERV.
have LE: t1 <= t2.
{ rewrite leqNgt; apply/negP; intros CONTR.
by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.
}
move=> j t1 t2 k SERV.
have LE: t1 < t2 by move: (service_during_ge _ _ _ _ SERV).
induction k; first by apply positive_service_during in SERV.
feed IHk; first by apply ltn_trans with k.+1.
move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].
have SERVk1: service_during sched j t1 t.+1 = k.+1.
{ rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.
rewrite SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.
by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=.
}
rewrite /service_during big_nat1 service_at_def /=.
by rewrite eqb1 -scheduled_at_def /=.
}
move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.
{ by apply/andP; split; first apply leq_trans with t. }
rewrite SERVk1 -addn1 leq_add2l; move => SERV.
destruct (scheduled_at sched j t.+1) eqn:SCHED.
- exists t.+1; repeat split; try done. apply/andP; split.
+ apply leq_trans with t; by done.
+ apply leq_trans with t; by done.
+ rewrite ltnNge; apply/negP; intros CONTR.
by move: SERV; rewrite /service_during big_geq.
- apply negbT in SCHED.
move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [x [INx SCHEDx]].
rewrite lt0b in SCHEDx.
rewrite service_at_def lt0b in SCHEDx.
rewrite mem_iota subnKC in INx; last by done.
move: INx => /andP [INx1 INx2].
move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A.
feed A; first by rewrite scheduled_at_def/=.
move: A => [y [/andP [T1 T4] [T2 T3]]].
exists y; repeat split; try done.
exists y; repeat split => //.
+ apply/andP; split.
apply leq_trans with t; first by done.
apply leq_trans with t; first by done.
apply ltnW, ltn_trans with t.+1; by done.
by apply leq_ltn_trans with x.
by apply leq_ltn_trans with x.
+ rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].
unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.
rewrite -{2}[k.+1]addn0 eqn_add2l.
rewrite big_nat_cond big1 //; move => z /andP [H5 _].
by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
apply/eqP.
rewrite service_at_def eqb0.
by specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
Qed.
End IncrementalService.
(** * Automation *)
(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically. *)
Hint Resolve ideal_proc_model_is_a_uniprocessor_model
ideal_proc_model_ensures_ideal_progress
......@@ -202,20 +243,20 @@ Hint Resolve ideal_proc_model_is_a_uniprocessor_model
(** We also provide tactics for case analysis on ideal processor state. *)
(** The first tactic generates two sub-goals: one with idle processor and
(** The first tactic generates two sub-goals: one with idle processor and
the other with processor executing a job named [JobName]. *)
Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
let Idle := fresh "Idle" in
let Sched := fresh "Sched_" JobName in
destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].
(** The second tactic is similar to the first, but it additionally generates
(** The second tactic is similar to the first, but it additionally generates
two equalities: [sched t = None] and [sched t = Some j]. *)
Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
let Idle := fresh "Idle" in
let IdleEq := fresh "Eq" Idle in
let Sched := fresh "Sched_" JobName in
let Sched := fresh "Sched_" JobName in
let SchedEq := fresh "Eq" Sched in
destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
[move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
| move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
\ No newline at end of file
| move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
......@@ -185,7 +185,9 @@ Section IdealModelLemmas.
eapply arrived_between_implies_in_arrivals; eauto 2.
by apply H_jobs_must_arrive_to_execute in SCHED; apply leq_ltn_trans with x.
}
by move: L; simpl;rewrite eqb0; move => /eqP EQ.
move: SCHED L => /=.
rewrite scheduled_at_def service_at_def => /eqP-> /eqP.
by rewrite eqxx.
Qed.
(** In this section, we prove that the service received by any set of jobs
......@@ -205,13 +207,13 @@ Section IdealModelLemmas.
intros t.
case SCHED: (sched t) => [j | ]; simpl.
{ case ARR: (j \in jobs).
{ rewrite (big_rem j) //=; simpl.
rewrite /service_at /scheduled_at SCHED; simpl.
{ rewrite (big_rem j) //=.
rewrite /service_at /scheduled_at SCHED /=.
rewrite -[1]addn0 leq_add //.
- by rewrite eq_refl; case (P j).
- by rewrite service_in_def /= eq_refl; case (P j).
- rewrite leqn0 big1_seq; first by done.
move => j' /andP [_ ARRj'].
apply/eqP; rewrite eqb0.
apply/eqP. rewrite service_in_def eqb0.
apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
inversion CONTR; subst j'; clear CONTR.
rewrite rem_filter in ARRj'; last by done.
......@@ -221,8 +223,8 @@ Section IdealModelLemmas.
{ apply leq_trans with 0; last by done.
rewrite leqn0 big1_seq; first by done.
move => j' /andP [_ ARRj'].
apply/eqP; rewrite eqb0.
rewrite /scheduled_at SCHED.
apply/eqP.
rewrite service_at_def eqb0 SCHED.
apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
inversion CONTR; clear CONTR.
by subst j'; rewrite ARR in ARRj'.
......@@ -231,7 +233,7 @@ Section IdealModelLemmas.
{ apply leq_trans with 0; last by done.
rewrite leqn0 big1_seq; first by done.
move => j' /andP [_ ARRj'].
by rewrite /service_at /scheduled_at SCHED.
by rewrite service_at_def SCHED.
}
Qed.
......
......@@ -215,7 +215,7 @@ Section ModelWithLimitedPreemptions.
rewrite big_nat_recr //=.
rewrite eqn_add2l eq_sym.
rewrite scheduled_at_def in NSCHED.
by rewrite eqb0. }
by rewrite service_at_def eqb0. }
rewrite -[job_preemptable _ _]Bool.negb_involutive.
apply/negP; intros CONTR.
move: NSCHED => /negP NSCHED; apply: NSCHED.
......
......@@ -63,7 +63,7 @@ Section FullyNonPreemptiveModel.
* by rewrite /service /service_during big_nat_recr //= leq_addr.
* rewrite -addn1; apply leq_trans with (service sched j t.+2).
have <-: (service_at sched j t.+1) = 1.
{ by apply/eqP; rewrite eqb1 -scheduled_at_def. }
{ by apply/eqP; rewrite service_at_def eqb1 -scheduled_at_def. }
by rewrite -big_nat_recr //=.
by apply completion.service_at_most_cost; eauto 2 with basic_facts.
Qed.
......
......@@ -104,7 +104,7 @@ Section ReplaceAtFacts.
move=> NOT_IN_NEW NOT_IN_OLD t.
rewrite /service_at.
case: (boolP (t == t')) => /eqP TT.
- rewrite !TT !service_implies_scheduled //; by apply negbTE.
- by rewrite !TT !service_in_implies_scheduled_in //; apply negbTE.
- rewrite rest_of_schedule_invariant//.
Qed.
......
......@@ -32,19 +32,34 @@ Class ProcessorState (Job : JobType) (State : Type) :=
(** For a given processor state and core, the [scheduled_on] predicate
checks whether a given job is running on the given core. *)
scheduled_on : Job -> State -> Core -> bool;
(** For a given processor state, the [scheduled_in] predicate checks
whether a given job is running on any core in that state. *)
scheduled_in (j : Job) (s : State) : bool :=
[exists c : Core, scheduled_on j s c];
(** For a given processor state, the [service_in] function determines how
much service a given job receives in that state (across all cores). *)
service_in : Job -> State -> work;
(** For a given processor state, a job does not receive service if it is
not scheduled in that state *)
service_implies_scheduled :
forall j s, ~~ scheduled_in j s -> service_in j s = 0
(** For a given processor state and core, the [service_on] function determines
how much service a given job receives on the given core). *)
service_on : Job -> State -> Core -> work;
(** For a given processor state and core, a job does not receive service if it is
not scheduled in that state on that core. *)
service_on_implies_scheduled_on :
forall j s r, ~~ scheduled_on j s r -> service_on j s r = 0
}.
(** The definitions above focus on cores. From these definitions, we
generically derive predicates about the whole processor state. **)
Section ProcessorIn.
Context {Job : JobType}.
Context {State : Type}.
Context `{ProcessorState Job State}.
(** For a given processor state, the [scheduled_in] predicate checks
whether a given job is running on any core in that state. *)
Definition scheduled_in (j : Job) (s : State) : bool :=
[exists c : Core, scheduled_on j s c].
(** For a given processor state, the [service_in] function determines how
much service a given job receives in that state (across all cores). *)
Definition service_in (j : Job) (s : State) : work :=
\sum_(r : Core) service_on j s r.
End ProcessorIn.
(** * Schedule Representation *)
(** In Prosa, schedules are represented as functions, which allows us to model
......@@ -55,6 +70,6 @@ Class ProcessorState (Job : JobType) (State : Type) :=
Definition schedule (PState : Type) := instant -> PState.
(** The following line instructs Coq to not let proofs use knowledge of how
[scheduled_on], [scheduled_in], and [service_in] are defined. Instead,
[scheduled_on] and [service_on] are defined. Instead,
proofs must rely on basic lemmas about processor state classes. *)
Global Opaque scheduled_on scheduled_in service_in.
Global Opaque scheduled_on service_on.
......@@ -38,13 +38,13 @@ Section State.
(** As this is a uniprocessor model, cores are implicitly defined
as the [unit] type containing a single element as a placeholder. *)
scheduled_on j s (_ : unit) := ideal_scheduled_at j s;
service_in j s := ideal_service_in j s;
service_on j s (_ : unit) := ideal_service_in j s;
}.
Next Obligation.
rewrite /ideal_service_in /nat_of_bool.
case: ifP H =>//= SOME /existsP[].
by exists tt.
by case: ifP H =>// SOME /negP [].
Defined.
End State.
(** ** Idle Instants *)
......@@ -60,7 +60,7 @@ Section IsIdle.
(** ... and any ideal uniprocessor schedule of such jobs. *)
Variable sched : schedule ((*ideal*)processor_state Job).
(** We say that the processor is idle at time t iff there is no job being scheduled. *)
(** We say that the processor is idle at time [t] iff there is no job being scheduled. *)
Definition is_idle (t : instant) := sched t == None.
End IsIdle.
From mathcomp Require Export fintype.
Require Export prosa.behavior.all.
Require Import prosa.analysis.facts.behavior.service.
(** * Multiprocessor State *)
......@@ -25,7 +26,7 @@ Section Schedule.
Context `{ProcessorState Job processor_state}.
(** Given a desired number of processors [num_cpus], we define a finite type
of integers from 0 to [num_cpus - 1]. The purpose of this definition is
of integers from [0] to [num_cpus - 1]. The purpose of this definition is
to obtain a finite type (i.e., set of values) that can be enumerated in a
terminating computation.
......@@ -43,33 +44,35 @@ Section Schedule.
(** Based on this notion of multiprocessor state, we say that a given job [j]
is currently scheduled on a specific processor [cpu], according to the
given multiprocessor state [mps], if [j] is scheduled in the
given multiprocessor state [mps], iff [j] is scheduled in the
processor-local state [(mps cpu)]. *)
Let multiproc_scheduled_on (j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
Definition multiproc_scheduled_on
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= scheduled_in j (mps cpu).
(** The service received by a given job [j] in a given multiprocessor state
[mps] is given by the sum of the service received across all individual
processors of the multiprocessor. *)
Let multiproc_service_in (j : Job) (mps : multiprocessor_state)
:= \sum_(cpu < num_cpus) service_in j (mps cpu).
[mps] on a given processor of ID [cpu] is also a projection to the
processor-local state.
This definition is convertible to
[\sum_(cpu < num_cpus) multiproc_service_on j mps cpu]. *)
Definition multiproc_service_on
(j : Job) (mps : multiprocessor_state) (cpu : processor num_cpus)
:= service_in j (mps cpu).
(** Finally, we connect the above definitions with the generic Prosa
interface for processor models. *)
interface for processor models.
NB: The "cores" of this multiprocessor state are each its processors,
which themselves might contain several cores. *)
Global Program Instance multiproc_state : ProcessorState Job multiprocessor_state :=
{
scheduled_on := multiproc_scheduled_on;
service_in := multiproc_service_in
service_on := multiproc_service_on
}.
Next Obligation.
move: j s H0.
move=> j s /existsP Hsched.
apply/eqP.
rewrite sum_nat_eq0.
apply/forallP=>/= c.
rewrite service_implies_scheduled//.
case: (boolP (scheduled_in _ _))=>//= Habs.
exfalso; apply: Hsched.
by exists c.
move: j s r H0.
move=> j mps cpu.
by apply: service_in_implies_scheduled_in.
Defined.
End Schedule.
......@@ -37,7 +37,7 @@ Section State.
(** In contrast, job [j] receives service only if the given state [s] is
[Progress j]. *)
Definition spin_service_in (s : processor_state) : nat :=
Definition spin_service_on (s : processor_state) (_ : unit) : work :=
match s with
| Idle => 0
| Spin j' => 0
......@@ -51,13 +51,12 @@ Section State.
Global Program Instance pstate_instance : ProcessorState Job (processor_state) :=
{
scheduled_on := spin_scheduled_on;
service_in := spin_service_in
service_on := spin_service_on
}.
Next Obligation.
move: H.
case: s=>//= j' /existsP.
move: r H.
case: s=>//= j' _.
rewrite /nat_of_bool.
case: ifP=>//=_[].
by exists.
by case: ifP.
Defined.
End State.
......@@ -35,7 +35,7 @@ Section State.
(** If it is scheduled in state [s], job [j] receives service proportional
to the speed recorded in the state. *)
Definition varspeed_service_in (s : processor_state) : nat :=
Definition varspeed_service_on (s : processor_state) (_ : unit) : work :=
match s with
| Idle => 0
| Progress j' speed => if j' == j then speed else 0
......@@ -48,13 +48,12 @@ Section State.
Global Program Instance pstate_instance : ProcessorState Job processor_state :=
{
scheduled_on := varspeed_scheduled_on;
service_in := varspeed_service_in
service_on := varspeed_service_on
}.
Next Obligation.
move: H.
case: s=>//= j' v /existsP.
case: ifP=>//=_[].
by exists.
move: r H.
case: s=>//= j' v _.
by case: ifP.
Defined.
End State.