Commit 5a193c75 authored by Sergey Bozhko's avatar Sergey Bozhko

Add add instances of task_preemptable

parent a13cf394
From rt.util Require Import all nondecreasing.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import job task.
From rt.restructuring.model.preemption Require Import
valid_model job.parameters task.parameters rtc_threshold.valid_rtct
job.instance.limited valid_schedule task.instance.floating.
From rt.restructuring.analysis.basic_facts.preemption Require Import job.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Floating Non-Premptive Regions Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the model
with floating non-preemptive regions indeed defines a valid
preemption model with bounded non-preemptive regions. *)
Section FloatingNonPremptiveRegionsModel.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** In addition, we assume the existence of a function mapping a
task to its maximal non-preemptive segment ... *)
Context `{TaskMaxNonpreemptiveSegment Task}.
(** .. and the existence of functions mapping a
job to the sequence of its preemption points. *)
Context `{JobPreemptionPoints Job}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** Next, consider any ideal uniprocessor preemption-aware schedule
of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_preemption_aware_schedule:
valid_schedule_with_limited_preemptions arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Next, we assume that preemption points are defined by the model
with floating nonpreemptive regions. *)
Hypothesis H_valid_model_with_floating_nonpreemptive_regions:
valid_model_with_floating_nonpreemptive_regions arr_seq.
(** Then, we prove that the [job_preemptable and
task_max_nonpreemptive_segment] functions define
a model with bounded nonpremtive regions. *)
Lemma floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
Proof.
intros j ARR.
move: (H_valid_model_with_floating_nonpreemptive_regions) => LIM; move: LIM (LIM) => [LIM L] [[BEG [END NDEC]] MAX].
case: (posnP (job_cost j)) => [ZERO|POS].
- split.
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
exists 0; rewrite LE; split; first by apply/andP; split.
by eapply zero_in_preemption_points; eauto 2.
- split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
+ by apply MAX.
+ exists progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
+ move: NotIN => /eqP; rewrite eqbF_neg; move => NotIN.
edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2. move: N => /andP [N1 N2].
set ptl := nth 0 (job_preemption_points j) x.
set ptr := nth 0 (job_preemption_points j) x.+1.
exists ptr; split; first last.
* by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
* apply/andP; split; first by apply ltnW.
apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
-- rewrite addn1 ltn_add2r; apply N1.
-- unfold job_max_nonpreemptive_segment.
rewrite -addnA -leq_subLR -(leq_add2r 1).
rewrite [in X in _ <= X]addnC -leq_subLR.
rewrite !subn1 !addn1 prednK.
{ rewrite -[_.+1.-1]pred_Sn. rewrite /lengths_of_segments.
erewrite job_parameters_max_np_to_job_limited; eauto.
by apply distance_between_neighboring_elements_le_max_distance_in_seq. }
{ rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
exists 0, (job_cost j); repeat split.
- by eapply zero_in_preemption_points; eauto.
- by eapply job_cost_in_nonpreemptive_points; eauto.
- by apply/eqP; rewrite eq_sym -lt0n; apply POS.
}
Qed.
(** Which together with lemma [valid_fixed_preemption_points_model]
gives us the fact that functions [job_preemptable and
task_max_nonpreemptive_segment] define a valid preemption model
with bounded non-preemptive regions. *)
Corollary floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
Proof.
split.
- apply valid_fixed_preemption_points_model_lemma; auto.
by apply H_valid_model_with_floating_nonpreemptive_regions.
- apply floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
Qed.
End FloatingNonPremptiveRegionsModel.
Hint Resolve
valid_fixed_preemption_points_model_lemma
floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
From rt.util Require Import all nondecreasing.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.preemption Require Import
valid_model job.parameters task.parameters.
From rt.restructuring.model.preemption Require Import valid_schedule job.instance.limited task.instance.limited.
From rt.restructuring.analysis.basic_facts.preemption Require Import job.limited.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_preemption_points] to the
limited preemptions model indeed defines a valid preemption model
with bounded non-preemptive regions. *)
Section LimitedPreemptionsModel.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** In addition, we assume the existence of functions mapping a
job and task to the sequence of its preemption points. *)
Context `{JobPreemptionPoints Job}.
Context `{TaskPreemptionPoints Task}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** Next, consider any ideal uniprocessor preemption-aware schedule
of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_valid_schedule_with_limited_preemptions:
valid_schedule_with_limited_preemptions arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Consider an arbitrary task set ts. *)
Variable ts : list Task.
(** Next, we assume that preemption points are defined by the model
with fixed preemption points. *)
Hypothesis H_valid_fixed_preemption_points_model:
valid_fixed_preemption_points_model arr_seq ts.
(** Then we prove that functions [job_preemptable and
task_preemption_points] define a model with bounded nonpremtive
regions. *)
Lemma fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq .
Proof.
intros j ARR.
move: H_valid_fixed_preemption_points_model => [LIM FIX].
move: (LIM) => [BEG [END NDEC]]; move: (FIX) => [A1 [A2 [A3 [A4 A5]]]].
case: (posnP (job_cost j)) => [ZERO|POS].
- split.
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
+ move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
exists 0; rewrite LE; split; first by apply/andP; split.
by eapply zero_in_preemption_points; eauto 2.
- split; last (move => progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
+ rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment
/job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
by apply max_of_dominating_seq; intros; apply A5.
+ exists progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
+ move: NotIN => /eqP; rewrite eqbF_neg; move => NotIN.
edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2. move: N => /andP [N1 N2].
set ptl := nth 0 (job_preemption_points j) x.
set ptr := nth 0 (job_preemption_points j) x.+1.
exists ptr; split; first last.
* by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
* apply/andP; split; first by apply ltnW.
apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
-- rewrite addn1 ltn_add2r; apply N1.
-- unfold job_max_nonpreemptive_segment.
rewrite -addnA -leq_subLR -(leq_add2r 1).
rewrite [in X in _ <= X]addnC -leq_subLR.
rewrite !subn1 !addn1 prednK.
{ rewrite -[_.+1.-1]pred_Sn. rewrite /lengths_of_segments.
erewrite job_parameters_max_np_to_job_limited; eauto.
by apply distance_between_neighboring_elements_le_max_distance_in_seq. }
{ rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
exists 0, (job_cost j); repeat split.
- by eapply zero_in_preemption_points; eauto.
- by eapply job_cost_in_nonpreemptive_points; eauto.
- by apply/eqP; rewrite eq_sym -lt0n; apply POS.
}
Qed.
(** Which together with lemma [valid_fixed_preemption_points_model]
gives us the fact that functions [job_preemptable and
task_preemption_points] defines a valid preemption model with
bounded non-preemptive regions. *)
Corollary fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
Proof.
split.
- by apply valid_fixed_preemption_points_model_lemma; destruct H_valid_fixed_preemption_points_model.
- by apply fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
Qed.
End LimitedPreemptionsModel.
Hint Resolve
valid_fixed_preemption_points_model_lemma
fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.schedule Require Import nonpreemptive.
From rt.restructuring.model.preemption Require Import
job.instance.nonpreemptive task.instance.nonpreemptive.
From rt.restructuring.analysis.basic_facts.preemption Require Import
job.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Fully Non-Premptive Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the fully
non-preemptive model indeed defines a valid preemption model with
bounded non-preemptive regions. *)
Section FullyNonPreemptiveModel.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** Next, consider any ideal non-preemptive uniprocessor schedule of this arrival sequence... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_job_cost_le_task_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
(** Then we prove that [fully_nonpreemptive_model] function
defines a model with bounded nonpremtive regions.*)
Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
Proof.
have F: forall n, n = 0 \/ n > 0 by intros n; destruct n; [left | right].
intros j; split.
{ rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment; eauto 2.
erewrite job_max_nps_is_job_cost; eauto 2.
}
move => progr /andP [_ GE].
move: (F (progr)) => [EQ | GT].
{ exists progr; split.
- by apply/andP; split; [done | rewrite leq_addr].
- rewrite /job_preemptable /fully_nonpreemptive_model.
by apply/orP; left; rewrite EQ.
}
{ exists (maxn progr (job_cost j)).
have POS: 0 < job_cost j by apply leq_trans with progr.
split.
{ apply/andP; split; first by rewrite leq_maxl.
erewrite job_max_nps_is_job_cost; eauto 2; rewrite addnBA; last eauto 2.
rewrite geq_max; apply/andP; split.
- rewrite -addnBA; last by eauto 2.
by rewrite leq_addr.
- by rewrite addnC -addnBA // leq_addr.
}
{ apply/orP; right.
rewrite eqn_leq; apply/andP; split.
- by rewrite geq_max; apply/andP; split.
- by rewrite leq_max; apply/orP; right.
}
}
Qed.
(** Which together with lemma [valid_fully_nonpreemptive_model]
gives us the fact that [fully_nonpreemptive_model] defined a valid
preemption model with bounded non-preemptive regions. *)
Corollary fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
Proof.
split.
- by apply valid_fully_nonpreemptive_model.
- by apply fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions.
Qed.
End FullyNonPreemptiveModel.
Hint Resolve
valid_fully_nonpreemptive_model
fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.preemption Require Import
valid_model job.instance.preemptive task.instance.preemptive.
From rt.restructuring.analysis.basic_facts.preemption Require Import
job.preemptive.
(** * Platform for Fully Premptive Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the fully
preemptive model indeed defines a valid preemption model with
bounded non-preemptive regions. *)
Section FullyPreemptiveModel.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any given schedule. *)
Variable sched : schedule PState.
(** We prove that [fully_preemptive_model] function
defines a model with bounded nonpremtive regions.*)
Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
Proof.
intros j ARR; split.
- case: (posnP (job_cost j)) => [ZERO|POS].
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_0.
+ by rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment job_max_nps_is_ε.
- intros t; exists t; split.
+ by apply/andP; split; [ done | rewrite leq_addr].
+ by done.
Qed.
(** Which together with lemma [valid_fully_preemptive_model] gives
us the fact that [fully_preemptive_model] defined a valid
preemption model with bounded non-preemptive regions. *)
Corollary fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
Proof.
split.
apply valid_fully_preemptive_model.
apply fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions.
Qed.
End FullyPreemptiveModel.
Hint Resolve
valid_fully_preemptive_model
fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_facts.
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import model.job model.task.
From rt.restructuring.model.preemption Require Import job.parameters task.parameters.
From rt.restructuring.model.preemption Require Import job.instance.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Models with Floating Non-Preemptive Regions *)
(** In this section, we introduce a set of requirements for function
[task_max_nonpr_segment], so it is coherent with model with
floating non-preemptive regions. *)
Section ModelWithFloatingNonpreemptiveRegions.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
(** ... 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}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** We require [task_max_nonpreemptive_segment (job_task j)] to be
an upper bound of the lenght of the max nonpreemptive segment of
job [j]. *)
Definition job_max_np_segment_le_task_max_np_segment :=
forall (j : Job),
arrives_in arr_seq j ->
job_max_nonpreemptive_segment j <= task_max_nonpreemptive_segment (job_task j).
(** We define a valid model with floating nonpreemptive regions as the
model with floating nonpreemptive regions at the task-level and
valid model with limited preemptions at the job-level. *)
Definition valid_model_with_floating_nonpreemptive_regions :=
valid_limited_preemptions_job_model arr_seq /\
job_max_np_segment_le_task_max_np_segment.
End ModelWithFloatingNonpreemptiveRegions.
From rt.util Require Import all nondecreasing.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import model.job model.task.
From rt.restructuring.model.preemption Require Import job.parameters task.parameters.
From rt.restructuring.model.preemption Require Import job.instance.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * 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. *)
Section ModelWithFixedPreemptionPoints.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskPreemptionPoints Task}.
(** ... 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}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** Consider an arbitrary task set ts. *)
Variable ts : list Task.
(** 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 :=
forall 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 :=
forall 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 :=
forall 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 :=
forall 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 :=
forall 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 :=
forall 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.
(** 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.
From rt.util Require Export all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import model.job model.task.
From rt.restructuring.model.preemption Require Export
valid_model job.parameters task.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Fully Non-Preemptive Model *)
(** In this section, we instantiate function
[task_max_nonpreemptive_segment] for the fully non-preemptive
model. *)
Section FullyNonPreemptiveModel.
(** Consider any type of jobs. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** In fully non-preemptive model no job can be preempted until its
completion. The maximal non-preemptive segment of a job
[j] has length [job_cost j] which is bounded by [task_cost tsk].*)
Global Program Instance fully_nonpreemptive_model : TaskMaxNonpreemptiveSegment Task :=
{
task_max_nonpreemptive_segment (tsk : Task) := task_cost tsk
}.
End FullyNonPreemptiveModel.
From rt.util Require Export all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import model.job model.task.
From rt.restructuring.model.preemption Require Import
valid_model job.parameters task.parameters.
(** * Platform for Fully Preemptive Model *)
(** In this section, we instantiate function
[task_max_nonpreemptive_segment] for the fully preemptive model. *)
Section FullyPreemptiveModel.
(** Consider any type of jobs. *)
Context {Task : J