Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.util.fixpoint.
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * 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]. *)SectionRTAforFullyPreemptiveFPModelwithArrivalCurves.(** We assume ideal uni-processor schedules. *)#[local] Existing Instanceideal.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 Instancefully_preemptive_job_model.#[local] Existing Instancefully_preemptive_task_model.#[local] Existing Instancefully_preemptive_rtc_threshold.(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)Variablearr_seq : arrival_sequence Job.HypothesisH_valid_arrival_sequence : valid_arrival_sequence arr_seq.(** Consider an arbitrary task set [ts], ... *)Variablets : list Task.(** ... assume that all jobs come from the task set, ... *)HypothesisH_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 . *)HypothesisH_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}.HypothesisH_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.HypothesisH_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.(** Let [tsk] be any task in [ts] that is to be analyzed. *)Variabletsk : Task.HypothesisH_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] Instancesequential_readiness : JobReady _ _ :=
sequential_ready_instance arr_seq.(** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)Variablesched : schedule (ideal.processor_state Job).HypothesisH_sched_valid : valid_schedule sched arr_seq.HypothesisH_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.(** Finally, we assume that the schedule is work-conserving ... *)HypothesisH_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}.HypothesisH_priority_is_reflexive : reflexive_priorities.HypothesisH_priority_is_transitive : transitive_priorities.HypothesisH_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. *)Variableh : nat.(** We let [L] denote the bound on the maximum busy-window length ... *)VariableL : duration.(** ... and assume that it has been found by means of a successful fixpoint search. *)HypothesisH_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. *)Letis_in_search_space := is_in_search_space tsk L.(** We let [R] denote [tsk]'s response-time bound ... *)VariableR : 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. *)LetrecurrenceAF := task_request_bound_function tsk (A + ε)
+ total_ohep_request_bound_function_FP ts tsk (A + F)
- A.HypothesisH_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. *)
forallA : duration,
bounded_pi.is_in_search_space tsk L A ->
existsF : duration,
task_request_bound_function tsk (A + ε) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\
F <= R
forallA : duration,
bounded_pi.is_in_search_space tsk L A ->
existsF : duration,
task_request_bound_function tsk (A + ε) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\
F <= R
forallA : duration,
bounded_pi.is_in_search_space tsk L A ->
existsF : duration,
task_request_bound_function tsk (A + ε) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
forallA : duration,
bounded_pi.is_in_search_space tsk L A ->
existsF : duration,
task_request_bound_function tsk (A + ε) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R
bounded_pi.is_in_search_space tsk L A ->
existsF : duration,
task_request_bound_function tsk (A + ε) +
total_ohep_request_bound_function_FP ts tsk (A + F) <=
A + F /\ F <= R