Library prosa.results.arm.fp.floating_nonpreemptive
Require Import prosa.analysis.facts.readiness.basic.
Require Export prosa.model.composite.valid_task_arrival_sequence.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
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.sbf.average.
Require Export prosa.model.composite.valid_task_arrival_sequence.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
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.sbf.average.
RTA for FP Scheduling with Floating Non-Preemptive Regions on Uniprocessors under the Average Resource Model
Defining the System Model
- tasks, jobs, and their parameters,
- the task set and the task under analysis,
- the processor model,
- the sequence of job arrivals,
- the absence of self-suspensions,
- an arbitrary schedule of the task set, and finally,
- the resource-supply 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}.
`{JobPreemptionPoints Job}.
We assume that jobs are limited-preemptive.
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
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.
Assume a model with floating non-preemptive regions. I.e., for each task
only the length of the maximal non-preemptive segment is known and each
job is divided into a number of non-preemptive segments by inserting
preemption points.
Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq.
valid_model_with_floating_nonpreemptive_regions arr_seq.
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 that corresponds to the given arrival sequence arr_seq (and
hence the given task set ts).
Variable sched : schedule PState.
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 that jobs of the same
task are executed in the order of their arrival.
Average Resource Model
[t1, t2), and given a
resource period Π, a resource allocation time Θ, and a supply delay
ν, the processor provides at least (t2 - t1 - ν) ⋅ Θ / Π units of
supply. Intuitively, this means that on _average, the processor
delivers Θ units of output every Π units of time, while the
distribution of supply is not ideal and is subject to fluctuations bounded
by ν. Furthermore, let arm_sbf Π Θ ν denote the SBF, which, as proven
in prosa.analysis.facts.model.sbf.average, is a valid SBF.
Variables Π Θ ν : duration.
Hypothesis H_average_resource_model : average_resource_model Π Θ ν sched.
Hypothesis H_average_resource_model : average_resource_model Π Θ ν sched.
Maximum Length of a Busy Interval
Definition busy_window_recurrence_solution (L : duration) :=
L > 0
∧ arm_sbf Π Θ ν L ≥ blocking_bound ts tsk + total_hep_request_bound_function_FP ts tsk L.
L > 0
∧ arm_sbf Π Θ ν L ≥ blocking_bound ts tsk + total_hep_request_bound_function_FP ts tsk L.
Response-Time Bound
Definition rta_recurrence_solution L R :=
∀ (A : duration),
is_in_search_space tsk L A →
∃ (F : duration),
arm_sbf Π Θ ν F ≥ blocking_bound ts tsk
+ task_request_bound_function tsk (A + ε)
+ total_ohep_request_bound_function_FP ts tsk F
∧ A + R ≥ F.
∀ (A : duration),
is_in_search_space tsk L A →
∃ (F : duration),
arm_sbf Π Θ ν F ≥ blocking_bound ts tsk
+ task_request_bound_function tsk (A + ε)
+ total_ohep_request_bound_function_FP ts tsk F
∧ A + R ≥ F.
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 floating non-preemptive regions on a
unit-speed uniprocessor under the average resource model.