diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
new file mode 100644
index 0000000000000000000000000000000000000000..253ed20de8ff35b2899cd6a55acabfc6b8fc76f1
--- /dev/null
+++ b/model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v
@@ -0,0 +1,632 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+ rt.model.arrival.basic.task_arrival
+ rt.model.priority.
+Require Import rt.model.schedule.uni.service
+ rt.model.schedule.uni.workload
+ rt.model.schedule.uni.schedule
+ rt.model.schedule.uni.response_time.
+Require Import rt.model.schedule.uni.limited.schedule
+ rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound
+ rt.model.schedule.uni.limited.rbf.
+Require Import rt.model.arrival.curves.bounds
+ rt.analysis.uni.arrival_curves.workload_bound.
+Require Import rt.model.schedule.uni.nonpreemptive.schedule
+ rt.model.schedule.uni.limited.platform.limited
+ rt.model.schedule.uni.limited.platform.preemptive
+ rt.model.schedule.uni.limited.platform.nonpreemptive.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for concrete models *)
+(** In this module we prove the RTA theorems for (1) fully preemptive FP model,
+ (2) fully nonpreemptive FP model, (3) FP with fixed premption points, and
+ (4) FP with floating nonpreemptive regions. *)
+Module RTAforConcreteModels.
+
+ Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
+ ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
+ RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves NonpreemptiveSchedule
+ FullyNonPreemptivePlatform FullyPreemptivePlatform.
+
+ Section Analysis.
+
+ Context {Task: eqType}.
+ Variable task_cost: Task -> time.
+
+ Context {Job: eqType}.
+ Variable job_arrival: Job -> time.
+ Variable job_cost: Job -> time.
+ Variable job_task: Job -> Task.
+
+ (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+ Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+ (* Consider an arbitrary task set ts. *)
+ Variable ts: list Task.
+
+ (* Assume that all jobs come from the task set... *)
+ Hypothesis H_all_jobs_from_taskset:
+ forall j, arrives_in arr_seq j -> job_task j \in ts.
+
+ (* ...and the cost of a job cannot be larger than the task cost. *)
+ Hypothesis H_job_cost_le_task_cost:
+ cost_of_jobs_from_arrival_sequence_le_task_cost
+ task_cost job_cost job_task arr_seq.
+
+ (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts
+ [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
+ that equals 0 for the empty interval delta = 0. *)
+ Variable max_arrivals: Task -> time -> nat.
+ Hypothesis H_family_of_proper_arrival_curves:
+ family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
+
+ (* Let tsk be any task in ts that is to be analyzed. *)
+ Variable tsk: Task.
+ Hypothesis H_tsk_in_ts: tsk \in ts.
+
+ (* Next, consider any uniprocessor schedule... *)
+ Variable sched: schedule Job.
+ Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+
+ (* ... where jobs do not execute before their arrival nor after completion. *)
+ Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+ Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+ (* We also assume that the schedule is a work-conserving schedule. *)
+ Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+
+ (* Assume we have sequential jobs, i.e, jobs from the same
+ task execute in the order of their arrival. *)
+ Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
+
+ (* 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.
+ Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+
+ (* Let's define some local names for clarity. *)
+ Let response_time_bounded_by :=
+ is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
+ Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
+ Let total_hep_rbf :=
+ total_hep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
+ Let total_ohep_rbf :=
+ total_ohep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
+
+ (** * RTA for fully preemptive FP model *)
+ (** In this module we prove the RTA theorem for fully preemptive FP model *)
+ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
+
+ (* First, we assume that the schedule respects the FP policy under a fully preemptive model. *)
+ Hypothesis H_respects_policy:
+ respects_FP_policy_at_preemption_point
+ job_arrival job_cost job_task arr_seq sched
+ (can_be_preempted_for_fully_preemptive_model) higher_eq_priority.
+
+ (* Let L be any positive fixed point of the busy interval recurrence, determined by
+ the sum of blocking and higher-or-equal-priority workload. *)
+ Variable L: time.
+ Hypothesis H_L_positive: L > 0.
+ Hypothesis H_fixed_point: L = total_hep_rbf L.
+
+ (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+ Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
+
+ (* Next, consider any value R, and assume that for any given arrival A from search space
+ there is a solution of the response-time bound recurrence which is bounded by R. *)
+ Variable R: nat.
+ Hypothesis H_R_is_maximum:
+ forall A,
+ is_in_search_space A ->
+ exists F,
+ A + F = task_rbf (A + ε) + total_ohep_rbf (A + F) /\
+ F <= R.
+
+ (* Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
+ to establish a response-time bound for the more concrete model of fully preemptive scheduling. *)
+ Theorem uniprocessor_response_time_bound_fully_preemptive_fp:
+ response_time_bounded_by tsk R.
+ Proof.
+ have BLOCK: RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.blocking_bound (fun _ => ε) higher_eq_priority ts tsk = 0.
+ { by rewrite /RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.blocking_bound subnn big1_eq. }
+ eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
+ (task_max_nps := fun _ => ε)
+ (can_be_preempted := fun j prog => true)
+ (task_lock_in_service := fun tsk => task_cost tsk)
+ (job_lock_in_service := fun j => job_cost j)
+ (job_max_nps := fun j => ε); eauto 2; try done.
+ - by eapply fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions.
+ - repeat split; try done.
+ intros ? ? ? ARR; move => LE COMPL /negP NCOMPL.
+ exfalso; apply: NCOMPL.
+ apply completion_monotonic with t; try done.
+ rewrite /completed_by eqn_leq; apply/andP; split; try done.
+ - repeat split; try done.
+ rewrite /task_lock_in_service_le_task_cost. by done.
+ unfold task_lock_in_service_bounds_job_lock_in_service.
+ by intros ? ARR TSK; rewrite -TSK; apply H_job_cost_le_task_cost.
+ - by rewrite BLOCK add0n.
+ - move => A /andP [LT NEQ].
+ specialize (H_R_is_maximum A); feed H_R_is_maximum.
+ { by apply/andP; split. }
+ move: H_R_is_maximum => [F [FIX BOUND]].
+ exists F; split.
+ + by rewrite BLOCK add0n subnn subn0.
+ + by rewrite subnn addn0.
+ Qed.
+
+ End RTAforFullyPreemptiveFPModelwithArrivalCurves.
+
+ (** * RTA for fully nonpreemptive FP model *)
+ (** In this module we prove the RTA theorem for the fully nonpreemptive FP model. *)
+ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
+
+ (* First, assume that the schedule is nonpreemptive... *)
+ Hypothesis H_nonpreemptive_sched: is_nonpreemptive_schedule job_cost sched.
+
+ (* ... which respects the FP policy under a fully nonpreemptive model. *)
+ Hypothesis H_respects_policy:
+ respects_FP_policy_at_preemption_point
+ job_arrival job_cost job_task arr_seq sched
+ (can_be_preempted_for_fully_nonpreemptive_model job_cost) higher_eq_priority.
+
+ (* 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 - ε).
+
+ (* Let L be any positive fixed point of the busy interval recurrence, determined by
+ the sum of blocking and higher-or-equal-priority workload. *)
+ Variable L: time.
+ Hypothesis H_L_positive: L > 0.
+ Hypothesis H_fixed_point: L = blocking_bound + total_hep_rbf L.
+
+ (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+ Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
+
+ (* Next, consider any value R, and assume that for any given arrival A from search space
+ there is a solution of the response-time bound recurrence which is bounded by R. *)
+ Variable R: nat.
+ Hypothesis H_R_is_maximum:
+ forall A,
+ is_in_search_space A ->
+ exists F,
+ A + F = blocking_bound
+ + (task_rbf (A + ε) - (task_cost tsk - ε))
+ + total_ohep_rbf (A + F) /\
+ F + (task_cost tsk - ε) <= R.
+
+ (* Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
+ to establish a response-time bound for the more concrete model of fully nonpreemptive scheduling. *)
+ Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp:
+ response_time_bounded_by tsk R.
+ Proof.
+ move: (posnP (task_cost tsk)) => [ZERO|POS].
+ { intros j ARR TSK.
+ have ZEROj: job_cost j = 0.
+ { move: (H_job_cost_le_task_cost j ARR) => NEQ.
+ rewrite /job_cost_le_task_cost TSK ZERO in NEQ.
+ by apply/eqP; rewrite -leqn0.
+ }
+ rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
+ - by apply H_completed_jobs_dont_execute.
+ - by rewrite ZEROj.
+ }
+ eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
+ (job_max_nps := fun j => job_cost j)
+ (task_max_nps := fun tsk => task_cost tsk)
+ (job_lock_in_service := fun j => ε)
+ (task_lock_in_service := fun tsk => ε)
+ (L0 := L); eauto 2.
+ - by eapply fully_nonpreemptive_model_is_correct; eauto 2.
+ - eapply fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions; eauto 2.
+ - repeat split; try done.
+ - intros j t t' ARR LE SERV NCOMPL.
+ rewrite /service in SERV; apply incremental_service_during in SERV.
+ move: SERV => [t_first [/andP [_ H1] [H2 H3]]].
+ apply H_nonpreemptive_sched with t_first; try done.
+ by apply leq_trans with t; first apply ltnW.
+ - repeat split; try done.
+ Qed.
+
+ End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
+
+ (** * RTA for FP-schedulers with fixed premption points *)
+ (** In this module we prove a general RTA theorem for FP-schedulers with fixed preemption points *)
+ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
+
+ (* First, we assume we have the model with fixed preemption points.
+ I.e., each task is divided into a number of nonpreemptive segments
+ by inserting staticaly predefined preemption points. *)
+ Variable job_preemption_points: Job -> seq time.
+ Variable task_preemption_points: Task -> seq time.
+ Hypothesis H_model_with_fixed_preemption_points:
+ fixed_preemption_points_model
+ task_cost job_cost job_task arr_seq
+ job_preemption_points task_preemption_points ts.
+
+ (* Next, assume that the schedule is a schedule with limited preemptions... *)
+ Hypothesis H_schedule_with_limited_preemptions:
+ is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.
+
+ (* ... which respects the FP policy under a model with fixed preemption points. *)
+ Hypothesis H_respects_policy:
+ respects_FP_policy_at_preemption_point
+ job_arrival job_cost job_task arr_seq sched
+ (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.
+
+ (* We also have a set of functions that map job or task
+ to its max or last nonpreemptive segment. *)
+ Let job_max_nps := job_max_nps job_preemption_points.
+ Let job_last_nps := job_last_nps job_preemption_points.
+ Let task_max_nps := task_max_nps task_preemption_points.
+ Let task_last_nps := task_last_nps task_preemption_points.
+
+ (* 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_max_nps 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. *)
+ Variable L: time.
+ Hypothesis H_L_positive: L > 0.
+ Hypothesis H_fixed_point: L = blocking_bound + total_hep_rbf L.
+
+ (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+ Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
+
+ (* Next, consider any value R, and assume that for any given arrival A from search space
+ there is a solution of the response-time bound recurrence which is bounded by R. *)
+ Variable R: nat.
+ Hypothesis H_R_is_maximum:
+ forall A,
+ is_in_search_space A ->
+ exists F,
+ A + F = blocking_bound
+ + (task_rbf (A + ε) - (task_last_nps tsk - ε))
+ + total_ohep_rbf (A + F) /\
+ F + (task_last_nps tsk - ε) <= R.
+
+ (* Now, we can reuse the results for the abstract model with bounded nonpreemptive segments
+ to establish a response-time bound for the more concrete model of fixed preemption points. *)
+ Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
+ response_time_bounded_by tsk R.
+ Proof.
+ move: (H_model_with_fixed_preemption_points) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
+ move: (MLP) => [EMPTj [LSMj [BEGj [ENDj HH]]]].
+ move: (posnP (task_cost tsk)) => [ZERO|POSt].
+ { intros j ARR TSK.
+ move: (H_job_cost_le_task_cost _ ARR) => POSt.
+ move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
+ rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
+ - by eauto 2.
+ - by rewrite Z.
+ }
+ have Fact2: 1 < size (task_preemption_points tsk).
+ { have Fact2: 0 < size (task_preemption_points tsk).
+ { apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
+ move: (END _ H_tsk_in_ts) => EQ.
+ move: EQ; rewrite /NondecreasingSequence.last -nth_last nth_default; last by rewrite CONTR.
+ by intros; rewrite -EQ in POSt.
+ }
+ have EQ: 2 = size [::0; task_cost tsk]; first by done.
+ rewrite EQ; clear EQ.
+ apply subseq_leq_size.
+ rewrite !cons_uniq.
+ { apply/andP; split.
+ rewrite in_cons negb_or; apply/andP; split; last by done.
+ rewrite neq_ltn; apply/orP; left; eauto 2.
+ apply/andP; split; by done. }
+ intros t EQ; move: EQ; rewrite !in_cons.
+ move => /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
+ { rewrite EQ; clear EQ.
+ move: (BEG _ H_tsk_in_ts) => EQ.
+ rewrite -EQ; clear EQ.
+ rewrite /NondecreasingSequence.first -nth0.
+ apply/(nthP 0).
+ exists 0; by done.
+ }
+ { rewrite EQ; clear EQ.
+ move: (END _ H_tsk_in_ts) => EQ.
+ rewrite -EQ; clear EQ.
+ rewrite /NondecreasingSequence.last -nth_last.
+ apply/(nthP 0).
+ exists ((size (task_preemption_points tsk)).-1); last by done.
+ by rewrite -(leq_add2r 1) !addn1 prednK //.
+ }
+ }
+ eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
+ with (task_lock_in_service := fun tsk => (task_cost tsk - (task_last_nps tsk - ε)))
+ (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+ (L0 := L) (job_max_nps0 := job_max_nps)
+ (job_cost0 := job_cost )
+ ; eauto 2.
+ { by apply model_with_fixed_preemption_points_is_correct. }
+ {
+ eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2.
+ intros j ARR.
+ unfold ModelWithLimitedPreemptions.job_max_nps, task_max_nps, lengths_of_segments.
+ apply NondecreasingSequence.max_of_dominating_seq.
+ intros. apply HYP2.
+ by done.
+ }
+ { split; last split.
+ { intros j ARR POS.
+ rewrite subn_gt0.
+ rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
+ apply LSMj; try done.
+ rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
+ ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
+ apply leq_trans with (job_max_nps j);
+ first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
+ rewrite -ENDj; last by done.
+ by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ }
+ { by intros j ARR; rewrite leq_subLR leq_addl. }
+ { intros ? ? ? ARR LE LS NCOMPL.
+ rewrite subnBA in LS; last first.
+ apply LSMj; try done.
+ { rewrite lt0n; apply/negP; intros Z; move: Z => /eqP Z.
+ move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [LT|GT].
+ { by rewrite Z ltn0 in LT. }
+ { move: GT; rewrite ltnNge; move => /negP GT; apply: GT.
+ by eapply H_completed_jobs_dont_execute.
+ }
+ }
+ have EQ: exists Δ, t' = t + Δ.
+ { exists (t' - t); rewrite subnKC; by done. }
+ move: EQ => [Δ EQ]; subst t'; clear LE.
+ rewrite -subh1 in LS.
+ rewrite addn1 in LS.
+ apply H_schedule_with_limited_preemptions; first by done.
+ rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
+ intros CONTR.
+ move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [SERV|SERV]; last first.
+ { exfalso.
+ move: (H_completed_jobs_dont_execute j (t + Δ)); rewrite leqNgt; move => /negP T.
+ by apply: T.
+ }
+ { have NEQ: job_cost j - job_last_nps j < service sched j (t + Δ).
+ { apply leq_trans with (service sched j t); first by done.
+ rewrite /service /service_during [in X in _ <= X](@big_cat_nat _ _ _ t) //=.
+ rewrite leq_addr //.
+ rewrite leq_addr //.
+ }
+ clear LS.
+ rewrite -ENDj in NEQ, SERV; last by done.
+ rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ; last by eauto 2.
+ rewrite /NondecreasingSequence.last -nth_last in SERV.
+ have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
+ specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
+ rewrite CONTR in EQ.
+ feed_n 2 EQ; first by eauto 2.
+ {
+ apply/andP; split; first by done.
+ rewrite prednK; first by done.
+ rewrite -(leq_add2r 1) !addn1 prednK.
+ eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
+ eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2.
+ }
+ by done.
+ }
+ rewrite -ENDj; last by done.
+ apply leq_trans with (job_max_nps j).
+ - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
+ - by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ }
+ }
+ {
+ split.
+ - by rewrite /task_lock_in_service_le_task_cost leq_subLR leq_addl.
+ - intros j ARR TSK.
+ move: (posnP (job_cost j)) => [ZERO | POS].
+ { by rewrite ZERO. }
+ unfold task_last_nps.
+ rewrite !subnBA; first last.
+ apply LSMj; try done.
+ rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
+ apply HYP3.
+ by done.
+ rewrite -(ltn_add2r 1) !addn1 prednK //.
+ move: (Fact2) => Fact3.
+ rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
+ rewrite -subh1 -?[in X in _ <= X]subh1; first last.
+ { apply leq_trans with (job_max_nps j).
+ - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
+ - by rewrite -ENDj //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ }
+ { apply leq_trans with (task_max_nps tsk).
+ - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
+ - by rewrite -END //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ }
+ rewrite -ENDj; last eauto 2.
+ rewrite -END; last eauto 2.
+ rewrite !NondecreasingSequence.last_seq_minus_last_distance_seq.
+ have EQ: size (job_preemption_points j) = size (task_preemption_points tsk).
+ { rewrite -TSK.
+ by apply HYP1.
+ }
+ rewrite EQ; clear EQ.
+ rewrite leq_add2r.
+ apply NondecreasingSequence.domination_of_distances_implies_domination_of_seq; try done; eauto 2.
+ rewrite BEG // BEGj //.
+ eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
+ rewrite -TSK; apply HYP1; try done.
+ intros. rewrite -TSK; eauto 2.
+ eauto 2.
+ eauto 2.
+ }
+ { rewrite subKn; first by done.
+ rewrite /task_last_nps -(leq_add2r 1) subn1 !addn1 prednK; last first.
+ { rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
+ apply HYP3; try by done.
+ rewrite -(ltn_add2r 1) !addn1 prednK //.
+ move: (Fact2) => Fact3.
+ by rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
+ }
+ { apply leq_trans with (task_max_nps tsk).
+ - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
+ - rewrite -END; last by done.
+ apply ltnW; rewrite ltnS; try done.
+ by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ }
+ }
+ Qed.
+
+ End RTAforFixedPreemptionPointsModelwithArrivalCurves.
+
+ (** * RTA for FP-schedulers with floating nonpreemptive regions *)
+ (** In this module we prove a general RTA theorem for FP-schedulers with floating nonpreemptive regions *)
+ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
+
+ (* Assume we have the model with floating nonpreemptive regions.
+ I.e., for each task only the length of the maximal nonpreemptive
+ segment is known. *)
+ Variable job_preemption_points: Job -> seq time.
+ Variable task_max_nps: Task -> time.
+ Hypothesis H_task_model_with_floating_nonpreemptive_regions:
+ model_with_floating_nonpreemptive_regions
+ job_cost job_task arr_seq job_preemption_points task_max_nps.
+
+ (* Next, assume that the schedule is a schedule with limited preemptions... *)
+ Hypothesis H_schedule_with_limited_preemptions:
+ is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.
+
+ (* ... which respects the FP policy under a model with fixed preemption points. *)
+ Hypothesis H_respects_policy:
+ respects_FP_policy_at_preemption_point
+ job_arrival job_cost job_task arr_seq sched
+ (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.
+
+ (* Let's define some local names for clarity. *)
+ Let job_max_nps := job_max_nps job_preemption_points.
+ Let job_last_nps := job_last_nps job_preemption_points.
+
+ (* 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_max_nps 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. *)
+ Variable L: time.
+ Hypothesis H_L_positive: L > 0.
+ Hypothesis H_fixed_point: L = blocking_bound + total_hep_rbf L.
+
+ (* To reduce the time complexity of the analysis, recall the notion of search space. *)
+ Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
+
+ (* Next, consider any value R, and assume that for any given arrival A from search space
+ there is a solution of the response-time bound recurrence which is bounded by R. *)
+ Variable R: nat.
+ Hypothesis H_R_is_maximum:
+ forall A,
+ is_in_search_space A ->
+ exists F,
+ A + F = blocking_bound + task_rbf (A + ε) + total_ohep_rbf (A + F) /\
+ F <= R.
+
+ (* Now, we can reuse the results for the abstract model with bounded nonpreemptive segments
+ to establish a response-time bound for the more concrete model with floating nonpreemptive regions. *)
+ Theorem uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions:
+ response_time_bounded_by tsk R.
+ Proof.
+ move: (H_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
+ move: (LIMJ) => [ZERO [LSMj [BEG [END HH]]]].
+ eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
+ with (task_lock_in_service := fun tsk => task_cost tsk)
+ (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
+ (L0 := L) (job_max_nps0 := job_max_nps)
+ (job_cost0 := job_cost )
+ ; eauto 2.
+ { by apply model_with_fixed_preemption_points_is_correct. }
+ { by eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2. }
+ { split; last split.
+ { intros j ARR POS.
+ rewrite subn_gt0.
+ rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
+ apply LSMj; try done.
+ rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
+ ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
+ apply leq_trans with (job_max_nps j); first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
+ rewrite -END; last by done.
+ by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ }
+ { by intros j ARR; rewrite leq_subLR leq_addl. }
+ { intros ? ? ? ARR LE LS NCOMPL.
+ rewrite subnBA in LS; last first.
+ apply LSMj; try done.
+ { rewrite lt0n; apply/negP; intros Z; move: Z => /eqP Z.
+ move: NCOMPL. rewrite /completed_by neq_ltn. move => /orP [LT|GT].
+ { by rewrite Z ltn0 in LT. }
+ { move: GT; rewrite ltnNge; move => /negP GT; apply: GT.
+ by eapply H_completed_jobs_dont_execute.
+ }
+ }
+ have EQ: exists Δ, t' = t + Δ.
+ { exists (t' - t); rewrite subnKC; by done. }
+ move: EQ => [Δ EQ]; subst t'; clear LE.
+ rewrite -subh1 in LS.
+ rewrite addn1 in LS.
+ apply H_schedule_with_limited_preemptions; first by done.
+ rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
+ intros CONTR.
+ move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [SERV|SERV]; last first.
+ { exfalso.
+ move: (H_completed_jobs_dont_execute j (t + Δ)); rewrite leqNgt; move => /negP T.
+ by apply: T.
+ }
+ { have NEQ: job_cost j - (job_last_nps j) < service sched j (t + Δ).
+ { apply leq_trans with (service sched j t); first by done.
+ rewrite /service /service_during [in X in _ <= X](@big_cat_nat _ _ _ t) //=.
+ rewrite leq_addr //.
+ rewrite leq_addr //.
+ }
+ clear LS.
+ rewrite -END in NEQ, SERV; last by done.
+ rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ.
+ rewrite /NondecreasingSequence.last -nth_last in SERV.
+ have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
+ specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
+ rewrite CONTR in EQ.
+ feed_n 2 EQ; first by eauto 2.
+ {
+ apply/andP; split; first by done.
+ rewrite prednK; first by done.
+ rewrite -(leq_add2r 1) !addn1 prednK.
+ eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
+ eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2.
+ }
+ by done.
+ eauto 2.
+ }
+ rewrite -END; last by done.
+ apply leq_trans with (job_max_nps j).
+ - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
+ - by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
+ }
+ }
+ {
+ split.
+ - by rewrite /task_lock_in_service_le_task_cost.
+ - intros j ARR TSK.
+ apply leq_trans with (job_cost j); first by rewrite leq_subr.
+ by rewrite -TSK; eauto 2.
+ }
+ {
+ rewrite subnn.
+ intros.
+ apply H_R_is_maximum in H.
+ move: H => [F [EQ LE]].
+ exists F.
+ by rewrite subn0 addn0; split.
+ }
+ Qed.
+
+ End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
+
+ End Analysis.
+
+End RTAforConcreteModels.
\ No newline at end of file
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/fixed/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/fixed/response_time_bound.v
deleted file mode 100644
index efc312711eae96d7635f6cd82ce0ba5cd4448763..0000000000000000000000000000000000000000
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/fixed/response_time_bound.v
+++ /dev/null
@@ -1,330 +0,0 @@
-Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
- rt.model.arrival.basic.task_arrival
- rt.model.priority.
-Require Import rt.model.schedule.uni.service
- rt.model.schedule.uni.workload
- rt.model.schedule.uni.schedule
- rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.limited.schedule
- rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound
- rt.model.schedule.uni.limited.rbf.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
-Require Import rt.model.schedule.uni.limited.platform.limited.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
-(** * RTA for FP-schedulers with fixed premption points *)
-(** In this module we prove a general RTA theorem for FP-schedulers with fixed preemption points *)
-Module RTAforFixedPreemptionPointsModelwithArrivalCurves.
-
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
- ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
- RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
-
- Section Analysis.
-
- Context {Task: eqType}.
- Variable task_cost: Task -> time.
-
- Context {Job: eqType}.
- Variable job_arrival: Job -> time.
- Variable job_cost: Job -> time.
- Variable job_task: Job -> Task.
-
- (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
- Variable arr_seq: arrival_sequence Job.
- Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
- Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
-
- (* Consider an arbitrary task set ts. *)
- Variable ts: list Task.
-
- (* Assume that all jobs come from the task set... *)
- Hypothesis H_all_jobs_from_taskset:
- forall j, arrives_in arr_seq j -> job_task j \in ts.
-
- (* ...and the cost of a job cannot be larger than the task cost. *)
- Hypothesis H_job_cost_le_task_cost:
- cost_of_jobs_from_arrival_sequence_le_task_cost
- task_cost job_cost job_task arr_seq.
-
- (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts
- [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
- that equals 0 for the empty interval delta = 0. *)
- Variable max_arrivals: Task -> time -> nat.
- Hypothesis H_family_of_proper_arrival_curves:
- family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
-
- (* Assume we have the model with fixed preemption points. I.e., each task is divided into
- a number of nonpreemptive segments by inserting staticaly predefined preemption points. *)
- Variable job_preemption_points: Job -> seq time.
- Variable task_preemption_points: Task -> seq time.
- Hypothesis H_model_with_fixed_preemption_points:
- fixed_preemption_points_model
- task_cost job_cost job_task arr_seq
- job_preemption_points task_preemption_points ts.
-
- (* Let tsk be any task in ts that is to be analyzed. *)
- Variable tsk: Task.
- Hypothesis H_tsk_in_ts: tsk \in ts.
-
- (* Next, consider any uniprocessor schedule with limited preemptions... *)
- Variable sched: schedule Job.
- Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
- Hypothesis H_schedule_with_limited_preemptions:
- is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.
-
- (* ... where jobs do not execute before their arrival nor after completion. *)
- Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
- Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
-
- (* Assume we have sequential jobs, i.e, jobs from the same
- task execute in the order of their arrival. *)
- Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
-
- (* 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.
- Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
- Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
-
- (* Next, we assume that the schedule is a work-conserving schedule which
- respects the FP policy under a model with fixed preemption points. *)
- Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
- Hypothesis H_respects_policy:
- respects_FP_policy_at_preemption_point
- job_arrival job_cost job_task arr_seq sched
- (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.
-
- (* Let's define some local names for clarity. *)
- Let response_time_bounded_by :=
- is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
- Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
- Let total_hep_rbf :=
- total_hep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
- Let total_ohep_rbf :=
- total_ohep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
-
- (* We also have a set of functions that map job or task
- to its max or last nonpreemptive segment. *)
- Let job_max_nps := job_max_nps job_preemption_points.
- Let job_last_nps := job_last_nps job_preemption_points.
- Let task_max_nps := task_max_nps task_preemption_points.
- Let task_last_nps := task_last_nps task_preemption_points.
-
- (* Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
- Definition blocking :=
- \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk) (task_max_nps 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. *)
- Variable L: time.
- Hypothesis H_L_positive: L > 0.
- Hypothesis H_fixed_point: L = blocking + total_hep_rbf L.
-
- (* To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
-
- (* Next, consider any value R, and assume that for any given arrival A from search space
- there is a solution of the response-time bound recurrence which is bounded by R. *)
- Variable R: nat.
- Hypothesis H_R_is_maximum:
- forall A,
- is_in_search_space A ->
- exists F,
- A + F = blocking
- + (task_rbf (A + ε) - (task_last_nps tsk - ε))
- + total_ohep_rbf (A + F) /\
- F + (task_last_nps tsk - ε) <= R.
-
- (* Now, we can reuse the results for the abstract model of bounded nonpreemptive segments
- to establish a response time bound for the concrete model of fixed preemption points. *)
- Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
- response_time_bounded_by tsk R.
- Proof.
- move: (H_model_with_fixed_preemption_points) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
- move: (MLP) => [EMPTj [LSMj [BEGj [ENDj HH]]]].
- move: (posnP (task_cost tsk)) => [ZERO|POSt].
- { intros j ARR TSK.
- move: (H_job_cost_le_task_cost _ ARR) => POSt.
- move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
- rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
- - by eauto 2.
- - by rewrite Z.
- }
- have Fact2: 1 < size (task_preemption_points tsk).
- { have Fact2: 0 < size (task_preemption_points tsk).
- { apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
- move: (END _ H_tsk_in_ts) => EQ.
- move: EQ; rewrite /NondecreasingSequence.last -nth_last nth_default; last by rewrite CONTR.
- by intros; rewrite -EQ in POSt.
- }
- have EQ: 2 = size [::0; task_cost tsk]; first by done.
- rewrite EQ; clear EQ.
- apply subseq_leq_size.
- rewrite !cons_uniq.
- { apply/andP; split.
- rewrite in_cons negb_or; apply/andP; split; last by done.
- rewrite neq_ltn; apply/orP; left; eauto 2.
- apply/andP; split; by done. }
- intros t EQ; move: EQ; rewrite !in_cons.
- move => /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
- { rewrite EQ; clear EQ.
- move: (BEG _ H_tsk_in_ts) => EQ.
- rewrite -EQ; clear EQ.
- rewrite /NondecreasingSequence.first -nth0.
- apply/(nthP 0).
- exists 0; by done.
- }
- { rewrite EQ; clear EQ.
- move: (END _ H_tsk_in_ts) => EQ.
- rewrite -EQ; clear EQ.
- rewrite /NondecreasingSequence.last -nth_last.
- apply/(nthP 0).
- exists ((size (task_preemption_points tsk)).-1); last by done.
- by rewrite -(leq_add2r 1) !addn1 prednK //.
- }
- }
- eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
- with (task_lock_in_service := fun tsk => (task_cost tsk - (task_last_nps tsk - ε)))
- (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
- (L0 := L) (job_max_nps0 := job_max_nps)
- (job_cost0 := job_cost )
- ; eauto 2.
- { by apply model_with_fixed_preemption_points_is_correct. }
- {
- eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2.
- intros j ARR.
- unfold ModelWithLimitedPreemptions.job_max_nps, task_max_nps, lengths_of_segments.
- apply NondecreasingSequence.max_of_dominating_seq.
- intros. apply HYP2.
- by done.
- }
- { split; last split.
- { intros j ARR POS.
- rewrite subn_gt0.
- rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
- apply LSMj; try done.
- rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
- ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
- apply leq_trans with (job_max_nps j);
- first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
- rewrite -ENDj; last by done.
- by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- }
- { by intros j ARR; rewrite leq_subLR leq_addl. }
- { intros ? ? ? ARR LE LS NCOMPL.
- rewrite subnBA in LS; last first.
- apply LSMj; try done.
- { rewrite lt0n; apply/negP; intros Z; move: Z => /eqP Z.
- move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [LT|GT].
- { by rewrite Z ltn0 in LT. }
- { move: GT; rewrite ltnNge; move => /negP GT; apply: GT.
- by eapply H_completed_jobs_dont_execute.
- }
- }
- have EQ: exists Δ, t' = t + Δ.
- { exists (t' - t); rewrite subnKC; by done. }
- move: EQ => [Δ EQ]; subst t'; clear LE.
- rewrite -subh1 in LS.
- rewrite addn1 in LS.
- apply H_schedule_with_limited_preemptions; first by done.
- rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
- intros CONTR.
- move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [SERV|SERV]; last first.
- { exfalso.
- move: (H_completed_jobs_dont_execute j (t + Δ)); rewrite leqNgt; move => /negP T.
- by apply: T.
- }
- { have NEQ: job_cost j - job_last_nps j < service sched j (t + Δ).
- { apply leq_trans with (service sched j t); first by done.
- rewrite /service /service_during [in X in _ <= X](@big_cat_nat _ _ _ t) //=.
- rewrite leq_addr //.
- rewrite leq_addr //.
- }
- clear LS.
- rewrite -ENDj in NEQ, SERV; last by done.
- rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ; last by eauto 2.
- rewrite /NondecreasingSequence.last -nth_last in SERV.
- have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
- specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
- rewrite CONTR in EQ.
- feed_n 2 EQ; first by eauto 2.
- {
- apply/andP; split; first by done.
- rewrite prednK; first by done.
- rewrite -(leq_add2r 1) !addn1 prednK.
- eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
- eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2.
- }
- by done.
- }
- rewrite -ENDj; last by done.
- apply leq_trans with (job_max_nps j).
- - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- - by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- }
- }
- {
- split.
- - by rewrite /task_lock_in_service_le_task_cost leq_subLR leq_addl.
- - intros j ARR TSK.
- move: (posnP (job_cost j)) => [ZERO | POS].
- { by rewrite ZERO. }
- unfold task_last_nps.
- rewrite !subnBA; first last.
- apply LSMj; try done.
- rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
- apply HYP3.
- by done.
- rewrite -(ltn_add2r 1) !addn1 prednK //.
- move: (Fact2) => Fact3.
- rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
- rewrite -subh1 -?[in X in _ <= X]subh1; first last.
- { apply leq_trans with (job_max_nps j).
- - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- - by rewrite -ENDj //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- }
- { apply leq_trans with (task_max_nps tsk).
- - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- - by rewrite -END //; apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- }
- rewrite -ENDj; last eauto 2.
- rewrite -END; last eauto 2.
- rewrite !NondecreasingSequence.last_seq_minus_last_distance_seq.
- have EQ: size (job_preemption_points j) = size (task_preemption_points tsk).
- { rewrite -TSK.
- by apply HYP1.
- }
- rewrite EQ; clear EQ.
- rewrite leq_add2r.
- apply NondecreasingSequence.domination_of_distances_implies_domination_of_seq; try done; eauto 2.
- rewrite BEG // BEGj //.
- eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
- rewrite -TSK; apply HYP1; try done.
- intros. rewrite -TSK; eauto 2.
- eauto 2.
- eauto 2.
- }
- { rewrite subKn; first by done.
- rewrite /task_last_nps -(leq_add2r 1) subn1 !addn1 prednK; last first.
- { rewrite /ModelWithLimitedPreemptions.task_last_nps /NondecreasingSequence.last -nth_last.
- apply HYP3; try by done.
- rewrite -(ltn_add2r 1) !addn1 prednK //.
- move: (Fact2) => Fact3.
- by rewrite NondecreasingSequence.size_of_seq_of_distances // addn1 ltnS // in Fact2.
- }
- { apply leq_trans with (task_max_nps tsk).
- - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- - rewrite -END; last by done.
- apply ltnW; rewrite ltnS; try done.
- by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- }
- }
- Qed.
-
- End Analysis.
-
-End RTAforFixedPreemptionPointsModelwithArrivalCurves.
\ No newline at end of file
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/floating/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/floating/response_time_bound.v
deleted file mode 100644
index 67355fee552988d7e9534be9e5d168a4e2aabcc3..0000000000000000000000000000000000000000
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/floating/response_time_bound.v
+++ /dev/null
@@ -1,232 +0,0 @@
-Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job
- rt.model.arrival.basic.task_arrival
- rt.model.priority.
-Require Import rt.model.schedule.uni.service
- rt.model.schedule.uni.workload
- rt.model.schedule.uni.schedule
- rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.limited.schedule
- rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound
- rt.model.schedule.uni.limited.rbf.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
-Require Import rt.model.schedule.uni.limited.platform.limited.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
-(** * RTA for FP-schedulers with floating nonpreemptive regions *)
-(** In this module we prove a general RTA theorem for FP-schedulers with floating nonpreemptive regions *)
-Module RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
-
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
- ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform ModelWithLimitedPreemptions
- RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
-
- Section Analysis.
-
- Context {Task: eqType}.
- Variable task_cost: Task -> time.
-
- Context {Job: eqType}.
- Variable job_arrival: Job -> time.
- Variable job_cost: Job -> time.
- Variable job_task: Job -> Task.
-
- (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
- Variable arr_seq: arrival_sequence Job.
- Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
- Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
-
- (* Consider an arbitrary task set ts. *)
- Variable ts: list Task.
-
- (* Assume that all jobs come from the task set... *)
- Hypothesis H_all_jobs_from_taskset:
- forall j, arrives_in arr_seq j -> job_task j \in ts.
-
- (* ...and the cost of a job cannot be larger than the task cost. *)
- Hypothesis H_job_cost_le_task_cost:
- cost_of_jobs_from_arrival_sequence_le_task_cost
- task_cost job_cost job_task arr_seq.
-
- (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts
- [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
- that equals 0 for the empty interval delta = 0. *)
- Variable max_arrivals: Task -> time -> nat.
- Hypothesis H_family_of_proper_arrival_curves:
- family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
-
- (* Assume we have the model with floating nonpreemptive regions. I.e., for each
- task only the length of the maximal nonpreemptive segment is known. *)
- Variable job_preemption_points: Job -> seq time.
- Variable task_max_nps: Task -> time.
- Hypothesis H_task_model_with_floating_nonpreemptive_regions:
- model_with_floating_nonpreemptive_regions
- job_cost job_task arr_seq job_preemption_points task_max_nps.
-
- (* Let tsk be any task in ts that is to be analyzed. *)
- Variable tsk: Task.
- Hypothesis H_tsk_in_ts: tsk \in ts.
-
- (* Next, consider any uniprocessor schedule with limited preemptions...*)
- Variable sched: schedule Job.
- Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
- Hypothesis H_schedule_with_limited_preemptions:
- is_schedule_with_limited_preemptions arr_seq job_preemption_points sched.
-
- (* ... where jobs do not execute before their arrival nor after completion. *)
- Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
- Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
-
- (* Assume we have sequential jobs. *)
- Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
-
- (* 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.
- Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
- Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
-
- (* Next, we assume that the schedule is a work-conserving schedule which
- respects the FP policy under a model with fixed preemption points. *)
- Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
- Hypothesis H_respects_policy:
- respects_FP_policy_at_preemption_point
- job_arrival job_cost job_task arr_seq sched
- (can_be_preempted_for_model_with_limited_preemptions job_preemption_points) higher_eq_priority.
-
- (* Let's define some local names for clarity. *)
- Let response_time_bounded_by :=
- is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
- Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
- Let total_hep_rbf :=
- total_hep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
- Let total_ohep_rbf :=
- total_ohep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
- Let job_max_nps := job_max_nps job_preemption_points.
- Let job_last_nps := job_last_nps job_preemption_points.
-
- (* Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
- Definition blocking :=
- \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk) (task_max_nps 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. *)
- Variable L: time.
- Hypothesis H_L_positive: L > 0.
- Hypothesis H_fixed_point: L = blocking + total_hep_rbf L.
-
- (* To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
-
- (* Next, consider any value R, and assume that for any given arrival A from search space
- there is a solution of the response-time bound recurrence which is bounded by R. *)
- Variable R: nat.
- Hypothesis H_R_is_maximum:
- forall A,
- is_in_search_space A ->
- exists F,
- A + F = blocking + task_rbf (A + ε) + total_ohep_rbf (A + F) /\
- F <= R.
-
- (* Now, we can reuse the results for the abstract model of bounded nonpreemptive segments
- to establish a response time bound for the concrete model with floating nonpreemptive regions. *)
- Theorem uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions:
- response_time_bounded_by tsk R.
- Proof.
- move: (H_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
- move: (LIMJ) => [ZERO [LSMj [BEG [END HH]]]].
- eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
- with (task_lock_in_service := fun tsk => task_cost tsk)
- (job_lock_in_service := fun job => (job_cost job - (job_last_nps job - ε)))
- (L0 := L) (job_max_nps0 := job_max_nps)
- (job_cost0 := job_cost )
- ; eauto 2.
- { by apply model_with_fixed_preemption_points_is_correct. }
- { by eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2. }
- { split; last split.
- { intros j ARR POS.
- rewrite subn_gt0.
- rewrite subn1 -(leq_add2r 1) !addn1 prednK; last first.
- apply LSMj; try done.
- rewrite /job_last_nps /ModelWithLimitedPreemptions.job_last_nps
- ltnS /NondecreasingSequence.last -nth_last NondecreasingSequence.function_of_distances_is_correct.
- apply leq_trans with (job_max_nps j); first by apply NondecreasingSequence.distance_between_neighboring_elements_le_max_distance_in_seq.
- rewrite -END; last by done.
- by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- }
- { by intros j ARR; rewrite leq_subLR leq_addl. }
- { intros ? ? ? ARR LE LS NCOMPL.
- rewrite subnBA in LS; last first.
- apply LSMj; try done.
- { rewrite lt0n; apply/negP; intros Z; move: Z => /eqP Z.
- move: NCOMPL. rewrite /completed_by neq_ltn. move => /orP [LT|GT].
- { by rewrite Z ltn0 in LT. }
- { move: GT; rewrite ltnNge; move => /negP GT; apply: GT.
- by eapply H_completed_jobs_dont_execute.
- }
- }
- have EQ: exists Δ, t' = t + Δ.
- { exists (t' - t); rewrite subnKC; by done. }
- move: EQ => [Δ EQ]; subst t'; clear LE.
- rewrite -subh1 in LS.
- rewrite addn1 in LS.
- apply H_schedule_with_limited_preemptions; first by done.
- rewrite /can_be_preempted_for_model_with_limited_preemptions; apply/negP.
- intros CONTR.
- move: NCOMPL; rewrite /completed_by neq_ltn; move => /orP [SERV|SERV]; last first.
- { exfalso.
- move: (H_completed_jobs_dont_execute j (t + Δ)); rewrite leqNgt; move => /negP T.
- by apply: T.
- }
- { have NEQ: job_cost j - (job_last_nps j) < service sched j (t + Δ).
- { apply leq_trans with (service sched j t); first by done.
- rewrite /service /service_during [in X in _ <= X](@big_cat_nat _ _ _ t) //=.
- rewrite leq_addr //.
- rewrite leq_addr //.
- }
- clear LS.
- rewrite -END in NEQ, SERV; last by done.
- rewrite NondecreasingSequence.last_seq_minus_last_distance_seq in NEQ.
- rewrite /NondecreasingSequence.last -nth_last in SERV.
- have EQ := NondecreasingSequence.antidensity_of_nondecreasing_seq.
- specialize (EQ (job_preemption_points j) (service sched j (t + Δ)) (size (job_preemption_points j)).-2).
- rewrite CONTR in EQ.
- feed_n 2 EQ; first by eauto 2.
- {
- apply/andP; split; first by done.
- rewrite prednK; first by done.
- rewrite -(leq_add2r 1) !addn1 prednK.
- eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
- eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2.
- }
- by done.
- eauto 2.
- }
- rewrite -END; last by done.
- apply leq_trans with (job_max_nps j).
- - by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
- - by apply NondecreasingSequence.max_distance_in_seq_le_last_element_of_seq; eauto 2.
- }
- }
- {
- split.
- - by rewrite /task_lock_in_service_le_task_cost.
- - intros j ARR TSK.
- apply leq_trans with (job_cost j); first by rewrite leq_subr.
- by rewrite -TSK; eauto 2.
- }
- {
- rewrite subnn.
- intros.
- apply H_R_is_maximum in H.
- move: H => [F [EQ LE]].
- exists F.
- by rewrite subn0 addn0; split.
- }
- Qed.
-
- End Analysis.
-
-End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
\ No newline at end of file
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/nonpreemptive/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/nonpreemptive/response_time_bound.v
deleted file mode 100644
index 465d03480e57ff85ed7020eff9f2f88b4ae04fbe..0000000000000000000000000000000000000000
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/nonpreemptive/response_time_bound.v
+++ /dev/null
@@ -1,159 +0,0 @@
-Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
-Require Import rt.model.schedule.uni.service
- rt.model.schedule.uni.workload
- rt.model.schedule.uni.schedule
- rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.nonpreemptive.schedule.
-Require Import rt.model.schedule.uni.limited.schedule
- rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
-Require Import rt.model.schedule.uni.limited.platform.nonpreemptive.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
-(** * RTA for fully nonpreemptive FP model *)
-(** In this module we prove the RTA theorem for the fully nonpreemptive FP model. *)
-Module RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
-
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule
- NonpreemptiveSchedule Workload Service FullyNonPreemptivePlatform
- ResponseTime MaxArrivalsWorkloadBound LimitedPreemptionPlatform
- RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
-
- Section Analysis.
-
- Context {Task: eqType}.
- Variable task_cost: Task -> time.
-
- Context {Job: eqType}.
- Variable job_arrival: Job -> time.
- Variable job_cost: Job -> time.
- Variable job_task: Job -> Task.
-
- (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
- Variable arr_seq: arrival_sequence Job.
- Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
- Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
-
- (* Consider an arbitrary task set ts. *)
- Variable ts: list Task.
-
- (* Assume that all jobs come from the task set... *)
- Hypothesis H_all_jobs_from_taskset:
- forall j, arrives_in arr_seq j -> job_task j \in ts.
-
- (* ...and the cost of a job cannot be larger than the task cost. *)
- Hypothesis H_job_cost_le_task_cost:
- cost_of_jobs_from_arrival_sequence_le_task_cost
- task_cost job_cost job_task arr_seq.
-
- (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts
- [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
- that equals 0 for the empty interval delta = 0. *)
- Variable max_arrivals: Task -> time -> nat.
- Hypothesis H_family_of_proper_arrival_curves:
- family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
-
- (* Let tsk be any task in ts. *)
- Variable tsk: Task.
- Hypothesis H_tsk_in_ts: tsk \in ts.
-
- (* Next, consider any uniprocessor nonpreemptive schedule of this arrival sequence...*)
- Variable sched: schedule Job.
- Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
- Hypothesis H_nonpreemptive_sched: is_nonpreemptive_schedule job_cost sched.
-
- (* ... where jobs do not execute before their arrival nor after completion. *)
- Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
- Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
-
- (* Assume we have sequential jobs, i.e, jobs from the same
- task execute in the order of their arrival. *)
- Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
-
- (* 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.
- Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
- Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
-
- (* Next, we assume that the schedule is a work-conserving schedule which
- respects the FP policy under a fully nonpreemptive model. *)
- Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
- Hypothesis H_respects_policy:
- respects_FP_policy_at_preemption_point
- job_arrival job_cost job_task arr_seq sched
- (can_be_preempted_for_fully_nonpreemptive_model job_cost) higher_eq_priority.
-
- (* Let's define some local names for clarity. *)
- Let response_time_bounded_by :=
- is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
- Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
- Let total_hep_rbf :=
- total_hep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
- Let total_ohep_rbf :=
- total_ohep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
-
- (* Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
- Definition blocking :=
- \max_(tsk_other <- ts | ~~ higher_eq_priority 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. *)
- Variable L: time.
- Hypothesis H_L_positive: L > 0.
- Hypothesis H_fixed_point: L = blocking + total_hep_rbf L.
-
- (* To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
-
- (* Next, consider any value R, and assume that for any given arrival A from search space
- there is a solution of the response-time bound recurrence which is bounded by R. *)
- Variable R: nat.
- Hypothesis H_R_is_maximum:
- forall A,
- is_in_search_space A ->
- exists F,
- A + F = blocking
- + (task_rbf (A + ε) - (task_cost tsk - ε))
- + total_ohep_rbf (A + F) /\
- F + (task_cost tsk - ε) <= R.
-
- (* Now, we can reuse the results for the abstract model with fixed preemption points to
- establish a response-time bound for the more concrete model of fully nonpreemptive scheduling. *)
- Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp:
- response_time_bounded_by tsk R.
- Proof.
- move: (posnP (task_cost tsk)) => [ZERO|POS].
- { intros j ARR TSK.
- have ZEROj: job_cost j = 0.
- { move: (H_job_cost_le_task_cost j ARR) => NEQ.
- rewrite /job_cost_le_task_cost TSK ZERO in NEQ.
- by apply/eqP; rewrite -leqn0.
- }
- rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
- - by apply H_completed_jobs_dont_execute.
- - by rewrite ZEROj.
- }
- eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
- (job_max_nps := fun j => job_cost j)
- (task_max_nps := fun tsk => task_cost tsk)
- (job_lock_in_service := fun j => ε)
- (task_lock_in_service := fun tsk => ε)
- (L0 := L); eauto 2.
- - by eapply fully_nonpreemptive_model_is_correct; eauto 2.
- - eapply fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions; eauto 2.
- - repeat split; try done.
- - intros j t t' ARR LE SERV NCOMPL.
- rewrite /service in SERV; apply incremental_service_during in SERV.
- move: SERV => [t_first [/andP [_ H1] [H2 H3]]].
- apply H_nonpreemptive_sched with t_first; try done.
- by apply leq_trans with t; first apply ltnW.
- - repeat split; try done.
- Qed.
-
- End Analysis.
-
-End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
\ No newline at end of file
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/preemptive/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/preemptive/response_time_bound.v
deleted file mode 100644
index 7489a4a17f0718706076dc824cdb94dfdbfdb418..0000000000000000000000000000000000000000
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/preemptive/response_time_bound.v
+++ /dev/null
@@ -1,153 +0,0 @@
-Require Import rt.util.all.
-Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival rt.model.priority.
-Require Import rt.model.schedule.uni.service
- rt.model.schedule.uni.workload
- rt.model.schedule.uni.schedule
- rt.model.schedule.uni.response_time.
-Require Import rt.model.schedule.uni.limited.platform.preemptive
- rt.model.schedule.uni.limited.schedule
- rt.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound.
-Require Import rt.model.arrival.curves.bounds.
-Require Import rt.analysis.uni.arrival_curves.workload_bound.
-
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
-(** * RTA for fully preemptive FP model *)
-(* In this module we prove the RTA theorem for fully preemptive FP model *)
-Module RTAforFullyPreemptiveFPModelwithArrivalCurves.
-
- Import Epsilon Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service
- ResponseTime MaxArrivalsWorkloadBound FullyPreemptivePlatform LimitedPreemptionPlatform
- RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
-
- (* In this section we prove that the maximum among the solutions of the response-time bound
- recurrence for some set of parameters is a response time bound for tsk. *)
- Section Analysis.
-
- Context {Task: eqType}.
- Variable task_cost: Task -> time.
-
- Context {Job: eqType}.
- Variable job_arrival: Job -> time.
- Variable job_cost: Job -> time.
- Variable job_deadline: Job -> time.
- Variable job_task: Job -> Task.
-
- (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
- Variable arr_seq: arrival_sequence Job.
- Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
- Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
-
- (* Consider an arbitrary task set ts. *)
- Variable ts: list Task.
-
- (* Assume that all jobs come from the task set... *)
- Hypothesis H_all_jobs_from_taskset:
- forall j, arrives_in arr_seq j -> job_task j \in ts.
-
- (* ...and the cost of a job cannot be larger than the task cost. *)
- Hypothesis H_job_cost_le_task_cost:
- cost_of_jobs_from_arrival_sequence_le_task_cost
- task_cost job_cost job_task arr_seq.
-
- (* Let max_arrivals be a family of proper arrival curves, i.e., for any task tsk in ts
- [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function
- that equals 0 for the empty interval delta = 0. *)
- Variable max_arrivals: Task -> time -> nat.
- Hypothesis H_family_of_proper_arrival_curves:
- family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
-
- (* Let tsk be any task in ts. *)
- Variable tsk: Task.
- Hypothesis H_tsk_in_ts: tsk \in ts.
-
- (* Next, consider any uniprocessor schedule of the arrival sequence...*)
- Variable sched: schedule Job.
- Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
-
- (* ... where jobs do not execute before their arrival nor after completion. *)
- Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
- Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
-
- (* Assume we have sequential jobs. *)
- Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
-
- (* 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.
- Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
- Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
-
- (* Next, we assume that the schedule is a work-conserving schedule which
- respects the FP policy under a fully preemptive model. *)
- Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
- Hypothesis H_respects_policy:
- respects_FP_policy_at_preemption_point
- job_arrival job_cost job_task arr_seq sched
- (can_be_preempted_for_fully_preemptive_model) higher_eq_priority.
-
- (* Let's define some local names for clarity. *)
- Let response_time_bounded_by :=
- is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
- Let task_rbf := task_request_bound_function task_cost max_arrivals tsk.
- Let total_hep_rbf :=
- total_hep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
- Let total_ohep_rbf :=
- total_ohep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
-
- (* Let L be any positive fixed point of the busy interval recurrence, determined by
- the sum of blocking and higher-or-equal-priority workload. *)
- Variable L: time.
- Hypothesis H_L_positive: L > 0.
- Hypothesis H_fixed_point: L = total_hep_rbf L.
-
- (* To reduce the time complexity of the analysis, recall the notion of search space. *)
- Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
-
- (* Next, consider any value R, and assume that for any given arrival A from search space
- there is a solution of the response-time bound recurrence which is bounded by R. *)
- Variable R: nat.
- Hypothesis H_R_is_maximum:
- forall A,
- is_in_search_space A ->
- exists F,
- A + F = task_rbf (A + ε) + total_ohep_rbf (A + F) /\
- F <= R.
-
- (* Now, we can reuse the results for the abstract model with fixed preemption
- points to establish a response-time bound for the more concrete model
- of fully-preemptive scheduling. *)
- Theorem uniprocessor_response_time_bound_fully_preemptive_fp:
- response_time_bounded_by tsk R.
- Proof.
- have BLOCK: RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.blocking_bound (fun _ => ε) higher_eq_priority ts tsk = 0.
- { by rewrite /RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.blocking_bound subnn big1_eq. }
- eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
- (task_max_nps := fun _ => ε)
- (can_be_preempted := fun j prog => true)
- (task_lock_in_service := fun tsk => task_cost tsk)
- (job_lock_in_service := fun j => job_cost j)
- (job_max_nps := fun j => ε); eauto 2; try done.
- - by eapply fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions.
- - repeat split; try done.
- intros ? ? ? ARR; move => LE COMPL /negP NCOMPL.
- exfalso; apply: NCOMPL.
- apply completion_monotonic with t; try done.
- rewrite /completed_by eqn_leq; apply/andP; split; try done.
- - repeat split; try done.
- rewrite /task_lock_in_service_le_task_cost. by done.
- unfold task_lock_in_service_bounds_job_lock_in_service.
- by intros ? ARR TSK; rewrite -TSK; apply H_job_cost_le_task_cost.
- - by rewrite BLOCK add0n.
- - move => A /andP [LT NEQ].
- specialize (H_R_is_maximum A); feed H_R_is_maximum.
- { by apply/andP; split. }
- move: H_R_is_maximum => [F [FIX BOUND]].
- exists F; split.
- + by rewrite BLOCK add0n subnn subn0.
- + by rewrite subnn addn0.
- Qed.
-
- End Analysis.
-
-End RTAforFullyPreemptiveFPModelwithArrivalCurves.
\ No newline at end of file
diff --git a/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
index 2835be0353a56971bed32c29b5982985d0a47bb5..1d917819387d09eea134ff5d1ec2c674c7fe9505 100644
--- a/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
@@ -273,7 +273,11 @@ Module RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
F + (task_cost tsk - task_lock_in_service tsk) <= R.
(* Then, using the results for the general RTA for FP-schedulers, we establish a
- response-time bound for the more concrete model of bounded nonpreemptive segments. *)
+ response-time bound for the more concrete model of bounded nonpreemptive segments.
+ Note that in case of the general RTA for FP-schedulers, we just _assume_ that
+ the priority inversion is bounded. In this module we provide the preemption model
+ with bounded nonpreemptive segments and _prove_ that the priority inversion is
+ bounded. *)
Theorem uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments:
response_time_bounded_by tsk R.
Proof.
diff --git a/model/schedule/uni/limited/fixed_priority/response_time_bound.v b/model/schedule/uni/limited/fixed_priority/response_time_bound.v
index f5ca0b12e03e39775d558d994148899ed2743939..773e719a23183bd09a3fd1ae29dbba5fefe6eb31 100644
--- a/model/schedule/uni/limited/fixed_priority/response_time_bound.v
+++ b/model/schedule/uni/limited/fixed_priority/response_time_bound.v
@@ -12,7 +12,8 @@ Require Import rt.model.schedule.uni.limited.platform.definitions
rt.model.schedule.uni.limited.rbf
rt.model.schedule.uni.limited.abstract_RTA.definitions
rt.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space
- rt.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta.
+ rt.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta
+ rt.model.schedule.uni.limited.jlfp_instantiation.
Require Import rt.model.arrival.curves.bounds.
Require Import rt.analysis.uni.arrival_curves.workload_bound.
Require Import rt.model.schedule.uni.limited.busy_interval.
@@ -26,7 +27,7 @@ Module AbstractRTAforFPwithArrivalCurves.
Import Epsilon Job ArrivalCurves TaskArrival Priority ScheduleOfTask
UniprocessorSchedule Workload Service ResponseTime MaxArrivalsWorkloadBound
- LimitedPreemptionPlatform RBF BusyIntervalJLFP.
+ LimitedPreemptionPlatform RBF BusyIntervalJLFP JLFPInstantiation.
Section AbstractResponseTimeAnalysisForFP.
@@ -136,18 +137,6 @@ Module AbstractRTAforFPwithArrivalCurves.
Let total_ohep_rbf :=
total_ohep_request_bound_function_FP task_cost higher_eq_priority max_arrivals ts tsk.
- (* For proper calculation of interference (and interfering workload) of a job, we need to distinguish
- interference received from other jobs of the same task and other jobs of other tasks. In that
- regard, we introduce two additional relations. The first relation defines whether job j1 has a
- higher-than-or-equal-priority than job j2 and j1 is not equal to j2... *)
- Let another_job_with_higher_eq_priority j1 j2 :=
- jlfp_higher_eq_priority j1 j2 && (j1 != j2).
-
- (* ...and the second relation defines whether a job j from different task has a
- higher-or-equal-priority than priority of task tsk. *)
- Let job_from_another_task_with_higher_eq_priority j :=
- higher_eq_priority (job_task j) tsk && (job_task j != tsk).
-
(* Assume that there eixsts a constant priority_inversion_bound that bounds
the length of any priority inversion experienced by any job of tsk.
Sinse we analyze only task tsk, we ignore the lengths of priority
@@ -179,603 +168,26 @@ Module AbstractRTAforFPwithArrivalCurves.
+ (task_rbf (A + ε) - (task_cost tsk - task_lock_in_service tsk))
+ total_ohep_rbf (A + F) /\
F + (task_cost tsk - task_lock_in_service tsk) <= R.
-
- (** ** Interference and Interfering Workload *)
- (** In this section, we introduce definitions of interference, interfering
- workload and a function that bounds cumulative interference. *)
-
- (* In order to introduce the interference, first we need to recall the definition
- of priority inversion introduced in module limited.fixed_priority.busy_interval:
- [ Definition is_priority_inversion t := ]
- [ if sched t is Some jlp then ]
- [ ~~ jlfp_higher_eq_priority jlp j ]
- [ else false. ]
- I.e., we say that job j is incurring a priority inversion at time t
- if there exists a job with lower priority that executes at time t.
- In order to simplify things, we ignore the fact that according to this
- definition a job can incur priority inversion even before its release
- (or after completion). All such (potentially bad) cases do not cause
- 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: time) :=
- is_priority_inversion sched jlfp_higher_eq_priority j t.
-
- (* Next, we say that job j is incurring interference from another job with higher or equal
- priority at time t, if there exists job jhp (different from j) with a higher or equal priority
- that executes at time t. *)
- Definition is_interference_from_another_job_with_higher_eq_priority (j: Job) (t: time) :=
- if sched t is Some jhp then
- another_job_with_higher_eq_priority jhp j
- else false.
-
- (* Similarly, we say that job j is incurring interference from a job with higher or
- equal priority of another task at time t, if there exists a job jhp (of a different
- task) with higher or equal priority that executes at time t. *)
- Definition is_interference_from_another_task_with_higher_eq_priority (t: time) :=
- if sched t is Some jhp then
- job_from_another_task_with_higher_eq_priority jhp
- else false.
-
- (* Now, we define the notion of cumulative interference, called
- interfering_workload_of_jobs_with_hep_priority, that says
- how many units of workload are generated by jobs with higher
- or equal priority released at time t. *)
- Definition interfering_workload_of_jobs_with_hep_priority (j: Job) (t: time) :=
- \sum_(jhp <- jobs_arriving_at arr_seq t |
- another_job_with_higher_eq_priority jhp j) job_cost jhp.
-
- (* To use the theorem uniprocessor_response_time_bound_seq from the Abstract RTA module,
- we need to specify functions of interference and interfering workload. *)
+
(* Instantiation of Interference *)
(* We say that job j incurs interference at time t iff it cannot execute due to
- a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion. *)
- Let interference j t :=
- is_priority_inversion j t || is_interference_from_another_job_with_higher_eq_priority j t.
+ a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion.
+ (for more details see file limited.jlfp_instantiation.v) *)
+ Let interference (j: Job) (t: time) :=
+ interference sched jlfp_higher_eq_priority 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 t :=
- is_priority_inversion j t + interfering_workload_of_jobs_with_hep_priority j t.
+ function and interfering workload of jobs with higher or equal priority.
+ (for more details see file limited.limited.jlfp_instantiation.v) *)
+ Let interfering_workload (j: Job) (t: time) :=
+ interfering_workload job_cost arr_seq sched jlfp_higher_eq_priority j t.
(* Finally, we define the interference bound function as the sum of the priority
interference bound and the higher-or-equal-priority workload. *)
Let IBF R := priority_inversion_bound + total_ohep_rbf R.
- (* For each of the concepts defined above, we introduce a corresponding cumulative function: *)
- (* (a) cumulative priority inversion... *)
- Let cumulative_priority_inversion j t1 t2 :=
- \sum_(t1 <= t < t2) is_priority_inversion j t.
-
- (* ... (b) cumulative interference from other jobs with higher or equal priority... *)
- Let cumulative_interference_from_other_jobs j t1 t2 :=
- \sum_(t1 <= t < t2) is_interference_from_another_job_with_higher_eq_priority j t.
-
- (* ... (c) and cumulative interference from jobs with higher or equal priority from other tasks... *)
- Let cumulative_interference_from_other_tasks t1 t2 :=
- \sum_(t1 <= t < t2) is_interference_from_another_task_with_higher_eq_priority t.
-
- (* ... (d) cumulative interference... *)
- Let cumulative_interference j t1 t2 := \sum_(t1 <= t < t2) interference j t.
-
- (* ... (e) cumulative workload from jobs with higher or equal priority... *)
- Let cumulative_interfering_workload_of_jobs_with_hep_priority j t1 t2 :=
- \sum_(t1 <= t < t2) interfering_workload_of_jobs_with_hep_priority j t.
-
- (* ... (f) and cumulative interfering workload. *)
- Let cumulative_interfering_workload j t1 t2 := \sum_(t1 <= t < t2) interfering_workload j t.
-
- (* Instantiated functions usually do not have any useful lemmas about them. In order to
- reuse existing lemmas, we need to prove equivalence of the instantiated functions to
- some conventional notions. Instantiations given in this file are equivalent to
- service and workload. Further, we prove these equivalences formally. *)
-
- (* Before we present the formal proofs of the equivalences, we recall
- the notion of workload of higher or equal priority jobs. *)
- Let workload_of_other_jobs_with_hep_priority j t1 t2 :=
- workload_of_jobs job_cost (arrivals_between t1 t2)
- (fun jhp => another_job_with_higher_eq_priority jhp j).
-
- (* Similarly, we recall notions of service of higher or equal priority jobs from other tasks... *)
- Let service_of_jobs_from_other_tasks_with_hep_priority t1 t2 :=
- service_of_jobs sched (arrivals_between t1 t2) job_from_another_task_with_higher_eq_priority t1 t2.
-
- (* ... and service of all other jobs with higher or equal priority. *)
- Let service_of_other_jobs_with_hep_priority j t1 t2 :=
- service_of_jobs sched (arrivals_between t1 t2)
- (fun jhp => another_job_with_higher_eq_priority jhp j) t1 t2.
-
- (** ** Equivalences *)
-
- (** In this section we prove a few equivalences between definitions obtained by instantiation
- of definitions from the Abstract RTA module (interference and interfering workload) and
- definitions corresponding to the conventional concepts. *)
-
- (** As it was mentioned previously, instantiated functions of interference and interfering
- workload usually do not have any useful lemmas about them. Hovewer, it is possible to
- prove their equivalence to the more conventional notions like service or workload. Next
- we prove the equivalence between the instantiations and conventional notions. *)
- Section Equivalences.
-
- (* We prove that we can split cumulative interference into two parts: (1) cumulative priority
- inversion and (2) cumulative interference from jobs with higher or equal priority. *)
- Lemma cumulative_interference_split:
- forall j t1 t2,
- cumulative_interference j t1 t2
- = cumulative_priority_inversion j t1 t2 + cumulative_interference_from_other_jobs j t1 t2.
- Proof.
- rewrite /cumulative_interference /interference.
- intros; rewrite -big_split //=.
- apply/eqP; rewrite eqn_leq; apply/andP; split; rewrite leq_sum; try done.
- - intros t _; unfold is_priority_inversion, BusyIntervalJLFP.is_priority_inversion,
- is_interference_from_another_job_with_higher_eq_priority.
- case SCHED: (sched t) => [s | ]; last by done.
- unfold jlfp_higher_eq_priority, FP_to_JLFP.
- by case HP: (higher_eq_priority (job_task s) (job_task j)); simpl; rewrite ?addn0 ?add0n.
- - intros t _; unfold is_priority_inversion, BusyIntervalJLFP.is_priority_inversion,
- is_interference_from_another_job_with_higher_eq_priority.
- case SCHED: (sched t) => [s | ]; last by done.
- unfold another_job_with_higher_eq_priority, jlfp_higher_eq_priority, FP_to_JLFP.
- by case HP: (higher_eq_priority (job_task s) (job_task j)); simpl; rewrite ?addn0 ?add0n.
- Qed.
-
- (* Let j be any job of task tsk, and let upp_t be any time instant after job j's arrival.
- Then for any time interval before upp_t, the cumulative interference received by tsk
- is equal to sum of the cumulative priority inversion of job j and the cumulative interference
- incurred by task tsk due to other tasks. *)
- Lemma cumulative_task_interference_split:
- forall j t1 t2 upp_t,
- job_task j = tsk ->
- t2 <= upp_t ->
- j \in jobs_arrived_before arr_seq upp_t ->
- cumulative_task_interference interference tsk upp_t t1 t2 =
- cumulative_priority_inversion j t1 t2 +
- cumulative_interference_from_other_tasks t1 t2.
- Proof.
- rewrite /cumulative_task_interference /AbstractSeqRTA.cumul_task_interference
- /ScheduleOfTask.task_scheduled_at
- /cumulative_priority_inversion
- /cumulative_interference_from_other_tasks.
- clear H_R_is_maximum R.
- intros j t1 R upp TSK GE ARR.
- rewrite -big_split //=.
- rewrite big_nat_cond [X in _ = X]big_nat_cond.
- apply/eqP; rewrite eqn_leq; apply/andP; split.
- { apply leq_sum; intros t _.
- rewrite /interference /is_priority_inversion /BusyIntervalJLFP.is_priority_inversion
- /is_interference_from_another_task_with_higher_eq_priority
- /is_interference_from_another_job_with_higher_eq_priority
- /AbstractSeqRTA.task_interference_received_before
- /another_job_with_higher_eq_priority /job_from_another_task_with_higher_eq_priority
- /ScheduleOfTask.task_scheduled_at /jlfp_higher_eq_priority /FP_to_JLFP.
- case SCHED: (sched t) => [s | ]; last by rewrite has_pred0 addn0 leqn0 eqb0.
- case HP: (higher_eq_priority (job_task s) (job_task j)); simpl; last first.
- { by apply leq_trans with 1; [apply leq_b1 | rewrite leq_addr]. }
- rewrite add0n; rewrite TSK in HP.
- by case: (job_task s != tsk); first (rewrite HP; simpl; rewrite leq_b1).
- }
- { apply leq_sum; move => t /andP [/andP [_ LT'] _].
- rewrite /is_priority_inversion /is_interference_from_another_task_with_higher_eq_priority
- /BusyIntervalJLFP.is_priority_inversion
- /is_interference_from_another_job_with_higher_eq_priority /another_job_with_higher_eq_priority
- /job_from_another_task_with_higher_eq_priority /AbstractSeqRTA.task_interference_received_before
- /ScheduleOfTask.task_scheduled_at /jlfp_higher_eq_priority /FP_to_JLFP.
- case SCHED: (sched t) => [s | ]; last by done.
- rewrite -TSK; case TSKEQ: (job_task s == job_task j); simpl.
- { rewrite Bool.andb_false_r leqn0 addn0 eqb0.
- by move: TSKEQ => /eqP TSKEQ; rewrite TSKEQ Bool.negb_involutive. }
- have NEQ: s != j.
- { apply/negP; intros EQ; move: EQ => /eqP EQ.
- move: TSKEQ => /eqP TSKEQ; apply: TSKEQ.
- by rewrite EQ.
- }
- have Fact: forall b, ~~ b + b = true; first by intros b; destruct b.
- rewrite Bool.andb_true_r Fact; simpl; rewrite lt0b; clear Fact.
- apply/hasP; exists j.
- { rewrite /arrivals_of_task_before /arrivals_of_task_between.
- rewrite mem_filter; apply/andP; split; first by rewrite /is_job_of_task.
- by unfold jobs_arrived_before in ARR; apply jobs_arrived_between_sub with (t2 := 0) (t3 := upp).
- }
- { rewrite /interference /is_priority_inversion /BusyIntervalJLFP.is_priority_inversion
- /is_interference_from_another_job_with_higher_eq_priority
- /another_job_with_higher_eq_priority /FP_to_JLFP SCHED NEQ.
- by rewrite Bool.andb_true_r orNb.
- }
- }
- Qed.
-
- (* In this section we prove that the (abstract) cumulative interfering workload is equivalent to
- conventional workload, i.e., the one defined with concrete schedule parameters. *)
- Section InstantiatedWorkloadEquivalence.
-
- (* Let [t1,t2) be any time interval. *)
- Variables t1 t2: time.
-
- (* Then for any job j, the cumulative interfering workload is equal to the conventional workload. *)
- Lemma instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs:
- forall j,
- cumulative_interfering_workload_of_jobs_with_hep_priority j t1 t2
- = workload_of_other_jobs_with_hep_priority j t1 t2.
- Proof.
- intros.
- rewrite /workload_of_other_jobs_with_hep_priority /cumulative_interfering_workload_of_jobs_with_hep_priority.
- case NEQ: (t1 < t2); last first.
- { move: NEQ => /negP /negP; rewrite -leqNgt; move => NEQ.
- rewrite big_geq; last by done.
- rewrite /arrivals_between /jobs_arrived_between big_geq; last by done.
- by rewrite /workload_of_jobs big_nil.
- }
- { unfold interfering_workload_of_jobs_with_hep_priority, workload_of_jobs.
- have EX: exists k, t2 = t1 + k.
- { exists (t2 - t1). rewrite subnKC. by done. by rewrite ltnW. }
- move: EX => [k EQ]. subst t2. clear NEQ.
- induction k.
- { rewrite !addn0.
- rewrite big_geq; last by done.
- rewrite /arrivals_between /jobs_arrived_between big_geq; last by done.
- by rewrite /workload_of_jobs big_nil. }
- { rewrite addnS big_nat_recr //=; last by rewrite leq_addr.
- rewrite IHk.
- rewrite /arrivals_between /jobs_arrived_between big_nat_recr //=; last by rewrite leq_addr.
- by rewrite big_cat //=. }
- }
- Qed.
-
- End InstantiatedWorkloadEquivalence.
-
- (* In this section we prove that the (abstract) cumulative interference of jobs with higher or
- equal priority is equal to total service of jobs with higher or equal priority. *)
- Section InstantiatedServiceEquivalences.
-
- (* Consider any job j of tsk. *)
- Variable j: Job.
- Hypothesis H_j_arrives: arrives_in arr_seq j.
- Hypothesis H_job_of_tsk: job_task j = tsk.
-
- (* We consider an arbitrary time interval [t1, t) that starts with a quiet time. *)
- Variables t1 t: time.
- Hypothesis H_quiet_time: quiet_time j t1.
-
- (* Then for any job j, the (abstract) instantiated function of interference is
- equal to the total service of jobs with higher or equal priority. *)
- Lemma instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs:
- cumulative_interference_from_other_jobs j t1 t = service_of_other_jobs_with_hep_priority j t1 t.
- Proof.
- rewrite /service_of_other_jobs_with_hep_priority /cumulative_interference_from_other_jobs.
- case NEQ: (t1 <= t); last first.
- { apply negbT in NEQ; rewrite -ltnNge in NEQ.
- rewrite big_geq; last by apply ltnW.
- rewrite /service_of_jobs /arrivals_between /jobs_arrived_between big_geq; last by apply ltnW.
- by rewrite big_nil.
- }
- have EX: exists k, t = t1 + k.
- { by exists (t - t1); rewrite subnKC. } move: EX => [k EQ]; subst t; clear NEQ.
- induction k.
- { rewrite addn0 big_geq //.
- rewrite /arrivals_between /jobs_arrived_between big_geq //.
- by rewrite /service_of_jobs big_nil. }
- { rewrite addnS big_nat_recr //=; last by rewrite leq_addr.
- have Fact:
- arrivals_between t1 (t1 + k).+1 = jobs_arrived_between arr_seq t1 (t1 + k) ++ jobs_arriving_at arr_seq (t1 + k).
- { by rewrite /arrivals_between /jobs_arrived_between big_nat_recr //= leq_addr. }
- rewrite Fact.
- rewrite /service_of_jobs IHk big_cat //=; clear IHk.
-
- have EQ:
- \sum_(i0 <- jobs_arriving_at arr_seq (t1 + k) | another_job_with_higher_eq_priority i0 j)
- service_during sched i0 t1 (t1 + k).+1 =
- \sum_(i0 <- jobs_arriving_at arr_seq (t1 + k) | another_job_with_higher_eq_priority i0 j)
- service_during sched i0 (t1 + k) (t1 + k).+1.
- { rewrite /service_during; rewrite big_seq_cond [X in _ = X]big_seq_cond.
- apply/eqP; rewrite eqn_leq; apply/andP; split.
- { rewrite leq_sum //.
- move => jo /andP [ARR /andP [HP NTSK]].
- rewrite (@big_cat_nat _ _ _ (t1 + k)) //=; last by rewrite leq_addr.
- rewrite -[X in _ <= X]add0n leq_add //.
- rewrite leqn0 big_nat_cond big1 //.
- move => x /andP [/andP [_ LT] _].
- apply/eqP; rewrite eqb0; apply/negP; intros NSCHED.
- unfold jobs_must_arrive_to_execute, arrival_times_are_consistent in *.
- apply H_jobs_must_arrive_to_execute in NSCHED.
- unfold has_arrived in NSCHED.
- apply H_arrival_times_are_consistent in ARR.
- rewrite -ARR in LT.
- by move: LT; rewrite ltnNge; move => /negP LT. }
- { rewrite leq_sum //.
- move => jo /andP [ARR /andP [HP NTSK]].
- rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + k )) //=. rewrite leq_addl //.
- by rewrite leq_addr. }
- }
- rewrite EQ; clear EQ.
- apply/eqP; rewrite exchange_big //=.
- rewrite big_nat_recr //=; last by rewrite leq_addr.
- rewrite exchange_big //=.
- rewrite -addnA eqn_add2l.
- rewrite exchange_big //=.
- rewrite big_nat1.
- rewrite -big_cat //=.
- rewrite -Fact; clear Fact.
- unfold is_interference_from_another_job_with_higher_eq_priority.
- case SCHED: (sched (t1 + k)) => [jo | ]; simpl; last first.
- { by rewrite eq_sym big1 //; intros; rewrite /service_at /scheduled_at SCHED. }
- { case PRIO: (another_job_with_higher_eq_priority jo j); simpl; last first.
- { rewrite eq_sym big1 //.
- intros joo PRIO2.
- apply/eqP; rewrite eqb0; apply/negP; intros SCHED2.
- move: SCHED2 => /eqP SCHED2.
- rewrite SCHED2 in SCHED.
- inversion SCHED; subst joo.
- by rewrite PRIO in PRIO2.
- }
- { rewrite eqn_leq; apply/andP; split; last first.
- { apply service_of_jobs_le_1 with job_arrival; try done. }
- { rewrite (big_rem jo) //=.
- rewrite PRIO /service_at /scheduled_at SCHED eq_refl add1n; by done.
- apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival); try done.
- { unfold jobs_come_from_arrival_sequence in *.
- apply H_jobs_come_from_arrival_sequence with (t1 + k).
- by rewrite /scheduled_at SCHED. }
- move: PRIO => /andP [PRIO1 PRIO2].
- rewrite /arrived_between ltnS; apply/andP; split; last first.
- { by move: SCHED => /eqP SCHED; apply H_jobs_must_arrive_to_execute in SCHED. }
- { rewrite leqNgt; apply/negP; intros AB.
- move: (SCHED) => /eqP /negP SCHED2; apply: SCHED2; apply/negP.
- apply completed_implies_not_scheduled with job_cost; try done.
- apply completion_monotonic with t1; [ by done | by rewrite leq_addr | ].
- apply H_quiet_time; try done.
- by move: SCHED => /eqP SCHED; apply H_jobs_come_from_arrival_sequence in SCHED.
- }
- }
- }
- }
- }
- Qed.
-
- (* The same applies to the alternative definition of interference. *)
- Lemma instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks:
- cumulative_interference_from_other_tasks t1 t = service_of_jobs_from_other_tasks_with_hep_priority t1 t.
- Proof.
- rewrite /service_of_jobs_from_other_tasks_with_hep_priority /cumulative_interference_from_other_tasks.
- case NEQ: (t1 <= t); last first.
- { apply negbT in NEQ; rewrite -ltnNge in NEQ.
- rewrite big_geq; last by apply ltnW.
- rewrite /service_of_jobs /arrivals_between /jobs_arrived_between big_geq; last by apply ltnW.
- by rewrite big_nil.
- }
- have EX: exists k, t = t1 + k.
- { by exists (t - t1); rewrite subnKC. } move: EX => [k EQ]; subst t; clear NEQ.
- induction k.
- { rewrite addn0 big_geq; last by done.
- by rewrite /arrivals_between /jobs_arrived_between big_geq // /service_of_jobs big_nil. }
- { unfold service_of_jobs, service_during.
- rewrite addnS.
- rewrite big_nat_recr //=; last by rewrite leq_addr.
- have Fact:
- arrivals_between t1 (t1 + k).+1 =
- jobs_arrived_between arr_seq t1 (t1 + k) ++ jobs_arriving_at arr_seq (t1 + k).
- { by rewrite /arrivals_between /jobs_arrived_between big_nat_recr //= leq_addr. }
- rewrite Fact.
- rewrite /service_of_jobs IHk big_cat //=; clear IHk.
- have EQ:
- \sum_(i0 <- jobs_arriving_at arr_seq (t1 + k) |
- higher_eq_priority (job_task i0) tsk && (job_task i0 != tsk))
- service_during sched i0 t1 (t1 + k).+1
- =
- \sum_(i0 <- jobs_arriving_at arr_seq (t1 + k) |
- higher_eq_priority (job_task i0) tsk && (job_task i0 != tsk))
- service_during sched i0 (t1 + k) (t1 + k).+1.
- { rewrite /service_during.
- rewrite big_seq_cond [X in _ = X]big_seq_cond.
- apply/eqP; rewrite eqn_leq; apply/andP; split.
- { rewrite leq_sum //; move => jo /andP [ARR /andP [HP NTSK]].
- rewrite (@big_cat_nat _ _ _ (t1 + k)) //=; last by rewrite leq_addr.
- rewrite -[X in _ <= X]add0n leq_add // leqn0.
- rewrite big_nat_cond big1 //; move => x /andP [/andP [_ LT] _].
- apply/eqP; rewrite eqb0; apply/negP; intros NSCHED.
- apply H_jobs_must_arrive_to_execute in NSCHED.
- apply H_arrival_times_are_consistent in ARR.
- rewrite -ARR in LT.
- by move: LT; rewrite ltnNge; move => /negP LT.
- }
- { rewrite leq_sum //; move => jo /andP [ARR /andP [HP NTSK]].
- rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + k )) //=;last by rewrite leq_addr.
- by rewrite leq_addl //.
- }
- }
- rewrite EQ; clear EQ.
- apply/eqP.
- rewrite exchange_big //=.
- rewrite big_nat_recr //=; last by rewrite leq_addr.
- rewrite exchange_big //=.
- rewrite -addnA eqn_add2l.
- rewrite exchange_big //=.
- rewrite big_nat1.
- rewrite -big_cat //=.
- rewrite -Fact; clear Fact.
- case SCHED: (sched (t1 + k)) => [jo | ]; last first.
- { by rewrite eq_sym big1 //; rewrite /is_interference_from_another_task_with_higher_eq_priority /service_at /scheduled_at SCHED. }
- case PRIO: (higher_eq_priority (job_task jo) tsk && (job_task jo != tsk)).
- { rewrite eqn_leq; apply/andP; split.
- { rewrite (big_rem jo) //=.
- { rewrite /is_interference_from_another_task_with_higher_eq_priority /job_from_another_task_with_higher_eq_priority PRIO.
- by rewrite /service_at /scheduled_at SCHED eq_refl add1n PRIO. }
- { apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival); try done.
- { unfold jobs_come_from_arrival_sequence in *.
- apply H_jobs_come_from_arrival_sequence with (t1 + k).
- by rewrite /scheduled_at SCHED. }
- { move: PRIO => /andP [PRIO1 PRIO2].
- rewrite /arrived_between ltnS; apply/andP; split; last first.
- { by move: SCHED => /eqP SCHED; apply H_jobs_must_arrive_to_execute in SCHED. }
- { rewrite leqNgt; apply/negP; intros AB.
- move: (SCHED) => /eqP /negP SCHED2; apply: SCHED2.
- apply/negP.
- apply completed_implies_not_scheduled with job_cost; try done.
- apply completion_monotonic with t1; try done.
- rewrite leq_addr; by done.
- apply H_quiet_time; try done.
- { move: SCHED => /eqP SCHED.
- by apply H_jobs_come_from_arrival_sequence in SCHED. }
- { by rewrite /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk. }
- }
- }
- }
- }
- { rewrite /is_interference_from_another_task_with_higher_eq_priority /job_from_another_task_with_higher_eq_priority.
- rewrite SCHED PRIO.
- by eapply service_of_jobs_le_1; eauto.
- }
- }
- { rewrite eq_sym big1 /is_interference_from_another_task_with_higher_eq_priority /job_from_another_task_with_higher_eq_priority ?SCHED ?PRIO //.
- intros joo PRIO2.
- apply/eqP; rewrite eqb0; apply/negP; intros SCHED2.
- move: SCHED2 => /eqP SCHED2.
- rewrite SCHED2 in SCHED.
- inversion SCHED; subst joo.
- by rewrite PRIO in PRIO2.
- }
- }
- Qed.
-
- End InstantiatedServiceEquivalences.
-
- (* In this section we prove that the abstract definition of busy interval is equivalent to
- the conventional, concrete definition of busy interval for FP scheduling. *)
- Section BusyIntervalEquivalence.
-
- (* Consider any job j of tsk. *)
- Variable j: Job.
- Hypothesis H_j_arrives: arrives_in arr_seq j.
- Hypothesis H_job_of_tsk: job_task j = tsk.
- Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
-
- (* We prove that the concept of quiet time obtained by instantiating the abstract
- definition of quiet time coincides with the conventional definition of quiet time
- (which is defined in module limited.busy_interval). *)
- Lemma instantiated_quiet_time_equivalent_fp_quiet_time:
- forall t,
- quiet_time j t <->
- AbstractRTADefinitions.quiet_time job_arrival job_cost sched interference interfering_workload j t.
- Proof.
- intros t; split; intros.
- { unfold AbstractRTADefinitions.quiet_time; split.
- { unfold AbstractRTADefinitions.cumul_interference, AbstractRTADefinitions.cumul_interfering_workload.
- have T := cumulative_interference_split; rewrite /cumulative_interference in T.
- rewrite T !big_split //=; clear T.
- apply/eqP; rewrite eqn_add2l.
- have L11 := all_jobs_have_completed_equiv_workload_eq_service.
- have L2 := instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs;
- rewrite /cumulative_interfering_workload_of_jobs_with_hep_priority in L2.
- rewrite instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs ?L2; try done.
- rewrite eq_sym; apply/eqP.
- apply L11 with job_arrival; try done.
- intros.
- apply H; try done.
- apply in_arrivals_implies_arrived in H0; by done.
- move: H1 => /andP [H3 H4]; by done.
- by apply in_arrivals_implies_arrived_between with (job_arrival0 := job_arrival) in H0.
- }
- {
- unfold AbstractRTADefinitions.cumul_interference, AbstractRTADefinitions.cumul_interfering_workload, interference, interfering_workload.
- rewrite negb_and Bool.negb_involutive; apply/orP.
- case ARR: (arrived_before job_arrival j t); [right | by left].
- apply H; try done.
- by rewrite /jlfp_higher_eq_priority /FP_to_JLFP.
- }
- }
- { intros jhp ARR HP ARB.
- move: (posnP (job_cost jhp)) => [ZERO|POS].
- { rewrite /completed_by eqn_leq; apply/andP; split.
- - by apply H_completed_jobs_dont_execute.
- - by rewrite ZERO.
- }
- eapply all_jobs_have_completed_equiv_workload_eq_service with
- (P := (fun jhp => higher_eq_priority (job_task jhp) (job_task j)))
- (t1 := 0)(t2 := t); eauto 2; last first.
- eapply arrived_between_implies_in_arrivals; eauto 2.
- move: H => [H0 H1].
- move: H0.
- rewrite /AbstractRTADefinitions.cumul_interference /AbstractRTADefinitions.cumul_interfering_workload /interference /interfering_workload.
- have T := cumulative_interference_split; rewrite /cumulative_interference in T.
- rewrite T !big_split //=; clear T; move => /eqP; rewrite eqn_add2l.
- have L2 := instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs;
- rewrite /cumulative_interfering_workload_of_jobs_with_hep_priority /workload_of_other_jobs_with_hep_priority in L2.
- rewrite instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs ?L2; try done.
- rewrite /service_of_other_jobs_with_hep_priority; move => H2.
- have H2EQ:
- service_of_jobs sched (arrivals_between 0 t) (fun jhp : Job => higher_eq_priority (job_task jhp) (job_task j)) 0 t ==
- workload_of_jobs job_cost (arrivals_between 0 t) (fun jhp : Job => higher_eq_priority (job_task jhp) (job_task j)).
- { move: H1; rewrite negb_and Bool.negb_involutive -leqNgt; move => /orP [H1 | H1].
- { intros.
- have NOTIN: j \notin arrivals_between 0 t.
- { apply/memPn.
- intros jo IN; apply/negP; intros EQ; move: EQ => /eqP EQ.
- subst jo.
- unfold arrivals_between in *.
- apply in_arrivals_implies_arrived_between with (job_arrival0:= job_arrival) in IN; try done.
- by move: IN => /andP [_ IN]; move: H1; rewrite leqNgt; move => /negP LT; apply: LT.
- }
- by rewrite /service_of_jobs /workload_of_jobs !sum_notin_rem_eqn in H2.
- }
- { have JIN: j \in arrivals_between 0 t.
- { eapply completed_implies_scheduled_before in H1; eauto 2.
- apply arrived_between_implies_in_arrivals with (job_arrival0:= job_arrival); try done.
- move: H1 => [t' [H3 _]].
- apply/andP; split; first by done.
- move: H3 => /andP [H3e H3t].
- by apply leq_ltn_trans with t'.
- }
- have UNIC: uniq (arrivals_between 0 t).
- { by eapply arrivals_uniq; eauto 2. }
- unfold service_of_jobs, workload_of_jobs in H2.
- unfold service_of_jobs, workload_of_jobs.
- rewrite big_mkcond //=.
- rewrite (bigD1_seq j) //=.
- rewrite -big_mkcondl //=.
- move: H2 => /eqP H2. rewrite H2.
- rewrite [X in _ == X]big_mkcond //=.
- rewrite [X in _ == X](bigD1_seq j) //=.
- rewrite -big_mkcondl //=.
- rewrite eqn_add2r.
- move: H1 => /eqP H1.
- by rewrite -H1.
- }
- }
- unfold workload_of_jobs in *.
- unfold workload_of_jobs in H2EQ. move: H2EQ => /eqP H2EQ. rewrite -H2EQ.
- clear H2EQ.
- by done.
- }
- Qed.
-
- (* Based on that, we prove that the concept of busy interval obtained by instantiating the abstract
- definition of busy interval coincides with the conventional definition of busy interval. *)
- Lemma instantiated_busy_interval_equivalent_fp_busy_interval:
- forall t1 t2,
- busy_interval j t1 t2 <->
- AbstractRTADefinitions.busy_interval job_arrival job_cost sched interference interfering_workload j t1 t2.
- Proof.
- split.
- { move => [[LT [QTt1 [NQT REL]] QTt2]].
- - split; last by eapply instantiated_quiet_time_equivalent_fp_quiet_time in QTt2; eauto 2.
- - split; first by done.
- - split; first by apply instantiated_quiet_time_equivalent_fp_quiet_time in QTt1; eauto 2.
- by intros t NEQ QT; eapply NQT; eauto 2; apply instantiated_quiet_time_equivalent_fp_quiet_time.
- }
- { move => [[REL [QTt1 NQT]] QTt2].
- move: (REL) => /andP [NEQ1 NEQ2].
- - split; last by eapply instantiated_quiet_time_equivalent_fp_quiet_time; eauto 2.
- - split; first by apply leq_ltn_trans with (job_arrival j).
- - split; first by eapply instantiated_quiet_time_equivalent_fp_quiet_time; eauto 2.
- - split; first by intros t NEQ QT; eapply NQT; eauto 2; eapply instantiated_quiet_time_equivalent_fp_quiet_time in QT; eauto 2.
- - by done.
- }
- Qed.
-
- End BusyIntervalEquivalence.
-
- End Equivalences.
-
(** ** Filling Out Hypotheses Of Abstract RTA Theorem *)
(** In this section we prove that all preconditions necessary to use the abstract theorem are satisfied. *)
Section FillingOutHypothesesOfAbstractRTATheorem.
@@ -802,7 +214,9 @@ Module AbstractRTAforFPwithArrivalCurves.
- by subst s; rewrite /scheduled_at SCHED.
}
{ exfalso; clear HYP1 HYP2.
- apply instantiated_busy_interval_equivalent_fp_busy_interval in BUSY; try done.
+ eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; try done; first last.
+ { by intros x; apply H_priority_is_reflexive. }
+ { by apply job_task. }
have EQ:= not_quiet_implies_not_idle
job_arrival job_cost arr_seq _
sched jlfp_higher_eq_priority j _ _ _ _ _ _ t1 t2 _ t.
@@ -814,7 +228,8 @@ Module AbstractRTAforFPwithArrivalCurves.
}
{ move: HYP => /eqP HYP.
apply/negP.
- rewrite /interference /is_priority_inversion /BusyIntervalJLFP.is_priority_inversion
+ rewrite /interference /JLFPInstantiation.interference /is_priority_inversion
+ /BusyIntervalJLFP.is_priority_inversion
/jlfp_higher_eq_priority /is_interference_from_another_job_with_higher_eq_priority HYP negb_or.
apply/andP; split.
- by rewrite Bool.negb_involutive /FP_to_JLFP.
@@ -823,13 +238,15 @@ Module AbstractRTAforFPwithArrivalCurves.
Qed.
(* Next, we prove that the interference and interfering workload
- functions are consistent with the task service. *)
+ functions are consistent with sequential jobs. *)
Lemma instantiated_interference_and_workload_consistent_with_sequential_jobs:
AbstractSeqRTA.interference_and_workload_consistent_with_sequential_jobs
job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload.
Proof.
intros j t1 t2 ARR TSK POS BUSY.
- apply instantiated_busy_interval_equivalent_fp_busy_interval in BUSY; try by done.
+ eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; first last; try by done.
+ { by intros x; apply H_priority_is_reflexive. }
+ { by apply job_task. }
eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2; intros s ARRs TSKs.
move: (BUSY) => [[_ [QT _]] _].
apply QT.
@@ -863,7 +280,8 @@ Module AbstractRTAforFPwithArrivalCurves.
move: EX => [t1 [t2 [H1 [H2 GGG]]]].
exists t1, t2; split; first by done.
split; first by done.
- by eapply instantiated_busy_interval_equivalent_fp_busy_interval; eauto 2.
+ eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2.
+ by intros x; apply H_priority_is_reflexive.
Qed.
(* Next, we prove that IBF is indeed an interference bound.
@@ -892,20 +310,23 @@ Module AbstractRTAforFPwithArrivalCurves.
- by apply H_completed_jobs_dont_execute.
- by rewrite ZERO.
}
- eapply instantiated_busy_interval_equivalent_fp_busy_interval in BUSY; try done.
+ eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; first last; try done.
+ { by intros x; apply H_priority_is_reflexive. }
+ { by apply job_task. }
have T123 := cumulative_task_interference_split.
rewrite /cumulative_task_interference in T123.
- rewrite (T123 j); eauto 2; last first.
+ rewrite (T123 _ _ job_arrival job_cost _ _ _ _ _ _ _ _ j); eauto 2; last first.
{ move: BUSY => [[_ [_ [_ /andP [GE LT]]]] _].
by eapply arrived_between_implies_in_arrivals; eauto 2. }
+ { by apply any_reflexive_FP_respects_sequential_jobs. }
unfold IBF, interference.
rewrite leq_add; try done.
{ unfold is_priority_inversion, FP_to_JLFP.
unfold priority_inversion_is_bounded_by in *.
move: (H_priority_inversion_is_bounded j ARR TSK) => BOUND.
- apply leq_trans with (cumulative_priority_inversion j t1 (t1 + R0)).
+ apply leq_trans with (cumulative_priority_inversion sched jlfp_higher_eq_priority j t1 (t1 + R0)).
{ by done. }
- { apply leq_trans with (cumulative_priority_inversion j t1 t2).
+ { apply leq_trans with (cumulative_priority_inversion sched jlfp_higher_eq_priority j t1 t2).
{ rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + R0)) //=.
- by rewrite leq_addr.
- by rewrite leq_addr.
@@ -915,15 +336,17 @@ Module AbstractRTAforFPwithArrivalCurves.
}
}
{ intros.
- rewrite (instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks j); last first.
+ rewrite
+ (instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks
+ job_arrival job_cost _ arr_seq); last first; try done.
{ by unfold quiet_time; move: BUSY => [[_ [H1 H2]] _]. }
- { by done. }
- apply leq_trans with (workload_of_jobs job_cost (arrivals_between t1 (t1 + R0))
- job_from_another_task_with_higher_eq_priority).
+ apply leq_trans with
+ (workload_of_jobs
+ job_cost (arrivals_between t1 (t1 + R0))
+ (fun jhp : Job => jlfp_higher_eq_priority jhp j && (job_task jhp != job_task j))).
{ by apply service_of_jobs_le_workload. }
{ rewrite /workload_of_jobs
- /total_ohep_rbf /total_ohep_request_bound_function_FP
- /job_from_another_task_with_higher_eq_priority.
+ /total_ohep_rbf /total_ohep_request_bound_function_FP.
rewrite -TSK; apply total_workload_le_total_rbf; try done.
by intros tsko INo; move: (H_family_of_proper_arrival_curves tsko INo) => [ARRB _].
}
@@ -971,7 +394,7 @@ Module AbstractRTAforFPwithArrivalCurves.
by rewrite -EQ.
Qed.
- (* Then, there exists a solution for the response-time recurrence. *)
+ (* Then, there exists a solution for the response-time recurrence (in the abstract sense). *)
Corollary correct_search_space:
exists F,
A + F = task_rbf (A + ε) - (task_cost tsk - task_lock_in_service tsk) + IBF (A + F) /\