Library prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.concrete_models.response_time_bound
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.limited.schedule
prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound
prosa.classic.model.schedule.uni.limited.rbf.
Require Import prosa.classic.model.arrival.curves.bounds
prosa.classic.analysis.uni.arrival_curves.workload_bound.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule
prosa.classic.model.schedule.uni.limited.platform.limited
prosa.classic.model.schedule.uni.limited.platform.preemptive
prosa.classic.model.schedule.uni.limited.platform.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.limited.schedule
prosa.classic.model.schedule.uni.limited.fixed_priority.nonpr_reg.response_time_bound
prosa.classic.model.schedule.uni.limited.rbf.
Require Import prosa.classic.model.arrival.curves.bounds
prosa.classic.analysis.uni.arrival_curves.workload_bound.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule
prosa.classic.model.schedule.uni.limited.platform.limited
prosa.classic.model.schedule.uni.limited.platform.preemptive
prosa.classic.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 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:
∀ 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.
Import 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:
∀ 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:
∀ A,
is_in_search_space A →
∃ 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.
End 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:
∀ A,
is_in_search_space A →
∃ 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.
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:
∀ A,
is_in_search_space A →
∃ 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.
End 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:
∀ A,
is_in_search_space A →
∃ 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.
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:
∀ A,
is_in_search_space A →
∃ 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.
End 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:
∀ A,
is_in_search_space A →
∃ 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.
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:
∀ A,
is_in_search_space A →
∃ 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.
End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
End Analysis.
End RTAforConcreteModels.
(* 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:
∀ A,
is_in_search_space A →
∃ 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.
End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
End Analysis.
End RTAforConcreteModels.