Commit 4c91dcff authored by Sergey Bozhko's avatar Sergey Bozhko Committed by Björn Brandenburg

Use Context declaration for priority type classes

parent a5393afb
......@@ -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.
......
......@@ -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. *)
......
......@@ -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.
......
......@@ -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
......
......@@ -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].
......
......@@ -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. }
......
......@@ -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.
......
......@@ -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].
......
......@@ -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) :=
......
......@@ -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.