Library rt.restructuring.model.task.preemption.limited_preemptive
Require Export rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.preemption.limited_preemptive.
Platform for Models with Limited Preemptions
In this section, we introduce a set of requirements for function task_preemption_points, so it is coherent with limited preemptions model.
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 `{JobPreemptionPoints Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptionPoints Job}.
Consider any arrival sequence.
Consider an arbitrary task set ts.
Next, we describe structural properties that a sequence of
preemption points of task should satisfy.
(1) We require the sequence of preemption points to contain the beginning...
Definition task_beginning_of_execution_in_preemption_points :=
∀ tsk, tsk \in ts → first0 (task_preemption_points tsk) = 0.
∀ tsk, tsk \in ts → first0 (task_preemption_points tsk) = 0.
... and (2) the end of execution for any job j.
Definition task_end_of_execution_in_preemption_points :=
∀ tsk, tsk \in ts → last0 (task_preemption_points tsk) = task_cost tsk.
∀ tsk, tsk \in ts → last0 (task_preemption_points tsk) = task_cost tsk.
(3) We require the sequence of preemption points
to be a nondecreasing sequence.
Definition task_preemption_points_is_nondecreasing_sequence :=
∀ tsk, tsk \in ts → nondecreasing_sequence (task_preemption_points tsk).
∀ tsk, tsk \in ts → nondecreasing_sequence (task_preemption_points tsk).
(4) Next, we require the number of nonpreemptive segments of a job to be
equal to the number of nonpreemptive segments of its task. Note that
some of nonpreemptive segments of a job can have zero length, nonetheless
the number of segments should match.
Definition job_consists_of_the_same_number_of_segments_as_task :=
∀ j,
arrives_in arr_seq j →
size (job_preemption_points j) = size (task_preemption_points (job_task j)).
∀ j,
arrives_in arr_seq j →
size (job_preemption_points j) = size (task_preemption_points (job_task j)).
(5) We require lengths of nonpreemptive segments of a job to be bounded
by lenghts of the corresponding segments of its task.
Definition lengths_of_task_segments_bound_length_of_job_segments :=
∀ j n,
arrives_in arr_seq j →
nth 0 (distances (job_preemption_points j)) n
≤ nth 0 (distances (task_preemption_points (job_task j))) n.
∀ j n,
arrives_in arr_seq j →
nth 0 (distances (job_preemption_points j)) n
≤ nth 0 (distances (task_preemption_points (job_task j))) n.
(6) Lastly, we ban empty nonpreemptive segments for tasks.
Definition task_segments_are_nonempty :=
∀ tsk n,
(tsk \in ts) →
n < size (distances (task_preemption_points tsk)) →
ε ≤ nth 0 (distances (task_preemption_points tsk)) n.
∀ tsk n,
(tsk \in ts) →
n < size (distances (task_preemption_points tsk)) →
ε ≤ nth 0 (distances (task_preemption_points tsk)) n.
We define a valid task-level model with fixed preemption points
as a concatenation of the hypotheses above.
Definition valid_fixed_preemption_points_task_model :=
task_beginning_of_execution_in_preemption_points ∧
task_end_of_execution_in_preemption_points ∧
task_preemption_points_is_nondecreasing_sequence ∧
job_consists_of_the_same_number_of_segments_as_task ∧
lengths_of_task_segments_bound_length_of_job_segments ∧
task_segments_are_nonempty.
task_beginning_of_execution_in_preemption_points ∧
task_end_of_execution_in_preemption_points ∧
task_preemption_points_is_nondecreasing_sequence ∧
job_consists_of_the_same_number_of_segments_as_task ∧
lengths_of_task_segments_bound_length_of_job_segments ∧
task_segments_are_nonempty.
We define a valid model with fixed preemption points as
a model with fixed preemptions points at the task-level
and model with limited preemptions at the job-level.
Definition valid_fixed_preemption_points_model :=
valid_limited_preemptions_job_model arr_seq ∧
valid_fixed_preemption_points_task_model.
End ModelWithFixedPreemptionPoints.
valid_limited_preemptions_job_model arr_seq ∧
valid_fixed_preemption_points_task_model.
End ModelWithFixedPreemptionPoints.
Task's Run to Completion Threshold
In this section, we instantiate function task run to completion threshold for the limited preemptions model.
Consider any type of tasks.
In the model with limited preemptions, no job can be preempted after
a job reaches its last non-preemptive segment. Thus, we can
set task's run to completion threshold to task_cost tsk -
(task_last_nonpr_seg tsk - ε) which is always greater than
job_cost j - (job_last_nonpr_seg j - ε).
Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) :=
task_cost tsk - (task_last_nonpr_segment tsk - ε)
}.
End TaskRTCThresholdLimitedPreemptions.
{
task_run_to_completion_threshold (tsk : Task) :=
task_cost tsk - (task_last_nonpr_segment tsk - ε)
}.
End TaskRTCThresholdLimitedPreemptions.