diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index f3fada868f4f701967ab87cb1792a819f4ac1708..e652e58b7461d942c2cb9c3acd088b69008417c9 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -255,7 +255,7 @@ Section Sequential_Abstract_RTA.
move: (H_busy_interval) => [[/andP [AFR1 AFR2] [QT _]] _].
have L12 := completed_before_beginning_of_busy_interval LT.
apply completion_monotonic with (t' := t) in L12; try done.
- by move: PEND => /andP [_ /negP T2].
+ by move: PEND => /andP [_ /negP T2].
Qed.
End CompletionOfJobsFromSameTask.
@@ -333,8 +333,9 @@ Section Sequential_Abstract_RTA.
case INT: (interference j t); last by done.
simpl; 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].
+ rewrite mem_filter; apply/andP; split.
+ - by rewrite H_job_of_tsk.
+ - by apply arrived_between_implies_in_arrivals.
Qed.
End Case1.
@@ -368,13 +369,14 @@ Section Sequential_Abstract_RTA.
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.
+ (neqbool_to_neqprop H_not_job_of_tsk) TSK2). }
+ rewrite ZERO ?addn0 add0n; simpl; clear ZERO.
case INT: (interference j t); last by done.
simpl; 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].
+ rewrite mem_filter; apply/andP; split.
+ - by rewrite H_job_of_tsk.
+ - by eapply arrived_between_implies_in_arrivals.
Qed.
End Case2.
@@ -410,8 +412,7 @@ Section Sequential_Abstract_RTA.
move: (H_work_conserving j t1 t2 t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval NEQT) => [Hn _].
apply/eqP;rewrite eq_sym eqb_id; apply/negPn/negP; intros CONTR; move: CONTR => /negP CONTR.
apply Hn in CONTR; rewrite scheduled_at_def in CONTR; simpl in CONTR.
- by rewrite H_sched [Some j' == Some j](negbTE (option_inj_neq (neq_sym H_j_neq_j'))) in CONTR.
- }
+ 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. }
{ intros. have ARR:= arrives_after_beginning_of_busy_interval j j' _ _ _ _ _ t1 t2 _ t.
@@ -419,12 +420,12 @@ Section Sequential_Abstract_RTA.
{ by move: H_not_job_of_tsk => /eqP TSK; rewrite TSK. }
{ move: H_sched => /eqP SCHEDt.
apply scheduled_implies_pending;
- auto using ideal_proc_model_ensures_ideal_progress.
+ auto using ideal_proc_model_ensures_ideal_progress.
by rewrite scheduled_at_def. }
case_eq (job_arrival j' <= job_arrival j) => ARRNEQ.
{ move: ARR => /andP [Ð Ð _].
eapply arrived_between_implies_in_arrivals; eauto 2.
- by apply/andP; split; last rewrite /A subnKC // addn1 ltnS. }
+ by apply/andP; split; last rewrite /A subnKC // addn1 ltnS. }
{ exfalso.
apply negbT in ARRNEQ; rewrite -ltnNge in ARRNEQ.
move: (H_sequential_tasks j j' t) => CONTR.
@@ -433,8 +434,7 @@ Section Sequential_Abstract_RTA.
{ by move: H_sched => /eqP SCHEDt; rewrite scheduled_at_def. }
move: H_job_j_is_not_completed => /negP T; apply: T.
apply completion_monotonic with t; try done.
- by apply ltnW; move: H_t_in_interval => /andP [_ NEQ]. }
- }
+ by apply ltnW; move: H_t_in_interval => /andP [_ NEQ]. } }
Qed.
End Case3.
@@ -454,7 +454,7 @@ Section Sequential_Abstract_RTA.
have j_is_in_arrivals_between: j \in arrivals_between t1 (t1 + A + ε).
{ eapply arrived_between_implies_in_arrivals; eauto 2.
move: (H_busy_interval) => [[/andP [GE _] [_ _]] _].
- by apply/andP; split; last rewrite /A subnKC // addn1.
+ by apply/andP; split; last rewrite /A subnKC // addn1.
} intros.
rewrite /cumul_task_interference /definitions.cumul_interference
/Sequential_Abstract_RTA.cumul_task_interference /task_interference_received_before
@@ -464,12 +464,12 @@ Section Sequential_Abstract_RTA.
move: (H_work_conserving j _ _ t H_j_arrives H_job_of_tsk H_job_cost_positive H_busy_interval) => WORK.
feed WORK.
{ move: H_t_in_interval => /andP [NEQ1 NEQ2].
- by apply/andP; split; last apply ltn_trans with (t1 + x). }
+ by apply/andP; split; last apply ltn_trans with (t1 + x). }
move: WORK => [_ ZIJT].
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].
+ by exists j; split; [apply j_is_in_arrivals_between | rewrite /job_of_task H_job_of_tsk H_sched !eq_refl].
Qed.
End Case4.
@@ -502,12 +502,12 @@ Section Sequential_Abstract_RTA.
Lemma cumul_interference_plus_sched_le_serv_of_task_plus_cumul_task_interference:
cumul_interference j t1 (t1 + x)
<= (task_service_of_jobs_in (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
- - service_during sched j t1 (t1 + x)) + cumul_task_interference t2 t1 (t1 + x).
+ - service_during sched j t1 (t1 + x)) + cumul_task_interference t2 t1 (t1 + x).
Proof.
have j_is_in_arrivals_between: j \in arrivals_between t1 (t1 + A + ε).
{ eapply arrived_between_implies_in_arrivals; eauto 2.
move: (H_busy_interval) => [[/andP [GE _] [_ _]] _].
- by apply/andP; split; last rewrite /A subnKC // addn1.
+ by apply/andP; split; last rewrite /A subnKC // addn1.
}
rewrite /cumul_interference /cumul_interference /task_service_of_jobs_in
/service_of_jobs.task_service_of_jobs_in
@@ -515,11 +515,11 @@ Section Sequential_Abstract_RTA.
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. }
+ 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.
+ by apply interference_plus_sched_le_serv_of_task_plus_task_interference.
Qed.
(** On the other hand, the service terms in the inequality
@@ -533,7 +533,7 @@ Section Sequential_Abstract_RTA.
have j_is_in_arrivals_between: j \in arrivals_between t1 (t1 + A + ε).
{ eapply arrived_between_implies_in_arrivals; eauto 2.
move: (H_busy_interval) => [[/andP [GE _] [_ _]] _].
- by apply/andP; split; last rewrite /A subnKC // addn1.
+ by apply/andP; split; last rewrite /A subnKC // addn1.
}
rewrite leq_add2r.
rewrite /task_workload /task_service_of_jobs_in
@@ -543,7 +543,7 @@ Section Sequential_Abstract_RTA.
rewrite addnC -addnBA; last by done.
rewrite [X in _ <= X - _]addnC -addnBA; last by done.
rewrite !subnn !addn0.
- by apply service_of_jobs_le_workload; auto using ideal_proc_model_provides_unit_service.
+ by apply service_of_jobs_le_workload; auto using ideal_proc_model_provides_unit_service.
Qed.
(** Finally, we show that the cumulative interference of job j in the interval <<[t1, t1 + x)>>
@@ -576,16 +576,16 @@ Section Sequential_Abstract_RTA.
(task_cost tsk * number_of_task_arrivals arr_seq tsk t1 (t1 + A + ε) - task_cost tsk); last first.
{ rewrite leq_sub2r // leq_mul2l; apply/orP; right.
rewrite -addnA -{2}[(A+1)](addKn t1).
- by apply H_is_arrival_curve; auto using leq_addr. }
+ by apply H_is_arrival_curve; auto using leq_addr. }
have Fact6: j \in arrivals_between (t1 + A) (t1 + A + ε).
{ apply arrived_between_implies_in_arrivals; try done.
apply/andP; split; rewrite /A subnKC //.
- by rewrite addn1 ltnSn //. }
+ by rewrite addn1 ltnSn //. }
have Fact4: j \in arrivals_at arr_seq (t1 + A).
{ by move: ARR => [t ARR]; rewrite subnKC //; feed (H_arrival_times_are_consistent j t); try (subst t). }
have Fact1: 1 <= number_of_task_arrivals arr_seq tsk (t1 + A) (t1 + A + ε).
{ rewrite /number_of_task_arrivals /task_arrivals_between /arrival_sequence.arrivals_between.
- by rewrite -count_filter_fun -has_count; apply/hasP; exists j; last rewrite TSK.
+ by rewrite -count_filter_fun -has_count; apply/hasP; exists j; last rewrite TSK.
}
rewrite (@num_arrivals_of_task_cat _ _ _ _ _ (t1 + A)); last by apply/andP; split; rewrite leq_addr //.
rewrite mulnDr.
@@ -594,9 +594,9 @@ Section Sequential_Abstract_RTA.
{ by apply workload_of_jobs_cat; apply/andP; split; rewrite leq_addr. } rewrite Step1; clear Step1.
rewrite -!addnBA; first last.
{ by rewrite /task_workload_between /workload.task_workload_between /task_workload
- /workload_of_jobs /job_of_task (big_rem j) //= TSK eq_refl leq_addr. }
+ /workload_of_jobs /job_of_task (big_rem j) //= TSK eq_refl leq_addr. }
{ apply leq_trans with (task_cost tsk); first by done.
- by rewrite -{1}[task_cost tsk]muln1 leq_mul2l; apply/orP; right. }
+ by rewrite -{1}[task_cost tsk]muln1 leq_mul2l; apply/orP; right. }
rewrite leq_add; [by done | by eapply task_workload_le_num_of_arrivals_times_cost; eauto | ].
rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs
/arrival_sequence.arrivals_between /number_of_task_arrivals /task_arrivals_between
@@ -608,7 +608,7 @@ Section Sequential_Abstract_RTA.
rewrite mulnDr mulnC muln1 -addnBA // subnn addn0 mulnC.
apply sum_majorant_constant.
move => j' ARR' /eqP TSK2.
- by rewrite -TSK2; apply H_valid_job_cost; exists (t1 + A); apply rem_in in ARR'.
+ by rewrite -TSK2; apply H_valid_job_cost; exists (t1 + A); apply rem_in in ARR'.
Qed.
(** Finally, we use the lemmas above to obtain the bound on
@@ -621,7 +621,7 @@ Section Sequential_Abstract_RTA.
have IN: j \in arrivals_between t1 (t1 + A + ε).
{ eapply arrived_between_implies_in_arrivals; eauto 2.
move: (H_busy_interval) => [[/andP [GE _] _] _].
- by apply/andP; split; last rewrite /A subnKC // addn1.
+ by apply/andP; split; last rewrite /A subnKC // addn1.
}
apply leq_trans with (task_workload_between t1 (t1+A+ε) - job_cost j + cumul_task_interference t2 t1 y).
- by apply cumulative_job_interference_le_task_interference_bound.
@@ -663,10 +663,10 @@ Section Sequential_Abstract_RTA.
rewrite addnBA; last first.
{ apply leq_trans with (task_rbf 1).
eapply task_rbf_1_ge_task_cost; eauto 2.
- eapply task_rbf_monotone; eauto 2.
- by rewrite addn1.
+ eapply task_rbf_monotone; eauto 2.
+ by rewrite addn1.
}
- by rewrite subnBA; auto; rewrite addnC.
+ by rewrite subnBA; auto; rewrite addnC.
Qed.
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
@@ -689,7 +689,7 @@ Section Sequential_Abstract_RTA.
move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
{ exfalso.
move: COMPL => /negP COMPL; apply: COMPL.
- by rewrite /service.completed_by /completed_by ZERO.
+ by rewrite /service.completed_by /completed_by ZERO.
}
set (A := job_arrival j - t1) in *.
apply leq_trans with
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index 08204f35c93ceb8732d20fc95f6b627db8671c80..b963583f2b7f3a06dbeb2e60e1185fe7883244b7 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -55,7 +55,7 @@ Section JLFPInstantiation.
earlier-arrived jobs of the same task. *)
Hypothesis H_JLFP_respects_sequential_tasks : policy_respects_sequential_tasks.
- (** Let [tsk] be any task in ts that is to be analyzed. *)
+ (** Let [tsk] be any task to be analyzed. *)
Variable tsk : Task.
(** For simplicity, let's define some local names. *)
@@ -66,7 +66,7 @@ Section JLFPInstantiation.
(** ** Interference and Interfering Workload *)
(** In this section, we introduce definitions of interference,
- interfering workload and a function that bounds cumulative interference. *)
+ interfering workload, and a function that bounds cumulative interference. *)
(** For proper calculation of interference and interfering workload
of a job, we need to distinguish interference received from other
@@ -83,13 +83,13 @@ Section JLFPInstantiation.
fun j1 j2 => hep_job j1 j2 && (job_task j1 != job_task j2).
(** In order to introduce the interference, first we need to recall the definition
- of priority inversion introduced in module limited.fixed_priority.busy_interval:
+ of priority inversion introduced in module analysis.definitions.priority_inversion:
[ Definition is_priority_inversion t := ]
[ if sched t is Some jlp then ]
[ ~~ higher_eq_priority jlp j ]
[ else false. ]
- I.e., we say that job j is incurring a priority inversion at time t
- if there exists a job with lower priority that executes at time t.
+ I.e., we say that job [j] is incurring a priority inversion at time [t]
+ if there exists a job with lower priority that executes at time [t].
In order to simplify things, we ignore the fact that according to this
definition a job can incur priority inversion even before its release
(or after completion). All such (potentially bad) cases do not cause
@@ -98,38 +98,42 @@ Section JLFPInstantiation.
Let is_priority_inversion (j : Job) (t : instant) :=
is_priority_inversion sched j t.
- (** Next, we say that job j is incurring interference from another job with higher or equal
- priority at time t, if there exists job [jhp] (different from j) with a higher or equal priority
- that executes at time t. *)
+ (** Next, we say that job [j] is incurring interference from another
+ job with higher or equal priority at time [t], if there exists a
+ job [jhp] (different from [j]) with higher or equal priority
+ that executes at time [t]. *)
Definition is_interference_from_another_hep_job (j : Job) (t : instant) :=
if sched t is Some jhp then
another_hep_job jhp j
else false.
- (** Similarly, we say that job j is incurring interference from a job with higher or
- equal priority of another task at time t, if there exists a job [jhp] (of a different task)
- with higher or equal priority that executes at time t. *)
+ (** Similarly, we say that job [j] is incurring interference from a
+ job with higher or equal priority of another task at time [t],
+ if there exists a job [jhp] (of a different task) with higher or
+ equal priority that executes at time [t]. *)
Definition is_interference_from_hep_job_from_another_task (j : Job) (t : instant) :=
if sched t is Some jhp then
hep_job_from_another_task jhp j
else false.
(** Now, we define the notion of cumulative interference, called
- interfering_workload_of_jobs_with_hep_priority, that says how
- many units of workload are generated by jobs with higher or equal
- priority released at time t. *)
+ [interfering_workload_of_hep_jobs], that says how many units of
+ workload are generated by jobs with higher or equal priority
+ released at time [t]. *)
Definition interfering_workload_of_hep_jobs (j : Job) (t : instant) :=
\sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.
(** Instantiation of Interference *)
- (** We say that job j incurs interference at time t iff it cannot execute due to
- a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion. *)
+ (** We say that job [j] incurs interference at time [t] iff it
+ cannot execute due to a higher-or-equal-priority job being
+ scheduled, or if it incurs a priority inversion. *)
Definition interference (j : Job) (t : instant) :=
is_priority_inversion j t || is_interference_from_another_hep_job j t.
(** Instantiation of Interfering Workload *)
- (** The interfering workload, in turn, is defined as the sum of the priority inversion
- function and interfering workload of jobs with higher or equal priority. *)
+ (** The interfering workload, in turn, is defined as the sum of the
+ priority inversion function and interfering workload of jobs
+ with higher or equal priority. *)
Definition interfering_workload (j : Job) (t : instant) :=
is_priority_inversion j t + interfering_workload_of_hep_jobs j t.
@@ -275,12 +279,13 @@ Section JLFPInstantiation.
(** Let <<[t1,t2)>> be any time interval. *)
Variables t1 t2 : instant.
- (** Consider any job j of [tsk]. *)
+ (** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
- (** Then for any job j, the cumulative interfering workload is equal to the conventional workload. *)
+ (** Then for any job [j], the cumulative interfering workload is
+ equal to the conventional workload. *)
Lemma instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs:
cumulative_interfering_workload_of_hep_jobs j t1 t2
= workload_of_other_hep_jobs j t1 t2.
@@ -373,7 +378,7 @@ Section JLFPInstantiation.
- rewrite leqn0 big1 //; intros joo PRIO2.
apply/eqP; rewrite eqb0; apply/eqP; intros C.
inversion C; subst joo; clear C.
- by rewrite PRIO2 in PRIO.
+ by rewrite PRIO2 in PRIO.
}
Qed.
diff --git a/analysis/definitions/task_schedule.v b/analysis/definitions/task_schedule.v
index e8f65b867403b56b60cdee2dd78478754d6489fe..83065b17e33aab0647e161bffef120d7c1debc4b 100644
--- a/analysis/definitions/task_schedule.v
+++ b/analysis/definitions/task_schedule.v
@@ -7,7 +7,7 @@ Require Export prosa.model.task.concept.
Require Export prosa.model.processor.ideal.
(** * Schedule of task *)
-(** In this section we define properties of schedule of a task *)
+(** In this section we define properties of the schedule of a task. *)
Section ScheduleOfTask.
(** Consider any type of tasks ... *)
@@ -40,8 +40,8 @@ Section ScheduleOfTask.
Definition task_service_during (t1 t2 : instant) :=
\sum_(t1 <= t < t2) task_service_at t.
- (** ...and the cumulative service received by [tsk] up to time t2,
+ (** ...and the cumulative service received by [tsk] up to time [t2],
i.e., in the interval <<[0, t2)>>. *)
- Definition task_service (t2 : instant) := task_service_during 0 t2.
+ Definition task_service (t2 : instant) := task_service_during 0 t2.
End ScheduleOfTask.
diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index 7c83f7fc006cbe35f76e4d1bcb8bf186a1200489..5e25d2d4857451bae7ab59e9fa0461895453df30 100644
--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -33,14 +33,14 @@ Section Composition.
t1 >= t2 -> service_during sched j t1 t2 = 0.
Proof.
move=> t1 t2 t1t2.
- rewrite /service_during big_geq //.
+ by rewrite /service_during big_geq //.
Qed.
(** Equally trivially, no job has received service prior to time zero. *)
Corollary service0:
service sched j 0 = 0.
Proof.
- rewrite /service service_during_geq //.
+ by rewrite /service service_during_geq //.
Qed.
(** Trivially, an interval consisting of one time unit is equivalent to
@@ -50,7 +50,7 @@ Section Composition.
service_during sched j t t.+1 = service_at sched j t.
Proof.
move => t.
- by rewrite /service_during big_nat_recr ?big_geq //.
+ by rewrite /service_during big_nat_recr ?big_geq //.
Qed.
(** Next, we observe that we can look at the service received during an
@@ -64,7 +64,7 @@ Section Composition.
= service_during sched j t1 t3.
Proof.
move => t1 t2 t3 /andP [t1t2 t2t3].
- by rewrite /service_during -big_cat_nat /=.
+ by rewrite /service_during -big_cat_nat /=.
Qed.
(** Since [service] is just a special case of [service_during], the same holds
@@ -76,7 +76,7 @@ Section Composition.
= service sched j t2.
Proof.
move=> t1 t2 t1t2.
- rewrite /service service_during_cat //.
+ by rewrite /service service_during_cat //.
Qed.
(** As a special case, we observe that the service during an interval can be
@@ -90,7 +90,7 @@ Section Composition.
move => t1 t2 t1t2.
have TIMES: t1 <= t1.+1 <= t2 by rewrite /(_ && _) ifT //.
have SPLIT := service_during_cat t1 t1.+1 t2 TIMES.
- by rewrite -service_during_instant //.
+ by rewrite -service_during_instant //.
Qed.
(** Symmetrically, we have the same for the end of the interval. *)
@@ -102,7 +102,7 @@ Section Composition.
Proof.
move=> t1 t2 t1t2.
rewrite -(service_during_cat t1 t2 t2.+1); last by rewrite /(_ && _) ifT //.
- rewrite service_during_instant //.
+ by rewrite service_during_instant //.
Qed.
(** And hence also for [service]. *)
@@ -112,7 +112,7 @@ Section Composition.
= service sched j t.+1.
Proof.
move=> t.
- rewrite /service. rewrite -service_during_last_plus_before //.
+ by rewrite /service -service_during_last_plus_before //.
Qed.
(** Finally, we deconstruct the service received during an interval <<[t1, t3)>>
@@ -126,7 +126,7 @@ Section Composition.
Proof.
move => t1 t2 t3 /andP [t1t2 t2t3].
rewrite -addnA service_during_first_plus_later// service_during_cat// /(_ && _) ifT//.
- by exact: ltnW.
+ by exact: ltnW.
Qed.
End Composition.
@@ -136,24 +136,24 @@ End Composition.
Section UnitService.
(** Consider any job type and any processor state. *)
- Context {Job: JobType}.
- Context {PState: Type}.
+ Context {Job : JobType}.
+ Context {PState : Type}.
Context `{ProcessorState Job PState}.
(** Let's consider a unit-service model... *)
Hypothesis H_unit_service: unit_service_proc_model PState.
(** ...and a given schedule. *)
- Variable sched: schedule PState.
+ Variable sched : schedule PState.
(** Let [j] be any job that is to be scheduled. *)
- Variable j: Job.
+ Variable j : Job.
(** First, we prove that the instantaneous service cannot be greater than 1, ... *)
Lemma service_at_most_one:
forall t, service_at sched j t <= 1.
Proof.
- by move=> t; rewrite /service_at.
+ by move=> t; rewrite /service_at.
Qed.
(** ...which implies that the cumulative service received by job [j] in any
@@ -176,31 +176,31 @@ Section UnitService.
Proof.
rewrite /is_step_function => t.
rewrite addn1 -service_last_plus_before leq_add2l.
- apply service_at_most_one.
+ by apply service_at_most_one.
Qed.
(** Next, consider any time [t]... *)
- Variable t: instant.
+ Variable t : instant.
- (** ...and let [s0] be any value less than the service received
+ (** ...and let [s] be any value less than the service received
by job [j] by time [t]. *)
- Variable s0: duration.
- Hypothesis H_less_than_s: s0 < service sched j t.
+ Variable s : duration.
+ Hypothesis H_less_than_s: s < service sched j t.
- (** Then, we show that there exists an earlier time [t0] where job [j] had [s0]
- units of service. *)
+ (** Then, we show that there exists an earlier time [t'] where job
+ [j] had [s] units of service. *)
Corollary exists_intermediate_service:
- exists t0,
- t0 < t /\
- service sched j t0 = s0.
+ exists t',
+ t' < t /\
+ service sched j t' = s.
Proof.
feed (exists_intermediate_point (service sched j));
[by apply service_is_a_step_function | intros EX].
feed (EX 0 t); first by done.
- feed (EX s0);
- first by rewrite /service /service_during big_geq //.
- by move: EX => /= [x_mid EX]; exists x_mid.
+ feed (EX s); first by rewrite /service /service_during big_geq //.
+ by move: EX => /= [x_mid EX]; exists x_mid.
Qed.
+
End ServiceIsAStepFunction.
End UnitService.
@@ -226,7 +226,7 @@ Section Monotonicity.
service sched j t1 <= service sched j t2.
Proof.
move=> t1 t2 let1t2.
- by rewrite -(service_cat sched j t1 t2 let1t2); apply: leq_addr.
+ by rewrite -(service_cat sched j t1 t2 let1t2); apply: leq_addr.
Qed.
End Monotonicity.
@@ -251,7 +251,7 @@ Section RelationToScheduled.
Proof.
rewrite /service_at /scheduled_at.
move=> t NOT_SCHED.
- rewrite service_implies_scheduled //.
+ by rewrite service_implies_scheduled //.
Qed.
(** Conversely, if a job receives service, then it must be scheduled. *)
@@ -261,7 +261,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 +272,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 +299,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]].
@@ -309,7 +309,7 @@ Section RelationToScheduled.
rewrite big_nat_eq0 => IS_ZERO.
have NO_SERVICE := IS_ZERO t TT.
apply lt0n_neq0 in SERVICE.
- by move/neqP in SERVICE; contradiction.
+ by move/neqP in SERVICE; contradiction.
}
Qed.
@@ -401,7 +401,7 @@ Section RelationToScheduled.
rewrite service_during_service_at.
exists t'; split => //.
move: SCHED. rewrite /scheduled_at /service_at.
- by apply (H_scheduled_implies_serviced j (sched t')).
+ by apply (H_scheduled_implies_serviced j (sched t')).
Qed.
(** ...which again applies to total service, too. *)
@@ -414,7 +414,7 @@ Section RelationToScheduled.
Proof.
move=> t [t' [TT SCHED]].
rewrite /service. apply scheduled_implies_cumulative_service.
- exists t'; split => //.
+ by exists t'; split => //.
Qed.
End GuaranteedService.
@@ -439,10 +439,10 @@ Section RelationToScheduled.
move=> t SERVICE.
have EX_SCHED := positive_service_implies_scheduled_before t SERVICE.
inversion EX_SCHED as [t'' [TIMES SCHED_AT]].
- exists t''; split; last by assumption.
+ exists t''; split; last by done.
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 +450,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 +461,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 +477,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); auto.
Qed.
(** Hence, one can ignore the service received by a job before its arrival
@@ -491,7 +491,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; split.
Qed.
(** ... which we can also state in terms of cumulative service. *)
@@ -500,7 +500,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.
@@ -537,7 +537,7 @@ 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 => //.
+ by apply IS_ZERO; apply/andP; split => //.
Qed.
(** We show that job [j] receives service at some point [t < t1]
@@ -548,8 +548,7 @@ Section RelationToScheduled.
Proof.
apply /idP/idP => /existsP [t SERVICED].
{
- have LE: t < t2
- by apply: (leq_trans _ H_t1_le_t2) => //.
+ have LE: t < t2 by apply: (leq_trans _ H_t1_le_t2) => //.
by apply /existsP; exists (Ordinal LE).
}
{
@@ -585,8 +584,9 @@ 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.
End RelationToScheduled.
@@ -650,6 +650,7 @@ Section ServiceInTwoSchedules.
identical_prefix sched1 sched2 h ->
forall j, service sched1 j h = service sched2 j h.
Proof.
- move=> h IDENT j; by apply equal_prefix_implies_same_service_during. Qed.
+ by move=> h IDENT j; apply equal_prefix_implies_same_service_during.
+ Qed.
End ServiceInTwoSchedules.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index 8f0607e8c5be6fd15aee0aa63fe594a4f2d2f806..ee074f8321133e8534603ec1a7e1701598dc8000 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -28,7 +28,7 @@ Section ExistsBusyIntervalJLFP.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-
+
(** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
@@ -62,7 +62,7 @@ Section ExistsBusyIntervalJLFP.
Let busy_interval t1 t2 := busy_interval arr_seq sched j t1 t2.
Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by arr_seq sched j K.
- (** We begin by proving a basic lemma about completion of the job within its busy interval. *)
+ (** We begin by proving a basic lemma about busy intervals. *)
Section BasicLemma.
(** Assume that the priority relation is reflexive. *)
@@ -72,7 +72,7 @@ Section ExistsBusyIntervalJLFP.
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval t1 t2.
- (** We prove that job j completes by the end of the busy interval. *)
+ (** We prove that job [j] completes by the end of the busy interval. *)
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
Proof.
@@ -85,17 +85,17 @@ Section ExistsBusyIntervalJLFP.
End BasicLemma.
(** In this section, we prove that during a busy interval there
- always exists a pending job. *)
+ always exists a pending job. *)
Section ExistsPendingJob.
- (** Let [[t1, t2]] be any interval where time t1 is quiet and time t2 is not quiet. *)
+ (** Let <<[t1, t2]>> be any interval where time [t1] is quiet and time [t2] is not quiet. *)
Variable t1 t2 : instant.
Hypothesis H_interval : t1 <= t2.
Hypothesis H_quiet : quiet_time t1.
Hypothesis H_not_quiet : ~ quiet_time t2.
- (** Then, we prove that there is a job pending at time t2
- that has higher or equal priority (with respect of [tsk]). *)
+ (** Then, we prove that there is a job pending at time [t2]
+ that has higher or equal priority (with respect to [tsk]). *)
Lemma not_quiet_implies_exists_pending_job:
exists j_hp,
arrives_in arr_seq j_hp /\
@@ -110,7 +110,7 @@ Section ExistsBusyIntervalJLFP.
move: (ARR) => INarr.
apply in_arrivals_implies_arrived_between in ARR; last by done.
apply in_arrivals_implies_arrived in INarr.
- by exists j_hp; repeat split; last by apply/negP.
+ by exists j_hp; repeat split; last by apply/negP.
}
{
apply negbT in COMP; rewrite -all_predC in COMP.
@@ -119,15 +119,15 @@ Section ExistsBusyIntervalJLFP.
destruct (ltnP (job_arrival j_hp) t1) as [BEFORE | AFTER];
first by specialize (QUIET j_hp IN HP BEFORE); apply completion_monotonic with (t := t1).
feed (COMP j_hp).
- by eapply arrived_between_implies_in_arrivals; eauto 1; apply/andP; split.
- by rewrite /= HP andbT negbK in COMP.
+ { by eapply arrived_between_implies_in_arrivals; eauto 1; apply/andP; split. }
+ by rewrite /= HP andbT negbK in COMP.
}
Qed.
End ExistsPendingJob.
(** In this section, we prove that during a busy interval the
- processor is never idle. *)
+ processor is never idle. *)
Section ProcessorAlwaysBusy.
(** Assume that the schedule is work-conserving ... *)
@@ -141,8 +141,8 @@ Section ExistsBusyIntervalJLFP.
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix t1 t2.
- (** We prove that if the processor is idle at a time instant t, then
- the next time instant [t+1] will be a quiet time. *)
+ (** We prove that if the processor is idle at a time instant [t],
+ then the next time instant [t+1] will be a quiet time. *)
Lemma idle_time_implies_quiet_time_at_the_next_time_instant:
forall (t : instant),
is_idle sched t ->
@@ -161,12 +161,12 @@ Section ExistsBusyIntervalJLFP.
- by move: IDLE => /eqP IDLE; rewrite /scheduled_at scheduled_in_def IDLE.
}
move: IDLE WC => /eqP IDLE [jo SCHED].
- by rewrite scheduled_at_def IDLE in SCHED.
+ by rewrite scheduled_at_def IDLE in SCHED.
Qed.
-
- (** Next, we prove that at any time instant t within the busy interval there exists a job
- [jhp] such that (1) job [jhp] is pending at time [t] and (2) job [jhp] has higher-or-equal
- priority than task [tsk]. *)
+
+ (** Next, we prove that at any time instant [t] within the busy interval there exists a job
+ [jhp] such that (1) job [jhp] is pending at time [t] and (2) job [jhp] has higher-or-equal
+ priority than task [tsk]. *)
Lemma pending_hp_job_exists:
forall t,
t1 <= t < t2 ->
@@ -194,7 +194,7 @@ Section ExistsBusyIntervalJLFP.
- move: T => [ARR [PEN HP]].
rewrite mem_filter; apply/andP; split; first (apply/andP; split); try done.
eapply arrived_between_implies_in_arrivals; try done.
- by apply/andP; split; last rewrite ltnS; move: PEN => /andP [T _].
+ by apply/andP; split; last rewrite ltnS; move: PEN => /andP [T _].
} move: EX => [hp__seq SE]; case FL: (hp__seq) => [ | jhp jhps].
+ subst hp__seq; exfalso.
move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| GE].
@@ -206,14 +206,14 @@ Section ExistsBusyIntervalJLFP.
repeat split; try done; first apply/andP; split; try done.
apply/negP; intros COMLP.
move: NCOMP => /negP NCOMP; apply: NCOMP.
- by apply completion_monotonic with t1.
+ by apply completion_monotonic with t1.
* apply NQT with t; first by apply/andP; split.
intros jhp ARR HP ARRB; apply negbNE; apply/negP; intros NCOMP.
move: (SE jhp) => [_ SE2].
rewrite in_nil in SE2; feed SE2; [clear SE2 | by done].
by repeat split; auto; apply/andP; split; first apply ltnW.
+ move: (SE jhp)=> [SE1 _]; subst; clear SE.
- by exists jhp; apply SE1; rewrite in_cons; apply/orP; left.
+ by exists jhp; apply SE1; rewrite in_cons; apply/orP; left.
Qed.
(** We prove that at any time instant [t] within <<[t1, t2)>> the processor is not idle. *)
@@ -249,19 +249,20 @@ Section ExistsBusyIntervalJLFP.
Variable t1 : instant.
Hypothesis H_quiet_time : quiet_time t1.
- (** Assume that there is no quiet time in the interval (t1, t1 + Δ]. *)
+ (** Assume that there is no quiet time in the interval <<(t1, t1 + Δ]>>. *)
Variable Δ : duration.
Hypothesis H_no_quiet_time : forall t, t1 < t <= t1 + Δ -> ~ quiet_time t.
- (** For clarity, we introduce a notion of the total service of jobs released in
- time interval <<[t_beg, t_end)>> during the time interval [t1, t1 + Δ). *)
+ (** For clarity, we introduce a notion of the total service of
+ jobs released in time interval <<[t_beg, t_end)>> during the
+ time interval <<[t1, t1 + Δ)>>. *)
Let service_received_by_hep_jobs_released_during t_beg t_end :=
service_of_higher_or_equal_priority_jobs
sched (arrivals_between t_beg t_end) j t1 (t1 + Δ).
(** We prove that jobs with higher-than-or-equal priority that
- released before time instant t1 receive no service after
- time instant t1. *)
+ released before time instant [t1] receive no service after time
+ instant [t1]. *)
Lemma hep_jobs_receive_no_service_before_quiet_time:
service_received_by_hep_jobs_released_during t1 (t1 + Δ) =
service_received_by_hep_jobs_released_during 0 (t1 + Δ).
@@ -328,10 +329,8 @@ Section ExistsBusyIntervalJLFP.
apply H_jobs_come_from_arrival_sequence with t'; try done.
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 apply leq_ltn_trans with t'.
+ - by rewrite lt0b -scheduled_at_def. } }
Qed.
End QuietTimeAndServiceOfJobs.
@@ -352,14 +351,15 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_priority_is_reflexive: reflexive_priorities.
Hypothesis H_priority_is_transitive: transitive_priorities.
- (** Next, we recall the notion of workload of all jobs released in a given interval
- <<[t1, t2)>> that have higher-or-equal priority w.r.t the job j being analyzed. *)
+ (** Next, we recall the notion of workload of all jobs released in
+ a given interval <<[t1, t2)>> that have higher-or-equal
+ priority w.r.t. the job [j] being analyzed. *)
Let hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs j (arrivals_between t1 t2).
(** With regard to the jobs with higher-or-equal priority that are released
in a given interval <<[t1, t2)>>, we also recall the service received by these
- jobs in the same interval [t1, t2). *)
+ jobs in the same interval <<[t1, t2)>>. *)
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs
sched (arrivals_between t1 t2) j t1 t2.
@@ -367,15 +367,15 @@ Section ExistsBusyIntervalJLFP.
(** Now we begin the proof. First, we show that the busy interval is bounded. *)
Section BoundingBusyInterval.
- (** Suppose that job j is pending at time t_busy. *)
+ (** Suppose that job [j] is pending at time [t_busy]. *)
Variable t_busy : instant.
Hypothesis H_j_is_pending : job_pending_at j t_busy.
(** First, we show that there must exist a busy interval prefix. *)
Section LowerBound.
- (** Since job j is pending, there is a (potentially unbounded)
- busy interval that starts no later than with the arrival of j. *)
+ (** Since job [j] is pending, there is a (potentially unbounded)
+ busy interval that starts no later than with the arrival of [j]. *)
Lemma exists_busy_interval_prefix:
exists t1,
busy_interval_prefix t1 t_busy.+1 /\
@@ -422,43 +422,46 @@ Section ExistsBusyIntervalJLFP.
Qed.
End LowerBound.
-
- (** Next we prove that, if there is a point where the requested workload
- is upper-bounded by the supply, then the busy interval eventually ends. *)
+
+ (** Next we prove that, if there is a point where the requested
+ workload is upper-bounded by the supply, then the busy
+ interval eventually ends. *)
Section UpperBound.
- (** Consider any busy interval prefix of job j. *)
+ (** Consider any busy interval prefix of job [j]. *)
Variable t1 : instant.
Hypothesis H_is_busy_prefix : busy_interval_prefix t1 t_busy.+1.
- (** Let priority_inversion_bound be a constant which bounds
- length of a priority inversion. *)
+ (** Let [priority_inversion_bound] be a constant that bounds
+ the length of any priority inversion. *)
Variable priority_inversion_bound: instant.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
(** Next, assume that for some positive delta, the sum of requested workload
- at time [t1 + delta] and constant priority_inversion_bound is bounded by
- delta (i.e., the supply). *)
+ at time [t1 + delta] and constant priority_inversion_bound is bounded by
+ delta (i.e., the supply). *)
Variable delta : duration.
Hypothesis H_delta_positive : delta > 0.
Hypothesis H_workload_is_bounded :
priority_inversion_bound + hp_workload t1 (t1 + delta) <= delta.
- (** If there is a quiet time by time (t1 + delta), it trivially follows that
- the busy interval is bounded.
- Thus, let's consider first the harder case where there is no quiet time,
- which turns out to be impossible. *)
+ (** If there is a quiet time by time [t1 + delta], it
+ trivially follows that the busy interval is bounded.
+ Thus, let's consider first the harder case where there is
+ no quiet time, which turns out to be impossible. *)
Section CannotBeBusyForSoLong.
- (** Assume that there is no quiet time in the interval (t1, t1 + delta]. *)
+ (** Assume that there is no quiet time in the interval <<(t1, t1 + delta]>>. *)
Hypothesis H_no_quiet_time:
forall t, t1 < t <= t1 + delta -> ~ quiet_time t.
- (** Since the interval is always non-quiet, the processor is always busy
- with tasks of higher-or-equal priority or some lower priority job which was scheduled,
- i.e., the sum of service done by jobs with actual arrival time in <<[t1, t1 + delta)>>
- and priority inversion equals delta. *)
+ (** Since the interval is always non-quiet, the processor is
+ always busy with tasks of higher-or-equal priority or
+ some lower priority job which was scheduled, i.e., the
+ sum of service done by jobs with actual arrival time in
+ <<[t1, t1 + delta)>> and priority inversion equals
+ [delta]. *)
Lemma busy_interval_has_uninterrupted_service:
delta <= priority_inversion_bound + hp_service t1 (t1 + delta).
Proof.
@@ -479,7 +482,7 @@ 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 //. }
+ { by 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.
@@ -488,22 +491,23 @@ Section ExistsBusyIntervalJLFP.
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. } } }
+ by inversion CONTR; clear 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.
- by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + delta)) //=; rewrite leq_addr.
+ by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + delta)) //=; rewrite leq_addr.
- apply H_priority_inversion_is_bounded; repeat split; try done.
+ by rewrite -addn1 leq_add2l.
+ move => t' /andP [LT GT]; apply H_no_quiet_time.
- by apply/andP; split; [ | rewrite ltnW ].
+ by apply/andP; split; [ | rewrite ltnW ].
+ move: EXj => /andP [T1 T2].
- by apply/andP; split; [done | apply ltn_trans with (t_busy.+1)].
+ by apply/andP; split; [done | apply ltn_trans with (t_busy.+1)].
}
Qed.
- (** Moreover, the fact that the interval is not quiet also implies
- that there's more workload requested than service received. *)
+ (** Moreover, the fact that the interval is not quiet also
+ implies that there's more workload requested than
+ service received. *)
Lemma busy_interval_too_much_workload:
hp_workload t1 (t1 + delta) > hp_service t1 (t1 + delta).
Proof.
@@ -543,8 +547,9 @@ Section ExistsBusyIntervalJLFP.
by rewrite ltnNge; apply/negP.
Qed.
- (** Using the two lemmas above, we infer that the workload is larger than the
- interval length. However, this contradicts the assumption H_workload_is_bounded. *)
+ (** Using the two lemmas above, we infer that the workload
+ is larger than the interval length. However, this
+ contradicts the assumption [H_workload_is_bounded]. *)
Corollary busy_interval_workload_larger_than_interval:
priority_inversion_bound + hp_workload t1 (t1 + delta) > delta.
Proof.
@@ -556,13 +561,14 @@ Section ExistsBusyIntervalJLFP.
End CannotBeBusyForSoLong.
- (** Since the interval cannot remain busy for so long, we prove that
- the busy interval finishes at some point t2 <= t1 + delta. *)
+ (** Since the interval cannot remain busy for so long, we
+ prove that the busy interval finishes at some point [t2 <=
+ t1 + delta]. *)
Lemma busy_interval_is_bounded:
exists t2,
t2 <= t1 + delta /\
busy_interval t1 t2.
- Proof.
+ Proof.
move: H_is_busy_prefix => [LT [QT [NQ NEQ]]].
destruct ([exists t2:'I_(t1 + delta).+1, (t2 > t1) && quiet_time_dec t2]) eqn:EX.
- have EX': exists (t2 : instant), ((t1 < t2 <= t1 + delta) && quiet_time_dec t2).
@@ -605,11 +611,11 @@ Section ExistsBusyIntervalJLFP.
Qed.
End UpperBound.
-
+
End BoundingBusyInterval.
- (** In this section, we show that from a workload bound we can infer
- the existence of a busy interval. *)
+ (** In this section, we show that from a workload bound we can
+ infer the existence of a busy interval. *)
Section BusyIntervalFromWorkloadBound.
(** Let priority_inversion_bound be a constant that bounds the length of a priority inversion. *)
@@ -618,18 +624,18 @@ Section ExistsBusyIntervalJLFP.
is_priority_inversion_bounded_by priority_inversion_bound.
(** Assume that for some positive delta, the sum of requested workload at
- time (t1 + delta) and priority inversion is bounded by delta (i.e., the supply). *)
+ time [t1 + delta] and priority inversion is bounded by delta (i.e., the supply). *)
Variable delta: duration.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
forall t, priority_inversion_bound + hp_workload t (t + delta) <= delta.
- (** Next, we assume that job j has positive cost, from which we can
- infer that there is a time in which j is pending. *)
+ (** Next, we assume that job [j] has positive cost, from which we
+ can infer that there is a time in which [j] is pending. *)
Hypothesis H_positive_cost: job_cost j > 0.
(** Therefore there must exists a busy interval <<[t1, t2)>> that
- contains the arrival time of j. *)
+ contains the arrival time of [j]. *)
Corollary exists_busy_interval:
exists t1 t2,
t1 <= job_arrival j < t2 /\
@@ -660,11 +666,12 @@ Section ExistsBusyIntervalJLFP.
}
by split.
Qed.
+
End BusyIntervalFromWorkloadBound.
(** If we know that the workload is bounded, we can also use the
- busy interval to infer a response-time bound. *)
+ busy interval to infer a response-time bound. *)
Section ResponseTimeBoundFromBusyInterval.
(** Let priority_inversion_bound be a constant that bounds the length of a priority inversion. *)
@@ -673,13 +680,13 @@ Section ExistsBusyIntervalJLFP.
is_priority_inversion_bounded_by priority_inversion_bound.
(** Assume that for some positive delta, the sum of requested workload at
- time (t1 + delta) and priority inversion is bounded by delta (i.e., the supply). *)
+ time [t1 + delta] and priority inversion is bounded by delta (i.e., the supply). *)
Variable delta: duration.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
forall t, priority_inversion_bound + hp_workload t (t + delta) <= delta.
- (** Then, job j must complete by (job_arrival j + delta). *)
+ (** Then, job [j] must complete by [job_arrival j + delta]. *)
Lemma busy_interval_bounds_response_time:
job_completed_by j (job_arrival j + delta).
Proof.
@@ -696,5 +703,5 @@ Section ExistsBusyIntervalJLFP.
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
-
+
End ExistsBusyIntervalJLFP.
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index cbebcf2f9ab1db0017d9f4e7e7fb6c759451ce74..7074b83928dc33e04d493c39cdfcf3c912ba9644 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -84,9 +84,9 @@ Section ExistsNoCarryIn.
{ by apply/andP; split; [apply ltnW | done]. }
}
move: NIDLE => [j' SCHED].
- by rewrite scheduled_at_def IDLE in SCHED.
+ by rewrite scheduled_at_def IDLE in SCHED.
Qed.
-
+
(** Moreover, an idle time implies no carry in at the next time instant. *)
Lemma idle_instant_implies_no_carry_in_at_t_pl_1 :
forall t,
@@ -106,7 +106,7 @@ Section ExistsNoCarryIn.
}
}
move: NIDLE => [j' SCHED].
- by rewrite scheduled_at_def IDLE in SCHED.
+ by rewrite scheduled_at_def IDLE in SCHED.
Qed.
(** Let the priority relation be reflexive. *)
@@ -129,33 +129,34 @@ Section ExistsNoCarryIn.
Hypothesis H_delta_positive: Δ > 0.
Hypothesis H_workload_is_bounded: forall t, total_workload t (t + Δ) <= Δ.
- (** Next we prove that since for any time instant t there is a point where
- the total workload is upper-bounded by the supply the processor encounters
- no carry-in instants at least every Δ time units. *)
+ (** Next we prove that, since for any time instant [t] there is a
+ point where the total workload is upper-bounded by the supply,
+ the processor encounters no-carry-in instants at least every [Δ]
+ time units. *)
Section ProcessorIsNotTooBusy.
- (** We start by proving that the processor has no carry-in at
- the beginning (i.e., has no carry-in at time instant 0). *)
+ (** We start by proving that the processor has no carry-in at the
+ beginning (i.e., has no carry-in at time instant [0]). *)
Lemma no_carry_in_at_the_beginning :
no_carry_in 0.
Proof.
intros s ARR AB; exfalso.
- by rewrite /arrived_before ltn0 in AB.
+ by rewrite /arrived_before ltn0 in AB.
Qed.
- (** In this section, we prove that for any time instant t there
- exists another time instant t' ∈ (t, t + Δ] such that the
- processor has no carry-in at time t'. *)
+ (** In this section, we prove that for any time instant [t] there
+ exists another time instant <<t' ∈ (t, t + Δ]>> such that the
+ processor has no carry-in at time [t']. *)
Section ProcessorIsNotTooBusyInduction.
- (** Consider an arbitrary time instant t... *)
- Variable t: duration.
+ (** Consider an arbitrary time instant [t]... *)
+ Variable t : duration.
- (** ...such that the processor has no carry-in at time t. *)
- Hypothesis H_no_carry_in: no_carry_in t.
+ (** ...such that the processor has no carry-in at time [t]. *)
+ Hypothesis H_no_carry_in : no_carry_in t.
(** First, recall that the total service is bounded by the total workload. Therefore
- the total service of jobs in the interval <<[t, t + Δ)>> is bounded by Δ. *)
+ the total service of jobs in the interval <<[t, t + Δ)>> is bounded by [Δ]. *)
Lemma total_service_is_bounded_by_Δ :
total_service t (t + Δ) <= Δ.
Proof.
@@ -166,12 +167,12 @@ Section ExistsNoCarryIn.
Qed.
(** Next we consider two cases:
- (1) The case when the total service is strictly less than Δ,
- (2) And when the total service is equal to Δ. *)
+ (1) The case when the total service is strictly less than [Δ], and
+ (2) the case when the total service is equal to [Δ]. *)
- (** In the first case, we use the pigeonhole principle to conclude
- that there is an idle time instant; which in turn implies existence
- of a time instant with no carry-in. *)
+ (** In the first case, we use the pigeonhole principle to
+ conclude that there is an idle time instant; which in turn
+ implies existence of a time instant with no carry-in. *)
Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
total_service t (t + Δ) < Δ ->
exists δ, δ < Δ /\ no_carry_in (t.+1 + δ).
@@ -185,7 +186,7 @@ Section ExistsNoCarryIn.
rewrite addn0; subst t_idle.
intros s ARR BEF.
apply idle_instant_implies_no_carry_in_at_t_pl_1 in IDLE; try done.
- by apply IDLE.
+ by apply IDLE.
}
have EX: exists γ, t_idle = t + γ.
{ by exists (t_idle - t); rewrite subnKC // ltnW. }
@@ -195,13 +196,16 @@ Section ExistsNoCarryIn.
- apply leq_trans with γ. by rewrite prednK. by rewrite ltnW.
- rewrite -subn1 -addn1 -addnA subnKC //.
intros s ARR BEF.
- by apply idle_instant_implies_no_carry_in_at_t.
+ by apply idle_instant_implies_no_carry_in_at_t.
Qed.
-
- (** In the second case, the total service within the time interval <<[t, t + Δ)>> is equal to Δ.
- On the other hand, we know that the total workload is lower-bounded by the total service
- and upper-bounded by Δ. Therefore, the total workload is equal to total service this
- implies completion of all jobs by time [t + Δ] and hence no carry-in at time [t + Δ]. *)
+
+ (** In the second case, the total service within the time
+ interval <<[t, t + Δ)>> is equal to [Δ]. On the other hand,
+ we know that the total workload is lower-bounded by the
+ total service and upper-bounded by [Δ]. Therefore, the total
+ workload is equal to the total service, which implies
+ completion of all jobs by time [t + Δ] and hence no carry-in
+ at time [t + Δ]. *)
Lemma completion_of_all_jobs_implies_no_carry_in :
total_service t (t + Δ) = Δ ->
no_carry_in (t + Δ).
@@ -231,7 +235,7 @@ Section ExistsNoCarryIn.
rewrite -service_of_jobs_cat_arrival_interval; last first.
apply/andP; split; [by done| by rewrite leq_addr].
rewrite EQserv.
- by apply H_workload_is_bounded.
+ by apply H_workload_is_bounded.
}
intros s ARR BEF.
eapply workload_eq_service_impl_all_jobs_have_completed; eauto 2; try done.
@@ -240,7 +244,7 @@ Section ExistsNoCarryIn.
End ProcessorIsNotTooBusyInduction.
- (** Finally, we show that any interval of length Δ contains a time instant with no carry-in. *)
+ (** Finally, we show that any interval of length [Δ] contains a time instant with no carry-in. *)
Lemma processor_is_not_too_busy :
forall t, exists δ, δ < Δ /\ no_carry_in (t + δ).
Proof.
@@ -259,16 +263,16 @@ Section ExistsNoCarryIn.
- by apply low_total_service_implies_existence_of_time_with_no_carry_in.
}
Qed.
-
+
End ProcessorIsNotTooBusy.
- (** Consider an arbitrary job j with positive cost. *)
+ (** Consider an arbitrary job [j] with positive cost. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** We show that there must exist a busy interval <<[t1, t2)>> that
- contains the arrival time of j. *)
+ contains the arrival time of [j]. *)
Corollary exists_busy_interval_from_total_workload_bound :
exists t1 t2,
t1 <= job_arrival j < t2 /\
@@ -294,7 +298,7 @@ Section ExistsNoCarryIn.
move: (PREFIX) => [_ [_ [NQT _]]].
move: (NQT t2); clear NQT; move => NQT.
feed NQT; first by (apply/andP; split; [|rewrite ltnS]).
- by apply: NQT; apply/quiet_time_P.
+ by apply: NQT; apply/quiet_time_P.
}
exists t2; split; last split; first by done.
{ apply leq_trans with (t1.+1 + δ); [by done | by rewrite addSn ltn_add2l]. }
@@ -305,7 +309,7 @@ Section ExistsNoCarryIn.
+ by apply/andP; split; last (apply leq_trans with t2; [apply ltnW | ]).
+ by apply/quiet_time_P.
}
- by move: LTt; rewrite ltnNge; move => /negP LTt; apply: LTt.
+ by move: LTt; rewrite ltnNge; move => /negP LTt; apply: LTt.
- by apply/quiet_time_P.
}
Qed.
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 361712d0da989258a3a3c1bb3b449cecd1fee40f..89adb263233906cd2e2c08354c54e724e28402c8 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -186,14 +186,14 @@ Section PriorityInversionIsBounded.
Variable t : instant.
Hypothesis H_t_in_busy_interval : t1 <= t < t2.
Hypothesis H_t_preemption_time : preemption_time sched t.
-
+
(** First note since [t] lies inside the busy interval,
the processor cannot be idle at time [t]. *)
Lemma instant_t_is_not_idle:
~ is_idle sched t.
Proof.
- intros Idle.
- by exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2.
+ intros IDLE.
+ by exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2.
Qed.
(** Next we consider two cases: (1) when [t] is less than [t2 - 1] and (2) [t] is equal to [t2 - 1]. *)
@@ -207,8 +207,8 @@ Section PriorityInversionIsBounded.
rewrite leq_eqVlt in TEMP; move: TEMP => /orP [/eqP EQUALt2m1 | LTt2m1].
- right; auto.
- left; auto.
- Qed.
-
+ Qed.
+
(** In case when [t < t2 - 1], we use the fact that time instant
[t+1] is not a quiet time. The later implies that there is a
pending higher-or-equal priority job at time [t]. Thus, the
@@ -327,8 +327,8 @@ Section PriorityInversionIsBounded.
have COMP: job_completed_by jhp t by apply completion_monotonic with (t0 := t1).
apply completed_implies_not_scheduled in COMP; last by done.
by move: COMP => /negP COMP; apply COMP.
- Qed.
-
+ Qed.
+
(** From the above lemmas we prove that there is a job [jhp] that is (1) scheduled at time [t],
(2) has higher-or-equal priority, and (3) arrived between [t1] and [t2]. *)
Corollary not_quiet_implies_exists_scheduled_hp_job_at_preemption_point:
@@ -346,8 +346,8 @@ Section PriorityInversionIsBounded.
- by apply scheduled_at_preemption_time_implies_arrived_between_within_busy_interval.
- by apply scheduled_at_preemption_time_implies_higher_or_equal_priority.
- by done.
- Qed.
-
+ Qed.
+
End ProcessorBusyWithHEPJobAtPreemptionPoints.
(** Next we prove that every nonpreemptive segment
@@ -445,7 +445,7 @@ Section PriorityInversionIsBounded.
apply completed_implies_not_scheduled in COMP; last by done.
by move: COMP => /negP COMP; apply COMP.
Qed.
-
+
(** Now, suppose there exists some constant K that bounds the distance to
a preemption time from the beginning of the busy interval. *)
Variable K : duration.
@@ -465,11 +465,11 @@ Section PriorityInversionIsBounded.
move => t /andP [GE LT].
move: H_preemption_time_exists => [prt [PR /andP [GEprt LEprt]]].
apply not_quiet_implies_exists_scheduled_hp_job_after_preemption_point with (tp := prt); eauto 2.
- - apply/andP; split; first by done.
- apply leq_ltn_trans with (t1 + K); first by done.
- by apply leq_ltn_trans with t.
+ - apply/andP; split; first by done.
+ apply leq_ltn_trans with (t1 + K); first by done.
+ by apply leq_ltn_trans with t.
- apply/andP; split; last by done.
- by apply leq_trans with (t1 + K).
+ by apply leq_trans with (t1 + K).
Qed.
End PreemptionTimeAndPriorityInversion.
@@ -521,7 +521,7 @@ Section PriorityInversionIsBounded.
move: LP => /negP LP; apply: LP.
by have ->: jlp = jhp by eapply ideal_proc_model_is_a_uniprocessor_model; eauto.
Qed.
-
+
(** Moreover, we show that lower-priority jobs that are scheduled
inside the busy-interval prefix <<[t1,t2)>> must be scheduled
before that interval. *)
@@ -555,7 +555,7 @@ Section PriorityInversionIsBounded.
- by rewrite -addn1 in LT2; apply subh3 in LT2; rewrite subn1 in LT2.
- by apply leq_trans with t1; first apply leq_pred.
Qed.
-
+
(** Thus, there must be a preemption time in the interval [t1, t1
+ max_priority_inversion t1]. That is, if a job with
higher-or-equal priority is scheduled at time instant t1, then
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 078603cf73736a535f921c7bd0cb43b44b23a1a8..17f5bcbd1e451123eaeac825945c18deff357585 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -30,7 +30,7 @@ Section GenericModelLemmas.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (** ... and any schedule of this arrival sequence ...*)
+ (** ... and any schedule of this arrival sequence ... *)
Variable sched : schedule PState.
(** ... where jobs do not execute before their arrival or after completion. *)
@@ -94,7 +94,7 @@ Section GenericModelLemmas.
move => j /andP [ARR Ps].
apply service_before_job_arrival_zero with H0; auto.
eapply in_arrivals_implies_arrived_between in ARR; eauto 2.
- by move: ARR => /andP [N1 N2]; apply leq_trans with t.
+ by move: ARR => /andP [N1 N2]; apply leq_trans with t.
Qed.
(** We show that the total service of jobs released in a time interval <<[t1,t2)>>
@@ -266,7 +266,7 @@ Section IdealModelLemmas.
End ServiceOfJobsIsBoundedByLength.
(** In this section, we introduce a connection between the cumulative
- service, cumulative workload, and completion of jobs. *)
+ service, cumulative workload, and completion of jobs. *)
Section WorkloadServiceAndCompletion.
(** Consider an arbitrary time interval <<[t1, t2)>>. *)
@@ -280,16 +280,15 @@ Section IdealModelLemmas.
(** And state the proposition that all jobs are completed by time
[t_compl]. Next we show that this proposition is equivalent to
- the fact that the workload of the jobs is equal to the service
- received by the jobs. *)
+ the fact that [workload of jobs = service of jobs]. *)
Let all_jobs_completed_by t_compl :=
forall j, j \in jobs -> P j -> completed_by j t_compl.
- (** First, we prove that if the workload of [jobs] is equal to the service
- of [jobs], then any job in [jobs] is completed by time [t_compl]. *)
- Lemma workload_eq_service_impl_all_jobs_have_completed:
- workload_of_jobs P jobs =
- service_of_jobs sched P jobs t1 t_compl ->
+ (** First, we prove that if the workload of [jobs] is equal to the
+ service of [jobs], then any job in [jobs] is completed by time
+ [t_compl]. *)
+ Lemma workload_eq_service_impl_all_jobs_have_completed :
+ workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl ->
all_jobs_completed_by t_compl.
Proof.
unfold jobs; intros EQ j ARR Pj; move: (ARR) => ARR2.
@@ -318,7 +317,7 @@ Section IdealModelLemmas.
(** And vice versa, the fact that any job in [jobs] is completed by time [t_compl]
implies that the workload of [jobs] is equal to the service of [jobs]. *)
- Lemma all_jobs_have_completed_impl_workload_eq_service:
+ Lemma all_jobs_have_completed_impl_workload_eq_service :
all_jobs_completed_by t_compl ->
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl.
@@ -328,7 +327,8 @@ Section IdealModelLemmas.
{ intros j t LE ARR.
eapply in_arrivals_implies_arrived_between in ARR; eauto 2; move: ARR => /andP [GE LT].
eapply cumulative_service_before_job_arrival_zero; eauto 2.
- by apply leq_trans with t1. }
+ by apply leq_trans with t1.
+ }
destruct (t_compl <= t1) eqn:EQ.
{ unfold service_of_jobs. unfold service_during.
rewrite exchange_big //=.
@@ -356,11 +356,10 @@ Section IdealModelLemmas.
}
Qed.
- (** Using the lemmas above, we prove equivalence. *)
- Corollary all_jobs_have_completed_equiv_workload_eq_service:
+ (** Using the lemmas above, we prove the equivalence. *)
+ Corollary all_jobs_have_completed_equiv_workload_eq_service :
all_jobs_completed_by t_compl <->
- workload_of_jobs P jobs =
- service_of_jobs sched P jobs t1 t_compl.
+ workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl.
Proof.
split.
- by apply all_jobs_have_completed_impl_workload_eq_service.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 160266bdb3cbb797546adbeec9048687c502a10b..2423eacc1f1fb43adda0550030a958b11421a85a 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -4,12 +4,15 @@ Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.results.edf.rta.bounded_pi.
Require Export prosa.analysis.facts.busy_interval.priority_inversion.
-(** Throughout this file, we assume ideal uni-processor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules ... *)
Require Import prosa.model.processor.ideal.
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** ... and the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
Require Import prosa.model.readiness.basic.
+
(** * RTA for EDF with Bounded Non-Preemptive Segments *)
(** In this section we instantiate the Abstract RTA for EDF-schedulers
@@ -37,7 +40,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (** For clarity, let's denote the relative deadline of a task as D. *)
+ (** For clarity, let's denote the relative deadline of a task as [D]. *)
Let D tsk := task_deadline tsk.
(** Consider the EDF policy that indicates a higher-or-equal priority relation.
@@ -199,7 +202,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
rewrite /D; ssrlia.
}
Qed.
-
+
(** Using the lemma above, we prove that the priority inversion of the task is bounded by
the maximum length of a nonpreemptive section of lower-priority tasks. *)
Lemma priority_inversion_is_bounded:
@@ -246,7 +249,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Qed.
End PriorityInversionIsBounded.
-
+
(** ** Response-Time Bound *)
(** In this section, we prove that the maximum among the solutions of the response-time
bound recurrence is a response-time bound for [tsk]. *)
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 2e537c1880b6b8522d1b25d8fd6ef29079201711..1ebccdbdcac7f14651d267f8bbf032b61d80df1e 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -7,10 +7,12 @@ Require Import prosa.model.task.absolute_deadline.
Require Import prosa.analysis.abstract.ideal_jlfp_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** Throughout this file, we assume ideal uni-processor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules ... *)
Require Import prosa.model.processor.ideal.
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** ... and the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
Require Import prosa.model.readiness.basic.
@@ -185,7 +187,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
+ (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk))
+ bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - task_rtct tsk) <= R.
-
(** To use the theorem uniprocessor_response_time_bound_seq from the Abstract RTA module,
we need to specify functions of interference, interfering workload and IBF. *)
@@ -227,8 +228,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
{ exfalso; clear HYP1 HYP2.
eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto 2 with basic_facts.
move: BUSY => [PREF _].
- by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts.
- }
+ by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
{ clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo.
rewrite EqSched_jo in HYP1, HYP2.
move: HYP1 HYP2.
@@ -585,7 +585,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
eapply leq_trans. eapply total_service_is_bounded_by_total_workload; eauto 2.
eapply leq_trans. eapply reorder_summation; eauto 2.
eapply leq_trans. eapply sum_of_workloads_is_at_most_bound_on_total_hep_workload; eauto 2.
- by done.
+ by done.
Qed.
End TaskInterferenceIsBoundedByIBF.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 9fd0ccfd8b5b9fe5eade9a493c0d28d5042cf6e0..d4657d0ed843bff11b4541ccad9c61a97fa0e6e8 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -149,13 +149,12 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
move: (LIMJ) => [BEG [END _]].
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).
all: eauto 2 with basic_facts.
- { rewrite subnn.
- intros A SP.
- apply H_R_is_maximum in SP.
- move: SP => [F [EQ LE]].
- exists F.
- by rewrite subn0 addn0; split.
- }
+ rewrite subnn.
+ intros A SP.
+ apply H_R_is_maximum in SP.
+ move: SP => [F [EQ LE]].
+ exists F.
+ by rewrite subn0 addn0; split.
Qed.
-
+
End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 4d986221a026dd63726c26b0133a313bf2cbd798..3f4e8db23a7f02fa896378de26db5754b1609b09 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -74,7 +74,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
(** Next, we assume that the schedule is a work-conserving schedule... *)
- Hypothesis H_work_conserving : work_conserving arr_seq sched.
+ Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... and the schedule respects the policy defined by the
job_preemptable function (i.e., jobs have bounded nonpreemptive
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index df8e08b950246ba523b76dbdccbb896295fff9bb..594396ed9c4674849b4cadc65adfb33ff0e62879 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -139,7 +139,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
move: H_R_is_maximum => [F [FIX BOUND]].
exists F; split.
+ by rewrite BLOCK add0n subnn subn0.
- + by rewrite subnn addn0.
+ + by rewrite subnn addn0.
Qed.
-
+
End RTAforFullyPreemptiveEDFModelwithArrivalCurves.
+
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index c4a52ae066e703f5fb7a72ee767abbfc64aa34e8..9183cbafc5b466f0b0a075c9d16155d159a06d77 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -6,8 +6,9 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** In this module we prove the RTA theorem for EDF-schedulers with
fixed preemption points. *)
-(** Throughout this file, we assume the EDF priority policy, ideal uni-processor
- schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+(** Throughout this file, we assume the EDF priority policy, ideal
+ uni-processor schedules, and the classic (i.e., Liu & Layland)
+ readiness model. *)
Require Import prosa.model.priority.edf.
Require Import prosa.model.processor.ideal.
Require Import prosa.model.readiness.basic.
@@ -151,7 +152,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
{ intros j ARR TSK.
move: (H_valid_job_cost _ ARR) => POSt.
move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
- by rewrite /job_response_time_bound /completed_by Z.
+ by rewrite /job_response_time_bound /completed_by Z.
}
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).
all: eauto 2 with basic_facts.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index d2161dfcb89edc14b08452b0cf04264d2d8f1424..1137186a332e02f074d78d77969e1cff7e63f3b5 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -79,7 +79,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** Consider an arbitrary task set ts, ... *)
Variable ts : list Task.
-
+
(** ... assume that all jobs come from the task set, ... *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
@@ -159,7 +159,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
by inversion JINB as [ta' [JIN' _]]; exists ta'.
}
Qed.
-
+
(** Using the above lemma, we prove that the priority inversion of the task is bounded by blocking_bound. *)
Lemma priority_inversion_is_bounded:
priority_inversion_is_bounded_by
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 3200a6c1e05604038fda8f84ffb35079add61c32..b34024f6cc6b93759098c5e7eb58dbae818be192 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -51,7 +51,7 @@ Section AbstractRTAforFPwithArrivalCurves.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
+
(** Note that we differentiate between abstract and
classical notions of work conserving schedule. *)
Let work_conserving_ab := definitions.work_conserving arr_seq sched.
@@ -241,9 +241,8 @@ Section AbstractRTAforFPwithArrivalCurves.
edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2.
{ by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_rbf'. }
exists t1, t2; split; first by done.
- split.
- - by done.
- - by eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2 with basic_facts.
+ split; first by done.
+ by eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2 with basic_facts.
Qed.
(** Next, we prove that IBF is indeed an interference bound.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 1c50173fda107096dba32b844d7c9aaf5d2ec932..3d6aea28ed9bed38e1ee8dca6a74eb41442ed30e 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -145,7 +145,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
bound for the more concrete model of fixed preemption points. *)
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
-
+
Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
response_time_bounded_by tsk R.
Proof.
@@ -155,7 +155,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
{ intros j ARR TSK.
move: (H_valid_job_cost _ ARR) => POSt.
move: POSt; rewrite /valid_job_cost TSK ZERO leqn0; move => /eqP Z.
- by rewrite /job_response_time_bound /completed_by Z.
+ by rewrite /job_response_time_bound /completed_by Z.
}
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
with (L0 := L).