diff --git a/restructuring/analysis/abstract/ideal_jlfp_rta.v b/restructuring/analysis/abstract/ideal_jlfp_rta.v
index 8ac9d7343caa72631bfc80dde5d90eba9d727329..8b1d173e87e4bf01977d1bb0d8c57b7f4be7f2a4 100644
--- a/restructuring/analysis/abstract/ideal_jlfp_rta.v
+++ b/restructuring/analysis/abstract/ideal_jlfp_rta.v
@@ -46,7 +46,7 @@ Section JLFPInstantiation.
(** Consider a JLFP-policy that indicates a higher-or-equal priority relation,
and assume that this relation is reflexive and transitive. *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -75,12 +75,12 @@ Section JLFPInstantiation.
whether job [j1] has a higher-than-or-equal-priority than job [j2]
and [j1] is not equal to [j2]... *)
Let another_hep_job: JLFP_policy Job :=
- fun j1 j2 => higher_eq_priority j1 j2 && (j1 != j2).
+ fun j1 j2 => hep_job j1 j2 && (j1 != j2).
(** ...and the second relation defines whether a job [j1] has a higher-or-equal-priority than
job [j2] and the task of [j1] is not equal to task of [j2]. *)
Let hep_job_from_another_task: JLFP_policy Job :=
- fun j1 j2 => higher_eq_priority j1 j2 && (job_task j1 != job_task j2).
+ 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:
@@ -96,7 +96,7 @@ Section JLFPInstantiation.
problems, as each job is analyzed only within the corresponding busy
interval where the priority inversion behaves in the expected way. *)
Let is_priority_inversion (j : Job) (t : instant) :=
- is_priority_inversion sched higher_eq_priority j t.
+ 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
@@ -200,16 +200,15 @@ Section JLFPInstantiation.
intros; rewrite -big_split //=.
apply/eqP; rewrite eqn_leq; apply/andP; split; rewrite leq_sum; try done.
{ intros t _; unfold is_priority_inversion, priority_inversion.is_priority_inversion.
-
ideal_proc_model_sched_case_analysis_eq sched t s; first by done.
- case HP: (higher_eq_priority s j); simpl; rewrite ?addn0 ?add0n.
- all: by move: Sched_s; rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ HP.
+ destruct (hep_job s j) eqn:MM; simpl; rewrite ?addn0 ?add0n.
+ all: by move: Sched_s; rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ MM.
}
{ intros t _; unfold is_priority_inversion, priority_inversion.is_priority_inversion,
is_interference_from_another_hep_job.
ideal_proc_model_sched_case_analysis_eq sched t s; first by done.
unfold another_hep_job.
- case HP: (higher_eq_priority s j); simpl; rewrite ?addn0 ?add0n.
+ destruct (hep_job s j) eqn:HP; simpl; rewrite ?addn0 ?add0n.
all: by move: Sched_s; rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ HP.
}
Qed.
@@ -237,7 +236,7 @@ Section JLFPInstantiation.
/is_interference_from_hep_job_from_another_task
/is_interference_from_another_hep_job /hep_job_from_another_task.
ideal_proc_model_sched_case_analysis_eq sched t s; first by rewrite has_pred0 addn0 leqn0 eqb0.
- case HP: (higher_eq_priority s j); simpl.
+ destruct (hep_job s j) eqn:HP; simpl.
1-2: move: Sched_s; rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ HP.
+ rewrite add0n TSK.
by case: (job_task s != tsk); first rewrite Bool.andb_true_l leq_b1.
@@ -263,7 +262,7 @@ Section JLFPInstantiation.
apply/hasP; exists j.
* rewrite mem_filter; apply/andP; split; first by done.
by eapply arrivals_between_sub with (t2 := 0) (t3 := upp); eauto 2.
- * case HP: (higher_eq_priority s j); apply/orP; [right|left]; last by done.
+ * destruct (hep_job s j) eqn:HP; apply/orP; [right|left]; last by done.
by rewrite /is_interference_from_another_hep_job EQ
/another_hep_job NEQ Bool.andb_true_r.
Qed.
@@ -315,11 +314,11 @@ Section JLFPInstantiation.
time in the _classical_ sense as [quiet_time_cl], and the
notion of quiet time in the _abstract_ sense as
[quiet_time_ab]. *)
- Let quiet_time_cl := busy_interval.quiet_time arr_seq sched higher_eq_priority.
+ Let quiet_time_cl := busy_interval.quiet_time arr_seq sched.
Let quiet_time_ab := definitions.quiet_time sched interference interfering_workload.
(** Same for the two notions of a busy interval. *)
- Let busy_interval_cl := busy_interval.busy_interval arr_seq sched higher_eq_priority.
+ Let busy_interval_cl := busy_interval.busy_interval arr_seq sched.
Let busy_interval_ab := definitions.busy_interval sched interference interfering_workload.
(** In this section we prove that the (abstract) cumulative interference of jobs with higher or
@@ -453,9 +452,9 @@ Section JLFPInstantiation.
rewrite eq_sym; apply/eqP.
apply all_jobs_have_completed_equiv_workload_eq_service; try done.
intros; apply QT.
- - by apply in_arrivals_implies_arrived in H3.
- - by move: H4 => /andP [H6 H7].
- - by apply in_arrivals_implies_arrived_between in H3.
+ - by apply in_arrivals_implies_arrived in H4.
+ - by move: H5 => /andP [H6 H7].
+ - by apply in_arrivals_implies_arrived_between in H4.
}
{ rewrite negb_and Bool.negb_involutive; apply/orP.
case ARR: (arrived_before j t); [right | by left].
@@ -473,15 +472,14 @@ Section JLFPInstantiation.
rewrite /cumulative_interference /service_of_other_hep_jobs in CIS, IC1.
intros t [T0 T1]; intros jhp ARR HP ARB.
eapply all_jobs_have_completed_equiv_workload_eq_service with
- (P := fun jhp => higher_eq_priority jhp j) (t1 := 0) (t2 := t);
+ (P := fun jhp => hep_job jhp j) (t1 := 0) (t2 := t);
eauto 2; last eapply arrived_between_implies_in_arrivals; try done.
move: T0; rewrite /cumul_interference /cumul_interfering_workload.
rewrite CIS !big_split //=; move => /eqP; rewrite eqn_add2l.
rewrite IC1; last by apply zero_is_quiet_time.
have L2 := instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs;
rewrite /cumulative_interfering_workload_of_hep_jobs in L2.
- rewrite L2. move => T2.
- apply/eqP; rewrite eq_sym.
+ rewrite L2. move => T2. apply/eqP; rewrite eq_sym.
move: T1; rewrite negb_and Bool.negb_involutive -leqNgt; move => /orP [T1 | T1].
- have NOTIN: j \notin arrivals_between 0 t.
{ apply/memPn; intros jo IN; apply/negP; intros EQ; move: EQ => /eqP EQ.
@@ -502,7 +500,8 @@ Section JLFPInstantiation.
rewrite big_mkcond //= (bigD1_seq j) //= -big_mkcondl //=.
move: T2; rewrite /service_of_jobs; move => /eqP T2; rewrite T2.
rewrite [X in _ == X]big_mkcond //= [X in _ == X](bigD1_seq j) //= -big_mkcondl //=.
- rewrite eqn_add2r. erewrite H_priority_is_reflexive; eauto 2.
+ rewrite eqn_add2r; unfold hep_job.
+ erewrite H_priority_is_reflexive; eauto 2.
rewrite eqn_leq; apply/andP; split; try eauto 2.
by apply service_at_most_cost; eauto with basic_facts.
Qed.
diff --git a/restructuring/analysis/concepts/busy_interval.v b/restructuring/analysis/concepts/busy_interval.v
index f2cde4cd59feafbbc1eac0e121ee50aadebb9879..84620629c520e0c470ab2c16ecea82a6b3387e79 100644
--- a/restructuring/analysis/concepts/busy_interval.v
+++ b/restructuring/analysis/concepts/busy_interval.v
@@ -22,7 +22,7 @@ Section BusyIntervalJLFP.
Variable sched : schedule (ideal.processor_state Job).
(** Assume a given JLFP policy. *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
(** In this section, we define the notion of a busy interval. *)
Section BusyInterval.
@@ -36,7 +36,7 @@ Section BusyIntervalJLFP.
Definition quiet_time (t : instant) :=
forall (j_hp : Job),
arrives_in arr_seq j_hp ->
- higher_eq_priority j_hp j ->
+ hep_job j_hp j ->
arrived_before j_hp t ->
completed_by sched j_hp t.
@@ -67,7 +67,7 @@ Section BusyIntervalJLFP.
the arrival sequence that arrived before t has completed by that time. *)
Definition quiet_time_dec (j : Job) (t : instant) :=
all
- (fun j_hp => higher_eq_priority j_hp j ==> (completed_by sched j_hp t))
+ (fun j_hp => hep_job j_hp j ==> (completed_by sched j_hp t))
(arrivals_before arr_seq t).
(** We also show that the computational and propositional definitions are equivalent. *)
diff --git a/restructuring/analysis/concepts/priority_inversion.v b/restructuring/analysis/concepts/priority_inversion.v
index 04770f758c33ca8c2dfe00628160104fd412d884..a90e9f672bf17d38e4639974f89843c5171e5459 100644
--- a/restructuring/analysis/concepts/priority_inversion.v
+++ b/restructuring/analysis/concepts/priority_inversion.v
@@ -24,7 +24,7 @@ Section CumulativePriorityInversion.
Variable sched : schedule (ideal.processor_state Job).
(** Assume a given JLFP policy. *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
(** In this section, we define a notion of bounded priority inversion experienced by a job. *)
Section JobPriorityInversionBound.
@@ -44,7 +44,7 @@ Section CumulativePriorityInversion.
with jitter or self-suspensions. *)
Definition is_priority_inversion (t : instant) :=
if sched t is Some jlp then
- ~~ higher_eq_priority jlp j
+ ~~ hep_job jlp j
else false.
(** Then we compute the cumulative priority inversion incurred by
@@ -56,7 +56,7 @@ Section CumulativePriorityInversion.
priority inversion within any busy interval prefix is bounded by [B]. *)
Definition priority_inversion_of_job_is_bounded_by (B : duration) :=
forall (t1 t2 : instant),
- busy_interval_prefix arr_seq sched higher_eq_priority j t1 t2 ->
+ busy_interval_prefix arr_seq sched j t1 t2 ->
cumulative_priority_inversion t1 t2 <= B.
End JobPriorityInversionBound.
diff --git a/restructuring/analysis/concepts/request_bound_function.v b/restructuring/analysis/concepts/request_bound_function.v
index 2dba4e71f658f207e51e4898ca6999f4afa7df79..13aab3c1e015473a2ef22000b3c23ba8f3eadbe0 100644
--- a/restructuring/analysis/concepts/request_bound_function.v
+++ b/restructuring/analysis/concepts/request_bound_function.v
@@ -30,7 +30,7 @@ Section TaskWorkloadBoundedByArrivalCurves.
(** ... and an FP policy that indicates a higher-or-equal priority
relation. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
(** Let [MaxArrivals] denote any function that takes a task and an interval length
and returns the associated number of job arrivals of the task. *)
@@ -67,8 +67,8 @@ Section TaskWorkloadBoundedByArrivalCurves.
(** Recall the definition of higher-or-equal-priority task and the per-task
workload bound for FP scheduling. *)
- Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
- Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
+ Let is_hep_task tsk_other := hep_task tsk_other tsk.
+ Let is_other_hep_task tsk_other := hep_task tsk_other tsk && (tsk_other != tsk).
(** Using the sum of individual workload bounds, we define the following
bound for the total workload of tasks in any interval of length
diff --git a/restructuring/analysis/facts/busy_interval.v b/restructuring/analysis/facts/busy_interval.v
index dc9cdabce22aa23653285c3be6307a9c632a6e5a..9275bab698d5c2e4347340c44484a8169d0c7469 100644
--- a/restructuring/analysis/facts/busy_interval.v
+++ b/restructuring/analysis/facts/busy_interval.v
@@ -39,7 +39,7 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume a given JLFP policy. *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
(** For simplicity, let's define some local names. *)
Let job_pending_at := pending sched.
@@ -56,11 +56,11 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Recall the list of jobs that arrive in any interval. *)
- Let quiet_time t1 := quiet_time arr_seq sched higher_eq_priority j t1.
- Let quiet_time_dec t1 := quiet_time_dec arr_seq sched higher_eq_priority j t1.
- Let busy_interval_prefix t1 t2 := busy_interval_prefix arr_seq sched higher_eq_priority j t1 t2.
- Let busy_interval t1 t2 := busy_interval arr_seq sched higher_eq_priority j t1 t2.
- Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by arr_seq sched higher_eq_priority j K.
+ Let quiet_time t1 := quiet_time arr_seq sched j t1.
+ Let quiet_time_dec t1 := quiet_time_dec arr_seq sched j t1.
+ Let busy_interval_prefix t1 t2 := busy_interval_prefix arr_seq sched j t1 t2.
+ 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. *)
Section BasicLemma.
@@ -100,11 +100,11 @@ Section ExistsBusyIntervalJLFP.
exists j_hp,
arrives_in arr_seq j_hp /\
arrived_between j_hp t1 t2 /\
- higher_eq_priority j_hp j /\
+ hep_job j_hp j /\
~ job_completed_by j_hp t2.
Proof.
rename H_quiet into QUIET, H_not_quiet into NOTQUIET.
- destruct (has (fun j_hp => (~~ job_completed_by j_hp t2) && higher_eq_priority j_hp j)
+ destruct (has (fun j_hp => (~~ job_completed_by j_hp t2) && hep_job j_hp j)
(arrivals_between t1 t2)) eqn:COMP.
{ move: COMP => /hasP [j_hp ARR /andP [NOTCOMP HP]].
move: (ARR) => INarr.
@@ -173,7 +173,7 @@ Section ExistsBusyIntervalJLFP.
exists jhp,
arrives_in arr_seq jhp /\
job_pending_at jhp t /\
- higher_eq_priority jhp j.
+ hep_job jhp j.
Proof.
move => t /andP [GE LT]; move: (H_busy_interval_prefix) => [_ [QTt [NQT REL]]].
move: (ltngtP t1.+1 t2) => [GT|CONTR|EQ]; first last.
@@ -186,8 +186,8 @@ Section ExistsBusyIntervalJLFP.
+ by apply (H_priority_is_reflexive 0).
- by exfalso; move_neq_down CONTR; eapply leq_ltn_trans; eauto 2.
- have EX: exists hp__seq: seq Job,
- forall j__hp, j__hp \in hp__seq <-> arrives_in arr_seq j__hp /\ job_pending_at j__hp t /\ higher_eq_priority j__hp j.
- { exists (filter (fun jo => (job_pending_at jo t) && (higher_eq_priority jo j)) (arrivals_between 0 t.+1)).
+ forall j__hp, j__hp \in hp__seq <-> arrives_in arr_seq j__hp /\ job_pending_at j__hp t /\ hep_job j__hp j.
+ { exists (filter (fun jo => (job_pending_at jo t) && (hep_job jo j)) (arrivals_between 0 t.+1)).
intros; split; intros T.
- move: T; rewrite mem_filter; move => /andP [/andP [PEN HP] IN].
repeat split; eauto using in_arrivals_implies_arrived.
@@ -257,7 +257,7 @@ Section ExistsBusyIntervalJLFP.
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 higher_eq_priority (arrivals_between t_beg t_end) j t1 (t1 + Δ).
+ 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
@@ -355,15 +355,14 @@ Section ExistsBusyIntervalJLFP.
(** 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
- higher_eq_priority j (arrivals_between 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). *)
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs
- sched higher_eq_priority (arrivals_between t1 t2) j t1 t2.
+ sched (arrivals_between t1 t2) j t1 t2.
(** Now we begin the proof. First, we show that the busy interval is bounded. *)
Section BoundingBusyInterval.
@@ -467,11 +466,11 @@ Section ExistsBusyIntervalJLFP.
destruct (delta <= priority_inversion_bound) eqn:KLEΔ.
{ by apply leq_trans with priority_inversion_bound; last rewrite leq_addr. }
apply negbT in KLEΔ; rewrite -ltnNge in KLEΔ.
- apply leq_trans with (cumulative_priority_inversion sched higher_eq_priority j t1 (t1 + delta) + hp_service t1 (t1 + delta)).
+ apply leq_trans with (cumulative_priority_inversion sched j t1 (t1 + delta) + hp_service t1 (t1 + delta)).
{ rewrite /hp_service hep_jobs_receive_no_service_before_quiet_time //.
rewrite /service_of_higher_or_equal_priority_jobs /service_of_jobs sum_pred_diff.
rewrite addnBA; last first.
- { by rewrite big_mkcond //= leq_sum //; intros j' _; case (higher_eq_priority j' j). }
+ { by rewrite big_mkcond //= leq_sum //; intros j' _; case (hep_job j' j). }
rewrite addnC -addnBA.
{ intros. have TT := no_idle_time_within_non_quiet_time_interval.
by unfold service_of_jobs in TT; rewrite TT // leq_addr.
@@ -481,7 +480,7 @@ Section ExistsBusyIntervalJLFP.
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: (higher_eq_priority j1 j); simpl; first last.
+ { 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; first by done.
@@ -492,7 +491,7 @@ Section ExistsBusyIntervalJLFP.
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 higher_eq_priority j t1 t_busy.+1); last eauto 2.
+ - 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.
- apply H_priority_inversion_is_bounded; repeat split; try done.
+ by rewrite -addn1 leq_add2l.
@@ -512,7 +511,7 @@ Section ExistsBusyIntervalJLFP.
rename H_no_quiet_time into NOTQUIET,
H_is_busy_prefix into PREFIX.
set l := arrivals_between t1 (t1 + delta).
- set hep := higher_eq_priority.
+ set hep := hep_job.
unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs,
hp_workload, workload_of_higher_or_equal_priority_jobs, workload_of_jobs.
fold arrivals_between l hep.
@@ -536,7 +535,7 @@ Section ExistsBusyIntervalJLFP.
apply leq_add; last first.
{
apply leq_sum; intros j1 NEQ.
- destruct (higher_eq_priority j1 j); last by done.
+ destruct (hep_job j1 j); last by done.
by apply cumulative_service_le_job_cost, ideal_proc_model_provides_unit_service.
}
rewrite ignore_service_before_arrival; rewrite //; [| by apply ltnW].
diff --git a/restructuring/analysis/facts/carry_in.v b/restructuring/analysis/facts/carry_in.v
index 2b036253eb5bf7e22b202bd5b26ec39b0a0db113..35b0cb56c05136cab6a42edf5838efd1a738014b 100644
--- a/restructuring/analysis/facts/carry_in.v
+++ b/restructuring/analysis/facts/carry_in.v
@@ -42,14 +42,14 @@ Section ExistsNoCarryIn.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume a given JLFP policy. *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
(** For simplicity, let's define some local names. *)
Let job_pending_at := pending sched.
Let job_completed_by := completed_by sched.
Let arrivals_between := arrivals_between arr_seq.
Let no_carry_in := no_carry_in arr_seq sched.
- Let quiet_time := quiet_time arr_seq sched higher_eq_priority.
+ Let quiet_time := quiet_time arr_seq sched.
(** The fact that there is no carry-in at time instant t
trivially implies that t is a quiet time. *)
@@ -273,17 +273,17 @@ Section ExistsNoCarryIn.
exists t1 t2,
t1 <= job_arrival j < t2 /\
t2 <= t1 + Δ /\
- busy_interval arr_seq sched higher_eq_priority j t1 t2.
+ busy_interval arr_seq sched j t1 t2.
Proof.
rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.
edestruct (exists_busy_interval_prefix
- arr_seq H_arrival_times_are_consistent sched higher_eq_priority j ARR H_priority_is_reflexive (job_arrival j))
+ arr_seq H_arrival_times_are_consistent sched j ARR H_priority_is_reflexive (job_arrival j))
as [t1 [PREFIX GE]].
apply job_pending_at_arrival; auto.
move: GE => /andP [GE1 _].
exists t1; move: (processor_is_not_too_busy t1.+1) => [δ [LE QT]].
apply no_carry_in_implies_quiet_time with (j := j) in QT.
- have EX: exists t2, ((t1 < t2 <= t1.+1 + δ) && quiet_time_dec arr_seq sched higher_eq_priority j t2).
+ have EX: exists t2, ((t1 < t2 <= t1.+1 + δ) && quiet_time_dec arr_seq sched j t2).
{ exists (t1.+1 + δ); apply/andP; split.
- by apply/andP; split; first rewrite addSn ltnS leq_addr.
- by apply/quiet_time_P. }
diff --git a/restructuring/analysis/facts/priority_inversion.v b/restructuring/analysis/facts/priority_inversion.v
index b24ece23584b0ce2479e8a07deb52b6df4fbdee5..1e1eb9c93069dd1ca474157c5b2dfbdbab3b9acf 100644
--- a/restructuring/analysis/facts/priority_inversion.v
+++ b/restructuring/analysis/facts/priority_inversion.v
@@ -112,7 +112,7 @@ Section PriorityInversionIsBounded.
(** Consider a JLFP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
Hypothesis H_priority_is_reflexive: reflexive_priorities.
Hypothesis H_priority_is_transitive: transitive_priorities.
@@ -151,7 +151,7 @@ Section PriorityInversionIsBounded.
[j_lp], so the maximal length of priority inversion cannot be
negative. *)
Definition max_length_of_priority_inversion (j : Job) (t : instant) :=
- \max_(j_lp <- arrivals_before arr_seq t | ~~ higher_eq_priority j_lp j)
+ \max_(j_lp <- arrivals_before arr_seq t | ~~ hep_job j_lp j)
(job_max_nonpreemptive_segment j_lp - ε).
(** Next we prove that a priority inversion of a job is bounded by
@@ -171,7 +171,7 @@ Section PriorityInversionIsBounded.
(** Consider any busy interval prefix [t1, t2) of job j. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix:
- busy_interval_prefix arr_seq sched higher_eq_priority j t1 t2.
+ busy_interval_prefix arr_seq sched j t1 t2.
(** * Processor Executes HEP jobs after Preemption Point *)
(** In this section, we prove that at any time instant after any preemption point
@@ -220,7 +220,7 @@ Section PriorityInversionIsBounded.
t < t2.-1 ->
forall jhp,
scheduled_at sched jhp t ->
- higher_eq_priority jhp j.
+ hep_job jhp j.
Proof.
intros LTt2m1 jhp Sched_jhp.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
@@ -253,7 +253,7 @@ Section PriorityInversionIsBounded.
t = t2.-1 ->
forall jhp,
scheduled_at sched jhp t ->
- higher_eq_priority jhp j.
+ hep_job jhp j.
Proof.
intros EQUALt2m1 jhp Sched_jhp.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
@@ -299,7 +299,7 @@ Section PriorityInversionIsBounded.
Corollary scheduled_at_preemption_time_implies_higher_or_equal_priority:
forall jhp,
scheduled_at sched jhp t ->
- higher_eq_priority jhp j.
+ hep_job jhp j.
Proof.
move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
destruct t_lt_t2_or_t_eq_t2.
@@ -335,7 +335,7 @@ Section PriorityInversionIsBounded.
Corollary not_quiet_implies_exists_scheduled_hp_job_at_preemption_point:
exists j_hp,
arrived_between j_hp t1 t2 /\
- higher_eq_priority j_hp j /\
+ hep_job j_hp j /\
job_scheduled_at j_hp t.
Proof.
move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET INBI]]].
@@ -404,7 +404,7 @@ Section PriorityInversionIsBounded.
tp <= t < t2 ->
exists j_hp,
arrived_between j_hp t1 t.+1 /\
- higher_eq_priority j_hp j /\
+ hep_job j_hp j /\
job_scheduled_at j_hp t.
Proof.
move: (H_jobs_come_from_arrival_sequence) (H_work_conserving) => CONS WORK.
@@ -414,7 +414,7 @@ Section PriorityInversionIsBounded.
{ exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2.
by apply/andP; split; first apply leq_trans with tp. }
exists jhp.
- have HP: higher_eq_priority jhp j.
+ have HP: hep_job jhp j.
{ intros.
have SOAS := scheduling_of_any_segment_starts_with_preemption_time _ _ Sched_jhp.
move: SOAS => [prt [/andP [_ LE] [PR SCH]]].
@@ -460,7 +460,7 @@ Section PriorityInversionIsBounded.
t1 + K <= t < t2 ->
exists j_hp,
arrived_between j_hp t1 t.+1 /\
- higher_eq_priority j_hp j /\
+ hep_job j_hp j /\
job_scheduled_at j_hp t.
Proof.
move => t /andP [GE LT].
@@ -484,9 +484,9 @@ Section PriorityInversionIsBounded.
a quiet time [t+1] then this is the first time when this job is scheduled. *)
Lemma hp_job_not_scheduled_before_quiet_time:
forall jhp t,
- quiet_time arr_seq sched higher_eq_priority j t.+1 ->
+ quiet_time arr_seq sched j t.+1 ->
job_scheduled_at jhp t.+1 ->
- higher_eq_priority jhp j ->
+ hep_job jhp j ->
~~ job_scheduled_at jhp t.
Proof.
intros jhp t QT SCHED1 HP.
@@ -503,7 +503,7 @@ Section PriorityInversionIsBounded.
forall jlp t,
t1 <= t < t2 ->
job_scheduled_at jlp t ->
- ~~ higher_eq_priority jlp j ->
+ ~~ hep_job jlp j ->
job_arrival jlp < t1.
Proof.
move => jlp t /andP [GE LT] SCHED LP.
@@ -530,7 +530,7 @@ Section PriorityInversionIsBounded.
forall jlp t,
t1 <= t < t2 ->
job_scheduled_at jlp t ->
- ~~ higher_eq_priority jlp j ->
+ ~~ hep_job jlp j ->
exists t', t' < t1 /\ job_scheduled_at jlp t'.
Proof.
move => jlp t NEQ SCHED LP; move: (NEQ) => /andP [GE LT].
@@ -597,7 +597,7 @@ Section PriorityInversionIsBounded.
(** Assume that a job [jhp] with higher-or-equal priority is scheduled at time [t1]. *)
Variable jhp : Job.
Hypothesis H_jhp_is_scheduled : scheduled_at sched jhp t1.
- Hypothesis H_jhp_hep_priority : higher_eq_priority jhp j.
+ Hypothesis H_jhp_hep_priority : hep_job jhp j.
(** Then time instant [t1] is a preemption time. *)
Lemma preemption_time_exists_case2:
@@ -624,7 +624,7 @@ Section PriorityInversionIsBounded.
(** Assume that a job [jhp] with lower priority is scheduled at time [t1]. *)
Variable jlp : Job.
Hypothesis H_jlp_is_scheduled : scheduled_at sched jlp t1.
- Hypothesis H_jlp_low_priority : ~~ higher_eq_priority jlp j.
+ Hypothesis H_jlp_low_priority : ~~ hep_job jlp j.
(** To prove the lemma in this case we need a few auxiliary
facts about the first preemption point of job [jlp]. *)
@@ -810,7 +810,7 @@ Section PriorityInversionIsBounded.
move: (H_busy_interval_prefix) => [NEM [QT1 [NQT HPJ]]].
ideal_proc_model_sched_case_analysis sched t1 s.
- by apply preemption_time_exists_case1.
- - case PRIO: (higher_eq_priority s j).
+ - destruct (hep_job s j) eqn:PRIO.
+ by eapply preemption_time_exists_case2; eauto.
+ eapply preemption_time_exists_case3 with s; eauto.
by rewrite -eqbF_neg; apply /eqP.
diff --git a/restructuring/analysis/facts/rbf.v b/restructuring/analysis/facts/rbf.v
index 5c5a910bc355ff3adcf201ac3fa87ec8ea4d3862..5cdc4ffbcd564b64c82c6ad55feca86c01e6561f 100644
--- a/restructuring/analysis/facts/rbf.v
+++ b/restructuring/analysis/facts/rbf.v
@@ -35,7 +35,7 @@ Section ProofWorkloadBound.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
(** Consider an FP policy that indicates a higher-or-equal priority relation. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.
(** Consider a task set ts... *)
@@ -59,8 +59,8 @@ Section ProofWorkloadBound.
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
Let total_rbf := total_request_bound_function ts.
- Let total_hep_rbf := total_hep_request_bound_function_FP higher_eq_priority ts tsk.
- Let total_ohep_rbf := total_ohep_request_bound_function_FP higher_eq_priority ts tsk.
+ Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+ Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
(** Next, we consider any job [j] of [tsk]. *)
Variable j : Job.
@@ -128,14 +128,13 @@ Section ProofWorkloadBound.
total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
Proof.
set l := arrivals_between arr_seq t (t + delta).
- set hep := higher_eq_priority.
apply leq_trans with
- (\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
+ (\sum_(tsk' <- ts | hep_task tsk' tsk && (tsk' != tsk))
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{ intros.
rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
- have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk && (job_task x != tsk)).
+ have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk && (job_task x != tsk)).
rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
apply leq_sum; move => j0 /andP [IN0 HP0].
@@ -163,12 +162,11 @@ Section ProofWorkloadBound.
total_hep_workload t (t + delta) <= total_hep_rbf delta.
Proof.
set l := arrivals_between arr_seq t (t + delta).
- set hep := higher_eq_priority.
apply leq_trans with
- (n := \sum_(tsk' <- ts | hep tsk' tsk)
+ (n := \sum_(tsk' <- ts | hep_task tsk' tsk)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{ rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk.
- have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk).
+ have EXCHANGE := exchange_big_dep (fun x => hep_task (job_task x) tsk).
rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
apply leq_sum; move => j0 /andP [IN0 HP0].
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index 6e435225eda5215d1d3ff4b7e04bd5c9f42be72c..e6ed0146fb2bd28e9be41a125c887cf49cdcf440 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -48,10 +48,9 @@ Section ServiceOfJobs.
(** Next, we define the service received by jobs with higher or
equal priority under JLFP policies. *)
Section PerJobPriority.
-
+
(** Consider any JLDP policy. *)
- (* [FIXME]: This should be a nameless context declaration! *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
(** Let jobs denote any (finite) set of jobs. *)
Variable jobs : seq Job.
@@ -60,8 +59,7 @@ Section ServiceOfJobs.
Variable j : Job.
(** Based on the definition of jobs of higher or equal priority, ... *)
- (* [FIXME]: this should use [hep_job], not the named type class directly. *)
- Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
+ Let of_higher_or_equal_priority j_hp := hep_job j_hp j.
(** ...we define the service received during [[t1, t2)] by jobs of higher or equal priority. *)
Definition service_of_higher_or_equal_priority_jobs (t1 t2 : instant) :=
diff --git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index 42815dd533c9b838e53ef6b7798e1b830c5921ae..8394feac8d95a5e2aa89bfbfd393bf7b7798495a 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ -40,16 +40,13 @@ Section WorkloadOfJobs.
(** Consider any JLFP policy that indicates whether a job has
higher or equal priority. *)
- (* [FIXME]: should be a context declaration! *)
- Variable higher_eq_priority : JLFP_policy Job.
+ Context `{JLFP_policy Job}.
(** Let j be the job to be analyzed. *)
Variable j : Job.
(** Recall the notion of a job of higher or equal priority. *)
- Let of_higher_or_equal_priority j_hp :=
- (* [FIXME]: should be using [hep_job]! *)
- higher_eq_priority j_hp j.
+ Let of_higher_or_equal_priority j_hp := hep_job j_hp j.
(** Then, we define the workload of higher or equal priority of all jobs
with higher-or-equal priority than j. *)
diff --git a/restructuring/results/edf/rta/bounded_nps.v b/restructuring/results/edf/rta/bounded_nps.v
index 1cf857f23a2de096ee534916e43292bbc69bbe31..96e0dd951c8223172ab1dbb02d5bcca07c43918e 100644
--- a/restructuring/results/edf/rta/bounded_nps.v
+++ b/restructuring/results/edf/rta/bounded_nps.v
@@ -134,7 +134,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** Let's define some local names for clarity. *)
Let max_length_of_priority_inversion :=
- max_length_of_priority_inversion arr_seq EDF.
+ max_length_of_priority_inversion arr_seq.
Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
Let bound_on_total_hep_workload_changes_at :=
bound_on_total_hep_workload_changes_at ts tsk.
@@ -203,7 +203,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** 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:
- priority_inversion_is_bounded_by arr_seq sched _ tsk blocking_bound.
+ priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound.
Proof.
move => j ARR TSK POS t1 t2 PREF; move: (PREF) => [_ [_ [_ /andP [T _]]]].
destruct (leqP (t2 - t1) blocking_bound) as [NEQ|NEQ].
@@ -212,11 +212,11 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat.
rewrite leq_sum //.
intros t _; case: (sched t); last by done.
- by intros s; case: edf.EDF.
+ by intros s; destruct (hep_job s j).
}
edestruct @preemption_time_exists as [ppt [PPT NEQ2]]; eauto 2 with basic_facts.
move: NEQ2 => /andP [GE LE].
- apply leq_trans with (cumulative_priority_inversion sched _ j t1 ppt);
+ apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
last apply leq_trans with (ppt - t1).
- rewrite /cumulative_priority_inversion /is_priority_inversion.
rewrite (@big_cat_nat _ _ _ ppt) //=; last first.
@@ -239,10 +239,10 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
rewrite -[X in _ <= X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat.
rewrite leq_sum //.
intros t _; case: (sched t); last by done.
- by intros s; case: edf.EDF.
+ by intros s; destruct (hep_job s j).
- rewrite leq_subLR.
apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
- rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+ by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
Qed.
End PriorityInversionIsBounded.
diff --git a/restructuring/results/edf/rta/bounded_pi.v b/restructuring/results/edf/rta/bounded_pi.v
index 3a744cea66c0973e173e08796468745a16ec6296..f8cbcdcaeb2aec64893bf942f6d2ed9f75633823 100644
--- a/restructuring/results/edf/rta/bounded_pi.v
+++ b/restructuring/results/edf/rta/bounded_pi.v
@@ -139,7 +139,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
Variable priority_inversion_bound : duration.
Hypothesis H_priority_inversion_is_bounded:
priority_inversion_is_bounded_by
- arr_seq sched _ tsk priority_inversion_bound.
+ arr_seq sched tsk priority_inversion_bound.
(** Let L be any positive fixed point of the busy interval recurrence. *)
Variable L : duration.
@@ -196,13 +196,13 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** 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. *)
Let interference (j : Job) (t : instant) :=
- ideal_jlfp_rta.interference sched EDF j t.
+ ideal_jlfp_rta.interference sched 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. *)
Let interfering_workload (j : Job) (t : instant) :=
- ideal_jlfp_rta.interfering_workload arr_seq sched EDF j t.
+ ideal_jlfp_rta.interfering_workload arr_seq sched j t.
(** Finally, we define the interference bound function as the sum of the priority
interference bound and the higher-or-equal-priority workload. *)
@@ -246,7 +246,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
/is_interference_from_another_hep_job
HYP negb_or; apply/andP; split.
- - by rewrite Bool.negb_involutive /edf.EDF.
+ - by rewrite Bool.negb_involutive; eapply (EDF_is_reflexive 0).
- by rewrite negb_and Bool.negb_involutive; apply/orP; right.
}
Qed.
@@ -270,7 +270,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
apply QT; try done.
- eapply in_arrivals_implies_arrived; eauto 2.
- unfold edf.EDF, EDF; move: TSKs => /eqP TSKs.
- rewrite /job_deadline /job_deadline_from_task_deadline TSK TSKs leq_add2r.
+ rewrite /job_deadline /job_deadline_from_task_deadline /hep_job TSK TSKs leq_add2r.
by apply leq_trans with t1; [apply ltnW | ].
Qed.
@@ -336,10 +336,10 @@ Section AbstractRTAforEDFwithArrivalCurves.
[priority_inversion_bound] bounds cumulative priority inversion
follows from assumption [H_priority_inversion_is_bounded]. *)
Lemma cumulative_priority_inversion_is_bounded:
- cumulative_priority_inversion sched EDF j t1 (t1 + Δ) <= priority_inversion_bound.
+ cumulative_priority_inversion sched j t1 (t1 + Δ) <= priority_inversion_bound.
Proof.
unfold priority_inversion_is_bounded_by, EDF in *.
- apply leq_trans with (cumulative_priority_inversion sched _ j t1 t2).
+ apply leq_trans with (cumulative_priority_inversion sched j t1 t2).
- rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + Δ)) //=.
+ by rewrite leq_addr.
+ by rewrite /is_priority_inversion leq_addr.
@@ -360,15 +360,16 @@ Section AbstractRTAforEDFwithArrivalCurves.
other tasks. Which in turn means that cumulative
interference is bounded by service. *)
Lemma cumulative_interference_is_bounded_by_total_service:
- cumulative_interference_from_hep_jobs_from_other_tasks sched EDF j t1 (t1 + Δ)
+ cumulative_interference_from_hep_jobs_from_other_tasks sched j t1 (t1 + Δ)
<= service_of_jobs sched (EDF_not_from tsk) jobs t1 (t1 + Δ).
Proof.
move: (H_busy_interval) => [[/andP [JINBI JINBI2] [QT _]] _].
erewrite instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks;
eauto 2 with basic_facts.
- by rewrite -H_job_of_tsk /jobs.
- - by rewrite /edf.EDF /EDF instantiated_quiet_time_equivalent_quiet_time //;
- eauto 2 with basic_facts.
+ - rewrite /edf.EDF /EDF instantiated_quiet_time_equivalent_quiet_time //.
+ + by apply EDF_is_reflexive.
+ + by apply EDF_respects_sequential_tasks.
Qed.
(** By lemma [service_of_jobs_le_workload], the total
@@ -577,7 +578,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
- exfalso; move: NCOMPL => /negP COMPL; apply: COMPL.
by rewrite /completed_by /completed_by ZERO.
- move: (BUSY) => [[/andP [JINBI JINBI2] [QT _]] _].
- rewrite (cumulative_task_interference_split arr_seq sched _ _ _ tsk j);
+ rewrite (cumulative_task_interference_split arr_seq sched _ _ tsk j);
eauto 2 with basic_facts; last first.
{ by eapply arrived_between_implies_in_arrivals; eauto. }
rewrite /I leq_add //.
diff --git a/restructuring/results/fixed_priority/rta/bounded_nps.v b/restructuring/results/fixed_priority/rta/bounded_nps.v
index cf4d6dcbb176fce2145634684efad50ff6a717a8..58e4da3ee2b6de0c03ea3b97c9362d9df6665494 100644
--- a/restructuring/results/fixed_priority/rta/bounded_nps.v
+++ b/restructuring/results/fixed_priority/rta/bounded_nps.v
@@ -62,7 +62,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority
relation, and assume that the relation is reflexive and
transitive. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -112,15 +112,15 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** Let's define some local names for clarity. *)
Let max_length_of_priority_inversion :=
- max_length_of_priority_inversion arr_seq _.
+ max_length_of_priority_inversion arr_seq.
Let task_rbf := task_request_bound_function tsk.
- Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
- Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+ Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+ Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
(** We also define a bound for the priority inversion caused by jobs with lower priority. *)
Definition blocking_bound :=
- \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk)
+ \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
(task_max_nonpreemptive_segment tsk_other - ε).
(** ** Priority inversion is bounded *)
@@ -142,9 +142,9 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
/priority_inversion.max_length_of_priority_inversion.
apply leq_trans with
(\max_(j_lp <- arrivals_between arr_seq 0 t
- | ~~ higher_eq_priority (job_task j_lp) tsk)
+ | ~~ hep_task (job_task j_lp) tsk)
(task_max_nonpreemptive_segment (job_task j_lp) - ε)).
- { rewrite TSK.
+ { rewrite /hep_job TSK.
apply leq_big_max.
intros j' JINB NOTHEP.
rewrite leq_sub2r //.
@@ -164,7 +164,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(** 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
- arr_seq sched _ tsk blocking_bound.
+ arr_seq sched tsk blocking_bound.
Proof.
intros j ARR TSK POS t1 t2 PREF.
case NEQ: (t2 - t1 <= blocking_bound).
@@ -172,11 +172,11 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
rewrite /cumulative_priority_inversion /is_priority_inversion.
rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat leq_sum //.
intros t _; case: (sched t); last by done.
- by intros s; case: (FP_to_JLFP Job Task s j).
+ by intros s; case: (hep_job s j).
}
move: NEQ => /negP /negP; rewrite -ltnNge; move => BOUND.
edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2; move: NEQ => /andP [GE LE].
- apply leq_trans with (cumulative_priority_inversion sched _ j t1 ppt);
+ apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
last apply leq_trans with (ppt - t1); first last.
- rewrite leq_subLR.
apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
@@ -184,7 +184,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
- rewrite /cumulative_priority_inversion /is_priority_inversion.
rewrite -[X in _ <= X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat.
rewrite leq_sum //; intros t _; case: (sched t); last by done.
- by intros s; case: (FP_to_JLFP Job Task s j).
+ by intros s; case: (hep_job s j).
- rewrite /cumulative_priority_inversion /is_priority_inversion.
rewrite (@big_cat_nat _ _ _ ppt) //=; last first.
{ rewrite ltn_subRL in BOUND.
diff --git a/restructuring/results/fixed_priority/rta/bounded_pi.v b/restructuring/results/fixed_priority/rta/bounded_pi.v
index db9dc4e8e8c14b39a2378df032d635cd6cb85ae3..184a7948633eb7834a061b6154fca14445f56161 100644
--- a/restructuring/results/fixed_priority/rta/bounded_pi.v
+++ b/restructuring/results/fixed_priority/rta/bounded_pi.v
@@ -105,7 +105,7 @@ Section AbstractRTAforFPwithArrivalCurves.
Interference and Interfering Workload that actively use the concept of
priorities. We require the FP policy to be reflexive, so a job cannot
cause lower-priority interference (i.e. priority inversion) to itself. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
(** For clarity, let's define some local names. *)
@@ -121,12 +121,12 @@ Section AbstractRTAforFPwithArrivalCurves.
(** Using the sum of individual request bound functions, we define the request bound
function of all tasks with higher-or-equal priority (with respect to [tsk]). *)
- Let total_hep_rbf := total_hep_request_bound_function_FP higher_eq_priority ts tsk.
+ Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
(** Similarly, we define the request bound function of all tasks other
than [tsk] with higher-or-equal priority (with respect to [tsk]). *)
Let total_ohep_rbf :=
- total_ohep_request_bound_function_FP higher_eq_priority ts tsk.
+ total_ohep_request_bound_function_FP ts tsk.
(** Assume that there exists a constant priority_inversion_bound that bounds
the length of any priority inversion experienced by any job of [tsk].
@@ -135,7 +135,7 @@ Section AbstractRTAforFPwithArrivalCurves.
Variable priority_inversion_bound : duration.
Hypothesis H_priority_inversion_is_bounded:
priority_inversion_is_bounded_by
- arr_seq sched hep_job tsk priority_inversion_bound.
+ arr_seq sched tsk priority_inversion_bound.
(** Let L be any positive fixed point of the busy interval recurrence. *)
Variable L : duration.
@@ -164,15 +164,14 @@ Section AbstractRTAforFPwithArrivalCurves.
(** 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. *)
Let interference (j : Job) (t : instant) :=
- ideal_jlfp_rta.interference sched hep_job j t.
+ ideal_jlfp_rta.interference sched 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. *)
Let interfering_workload (j : Job) (t : instant) :=
- ideal_jlfp_rta.interfering_workload
- arr_seq sched (@FP_to_JLFP Job Task H1 higher_eq_priority) j t.
+ ideal_jlfp_rta.interfering_workload arr_seq sched j t.
(** Finally, we define the interference bound function as the sum of the priority
interference bound and the higher-or-equal-priority workload. *)
@@ -226,8 +225,8 @@ Section AbstractRTAforFPwithArrivalCurves.
apply QT.
- by apply in_arrivals_implies_arrived in ARRs.
- move: TSKs => /eqP TSKs.
- rewrite /FP_to_JLFP TSK -TSKs; eauto 2.
- by eapply H_priority_is_reflexive with (t := 0).
+ rewrite /hep_job /FP_to_JLFP TSK -TSKs; eauto 2.
+ by eapply (H_priority_is_reflexive 0); eauto.
- by eapply in_arrivals_implies_arrived_before; eauto 2.
Qed.
@@ -274,11 +273,10 @@ Section AbstractRTAforFPwithArrivalCurves.
{ move: BUSY => [[_ [_ [_ /andP [GE LT]]]] _].
by eapply arrived_between_implies_in_arrivals; eauto 2. }
unfold IBF, interference.
- apply respects_sequential_tasks; by done.
rewrite leq_add; try done.
{ move: (H_priority_inversion_is_bounded j ARR TSK) => BOUND.
- apply leq_trans with (cumulative_priority_inversion sched _ j t1 (t1 + R0)); first by done.
- apply leq_trans with (cumulative_priority_inversion sched _ j t1 t2); last first.
+ apply leq_trans with (cumulative_priority_inversion sched j t1 (t1 + R0)); first by done.
+ apply leq_trans with (cumulative_priority_inversion sched j t1 t2); last first.
{ by apply BOUND; move: BUSY => [PREF QT2]. }
rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + R0)) //=.
- by rewrite leq_addr.
diff --git a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
index ecc40a71fff7083698e6441bd73200bdb616c60b..4bb73c0f0900e1fe1b0f6ae5ad2d8a4cb8cd9653 100644
--- a/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -75,7 +75,7 @@ Section RTAforFloatingModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -92,13 +92,13 @@ Section RTAforFloatingModelwithArrivalCurves.
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
- Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
- Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+ Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+ Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
(** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
Let blocking_bound :=
- \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk)
+ \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
(task_max_nonpreemptive_segment tsk_other - ε).
(** Let L be any positive fixed point of the busy interval recurrence, determined by
diff --git a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
index 50b498aa3bad97b5cbe13a0ca23f6df8df40d8a9..0cf5969b488f0dca2f585fedbd38b8930ca61d3f 100644
--- a/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -66,14 +66,14 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
- Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
- Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+ Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+ Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
(** Assume we have sequential tasks, i.e, tasks from the same task
@@ -90,7 +90,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
Let blocking_bound :=
- \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk) (task_cost tsk_other - ε).
+ \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_cost tsk_other - ε).
(** Let L be any positive fixed point of the busy interval recurrence, determined by
the sum of blocking and higher-or-equal-priority workload. *)
diff --git a/restructuring/results/fixed_priority/rta/fully_preemptive.v b/restructuring/results/fixed_priority/rta/fully_preemptive.v
index 34d4e11aa36d762813d14e950e090ae6da259bdf..9195c46eeaf81cf274c634039219e607d74e7341 100644
--- a/restructuring/results/fixed_priority/rta/fully_preemptive.v
+++ b/restructuring/results/fixed_priority/rta/fully_preemptive.v
@@ -64,7 +64,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -81,8 +81,8 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
- Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
- Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+ Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+ Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
(** Let L be any positive fixed point of the busy interval recurrence, determined by
@@ -109,7 +109,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
Theorem uniprocessor_response_time_bound_fully_preemptive_fp:
response_time_bounded_by tsk R.
Proof.
- have BLOCK: blocking_bound higher_eq_priority ts tsk = 0.
+ have BLOCK: blocking_bound ts tsk = 0.
{ by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
/fully_preemptive.fully_preemptive_model subnn big1_eq. }
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
diff --git a/restructuring/results/fixed_priority/rta/limited_preemptive.v b/restructuring/results/fixed_priority/rta/limited_preemptive.v
index 735a3dd1a53dcf50a0dd9045188fba10e7bac16f..19fa54b29cbf2cdccfa223a3294b6be1d92cfa87 100644
--- a/restructuring/results/fixed_priority/rta/limited_preemptive.v
+++ b/restructuring/results/fixed_priority/rta/limited_preemptive.v
@@ -74,7 +74,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
(** Consider an FP policy that indicates a higher-or-equal priority relation,
and assume that the relation is reflexive and transitive. *)
- Variable higher_eq_priority : FP_policy Task.
+ Context `{FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
@@ -91,13 +91,13 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
(** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
- Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
- Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+ Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+ Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
(** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
Let blocking_bound :=
- \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk)
+ \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
(task_max_nonpreemptive_segment tsk_other - ε).
(** Let L be any positive fixed point of the busy interval recurrence, determined by