Library rt.analysis.uni.arrival_curves.workload_bound
Require Import rt.util.all.
Require Import rt.model.arrival.basic.job
rt.model.arrival.basic.task_arrival
rt.model.priority.
Require Import rt.model.schedule.uni.service
rt.model.schedule.uni.workload
rt.model.schedule.uni.schedule.
Require Import rt.model.arrival.curves.bounds.
Module MaxArrivalsWorkloadBound.
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service.
Section Lemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
(* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
(* Next, consider any uniprocessor schedule of this arrival sequence. *)
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
(* Consider an FP policy that indicates a higher-or-equal priority relation. *)
Variable higher_eq_priority: FP_policy Task.
Let jlfp_higher_eq_priority := FP_to_JLFP job_task higher_eq_priority.
(* For simplicity, let's define some local names. *)
Let arrivals_between := jobs_arrived_between arr_seq.
(* We define the notion of request bound function. *)
Section RequestBoundFunction.
(* Let max_arrivals denote any function that takes a task and an interval length
and returns the associated number of job arrivals of the task. *)
Variable max_arrivals: Task → time → nat.
(* In this section, we define a bound for the workload of a single task
under uniprocessor FP scheduling. *)
Section SingleTask.
(* Consider any task tsk that is to be scheduled in an interval of length delta. *)
Variable tsk: Task.
Variable delta: time.
(* We define the following workload bound for the task. *)
Definition task_request_bound_function := task_cost tsk × max_arrivals tsk delta.
End SingleTask.
(* In this section, we define a bound for the workload of multiple tasks. *)
Section AllTasks.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be any task in task set. *)
Variable tsk: Task.
(* Let delta be the length of the interval of interest. *)
Variable delta: time.
(* Recall the definition of higher-or-equal-priority task and
the per-task workload bound for FP scheduling. *)
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
(* Using the sum of individual workload bounds, we define the following bound
for the total workload of tasks in any interval of length delta. *)
Definition total_request_bound_function :=
\sum_(tsk <- ts) task_request_bound_function tsk delta.
(* Similarly, we define the following bound for the total workload of tasks of
higher-or-equal priority (with respect to tsk) in any interval of length delta. *)
Definition total_hep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_hep_task tsk_other)
task_request_bound_function tsk_other delta.
(* We also define bound for the total workload of higher-or-equal priority
tasks other than tsk in any interval of length delta. *)
Definition total_ohep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_other_hep_task tsk_other)
task_request_bound_function tsk_other delta.
End AllTasks.
End RequestBoundFunction.
(* In this section we prove some lemmas about request bound functions. *)
Section ProofWorkloadBound.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
(* Assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost_le_task_cost task_cost job_cost job_task j.
(* Next, we assume that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* Let max_arrivals be any arrival bound for taskset ts. *)
Variable max_arrivals: Task → time → nat.
Hypothesis H_is_arrival_bound:
is_arrival_bound_for_taskset job_task arr_seq max_arrivals ts.
(* Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function max_arrivals tsk.
Let total_rbf := total_request_bound_function max_arrivals ts.
Let total_hep_rbf := total_hep_request_bound_function_FP max_arrivals ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP max_arrivals ts tsk.
(* Next, we consider any job j of tsk. *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
(* We define whether two jobs j1 and j2 are from the same task. *)
Let same_task j1 j2 := job_task j1 == job_task j2.
(* Next, 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. *)
Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
(* Next, we recall the notions of total workload of jobs... *)
Let total_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2) (fun j ⇒ true).
(* ...notions of workload of higher or equal priority jobs... *)
Let total_hep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ jlfp_higher_eq_priority j_other j).
(* ... workload of other higher or equal priority jobs... *)
Let total_ohep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ other_higher_eq_priority j_other j).
(* ... and the workload of jobs of the same task as job j. *)
Let task_workload (t1: time) (t2: time) :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ same_task j_other j).
(* In this section we prove that the workload of any jobs is
no larger than the request bound function. *)
Section WorkloadIsBoundedByRBF.
(* Consider any time t and any interval of length delta. *)
Variable t: time.
Variable delta: time.
(* First, we prove that workload of task is no larger
than task request bound function. *)
Lemma task_workload_le_task_rbf:
task_workload t (t + delta) ≤ task_rbf delta.
(* Next, we prove that total workload of tasks is no larger
than total request bound function. *)
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) ≤ total_ohep_rbf delta.
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) ≤ total_hep_rbf delta.
Lemma total_workload_le_total_rbf'':
total_workload t (t + delta) ≤ total_rbf delta.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
End Lemmas.
End MaxArrivalsWorkloadBound.
Require Import rt.model.arrival.basic.job
rt.model.arrival.basic.task_arrival
rt.model.priority.
Require Import rt.model.schedule.uni.service
rt.model.schedule.uni.workload
rt.model.schedule.uni.schedule.
Require Import rt.model.arrival.curves.bounds.
Module MaxArrivalsWorkloadBound.
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service.
Section Lemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
(* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
(* Next, consider any uniprocessor schedule of this arrival sequence. *)
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
(* Consider an FP policy that indicates a higher-or-equal priority relation. *)
Variable higher_eq_priority: FP_policy Task.
Let jlfp_higher_eq_priority := FP_to_JLFP job_task higher_eq_priority.
(* For simplicity, let's define some local names. *)
Let arrivals_between := jobs_arrived_between arr_seq.
(* We define the notion of request bound function. *)
Section RequestBoundFunction.
(* Let max_arrivals denote any function that takes a task and an interval length
and returns the associated number of job arrivals of the task. *)
Variable max_arrivals: Task → time → nat.
(* In this section, we define a bound for the workload of a single task
under uniprocessor FP scheduling. *)
Section SingleTask.
(* Consider any task tsk that is to be scheduled in an interval of length delta. *)
Variable tsk: Task.
Variable delta: time.
(* We define the following workload bound for the task. *)
Definition task_request_bound_function := task_cost tsk × max_arrivals tsk delta.
End SingleTask.
(* In this section, we define a bound for the workload of multiple tasks. *)
Section AllTasks.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be any task in task set. *)
Variable tsk: Task.
(* Let delta be the length of the interval of interest. *)
Variable delta: time.
(* Recall the definition of higher-or-equal-priority task and
the per-task workload bound for FP scheduling. *)
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
(* Using the sum of individual workload bounds, we define the following bound
for the total workload of tasks in any interval of length delta. *)
Definition total_request_bound_function :=
\sum_(tsk <- ts) task_request_bound_function tsk delta.
(* Similarly, we define the following bound for the total workload of tasks of
higher-or-equal priority (with respect to tsk) in any interval of length delta. *)
Definition total_hep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_hep_task tsk_other)
task_request_bound_function tsk_other delta.
(* We also define bound for the total workload of higher-or-equal priority
tasks other than tsk in any interval of length delta. *)
Definition total_ohep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_other_hep_task tsk_other)
task_request_bound_function tsk_other delta.
End AllTasks.
End RequestBoundFunction.
(* In this section we prove some lemmas about request bound functions. *)
Section ProofWorkloadBound.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
(* Assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost_le_task_cost task_cost job_cost job_task j.
(* Next, we assume that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* Let max_arrivals be any arrival bound for taskset ts. *)
Variable max_arrivals: Task → time → nat.
Hypothesis H_is_arrival_bound:
is_arrival_bound_for_taskset job_task arr_seq max_arrivals ts.
(* Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function max_arrivals tsk.
Let total_rbf := total_request_bound_function max_arrivals ts.
Let total_hep_rbf := total_hep_request_bound_function_FP max_arrivals ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP max_arrivals ts tsk.
(* Next, we consider any job j of tsk. *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
(* We define whether two jobs j1 and j2 are from the same task. *)
Let same_task j1 j2 := job_task j1 == job_task j2.
(* Next, 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. *)
Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
(* Next, we recall the notions of total workload of jobs... *)
Let total_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2) (fun j ⇒ true).
(* ...notions of workload of higher or equal priority jobs... *)
Let total_hep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ jlfp_higher_eq_priority j_other j).
(* ... workload of other higher or equal priority jobs... *)
Let total_ohep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ other_higher_eq_priority j_other j).
(* ... and the workload of jobs of the same task as job j. *)
Let task_workload (t1: time) (t2: time) :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ same_task j_other j).
(* In this section we prove that the workload of any jobs is
no larger than the request bound function. *)
Section WorkloadIsBoundedByRBF.
(* Consider any time t and any interval of length delta. *)
Variable t: time.
Variable delta: time.
(* First, we prove that workload of task is no larger
than task request bound function. *)
Lemma task_workload_le_task_rbf:
task_workload t (t + delta) ≤ task_rbf delta.
(* Next, we prove that total workload of tasks is no larger
than total request bound function. *)
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) ≤ total_ohep_rbf delta.
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) ≤ total_hep_rbf delta.
Lemma total_workload_le_total_rbf'':
total_workload t (t + delta) ≤ total_rbf delta.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
End Lemmas.
End MaxArrivalsWorkloadBound.