Library prosa.results.edf.rta.fully_nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.results.edf.rta.bounded_nps.
Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
RTA for Fully Non-Preemptive EDF
In this module we prove the RTA theorem for the fully non-preemptive 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 fully non-preemptive task model.
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.
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 non-preemptive uniprocessor schedule of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
... 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 nonpreemptive
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 also define a bound for the priority inversion caused by jobs with lower priority.
Let blocking_bound :=
\max_(tsk_o <- ts | (tsk_o != tsk) && (task_deadline tsk_o > task_deadline tsk))
(task_cost tsk_o - ε).
\max_(tsk_o <- ts | (tsk_o != tsk) && (task_deadline tsk_o > task_deadline tsk))
(task_cost tsk_o - ε).
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: nat.
Hypothesis H_R_is_maximum:
∀ A,
is_in_search_space A →
∃ F,
A + F = blocking_bound + (task_rbf (A + ε) - (task_cost tsk - ε))
+ bound_on_total_hep_workload A (A + F) ∧
F + (task_cost tsk - ε) ≤ R.
Hypothesis H_R_is_maximum:
∀ A,
is_in_search_space A →
∃ F,
A + F = blocking_bound + (task_rbf (A + ε) - (task_cost tsk - ε))
+ bound_on_total_hep_workload A (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.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
Theorem uniprocessor_response_time_bound_fully_nonpreemptive_edf:
response_time_bounded_by tsk R.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2198)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
============================
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
Proof.
case: (posnP (task_cost tsk)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2221)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
============================
response_time_bounded_by tsk R
subgoal 2 (ID 2222) is:
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2221)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
============================
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
intros j ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2226)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_response_time_bound sched j R
----------------------------------------------------------------------------- *)
have ZEROj: job_cost j = 0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2231)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_cost j = 0
subgoal 2 (ID 2233) is:
job_response_time_bound sched j R
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2231)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_cost j = 0
----------------------------------------------------------------------------- *)
move: (H_valid_job_cost j ARR) ⇒ NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2235)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
NEQ : valid_job_cost j
============================
job_cost j = 0
----------------------------------------------------------------------------- *)
rewrite /valid_job_cost TSK ZERO in NEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2300)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
NEQ : job_cost j <= 0
============================
job_cost j = 0
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite -leqn0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 2233)
subgoal 1 (ID 2233) is:
job_response_time_bound sched j R
subgoal 2 (ID 2222) is:
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2233)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
ZERO : task_cost tsk = 0
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
ZEROj : job_cost j = 0
============================
job_response_time_bound sched j R
----------------------------------------------------------------------------- *)
by rewrite /job_response_time_bound /completed_by ZEROj.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2222)
subgoal 1 (ID 2222) is:
response_time_bounded_by tsk R
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 2222)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
POS : 0 < task_cost tsk
============================
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 2389)
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
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
H4 : 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_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched
arr_seq
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
blocking_bound := \max_(tsk_o <- ts | (tsk_o != tsk) &&
(task_deadline tsk <
task_deadline tsk_o))
(task_cost tsk_o - ε) : 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 : nat
H_R_is_maximum : forall A : duration,
is_in_search_space A ->
exists F : nat,
A + F =
blocking_bound +
(task_rbf (A + ε) - (task_cost tsk - ε)) +
bound_on_total_hep_workload A (A + F) /\
F + (task_cost tsk - ε) <= R
response_time_bounded_by := task_response_time_bound arr_seq sched
: Task -> duration -> Prop
POS : 0 < task_cost tsk
============================
consistent_arrival_times arr_seq
subgoal 2 (ID 2390) is:
arrival_sequence_uniq arr_seq
subgoal 3 (ID 2391) is:
jobs_come_from_arrival_sequence sched arr_seq
subgoal 4 (ID 2392) is:
jobs_must_arrive_to_execute sched
subgoal 5 (ID 2393) is:
completed_jobs_dont_execute sched
subgoal 6 (ID 2394) is:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
subgoal 7 (ID 2395) is:
sequential_tasks arr_seq sched
subgoal 8 (ID 2396) is:
work_conserving arr_seq sched
subgoal 9 (ID 2397) is:
respects_policy_at_preemption_point arr_seq sched
subgoal 10 (ID 2398) is:
all_jobs_from_taskset arr_seq ?ts0
subgoal 11 (ID 2399) is:
arrivals_have_valid_job_costs arr_seq
subgoal 12 (ID 2400) is:
valid_taskset_arrival_curve ?ts0 max_arrivals
subgoal 13 (ID 2401) is:
taskset_respects_max_arrivals arr_seq ?ts0
subgoal 14 (ID 2402) is:
tsk \in ?ts0
subgoal 15 (ID 2403) is:
valid_preemption_model arr_seq sched
subgoal 16 (ID 2404) is:
valid_task_run_to_completion_threshold arr_seq tsk
subgoal 17 (ID 2405) is:
0 < L
subgoal 18 (ID 2406) is:
L = total_request_bound_function ?ts0 L
subgoal 19 (ID 2407) 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 ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.