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.
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.
End RTAforFIFOModelwithArrivalCurves.