Library rt.restructuring.model.preemption.rtc_threshold.valid_rtct
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all nondecreasing.
From rt.restructuring.model Require Import job task.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model.preemption Require Import
valid_model job.parameters task.parameters.
Task's Run-to-Completion Threshold
Since a task model may not provide exact information about preemption point of a task, task's run-to-completion threshold cannot be defined in terms of preemption points of a task (unlike job's run-to-completion threshold). Therefore, we can assume the existence of a function that maps a task to its run-to-completion threshold. In this section we define the notion of a valid run-to-completion threshold of a task.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
In addition, we assume existence of a function
maping jobs to theirs preemption points ...
...and a function mapping tasks to theirs
run-to-completion threshold.
Consider any kind of processor state model, ...
... any job arrival sequence, ...
... and any given schedule.
A task's run-to-completion threshold should be at most the cost of the task.
Definition task_run_to_completion_threshold_le_task_cost tsk :=
task_run_to_completion_threshold tsk ≤ task_cost tsk.
task_run_to_completion_threshold tsk ≤ task_cost tsk.
We say that the run-to-completion threshold of a task tsk bounds
the job run-to-completionthreshold iff for any job j of task tsk
the job run-to-completion threshold is less than or equal to the
task run-to-completion threshold.
Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_run_to_completion_threshold j ≤ task_run_to_completion_threshold tsk.
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_run_to_completion_threshold j ≤ task_run_to_completion_threshold tsk.
We say that task_run_to_completion_threshold is a valid task
run-to-completion threshold for a task tsk iff
[task_run_to_completion_threshold tsk] is (1) no bigger than
tsk's cost, (2) for any job of task tsk
job_run_to_completion_threshold is bounded by
task_run_to_completion_threshold.