Library prosa.analysis.facts.model.rbf
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.request_bound_function.
Facts about Request Bound Functions (RBFs)
RBF is a Bound on Workload
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.
... any schedule corresponding to this arrival sequence, ...
Context {PState : Type} `{ProcessorState Job PState}.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
... and an FP policy that indicates a higher-or-equal priority relation.
Further, consider a task set ts...
Assume that the job costs are no larger than the task costs ...
... and that all jobs come from the task set.
Let max_arrivals be any arrival bound for task-set ts.
Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
Next, recall the notions of total workload of jobs...
... and the workload of jobs of the same task as job j.
Finally, let us define some local names for clarity.
Let task_rbf := task_request_bound_function tsk.
Let total_rbf := total_request_bound_function ts.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
Let total_rbf := total_request_bound_function ts.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
In this section, we prove that the workload of all jobs is
no larger than the request bound function.
First, we show that workload of task tsk is bounded by the number of
arrivals of the task times the cost of the task.
Lemma task_workload_le_num_of_arrivals_times_cost:
task_workload t (t + Δ)
≤ task_cost tsk × number_of_task_arrivals arr_seq tsk t (t + Δ).
task_workload t (t + Δ)
≤ task_cost tsk × number_of_task_arrivals arr_seq tsk t (t + Δ).
As a corollary, we prove that workload of task is no larger the than
task request bound function.
Next, we prove that total workload of tasks is no larger than the total
request bound function.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
We say that two jobs j1 and j2 are in relation
other_higher_eq_priority, iff j1 has higher or equal priority than j2 and
is produced by a different task.
Recall the notion of workload of higher or equal priority jobs...
Let total_hep_workload t1 t2 :=
workload_of_jobs (fun j_other ⇒ jlfp_higher_eq_priority j_other j)
(arrivals_between arr_seq t1 t2).
workload_of_jobs (fun j_other ⇒ jlfp_higher_eq_priority j_other j)
(arrivals_between arr_seq t1 t2).
... and workload of other higher or equal priority jobs.
Let total_ohep_workload t1 t2 :=
workload_of_jobs (fun j_other ⇒ other_higher_eq_priority j_other j)
(arrivals_between arr_seq t1 t2).
workload_of_jobs (fun j_other ⇒ other_higher_eq_priority j_other j)
(arrivals_between arr_seq t1 t2).
We prove that total workload of other tasks with higher-or-equal
priority is no larger than the total request bound function.
Next, we prove that total workload of all tasks with higher-or-equal
priority is no larger than the total request bound function.
Lemma total_workload_le_total_hep_rbf:
total_hep_workload t (t + Δ) ≤ total_hep_rbf Δ.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
total_hep_workload t (t + Δ) ≤ total_hep_rbf Δ.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent:
consistent_arrival_times arr_seq.
Hypothesis H_arrival_times_are_consistent:
consistent_arrival_times arr_seq.
Let tsk be any task.
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 Δ = 0.
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
Let's define some local names for clarity.
We prove that task_rbf is monotone.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Assume that tsk has a positive cost.
Next, we prove that cost of tsk is less than or equal to the
total_request_bound_function.
Lemma task_cost_le_sum_rbf :
∀ t,
t > 0 →
task_cost tsk ≤ total_request_bound_function ts t.
End RequestBoundFunctions.
∀ t,
t > 0 →
task_cost tsk ≤ total_request_bound_function ts t.
End RequestBoundFunctions.