Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.util.fixpoint.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ]
Require Export prosa.results.fixed_priority.rta.fully_preemptive.Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** * RTA for Fully Preemptive FP Scheduling with Computed Fixpoints *)
(** This module refines the general response-time bound for fully preemptive
fixed-priority scheduling in
[prosa.results.fixed_priority.rta.fully_preemptive]. Whereas the general
result assumes that all fixpoints are given, i.e., that they have been found
_somehow_ without imposing any assumptions on how they have been found, here
we _compute_ all relevant fixpoints using the procedures provided in
[prosa.util.fixpoint]. *)
(** ** Problem Setup and Analysis Context *)
(** To begin, we must set up the context as in
[prosa.results.fixed_priority.rta.fully_preemptive]. *)
Section RTAforFullyPreemptiveFPModelwithArrivalCurves .
(** We assume ideal uni-processor schedules. *)
#[local] Existing Instance ideal .processor_state.
(** Consider any type of tasks characterized by WCETs ... *)
Context {Task : TaskType} `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks, where each job is
characterized by an arrival time and an execution cost. *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobCost Job}.
(** We assume that jobs and tasks are fully preemptive. *)
#[local] Existing Instance fully_preemptive_job_model .
#[local] Existing Instance fully_preemptive_task_model .
#[local] Existing Instance fully_preemptive_rtc_threshold .
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence 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 : all_jobs_from_taskset arr_seq ts.
(** ... and that the cost of a job does not exceed the task's WCET . *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** 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 for [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.
(** Let [tsk] be any task in [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Recall that we assume sequential readiness, i.e., jobs of the same task
are executed in order of their arrival. *)
#[local] Instance sequential_readiness : JobReady _ _ :=
sequential_ready_instance arr_seq.
(** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
(** Finally, we assume that the schedule is work-conserving ... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... and that it respects a reflexive and transitive fixed-priority
scheduling policy [FP]. *)
Context {FP : FP_policy Task}.
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
Hypothesis H_priority_is_transitive : transitive_task_priorities FP.
Hypothesis H_respects_policy :
respects_FP_policy_at_preemption_point arr_seq sched FP.
(** ** Computation of the Fixpoints *)
(** In the following, we introduce the bound on the maximum busy-window length
[L] and the response-time bound [R] and assume that they have been are
calculated using the tools provided by [util.fixpoint]. *)
(** Let [h] denote the horizon for the fixpoint search, i.e., an upper bound
on the maximum relevant fixpoint. Practically speaking, this is the
threshold at which the fixpoint search is aborted and ends in failure.
Since we assume in the following that the fixpoint search terminated
successfully, it implies that [h] was chosen to be "sufficiently large";
it may hence be safely ignored in the following. *)
Variable h : nat.
(** We let [L] denote the bound on the maximum busy-window length ... *)
Variable L : duration.
(** ... and assume that it has been found by means of a successful fixpoint
search. *)
Hypothesis H_L_is_fixpoint :
Some L = find_fixpoint (total_hep_request_bound_function_FP ts tsk) h.
(** Recall the notion of the search space of the RTA for fixed-priority
scheduling. *)
Let is_in_search_space := is_in_search_space tsk L.
(** We let [R] denote [tsk]'s response-time bound ... *)
Variable R : duration.
(** ... and assume that it has been found by means of finding the maximum
among the fixpoints for each element in the search space with regard
to the following [recurrence] function. *)
Let recurrence A F := task_request_bound_function tsk (A + ε)
+ total_ohep_request_bound_function_FP ts tsk (A + F)
- A.
Hypothesis H_R_is_max_fixpoint :
Some R = find_max_fixpoint L is_in_search_space recurrence h.
(** ** Correctness of the Response-Time Bound *)
(** Using the lemmas from [util.fixpoints], we can show that all preconditions
of the general fully preemptive fixed-priority RTA theorem are met. *)
Theorem uniprocessor_response_time_bound_fully_preemptive_fp :
task_response_time_bound arr_seq sched tsk R.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h
task_response_time_bound arr_seq sched tsk R
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h
task_response_time_bound arr_seq sched tsk R
(* First, eliminate the trivial case of no higher- or equal-priority
interference. *)
case : (leqP (total_hep_request_bound_function_FP ts tsk ε) 0 );
first by rewrite leqn0 => /eqP ZERO; apply : pathological_total_hep_rbf_any_bound.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h
0 < total_hep_request_bound_function_FP ts tsk 1 ->
task_response_time_bound arr_seq sched tsk R
move => GT0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
task_response_time_bound arr_seq sched tsk R
(* Second, apply the general result. *)
eapply uniprocessor_response_time_bound_fully_preemptive_fp
with (L := L) (ts := ts) => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
0 < L
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
0 < L
apply : ffp_finds_positive_fixpoint; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
monotone leq
(total_hep_request_bound_function_FP ts tsk)
exact : total_hep_rbf_monotone. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
L = total_hep_request_bound_function_FP ts tsk L
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
L = total_hep_request_bound_function_FP ts tsk L
by apply : ffp_finds_fixpoint; eauto . } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
forall A : duration,
bounded_pi.is_in_search_space tsk L A ->
exists F : duration,
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1
forall A : duration,
bounded_pi.is_in_search_space tsk L A ->
exists F : duration,
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
move => A.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1 A : duration
bounded_pi.is_in_search_space tsk L A ->
exists F : duration,
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
rewrite /bounded_pi.is_in_search_space => /andP[LT IN_SP].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1 A : duration LT : A < L IN_SP : task_request_bound_function tsk A
!= task_request_bound_function tsk (A + 1 )
exists F : duration,
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
have IN_SP' : (A < L) && is_in_search_space A
by repeat (apply /andP; split ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1 A : duration LT : A < L IN_SP : task_request_bound_function tsk A
!= task_request_bound_function tsk (A + 1 ) IN_SP' : (A < L) && is_in_search_space A
exists F : duration,
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
move : (fmf_is_maximum _ _ H_R_is_max_fixpoint IN_SP') => [F FIX BOUND].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1 A : duration LT : A < L IN_SP : task_request_bound_function tsk A
!= task_request_bound_function tsk (A + 1 ) IN_SP' : (A < L) && is_in_search_space A F : nat FIX : Some F = find_fixpoint (recurrence A) h BOUND : F <= R
exists F : duration,
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
exists F ; split => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1 A : duration LT : A < L IN_SP : task_request_bound_function tsk A
!= task_request_bound_function tsk (A + 1 ) IN_SP' : (A < L) && is_in_search_space A F : nat FIX : Some F = find_fixpoint (recurrence A) h BOUND : F <= R
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F
have : F = recurrence A F
by apply : ffp_finds_fixpoint; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
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 H3 : 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 (ideal.processor_state Job) H_sched_valid : valid_schedule sched arr_seq H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_work_conserving : work_conserving arr_seq sched FP : FP_policy Task H_priority_is_reflexive : reflexive_task_priorities FP H_priority_is_transitive : transitive_task_priorities
FP H_respects_policy : respects_FP_policy_at_preemption_point
arr_seq sched FP h : nat L : duration H_L_is_fixpoint : Some L =
find_fixpoint
(total_hep_request_bound_function_FP
ts tsk) h is_in_search_space := bounded_pi.is_in_search_space tsk
L : nat -> bool R : duration recurrence := fun A F : nat =>
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts
tsk (A + F) - A: nat -> nat -> nat H_R_is_max_fixpoint : Some R =
find_max_fixpoint L
is_in_search_space recurrence
h GT0 : 0 < total_hep_request_bound_function_FP ts tsk 1 A : duration LT : A < L IN_SP : task_request_bound_function tsk A
!= task_request_bound_function tsk (A + 1 ) IN_SP' : (A < L) && is_in_search_space A F : nat FIX : Some F = find_fixpoint (recurrence A) h BOUND : F <= R
F = recurrence A F ->
task_request_bound_function tsk (A + 1 ) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F
by rewrite /recurrence; lia . }
Qed .
End RTAforFullyPreemptiveFPModelwithArrivalCurves .