diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 27461995c45892f1e41ce6a03643640780bb5a56..31314466936bf70c058bf1d349593ed6fefc68ca 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -10,6 +10,18 @@ Section ArrivalPredicates.
(** Consider any kinds of jobs with arrival times. *)
Context {Job : JobType} `{JobArrival Job}.
+ (** Make hypothesis more easier to discover. *)
+ Lemma consistent_times_valid_arrival :
+ forall arr_seq,
+ valid_arrival_sequence arr_seq -> consistent_arrival_times arr_seq.
+ Proof. by move=> ? []. Qed.
+
+ (** Make hypothesis more easier to discover. *)
+ Lemma uniq_valid_arrival :
+ forall arr_seq,
+ valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq.
+ Proof. by move=> ? []. Qed.
+
(** A job that arrives in some interval <<[t1, t2)>> certainly arrives before
time [t2]. *)
Lemma arrived_between_before:
@@ -79,6 +91,26 @@ Section Arrived.
backlogged sched j t -> ~~ completed_by sched j t.
Proof. by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed.
+ (** Make hypothesis more easier to discover. *)
+ Lemma job_scheduled_implies_ready :
+ jobs_must_be_ready_to_execute sched ->
+ forall j t,
+ scheduled_at sched j t -> job_ready sched j t.
+ Proof. exact. Qed.
+
+ (** Make hypothesis more easier to discover. *)
+ Lemma valid_schedule_jobs_come_from_arrival_sequence :
+ forall arr_seq,
+ valid_schedule sched arr_seq ->
+ jobs_come_from_arrival_sequence sched arr_seq.
+ Proof. by move=> ? []. Qed.
+
+ (** Make hypothesis more easier to discover. *)
+ Lemma valid_schedule_jobs_must_be_ready_to_execute :
+ forall arr_seq,
+ valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched.
+ Proof. by move=> ? []. Qed.
+
End Arrived.
(** In this section, we establish useful facts about arrival sequence prefixes. *)
@@ -155,6 +187,12 @@ Section ArrivalSequencePrefix.
(** Assume that job arrival times are consistent. *)
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
+ (** Make hypothesis more easier to discover. *)
+ Lemma job_arrival_arrives_at :
+ forall {j t},
+ arrives_at arr_seq j t -> job_arrival j = t.
+ Proof. exact: H_consistent_arrival_times. Qed.
+
(** To simplify subsequent proofs, we restate the
[H_consistent_arrival_times] assumption as a trivial corollary. *)
Lemma job_arrival_at :
diff --git a/analysis/facts/readiness/sequential.v b/analysis/facts/readiness/sequential.v
index 8614b72c8a9f1965a714fa4d08e0fe06a5bd6c29..3e342d51f710c56177ae4d2b3f5836a29971d2b3 100644
--- a/analysis/facts/readiness/sequential.v
+++ b/analysis/facts/readiness/sequential.v
@@ -65,7 +65,8 @@ Section SequentialTasksReadiness.
- move: READY => /andP [PEND /allP ALL]; apply: ALL.
rewrite mem_filter; apply/andP; split; first by done.
by apply arrived_between_implies_in_arrivals => //.
- - by apply H_valid_schedule in SCHED; rewrite SCHED in NREADY.
+ - exfalso; apply/(negP NREADY)/job_scheduled_implies_ready => //.
+ exact: (valid_schedule_jobs_must_be_ready_to_execute sched arr_seq).
Qed.
(* Finally, we show that the sequential readiness model is a
diff --git a/analysis/facts/transform/wc_correctness.v b/analysis/facts/transform/wc_correctness.v
index 97f486e23e7e2a2c082a3c941b01109a3654b493..4d95f7eb58eb6269b2e4a5d09f42c689d1412a02 100644
--- a/analysis/facts/transform/wc_correctness.v
+++ b/analysis/facts/transform/wc_correctness.v
@@ -84,10 +84,9 @@ Section AuxiliaryLemmasWorkConservingTransformation.
move=> j t.
rewrite /find_swap_candidate.
destruct search_arg eqn:RES; last first.
- { move: (H_jobs_must_be_ready j t).
- rewrite /scheduled_at scheduled_in_def => READY SCHED_J.
- apply READY in SCHED_J.
- by apply (ready_implies_arrived sched). }
+ { rewrite -scheduled_in_def => sched_j.
+ apply: (ready_implies_arrived sched).
+ exact: job_scheduled_implies_ready. }
{ move=> /eqP SCHED_J.
move: RES => /search_arg_pred.
rewrite SCHED_J //. }
@@ -100,8 +99,8 @@ Section AuxiliaryLemmasWorkConservingTransformation.
Proof.
move=> j t SCHED_AT.
move: (swap_job_scheduled_cases _ _ _ _ _ SCHED_AT)=> [OTHER |[AT_T1 | AT_T2]].
- { have READY: job_ready sched j t by apply H_jobs_must_be_ready; rewrite -OTHER //.
- by apply (ready_implies_arrived sched). }
+ { apply: (ready_implies_arrived sched).
+ by apply: job_scheduled_implies_ready; rewrite // -OTHER. }
{ set t2 := find_swap_candidate arr_seq sched t1 in AT_T1.
move: AT_T1 => [EQ_T1 SCHED_AT'].
apply fsc_respects_has_arrived.
@@ -110,18 +109,18 @@ Section AuxiliaryLemmasWorkConservingTransformation.
rewrite EQ_T1 in SCHED_AT'.
rewrite SCHED_AT' /scheduled_at.
by rewrite scheduled_in_def. }
- { set t2 := find_swap_candidate arr_seq sched t1 in AT_T2.
- move: AT_T2 => [EQ_T2 SCHED_AT'].
- have ORDER: t1<=t2 by apply swap_candidate_is_in_future.
- have READY: job_ready sched j t1 by apply H_jobs_must_be_ready; rewrite -SCHED_AT' //.
- rewrite /job_ready /basic_ready_instance /pending /completed_by in READY.
- move: READY => /andP [ARR _].
- rewrite EQ_T2.
- rewrite /has_arrived in ARR.
- apply leq_trans with (n := t1) => //. }
+ set t2 := find_swap_candidate arr_seq sched t1 in AT_T2.
+ move: AT_T2 => [EQ_T2 SCHED_AT'].
+ have ORDER: t1<=t2 by apply swap_candidate_is_in_future.
+ have READY: job_ready sched j t1.
+ { by apply: job_scheduled_implies_ready; rewrite // -SCHED_AT'. }
+ rewrite /job_ready /basic_ready_instance /pending /completed_by in READY.
+ move: READY => /andP [ARR _].
+ rewrite EQ_T2.
+ exact: (leq_trans ARR).
Qed.
- (** Finally we show that, in the transformed schedule, jobs are scheduled
+ (** Finally we show that, in the transformed schedule, jobs are scheduled
only if they are ready. *)
Lemma fsc_jobs_must_be_ready_to_execute:
jobs_must_be_ready_to_execute sched'.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index ec72b8f43bcb87af9e95baf055022e56da31deea..78b8099a2ecd1295adf36dc1b0526dda4f88db4b 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -163,8 +163,9 @@ Section AbstractRTAforFIFOwithArrivalCurves.
{ rewrite negb_or /is_priority_inversion /is_priority_inversion
/is_interference_from_another_hep_job => /andP [HYP1 HYP2].
ideal_proc_model_sched_case_analysis_eq sched t jo.
- { exfalso; clear HYP1 HYP2.
- destruct H_valid_schedule as [A B].
+ { exfalso=> {HYP1 HYP2}.
+ have A : jobs_come_from_arrival_sequence sched arr_seq.
+ { exact: valid_schedule_jobs_come_from_arrival_sequence. }
eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try by rt_eauto.
move: BUSY => [PREF _].
by eapply not_quiet_implies_not_idle; rt_eauto. }
@@ -194,7 +195,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
busy_intervals_are_bounded_by arr_seq sched tsk interference interfering_workload L.
Proof.
intros j ARR TSK POS.
- destruct H_valid_schedule as [COME MUST ].
+ have COME : jobs_come_from_arrival_sequence sched arr_seq.
+ { exact: valid_schedule_jobs_come_from_arrival_sequence. }
edestruct exists_busy_interval_from_total_workload_bound
with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
{ by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
@@ -202,7 +204,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
split; first by done.
by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto. }
Qed.
-
+
(** In this section, we prove that, under FIFO scheduling, the cumulative priority inversion experienced
by a job [j] in any interval within its busy window is always [0]. We later use this fact to prove the bound on
the cumulative interference. *)
@@ -249,7 +251,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
- by move : INTER => /eqP INTER; rewrite -scheduled_at_def in INTER.
- by rewrite -ltnNge; apply leq_ltn_trans with (job_arrival j). }
apply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval;
- rt_eauto;last by done.
+ rt_eauto; last by [].
move : H_busy_interval => [ [_ [_ [QUIET /andP [ARR _ ]]]] _].
destruct (leqP t t1) as [LE | LT].
{ have EQ : t = job_arrival j by apply eq_trans with t1; lia.
@@ -260,17 +262,17 @@ Section AbstractRTAforFIFOwithArrivalCurves.
by apply leq_trans with (t1 + Δ) ; [| apply ltnW].
- by contradict QUIET. }
by destruct H_valid_schedule as [COME MUST]. } }
- { destruct H_valid_schedule as [READY MUST].
+ { have MUST : jobs_must_be_ready_to_execute sched.
+ { exact: (valid_schedule_jobs_must_be_ready_to_execute sched arr_seq). }
have HAS : has_arrived s t by eapply (jobs_must_arrive_to_be_ready sched).
rewrite scheduled_at_def in INTER.
unfold is_priority_inversion.
- move: INTER => /eqP ->.
- apply /negP; rewrite Bool.negb_involutive.
- by apply leq_trans with t; [apply HAS | apply ltnW]. }
- Unshelve.
- all: try by done.
+ move: INTER => /eqP ->; apply /negP; rewrite Bool.negb_involutive.
+ by apply leq_trans with t; [apply HAS | apply ltnW].
+ Unshelve.
+ all: by []. }
Qed.
-
+
End PriorityInversion.
(** Using the above lemma, we prove that IBF is indeed an interference bound. *)
@@ -278,7 +280,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
job_interference_is_bounded_by arr_seq sched tsk interference interfering_workload IBF.
Proof.
move => t1 t2 Δ j ARRj TSKj BUSY IN_BUSY NCOMPL.
- move: H_valid_schedule => [READY MUST ].
+ have COME : jobs_come_from_arrival_sequence sched arr_seq.
+ { exact: valid_schedule_jobs_come_from_arrival_sequence. }
rewrite /cumul_interference cumulative_interference_split.
have JPOS: job_cost_positive j by rewrite -ltnNge in NCOMPL; unfold job_cost_positive; lia.
move: (BUSY) => [ [ /andP [LE GT] [QUIETt1 _ ] ] [QUIETt2 EQNs]].
@@ -294,27 +297,27 @@ Section AbstractRTAforFIFOwithArrivalCurves.
( try ( apply (task_rbf_1_ge_task_cost arr_seq) with (j0 := j) => //= ) ||
apply (task_rbf_1_ge_task_cost arr_seq) with (j := j) => //=); first by auto.
by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
- { eapply leq_trans; last first.
- by erewrite leq_add2l; eapply task_rbf_excl_tsk_bounds_task_workload_excl_j; eauto 1.
- rewrite addnBA.
- { rewrite leq_sub2r //; eapply leq_trans.
- - apply sum_over_partitions_le => j' inJOBS.
- by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
- - rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite subnKC.
- rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=.
- apply leq_sum => tsk' _; rewrite andbC //=.
- destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by done.
- apply rem_in in IN.
- eapply leq_trans; last first.
- + by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
- + by rewrite addnBAC //= subnKC //= addn1; apply leqW. }
- { rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=.
- - by rewrite TSKj; apply leq_addr.
- - apply job_in_arrivals_between => //.
- by apply /andP; split; [| rewrite subnKC; [rewrite addn1 |]]. } } }
+ eapply leq_trans; last first.
+ by erewrite leq_add2l; eapply task_rbf_excl_tsk_bounds_task_workload_excl_j; eauto 1.
+ rewrite addnBA.
+ { rewrite leq_sub2r //; eapply leq_trans.
+ - apply sum_over_partitions_le => j' inJOBS.
+ by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
+ - rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite subnKC.
+ rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=.
+ apply leq_sum => tsk' _; rewrite andbC //=.
+ destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by [].
+ apply rem_in in IN.
+ eapply leq_trans; last first.
+ + by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
+ + by rewrite addnBAC //= subnKC //= addn1; apply leqW. }
+ rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=.
+ - by rewrite TSKj; apply leq_addr.
+ - apply job_in_arrivals_between => //.
+ by apply /andP; split; [| rewrite subnKC; [rewrite addn1 |]]. }
apply: arrivals_uniq => //.
apply: job_in_arrivals_between => //.
- by apply /andP; split; [ | rewrite addn1].
+ by apply /andP; split; [ | rewrite addn1].
Qed.
(** Finally, we show that there exists a solution for the response-time equation. *)