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.
[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]
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]
Require Export prosa.analysis.facts.model.restricted_supply.schedule.Require Export prosa.analysis.facts.preemption.task.nonpreemptive.Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.edf.Require Export prosa.analysis.abstract.restricted_supply.search_space.edf.Require Export prosa.analysis.facts.model.task_cost.Require Export prosa.analysis.facts.priority.edf.Require Export prosa.analysis.facts.blocking_bound.edf.Require Export prosa.analysis.facts.workload.edf_athep_bound.Require Export prosa.analysis.definitions.sbf.busy.(** * RTA for Fully Non-Preemptive EDF Scheduling on Restricted-Supply Uniprocessors *)(** In the following, we derive a response-time analysis for EDF schedulers, assuming a workload of sporadic real-time tasks characterized by arbitrary arrival curves executing upon a uniprocessor with arbitrary supply restrictions. To this end, we instantiate the _abstract Sequential Restricted-Supply Response-Time Analysis_ (aRSA) as provided in the [prosa.analysis.abstract.restricted_supply] module. *)SectionRTAforFullyNonPreemptiveEDFModelwithArrivalCurves.(** ** Defining the System Model *)(** Before any formal claims can be stated, an initial setup is needed to define the system model under consideration. To this end, we next introduce and define the following notions using Prosa's standard definitions and behavioral semantics: - processor model, - tasks, jobs, and their parameters, - the sequence of job arrivals, - worst-case execution time (WCET) and the absence of self-suspensions, - the set of tasks under analysis, - the task under analysis, and, finally, - an arbitrary schedule of the task set. *)(** *** Processor Model *)(** Consider a restricted-supply uniprocessor model, ... *)#[local] Existing Instancers_processor_state.(** ... where the minimum amount of supply is lower-bounded via a monotone unit-supply-bound function [SBF]. *)Context {SBF : SupplyBoundFunction}.HypothesisH_SBF_monotone : sbf_is_monotone SBF.HypothesisH_unit_SBF : unit_supply_bound_function SBF.(** *** Tasks and Jobs *)(** Consider any type of tasks, each characterized by a WCET [task_cost], relative deadline [task_deadline], and an arrival curve [max_arrivals], ... *)Context {Task : TaskType}.Context `{TaskCost Task}.Context `{TaskDeadline Task}.Context `{MaxArrivals Task}.(** ... and any type of jobs associated with these tasks, where each job has a task [job_task], a cost [job_cost], and an arrival time [job_arrival]. *)Context {Job : JobType}.Context `{JobTask Job Task}.Context `{JobCost Job}.Context `{JobArrival Job}.(** Furthermore, assume that jobs and tasks are fully non-preemptive. *)#[local] Existing Instancefully_nonpreemptive_job_model.#[local] Existing Instancefully_nonpreemptive_task_model.#[local] Existing Instancefully_nonpreemptive_rtc_threshold.(** *** The Job Arrival Sequence *)(** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)Variablearr_seq : arrival_sequence Job.HypothesisH_valid_arrival_sequence : valid_arrival_sequence arr_seq.(** *** Absence of Self-Suspensions and WCET Compliance *)(** We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready. *)#[local] Existing Instancebasic_ready_instance.(** We further require that a job's cost cannot exceed its task's stated WCET. *)HypothesisH_valid_job_cost : arrivals_have_valid_job_costs arr_seq.(** *** The Task Set *)(** We consider an arbitrary task set [ts] ... *)Variablets : seq Task.(** ... and assume that all jobs stem from tasks in this task set. *)HypothesisH_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.(** We assume that [max_arrivals] is a family of valid arrival curves that constrains the arrival sequence [arr_seq], i.e., for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival bound of [tsk], and ... *)HypothesisH_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.(** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)HypothesisH_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.(** *** The Task Under Analysis *)(** Let [tsk] be any task in [ts] that is to be analyzed. *)Variabletsk : Task.HypothesisH_tsk_in_ts : tsk \in ts.(** *** The Schedule *)(** Finally, consider any non-preemptive, work-conserving, valid restricted-supply uni-processor schedule of the given arrival sequence [arr_seq] (and hence the given task set [ts]) ... *)Variablesched : schedule (rs_processor_state Job).HypothesisH_valid_schedule : valid_schedule sched arr_seq.HypothesisH_work_conserving : work_conserving arr_seq sched.HypothesisH_nonpreemptive_sched : nonpreemptive_schedule sched.(** ... and assume that the schedule respects the EDF policy. *)HypothesisH_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).(** Last but not least, we assume that [SBF] properly characterizes all busy intervals (w.r.t. task [tsk]) in [sched]. That is, (1) [SBF 0 = 0] and (2) for any duration [Δ], at least [SBF Δ] supply is available in any busy-interval prefix of length [Δ]. *)HypothesisH_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.(** ** Workload Abbreviation *)(** For brevity, let's denote the relative deadline of a task as [D]. *)LetDtsk := task_deadline tsk.(** We introduce [task_rbf] as an abbreviation for the task request bound function of task [tsk]. *)Lettask_rbf := task_request_bound_function tsk.(** ** Length of Busy Interval *)(** The next step is to establish a bound on the maximum busy-window length, which aRTA requires to be given. *)(** To this end, let [L] be any positive constant such that ... *)VariableL : duration.HypothesisH_L_positive : 0 < L.(** ... [L] satisfies a fixed-point recurrence for the busy-interval-length bound (i.e., [total_RBF ts L <= SBF L] ... *)HypothesisH_fixed_point : total_request_bound_function ts L <= SBF L.(** ... and [SBF L] bounds [longest_busy_interval_with_pi ts tsk]. *)HypothesisH_L_bounds_bi_with_pi :
longest_busy_interval_with_pi ts tsk <= SBF L.(** ** Response-Time Bound *)(** Having established all necessary preliminaries, it is finally time to state the claimed response-time bound [R]. A value [R] is a response-time bound if, for any given offset [A] in the search space, the response-time bound recurrence has a solution [F] not exceeding [R]. *)VariableR : duration.HypothesisH_R_is_maximum :
forall (A : duration),
is_in_search_space ts tsk L A ->
exists (F : duration),
A <= F <= A + R
/\ blocking_bound ts tsk A
+ (task_rbf (A + ε) - (task_cost tsk - ε))
+ bound_on_athep_workload ts tsk A F
<= SBF F
/\ SBF F + (task_cost tsk - ε) <= SBF (A + R).(** Finally, using the sequential variant of abstract restricted-supply analysis, we establish that any such [R] is a sound response-time bound for the concrete model of fully-nonpreemptive EDF scheduling with arbitrary supply restrictions. *)
forallx : duration,
A <= x <= A + R /\
blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A x <=
SBF x /\ SBF x + (task_cost tsk - 1) <= SBF (A + R) ->
existsF : duration,
F <= A + R /\
task_request_bound_function tsk (A + 1) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (blocking_bound ts tsk)
(bound_on_athep_workload ts tsk) A F <=
SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
forallx : duration,
A <= x <= A + R /\
blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A x <= SBF x /\
SBF x + (task_cost tsk - 1) <= SBF (A + R) ->
existsF : duration,
F <= A + R /\
task_request_bound_function tsk (A + 1) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (blocking_bound ts tsk)
(bound_on_athep_workload ts tsk) A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <=
SBF (A + R)
SBF: SupplyBoundFunction H_SBF_monotone: sbf_is_monotone SBF H_unit_SBF: unit_supply_bound_function SBF Task: TaskType H: TaskCost Task H0: TaskDeadline Task H1: MaxArrivals Task Job: JobType H2: JobTask Job Task H3: JobCost Job H4: JobArrival Job arr_seq: arrival_sequence Job H_valid_arrival_sequence: valid_arrival_sequence
arr_seq H_valid_job_cost: arrivals_have_valid_job_costs
arr_seq ts: seq Task H_all_jobs_from_taskset: all_jobs_from_taskset
arr_seq ts H_is_arrival_curve: taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve: valid_taskset_arrival_curve ts
max_arrivals tsk: Task H_tsk_in_ts: tsk \in ts sched: schedule (rs_processor_state Job) H_valid_schedule: valid_schedule sched arr_seq H_work_conserving: work_conserving arr_seq sched H_nonpreemptive_sched: nonpreemptive_schedule sched H_respects_policy: respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF D:= [eta task_deadline]: Task -> duration task_rbf:= task_request_bound_function tsk: duration -> nat L: duration H_L_positive: 0 < L H_fixed_point: total_request_bound_function ts L <=
SBF L H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
ts tsk <= SBF L R: duration H_R_is_maximum: forallA : duration,
is_in_search_space ts tsk L A ->
existsF : duration,
A <= F <= A + R /\
blocking_bound ts tsk A +
(task_rbf (A + 1) -
(task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A F <=
SBF F /\
SBF F + (task_cost tsk - 1) <=
SBF (A + R) js: Job ARRs: arrives_in arr_seq js TSKs: job_of_task tsk js POS: 0 < job_cost js READ: work_bearing_readiness arr_seq sched VPR: valid_preemption_model arr_seq sched A: duration SP: search_space.is_in_search_space L
(funAΔ : duration =>
task_request_bound_function tsk (A + 1) -
task_cost tsk +
task_intra_IBF (blocking_bound ts tsk)
(bound_on_athep_workload ts tsk) A Δ) A F: duration LE: F <= A + R FIX1: blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A F <=
SBF F FIX2: SBF F + (task_cost tsk - 1) <= SBF (A + R)
task_request_bound_function tsk (A + 1) -
(task_cost tsk - task_rtct tsk) +
task_intra_IBF (blocking_bound ts tsk)
(bound_on_athep_workload ts tsk) A F <= SBF F /\
SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R)
SBF: SupplyBoundFunction H_SBF_monotone: sbf_is_monotone SBF H_unit_SBF: unit_supply_bound_function SBF Task: TaskType H: TaskCost Task H0: TaskDeadline Task H1: MaxArrivals Task Job: JobType H2: JobTask Job Task H3: JobCost Job H4: JobArrival Job arr_seq: arrival_sequence Job H_valid_arrival_sequence: valid_arrival_sequence
arr_seq H_valid_job_cost: arrivals_have_valid_job_costs
arr_seq ts: seq Task H_all_jobs_from_taskset: all_jobs_from_taskset
arr_seq ts H_is_arrival_curve: taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve: valid_taskset_arrival_curve ts
max_arrivals tsk: Task H_tsk_in_ts: tsk \in ts sched: schedule (rs_processor_state Job) H_valid_schedule: valid_schedule sched arr_seq H_work_conserving: work_conserving arr_seq sched H_nonpreemptive_sched: nonpreemptive_schedule sched H_respects_policy: respects_JLFP_policy_at_preemption_point
arr_seq sched (EDF Job) H_valid_SBF: valid_busy_sbf arr_seq sched tsk SBF D:= [eta task_deadline]: Task -> duration task_rbf:= task_request_bound_function tsk: duration -> nat L: duration H_L_positive: 0 < L H_fixed_point: total_request_bound_function ts L <=
SBF L H_L_bounds_bi_with_pi: longest_busy_interval_with_pi
ts tsk <= SBF L R: duration H_R_is_maximum: forallA : duration,
is_in_search_space ts tsk L A ->
existsF : duration,
A <= F <= A + R /\
blocking_bound ts tsk A +
(task_rbf (A + 1) -
(task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A F <=
SBF F /\
SBF F + (task_cost tsk - 1) <=
SBF (A + R) js: Job ARRs: arrives_in arr_seq js TSKs: job_of_task tsk js POS: 0 < job_cost js READ: work_bearing_readiness arr_seq sched VPR: valid_preemption_model arr_seq sched A: duration SP: search_space.is_in_search_space L
(funAΔ : duration =>
task_request_bound_function tsk (A + 1) -
task_cost tsk +
task_intra_IBF (blocking_bound ts tsk)
(bound_on_athep_workload ts tsk) A Δ) A F: duration LE: F <= A + R FIX1: blocking_bound ts tsk A +
(task_rbf (A + 1) - (task_cost tsk - 1)) +
bound_on_athep_workload ts tsk A F <=
SBF F FIX2: SBF F + (task_cost tsk - 1) <= SBF (A + R)
task_request_bound_function tsk (A + 1) -
(task_cost tsk - 1) +
(blocking_bound ts tsk A +
bound_on_athep_workload ts tsk A F) <= SBF F /\
SBF F + (task_cost tsk - 1) <= SBF (A + R)