Library prosa.classic.model.schedule.uni.limited.platform.limited
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Export prosa.classic.model.schedule.uni.limited.platform.definitions.
Require Export prosa.util.nondecreasing.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Export prosa.classic.model.schedule.uni.limited.platform.definitions.
Require Export prosa.util.nondecreasing.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Platform for models with limited preemptions
In module uni.limited.platform we introduce the notion of whether a job can be preempted at a given time (using a predicate can_be_preempted). In this section, we instantiate can_be_preempted for the model with fixed preemption points and model with floating nonpreemptive regions.
Module ModelWithLimitedPreemptions.
Import Job UniprocessorSchedule LimitedPreemptionPlatform.
Section ModelsWithLimitedPreemptions.
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.
Variable arr_seq: arrival_sequence Job.
Variable job_preemption_points: Job → seq time.
Section Definitions.
Section ModelWithLimitedPreemptions.
Definition lengths_of_segments j := distances (job_preemption_points j).
Definition job_max_nps (j : Job) := max0 (lengths_of_segments j).
Definition job_last_nps (j : Job) := last0 (lengths_of_segments j).
Definition job_with_zero_cost_consists_of_one_empty_segment :=
∀ j, arrives_in arr_seq j → job_cost j = 0 → job_preemption_points j = [::0; 0].
Definition last_segment_is_positive :=
∀ j, arrives_in arr_seq j → job_cost j > 0 → job_last_nps j > 0.
Definition beginning_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → first0 (job_preemption_points j) = 0.
Definition end_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → last0 (job_preemption_points j) = job_cost j.
Definition preemption_points_is_nondecreasing_sequence :=
∀ (j: Job),
arrives_in arr_seq j →
nondecreasing_sequence (job_preemption_points j).
Definition limited_preemptions_job_model :=
job_with_zero_cost_consists_of_one_empty_segment ∧
last_segment_is_positive ∧
beginning_of_execution_in_preemption_points ∧
end_of_execution_in_preemption_points ∧
preemption_points_is_nondecreasing_sequence.
End ModelWithLimitedPreemptions.
Section ModelWithFixedPreemptionPoints.
Variable task_preemption_points: Task → seq time.
Definition task_last_nps tsk := last0 (distances (task_preemption_points tsk)).
Definition task_max_nps tsk := max0 (distances (task_preemption_points tsk)).
Variable ts: list Task.
Definition task_beginning_of_execution_in_preemption_points :=
∀ tsk, tsk \in ts → first0 (task_preemption_points tsk) = 0.
Definition task_end_of_execution_in_preemption_points :=
∀ tsk, tsk \in ts → last0 (task_preemption_points tsk) = task_cost tsk.
Definition task_preemption_points_is_nondecreasing_sequence :=
∀ tsk, tsk \in ts → nondecreasing_sequence (task_preemption_points tsk).
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)).
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.
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.
Definition 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.
Definition fixed_preemption_points_model :=
limited_preemptions_job_model ∧
fixed_preemption_points_task_model.
End ModelWithFixedPreemptionPoints.
Section ModelWithFloatingNonpreemptiveRegions.
Variable task_max_nps: Task → time.
Definition job_max_np_segment_le_task_max_np_segment :=
∀ (j: Job),
arrives_in arr_seq j →
job_max_nps j ≤ task_max_nps (job_task j).
Definition model_with_floating_nonpreemptive_regions :=
limited_preemptions_job_model ∧
job_max_np_segment_le_task_max_np_segment.
End ModelWithFloatingNonpreemptiveRegions.
Definition can_be_preempted_for_model_with_limited_preemptions (j: Job) (progr: time) :=
progr \in job_preemption_points j.
Definition is_schedule_with_limited_preemptions (sched: schedule Job) :=
∀ j t,
arrives_in arr_seq j →
~~ can_be_preempted_for_model_with_limited_preemptions j (service sched j t) →
scheduled_at sched j t.
End Definitions.
Section Lemmas.
Variable sched: schedule Job.
Hypothesis H_is_schedule_with_limited_preemptions:
is_schedule_with_limited_preemptions sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Variable task_max_nps: Task → time.
Hypothesis H_limited_preemptions_job_model: limited_preemptions_job_model.
Hypothesis H_job_max_np_segment_le_task_max_np_segment:
job_max_np_segment_le_task_max_np_segment task_max_nps.
Section AuxiliaryLemmas.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Lemma list_of_preemption_point_is_not_empty:
0 < size (job_preemption_points j).
Lemma zero_in_preemption_points: 0 \in job_preemption_points j.
Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.
Corollary number_of_preemption_points_at_least_two: 2 ≤ size (job_preemption_points j).
End AuxiliaryLemmas.
Lemma model_with_fixed_preemption_points_is_correct:
correct_preemption_model arr_seq sched can_be_preempted_for_model_with_limited_preemptions.
Lemma model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments
job_cost job_task arr_seq can_be_preempted_for_model_with_limited_preemptions
job_max_nps task_max_nps.
End Lemmas.
End ModelsWithLimitedPreemptions.
End ModelWithLimitedPreemptions.
Import Job UniprocessorSchedule LimitedPreemptionPlatform.
Section ModelsWithLimitedPreemptions.
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.
Variable arr_seq: arrival_sequence Job.
Variable job_preemption_points: Job → seq time.
Section Definitions.
Section ModelWithLimitedPreemptions.
Definition lengths_of_segments j := distances (job_preemption_points j).
Definition job_max_nps (j : Job) := max0 (lengths_of_segments j).
Definition job_last_nps (j : Job) := last0 (lengths_of_segments j).
Definition job_with_zero_cost_consists_of_one_empty_segment :=
∀ j, arrives_in arr_seq j → job_cost j = 0 → job_preemption_points j = [::0; 0].
Definition last_segment_is_positive :=
∀ j, arrives_in arr_seq j → job_cost j > 0 → job_last_nps j > 0.
Definition beginning_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → first0 (job_preemption_points j) = 0.
Definition end_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → last0 (job_preemption_points j) = job_cost j.
Definition preemption_points_is_nondecreasing_sequence :=
∀ (j: Job),
arrives_in arr_seq j →
nondecreasing_sequence (job_preemption_points j).
Definition limited_preemptions_job_model :=
job_with_zero_cost_consists_of_one_empty_segment ∧
last_segment_is_positive ∧
beginning_of_execution_in_preemption_points ∧
end_of_execution_in_preemption_points ∧
preemption_points_is_nondecreasing_sequence.
End ModelWithLimitedPreemptions.
Section ModelWithFixedPreemptionPoints.
Variable task_preemption_points: Task → seq time.
Definition task_last_nps tsk := last0 (distances (task_preemption_points tsk)).
Definition task_max_nps tsk := max0 (distances (task_preemption_points tsk)).
Variable ts: list Task.
Definition task_beginning_of_execution_in_preemption_points :=
∀ tsk, tsk \in ts → first0 (task_preemption_points tsk) = 0.
Definition task_end_of_execution_in_preemption_points :=
∀ tsk, tsk \in ts → last0 (task_preemption_points tsk) = task_cost tsk.
Definition task_preemption_points_is_nondecreasing_sequence :=
∀ tsk, tsk \in ts → nondecreasing_sequence (task_preemption_points tsk).
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)).
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.
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.
Definition 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.
Definition fixed_preemption_points_model :=
limited_preemptions_job_model ∧
fixed_preemption_points_task_model.
End ModelWithFixedPreemptionPoints.
Section ModelWithFloatingNonpreemptiveRegions.
Variable task_max_nps: Task → time.
Definition job_max_np_segment_le_task_max_np_segment :=
∀ (j: Job),
arrives_in arr_seq j →
job_max_nps j ≤ task_max_nps (job_task j).
Definition model_with_floating_nonpreemptive_regions :=
limited_preemptions_job_model ∧
job_max_np_segment_le_task_max_np_segment.
End ModelWithFloatingNonpreemptiveRegions.
Definition can_be_preempted_for_model_with_limited_preemptions (j: Job) (progr: time) :=
progr \in job_preemption_points j.
Definition is_schedule_with_limited_preemptions (sched: schedule Job) :=
∀ j t,
arrives_in arr_seq j →
~~ can_be_preempted_for_model_with_limited_preemptions j (service sched j t) →
scheduled_at sched j t.
End Definitions.
Section Lemmas.
Variable sched: schedule Job.
Hypothesis H_is_schedule_with_limited_preemptions:
is_schedule_with_limited_preemptions sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Variable task_max_nps: Task → time.
Hypothesis H_limited_preemptions_job_model: limited_preemptions_job_model.
Hypothesis H_job_max_np_segment_le_task_max_np_segment:
job_max_np_segment_le_task_max_np_segment task_max_nps.
Section AuxiliaryLemmas.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Lemma list_of_preemption_point_is_not_empty:
0 < size (job_preemption_points j).
Lemma zero_in_preemption_points: 0 \in job_preemption_points j.
Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.
Corollary number_of_preemption_points_at_least_two: 2 ≤ size (job_preemption_points j).
End AuxiliaryLemmas.
Lemma model_with_fixed_preemption_points_is_correct:
correct_preemption_model arr_seq sched can_be_preempted_for_model_with_limited_preemptions.
Lemma model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments
job_cost job_task arr_seq can_be_preempted_for_model_with_limited_preemptions
job_max_nps task_max_nps.
End Lemmas.
End ModelsWithLimitedPreemptions.
End ModelWithLimitedPreemptions.