Library prosa.results.ovh.fp.limited_preemptive
Require Export prosa.model.job.properties.
Require Export prosa.model.composite.valid_task_arrival_sequence.
Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.analysis.facts.model.overheads.schedule.
Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.fp.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fp.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.model.overheads.sbf.fp.
Require Export prosa.model.composite.valid_task_arrival_sequence.
Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.analysis.facts.model.overheads.schedule.
Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.fp.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fp.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.model.overheads.sbf.fp.
RTA for FP Scheduling with Fixed Preemption Points on Uniprocessors with Overheads
Defining the System Model
- the processor model,
- tasks, jobs, and their parameters,
- the task set and the task under analysis,
- the sequence of job arrivals,
- the absence of self-suspensions,
- an arbitrary schedule of the task set, and finally,
- a supply-bound function to account for overhead-induced delays.
Processor Model
Tasks and Jobs
... and their associated jobs, where each job has a corresponding task
job_task, an execution time job_cost, an arrival time job_arrival,
and a list of preemption points
job_preemptive_points.
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{JobArrival Job} `{JobPreemptionPoints Job}.
We assume that jobs are limited-preemptive.
The Job Arrival Sequence
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_task_arrival_sequence : valid_task_arrival_sequence ts arr_seq.
Hypothesis H_valid_task_arrival_sequence : valid_task_arrival_sequence ts arr_seq.
We assume a model with fixed preemption points. I.e., each task is divided
into a number of non-preemptive segments by inserting statically
predefined preemption points.
Hypothesis H_valid_model_with_fixed_preemption_points :
valid_fixed_preemption_points_model arr_seq ts.
valid_fixed_preemption_points_model arr_seq ts.
Additionally, we assume that all jobs in arr_seq have positive execution
costs. This requirement is not fundamental to the analysis approach itself
but reflects an artifact of the current proof structure specific to upper
bounds on the total duration of overheads.
Absence of Self-Suspensions
The Schedule
Context {FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
Hypothesis H_priority_is_transitive : transitive_task_priorities FP.
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
Hypothesis H_priority_is_transitive : transitive_task_priorities FP.
Consider a work-conserving, valid uniprocessor schedule with limited
preemptions and explicit overheads that corresponds to the given arrival
sequence arr_seq (and hence the given task set ts).
Variable sched : schedule (overheads.processor_state Job).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_schedule_with_limited_preemptions :
schedule_respects_preemption_model arr_seq sched.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_schedule_with_limited_preemptions :
schedule_respects_preemption_model arr_seq sched.
We assume that the schedule respects the given FP scheduling policy.
Furthermore, we require that the schedule ensures two additional
properties: jobs of the same task are executed in the order of their
arrival, ...
... and preemptions occur only when strictly required by the scheduling
policy (specifically, a job is never preempted by another job of equal
priority).
Bounding the Total Overhead Duration
Variable DB CSB CRPDB : duration.
Hypothesis H_valid_overheads_model : overhead_resource_model sched DB CSB CRPDB.
Hypothesis H_valid_overheads_model : overhead_resource_model sched DB CSB CRPDB.
To conservatively account for the maximum cumulative delay that task tsk
may experience due to scheduling overheads, we introduce an overhead
bound. This term upper-bounds the maximum cumulative duration during
which processor cycles are "lost" to dispatch, context-switch, and
preemption-related delays in a given interval.
Under FP scheduling, the bound in an interval of length Δ is determined
by the arrivals of tasks with higher-or-equal priority relative to
tsk. Up to n such arrivals can lead to at most 1 + 2n segments
without a schedule change, each potentially incurring dispatch,
context-switch, and preemption-related overhead.
We denote this bound by overhead_bound for the task under analysis
tsk.
Let overhead_bound Δ :=
(DB + CSB + CRPDB) × (1 + 2 × \sum_(tsk_o <- ts | hep_task tsk_o tsk) max_arrivals tsk_o Δ).
(DB + CSB + CRPDB) × (1 + 2 × \sum_(tsk_o <- ts | hep_task tsk_o tsk) max_arrivals tsk_o Δ).
Workload Abbreviations
Additionally, we let total_hep_rbf denote the cumulative request-bound
function w.r.t. all tasks with higher-or-equal priority ...
... and use total_ohep_rbf as an abbreviation for the cumulative
request-bound function w.r.t. all tasks with higher-or-equal priority
other than task tsk itself.
Maximum Length of a Busy Interval
Definition busy_window_recurrence_solution (L : duration) :=
L > 0
∧ L ≥ overhead_bound L
+ blocking_bound ts tsk
+ total_hep_rbf L.
L > 0
∧ L ≥ overhead_bound L
+ blocking_bound ts tsk
+ total_hep_rbf L.
Response-Time Bound
Definition rta_recurrence_solution L R :=
∀ (A : duration),
is_in_search_space tsk L A →
∃ (F : duration),
A ≤ F ≤ A + R
∧ F ≥ overhead_bound F
+ blocking_bound ts tsk
+ (rbf tsk (A + ε) - (task_last_nonpr_segment tsk - ε))
+ total_ohep_rbf F
∧ A + R ≥ F + (overhead_bound (A + R) - overhead_bound F)
+ (task_last_nonpr_segment tsk - ε).
∀ (A : duration),
is_in_search_space tsk L A →
∃ (F : duration),
A ≤ F ≤ A + R
∧ F ≥ overhead_bound F
+ blocking_bound ts tsk
+ (rbf tsk (A + ε) - (task_last_nonpr_segment tsk - ε))
+ total_ohep_rbf F
∧ A + R ≥ F + (overhead_bound (A + R) - overhead_bound F)
+ (task_last_nonpr_segment tsk - ε).
Finally, using the sequential variant of abstract restricted-supply
analysis, we establish that, given a bound on the maximum busy-window
length L, any such R is indeed a sound response-time bound for task
tsk under FP scheduling with limited preemptions on a unit-speed
uniprocessor subject to scheduling overheads.
Theorem uniprocessor_response_time_bound_limited_fp :
∀ (L : duration),
busy_window_recurrence_solution L →
∀ (R : duration),
rta_recurrence_solution L R →
task_response_time_bound arr_seq sched tsk R.
Proof.
set (sSBF := fp_ovh_sbf_slow ts DB CSB CRPDB tsk).
move⇒ L [BW_POS BW_SOL] R SOL js ARRs TSKs.
have VAL1 : valid_preemption_model arr_seq sched
by apply valid_fixed_preemption_points_model_lemma, H_valid_model_with_fixed_preemption_points.
have [ZERO|POS] := posnP (job_cost js); first by rewrite /job_response_time_bound /completed_by ZERO.
have VBSBF : valid_busy_sbf arr_seq sched tsk (sSBF) by apply overheads_sbf_busy_valid ⇒ //=.
have USBF : unit_supply_bound_function (sSBF) by apply overheads_sbf_unit ⇒ //=.
have POStsk: 0 < task_cost tsk
by move: TSKs ⇒ /eqP <-; apply: leq_trans; [apply POS | apply H_valid_task_arrival_sequence].
eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) (SBF := sSBF) ⇒ //=.
- exact: instantiated_i_and_w_are_coherent_with_schedule.
- by exact: instantiated_interference_and_workload_consistent_with_sequential_tasks ⇒ //.
- eapply busy_intervals_are_bounded_rs_fp with (SBF := sSBF); try done.
+ by eapply instantiated_i_and_w_are_coherent_with_schedule.
+ by apply bound_preserved_under_slowed; unfold fp_blackout_bound, overhead_bound, total_hep_rbf in *; lia.
- apply: valid_pred_sbf_switch_predicate; last (eapply overheads_sbf_busy_valid) ⇒ //=.
by move ⇒ ? ? ? ? [? ?]; split ⇒ //; apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
- apply: instantiated_task_intra_interference_is_bounded; eauto 1 ⇒ //; first last.
+ by apply athep_workload_le_total_ohep_rbf.
+ apply: service_inversion_is_bounded ⇒ // ⇒ jo t1 t2 ARRo TSKo BUSYo.
unshelve rewrite (leqRW (nonpreemptive_segments_bounded_by_blocking _ _ _ _ _ _ _ _ _)) ⇒ //.
by instantiate (1 := fun _ ⇒ blocking_bound ts tsk).
- move ⇒ A SP; move: (SOL A) ⇒ [].
+ apply: search_space_sub ⇒ //=.
by apply: non_pathological_max_arrivals =>//; apply H_valid_task_arrival_sequence.
+ move ⇒ F [/andP [_ LE] [FIX1 FIX2]].
have [δ [LEδ EQ]]:= slowed_subtraction_value_preservation
(fp_blackout_bound ts DB CSB CRPDB tsk) F (ltac:(apply fp_blackout_bound_monotone ⇒ //)).
∃ δ; split; [lia | split].
× rewrite /sSBF /fp_ovh_sbf_slow -EQ.
apply: leq_trans; last by apply leq_subRL_impl; rewrite -!addnA in FIX1; apply FIX1.
have NEQ: total_ohep_request_bound_function_FP ts tsk δ ≤ total_ohep_rbf F by apply total_ohep_rbf_monotone ⇒ //.
erewrite last_segment_eq_cost_minus_rtct; [ | eauto | eauto ].
by move: FIX1; rewrite /task_intra_IBF; set (c := _ _ (A +1) - ( _ )); unfold total_ohep_rbf in *; lia.
× rewrite /sSBF /fp_ovh_sbf_slow -EQ.
apply bound_preserved_under_slowed, leq_subRL_impl; apply: leq_trans; last by apply FIX2.
erewrite last_segment_eq_cost_minus_rtct; [ | eauto | eauto ].
rewrite /task_rtct /constant /fp_blackout_bound /overhead_bound.
unfold overhead_bound in *; lia.
Qed.
End RTAforLimitedPreemptiveFPModelwithArrivalCurves.
∀ (L : duration),
busy_window_recurrence_solution L →
∀ (R : duration),
rta_recurrence_solution L R →
task_response_time_bound arr_seq sched tsk R.
Proof.
set (sSBF := fp_ovh_sbf_slow ts DB CSB CRPDB tsk).
move⇒ L [BW_POS BW_SOL] R SOL js ARRs TSKs.
have VAL1 : valid_preemption_model arr_seq sched
by apply valid_fixed_preemption_points_model_lemma, H_valid_model_with_fixed_preemption_points.
have [ZERO|POS] := posnP (job_cost js); first by rewrite /job_response_time_bound /completed_by ZERO.
have VBSBF : valid_busy_sbf arr_seq sched tsk (sSBF) by apply overheads_sbf_busy_valid ⇒ //=.
have USBF : unit_supply_bound_function (sSBF) by apply overheads_sbf_unit ⇒ //=.
have POStsk: 0 < task_cost tsk
by move: TSKs ⇒ /eqP <-; apply: leq_trans; [apply POS | apply H_valid_task_arrival_sequence].
eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) (SBF := sSBF) ⇒ //=.
- exact: instantiated_i_and_w_are_coherent_with_schedule.
- by exact: instantiated_interference_and_workload_consistent_with_sequential_tasks ⇒ //.
- eapply busy_intervals_are_bounded_rs_fp with (SBF := sSBF); try done.
+ by eapply instantiated_i_and_w_are_coherent_with_schedule.
+ by apply bound_preserved_under_slowed; unfold fp_blackout_bound, overhead_bound, total_hep_rbf in *; lia.
- apply: valid_pred_sbf_switch_predicate; last (eapply overheads_sbf_busy_valid) ⇒ //=.
by move ⇒ ? ? ? ? [? ?]; split ⇒ //; apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
- apply: instantiated_task_intra_interference_is_bounded; eauto 1 ⇒ //; first last.
+ by apply athep_workload_le_total_ohep_rbf.
+ apply: service_inversion_is_bounded ⇒ // ⇒ jo t1 t2 ARRo TSKo BUSYo.
unshelve rewrite (leqRW (nonpreemptive_segments_bounded_by_blocking _ _ _ _ _ _ _ _ _)) ⇒ //.
by instantiate (1 := fun _ ⇒ blocking_bound ts tsk).
- move ⇒ A SP; move: (SOL A) ⇒ [].
+ apply: search_space_sub ⇒ //=.
by apply: non_pathological_max_arrivals =>//; apply H_valid_task_arrival_sequence.
+ move ⇒ F [/andP [_ LE] [FIX1 FIX2]].
have [δ [LEδ EQ]]:= slowed_subtraction_value_preservation
(fp_blackout_bound ts DB CSB CRPDB tsk) F (ltac:(apply fp_blackout_bound_monotone ⇒ //)).
∃ δ; split; [lia | split].
× rewrite /sSBF /fp_ovh_sbf_slow -EQ.
apply: leq_trans; last by apply leq_subRL_impl; rewrite -!addnA in FIX1; apply FIX1.
have NEQ: total_ohep_request_bound_function_FP ts tsk δ ≤ total_ohep_rbf F by apply total_ohep_rbf_monotone ⇒ //.
erewrite last_segment_eq_cost_minus_rtct; [ | eauto | eauto ].
by move: FIX1; rewrite /task_intra_IBF; set (c := _ _ (A +1) - ( _ )); unfold total_ohep_rbf in *; lia.
× rewrite /sSBF /fp_ovh_sbf_slow -EQ.
apply bound_preserved_under_slowed, leq_subRL_impl; apply: leq_trans; last by apply FIX2.
erewrite last_segment_eq_cost_minus_rtct; [ | eauto | eauto ].
rewrite /task_rtct /constant /fp_blackout_bound /overhead_bound.
unfold overhead_bound in *; lia.
Qed.
End RTAforLimitedPreemptiveFPModelwithArrivalCurves.