Library prosa.results.ovh.fifo.bounded_nps
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.jlfp.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fifo.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fifo_fixpoint.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.priority.fifo.
Require Export prosa.analysis.facts.priority.fifo_ahep_bound.
Require Export prosa.analysis.facts.model.overheads.sbf.fifo.
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.jlfp.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fifo.
Require Export prosa.analysis.abstract.restricted_supply.search_space.fifo_fixpoint.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.priority.fifo.
Require Export prosa.analysis.facts.priority.fifo_ahep_bound.
Require Export prosa.analysis.facts.model.overheads.sbf.fifo.
RTA for FIFO Scheduling 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
Context {Task : TaskType} `{TaskCost Task} `{MaxArrivals Task}
`{TaskRunToCompletionThreshold Task}.
`{TaskRunToCompletionThreshold Task}.
... 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_preemptable.
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 that tsk is described by a valid task run-to-completion
threshold. That is, there exists a task parameter task_rtct such that
task_rtct tsk is
Hypothesis H_valid_run_to_completion_threshold :
valid_task_run_to_completion_threshold arr_seq tsk.
valid_task_run_to_completion_threshold arr_seq tsk.
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
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_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
We assume that the schedule complies with some valid preemption model.
Under FIFO scheduling, the specific choice of preemption model does not
matter, since the resulting schedule behaves as if it were non-preemptive:
jobs are executed in arrival order without preemption.
We assume that the schedule respects the FIFO scheduling policy.
Furthermore, we require that the schedule has no superfluous preemptions;
that is, 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 FIFO scheduling, the bound in an interval of length Δ is
determined by the total number of arrivals in the system. In this case, up
to n such arrivals can lead to at most 1 + n segments without a
schedule change, each potentially incurring dispatch, context-switch, and
preemption-related overhead. Unlike JLFP and FP, FIFO does not require
doubling the arrivals (i.e., 1 + 2n), because all jobs are treated
uniformly and there are no preemptions caused by higher-priority jobs.
We denote this bound by overhead_bound for the task under analysis
tsk.
Workload Abbreviations
Maximum Length of a Busy Interval
Definition busy_window_recurrence_solution (L : duration) :=
L > 0
∧ L ≥ overhead_bound L + total_request_bound_function ts L.
L > 0
∧ L ≥ overhead_bound L + total_request_bound_function ts L.
Response-Time Bound
Definition rta_recurrence_solution L R :=
∀ (A : duration),
is_in_search_space ts L A →
∃ (F : duration),
A ≤ F ≤ A + R
∧ F ≥ overhead_bound F + total_request_bound_function ts (A + ε).
∀ (A : duration),
is_in_search_space ts L A →
∃ (F : duration),
A ≤ F ≤ A + R
∧ F ≥ overhead_bound F + total_request_bound_function ts (A + ε).
Finally, using the abstract restricted-supply analysis, we establish that
any R that satisfies the stated equation is a sound response-time bound
for FIFO scheduling on a unit-speed uniprocessor subject to scheduling
overheads.
Theorem uniprocessor_response_time_bound_fifo :
∀ (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 := fifo_ovh_sbf_slow ts DB CSB CRPDB).
move⇒ L [BW_POS BW_SOL] R SOL js ARRs TSKs.
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
with (L := L) (intra_IBF := fun A Δ ⇒ (\sum_(tsko <- ts) task_request_bound_function tsko (A + ε)) - task_cost tsk) ⇒ //.
- exact: instantiated_i_and_w_are_coherent_with_schedule.
- eapply busy_intervals_are_bounded_rs_jlfp with (blocking_bound := fun _ ⇒ 0)=> //.
+ exact: instantiated_i_and_w_are_coherent_with_schedule.
+ by apply: FIFO_implies_no_service_inversion.
+ apply bound_preserved_under_slowed.
by move: BW_SOL; rewrite add0n /sSBF /fifo_blackout_bound /overhead_bound; lia.
- apply: valid_pred_sbf_switch_predicate; last (eapply overheads_sbf_busy_valid) ⇒ //=.
move ⇒ ? ? ? ? [? ?]; split ⇒ //.
by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
- move ⇒ t1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
move: (OFF _ _ BUSY) ⇒ EQA; subst A.
have [ZERO|POSj] := posnP (job_cost j).
{ by exfalso; rewrite /completed_by ZERO in NCOMPL. }
eapply leq_trans; first by eapply cumulative_intra_interference_split ⇒ //.
rewrite -[leqRHS]add0n leq_add //.
+ rewrite (leqRW (service_inversion_widen _ _ _ _ _ _ _ _ _)).
× apply: FIFO_implies_no_service_inversion ⇒ //.
by apply instantiated_busy_interval_equivalent_busy_interval ⇒ //.
× by done.
× by done.
+ unshelve apply: bound_on_hep_workload; (try apply H_fixed_point).
all: try apply H_L_positive.
all: try done.
apply instantiated_busy_interval_equivalent_busy_interval ⇒ //.
- apply: soln_abstract_response_time_recurrence ⇒ //.
+ by apply overheads_sbf_monotone.
+ by apply: non_pathological_max_arrivals =>//; apply H_valid_task_arrival_sequence.
+ move ⇒ A SP; move: (SOL A) ⇒ [] ⇒ // ⇒ δ [INδ FIXδ].
∃ δ; split; [done | apply bound_preserved_under_slowed].
by move: FIXδ; rewrite /sSBF /fifo_blackout_bound /overhead_bound; lia.
Qed.
End RTAforFIFOModelwithArrivalCurves.
∀ (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 := fifo_ovh_sbf_slow ts DB CSB CRPDB).
move⇒ L [BW_POS BW_SOL] R SOL js ARRs TSKs.
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
with (L := L) (intra_IBF := fun A Δ ⇒ (\sum_(tsko <- ts) task_request_bound_function tsko (A + ε)) - task_cost tsk) ⇒ //.
- exact: instantiated_i_and_w_are_coherent_with_schedule.
- eapply busy_intervals_are_bounded_rs_jlfp with (blocking_bound := fun _ ⇒ 0)=> //.
+ exact: instantiated_i_and_w_are_coherent_with_schedule.
+ by apply: FIFO_implies_no_service_inversion.
+ apply bound_preserved_under_slowed.
by move: BW_SOL; rewrite add0n /sSBF /fifo_blackout_bound /overhead_bound; lia.
- apply: valid_pred_sbf_switch_predicate; last (eapply overheads_sbf_busy_valid) ⇒ //=.
move ⇒ ? ? ? ? [? ?]; split ⇒ //.
by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
- move ⇒ t1 t2 Δ j ARR TSK BUSY LT NCOMPL A OFF.
move: (OFF _ _ BUSY) ⇒ EQA; subst A.
have [ZERO|POSj] := posnP (job_cost j).
{ by exfalso; rewrite /completed_by ZERO in NCOMPL. }
eapply leq_trans; first by eapply cumulative_intra_interference_split ⇒ //.
rewrite -[leqRHS]add0n leq_add //.
+ rewrite (leqRW (service_inversion_widen _ _ _ _ _ _ _ _ _)).
× apply: FIFO_implies_no_service_inversion ⇒ //.
by apply instantiated_busy_interval_equivalent_busy_interval ⇒ //.
× by done.
× by done.
+ unshelve apply: bound_on_hep_workload; (try apply H_fixed_point).
all: try apply H_L_positive.
all: try done.
apply instantiated_busy_interval_equivalent_busy_interval ⇒ //.
- apply: soln_abstract_response_time_recurrence ⇒ //.
+ by apply overheads_sbf_monotone.
+ by apply: non_pathological_max_arrivals =>//; apply H_valid_task_arrival_sequence.
+ move ⇒ A SP; move: (SOL A) ⇒ [] ⇒ // ⇒ δ [INδ FIXδ].
∃ δ; split; [done | apply bound_preserved_under_slowed].
by move: FIXδ; rewrite /sSBF /fifo_blackout_bound /overhead_bound; lia.
Qed.
End RTAforFIFOModelwithArrivalCurves.