Library prosa.results.edf.rta.floating_nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
RTA for EDF with Floating Non-Preemptive Regions
In this module we prove the RTA theorem for floating non-preemptive regions EDF model.
Require Import prosa.model.priority.edf.
Require Import prosa.model.processor.ideal.
Require Import prosa.model.readiness.basic.
Require Import prosa.model.processor.ideal.
Require Import prosa.model.readiness.basic.
Furthermore, we assume the task model with floating non-preemptive regions.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any arrival sequence with consistent, non-duplicate arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
Assume we have the 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 level is divided into a number
of non-preemptive segments by inserting preemption points.
Context `{JobPreemptionPoints Job}
`{TaskMaxNonpreemptiveSegment Task}.
Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions:
valid_model_with_floating_nonpreemptive_regions arr_seq.
`{TaskMaxNonpreemptiveSegment Task}.
Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions:
valid_model_with_floating_nonpreemptive_regions arr_seq.
Consider an arbitrary task set ts, ...
... assume that all jobs come from this task set, ...
... and the cost of a job cannot be larger than the task cost.
Let max_arrivals be a family of valid 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.
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
Let [tsk] be any task in ts that is to be analyzed.
Next, consider any ideal uni-processor schedule with limited
preemptions of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_schedule_with_limited_preemptions:
schedule_respects_preemption_model arr_seq sched.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_schedule_with_limited_preemptions:
schedule_respects_preemption_model arr_seq sched.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Assume we have sequential tasks, i.e, jobs from the
same task execute in the order of their arrival.
Next, we assume that the schedule is a work-conserving schedule...
... and the schedule respects the policy defined by the
job_preemptable function (i.e., jobs have bounded non-preemptive
segments).
Total Workload and Length of Busy Interval
Next, we introduce [task_rbf] as an abbreviation
for the task request bound function of task [tsk].
Using the sum of individual request bound functions, we define the request bound
function of all tasks (total request bound function).
We define a bound for the priority inversion caused by jobs with lower priority.
Definition blocking_bound :=
\max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk))
(task_max_nonpreemptive_segment tsk_other - ε).
\max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk))
(task_max_nonpreemptive_segment tsk_other - ε).
Next, we define an upper bound on interfering workload received from jobs
of other tasks with higher-than-or-equal priority.
Let bound_on_total_hep_workload A Δ :=
\sum_(tsk_o <- ts | tsk_o != tsk)
rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
\sum_(tsk_o <- ts | tsk_o != tsk)
rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
Let L be any positive fixed point of the busy interval recurrence.
Response-Time Bound
Consider any value R, and assume that for any given arrival offset A in the search space,
there is a solution of the response-time bound recurrence which is bounded by R.
Variable R : duration.
Hypothesis H_R_is_maximum:
∀ (A : duration),
is_in_search_space A →
∃ (F : duration),
A + F = blocking_bound + task_rbf (A + ε) + bound_on_total_hep_workload A (A + F) ∧
F ≤ R.
Hypothesis H_R_is_maximum:
∀ (A : duration),
is_in_search_space A →
∃ (F : duration),
A + F = blocking_bound + task_rbf (A + ε) + bound_on_total_hep_workload A (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 with floating nonpreemptive
regions.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
Theorem uniprocessor_response_time_bound_edf_with_floating_nonpreemptive_regions:
response_time_bounded_by tsk R.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2199)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
============================
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
Proof.
move: (H_valid_task_model_with_floating_nonpreemptive_regions) ⇒ [LIMJ JMLETM].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2211)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
============================
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
move: (LIMJ) ⇒ [BEG [END _]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2234)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).
(* ----------------------------------[ coqtop ]---------------------------------
19 focused subgoals
(shelved: 1) (ID 2249)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
consistent_arrival_times arr_seq
subgoal 2 (ID 2250) is:
arrival_sequence_uniq arr_seq
subgoal 3 (ID 2251) is:
jobs_come_from_arrival_sequence sched arr_seq
subgoal 4 (ID 2252) is:
jobs_must_arrive_to_execute sched
subgoal 5 (ID 2253) is:
completed_jobs_dont_execute sched
subgoal 6 (ID 2254) is:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
subgoal 7 (ID 2255) is:
sequential_tasks arr_seq sched
subgoal 8 (ID 2256) is:
work_conserving arr_seq sched
subgoal 9 (ID 2257) is:
respects_policy_at_preemption_point arr_seq sched
subgoal 10 (ID 2258) is:
all_jobs_from_taskset arr_seq ?ts0
subgoal 11 (ID 2259) is:
arrivals_have_valid_job_costs arr_seq
subgoal 12 (ID 2260) is:
valid_taskset_arrival_curve ?ts0 max_arrivals
subgoal 13 (ID 2261) is:
taskset_respects_max_arrivals arr_seq ?ts0
subgoal 14 (ID 2262) is:
tsk \in ?ts0
subgoal 15 (ID 2263) is:
valid_preemption_model arr_seq sched
subgoal 16 (ID 2264) is:
valid_task_run_to_completion_threshold arr_seq tsk
subgoal 17 (ID 2265) is:
0 < L
subgoal 18 (ID 2266) is:
L = total_request_bound_function ?ts0 L
subgoal 19 (ID 2267) is:
forall A : duration,
bounded_pi.is_in_search_space ?ts0 tsk L A ->
exists F : duration,
A + F =
bounded_nps.blocking_bound ?ts0 tsk +
(task_request_bound_function tsk (A + ε) -
(task_cost tsk - task_run_to_completion_threshold tsk)) +
\sum_(tsk_o <- ?ts0 | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R
----------------------------------------------------------------------------- *)
all: eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2267)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
forall A : duration,
bounded_pi.is_in_search_space ts tsk L A ->
exists F : duration,
A + F =
bounded_nps.blocking_bound ts tsk +
(task_request_bound_function tsk (A + ε) -
(task_cost tsk - task_run_to_completion_threshold tsk)) +
\sum_(tsk_o <- ts | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2267)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
forall A : duration,
bounded_pi.is_in_search_space ts tsk L A ->
exists F : duration,
A + F =
bounded_nps.blocking_bound ts tsk +
(task_request_bound_function tsk (A + ε) -
(task_cost tsk - task_run_to_completion_threshold tsk)) +
\sum_(tsk_o <- ts | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R
----------------------------------------------------------------------------- *)
rewrite subnn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2294)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
============================
forall A : duration,
bounded_pi.is_in_search_space ts tsk L A ->
exists F : duration,
A + F =
bounded_nps.blocking_bound ts tsk +
(task_request_bound_function tsk (A + ε) - 0) +
\sum_(tsk_o <- ts | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
F + 0 <= R
----------------------------------------------------------------------------- *)
intros A SP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2296)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
A : duration
SP : bounded_pi.is_in_search_space ts tsk L A
============================
exists F : duration,
A + F =
bounded_nps.blocking_bound ts tsk +
(task_request_bound_function tsk (A + ε) - 0) +
\sum_(tsk_o <- ts | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
F + 0 <= R
----------------------------------------------------------------------------- *)
apply H_R_is_maximum in SP.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2297)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
A : duration
SP : exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
============================
exists F : duration,
A + F =
bounded_nps.blocking_bound ts tsk +
(task_request_bound_function tsk (A + ε) - 0) +
\sum_(tsk_o <- ts | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
F + 0 <= R
----------------------------------------------------------------------------- *)
move: SP ⇒ [F [EQ LE]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2321)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
A, F : duration
EQ : A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F)
LE : F <= R
============================
exists F0 : duration,
A + F0 =
bounded_nps.blocking_bound ts tsk +
(task_request_bound_function tsk (A + ε) - 0) +
\sum_(tsk_o <- ts | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F0)) /\
F0 + 0 <= R
----------------------------------------------------------------------------- *)
∃ F.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2323)
Task : TaskType
H : TaskCost Task
H0 : TaskDeadline Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
H3 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq
H4 : JobPreemptionPoints Job
H5 : TaskMaxNonpreemptiveSegment Task
H_valid_task_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
ts : seq Task
H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
H6 : MaxArrivals Task
H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals
H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts
tsk : Task
H_tsk_in_ts : tsk \in ts
sched : schedule (processor_state Job)
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
H_schedule_with_limited_preemptions : schedule_respects_preemption_model
arr_seq sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_sequential_tasks : sequential_tasks arr_seq sched
H_work_conserving : work_conserving arr_seq sched
H_respects_policy : respects_policy_at_preemption_point arr_seq sched
rbf := task_request_bound_function : Task -> duration -> nat
task_rbf := rbf tsk : duration -> nat
total_rbf := total_request_bound_function ts : duration -> nat
bound_on_total_hep_workload := fun A Δ : nat =>
\sum_(tsk_o <- ts |
tsk_o != tsk)
rbf tsk_o
(minn
(A + ε + task_deadline tsk -
task_deadline tsk_o) Δ)
: nat -> nat -> nat
L : duration
H_L_positive : 0 < L
H_fixed_point : L = total_rbf L
is_in_search_space := bounded_pi.is_in_search_space ts tsk L
: duration -> bool
R : duration
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : duration,
A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F) /\
F <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
LIMJ : valid_limited_preemptions_job_model arr_seq
JMLETM : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
A, F : duration
EQ : A + F =
blocking_bound + task_rbf (A + ε) +
bound_on_total_hep_workload A (A + F)
LE : F <= R
============================
A + F =
bounded_nps.blocking_bound ts tsk +
(task_request_bound_function tsk (A + ε) - 0) +
\sum_(tsk_o <- ts | tsk_o != tsk)
task_request_bound_function tsk_o
(minn (A + ε + task_deadline tsk - task_deadline tsk_o) (A + F)) /\
F + 0 <= R
----------------------------------------------------------------------------- *)
by rewrite subn0 addn0; split.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.