Commit a13cf394 authored by Sergey Bozhko's avatar Sergey Bozhko

Add add instances of job_preemptable

parent 04db857c
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.preemption Require Import
valid_model valid_schedule job.parameters task.parameters
rtc_threshold.valid_rtct job.instance.limited.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the model with limited preemptions
indeed defines a valid preemption model. *)
Section ModelWithLimitedPreemptions.
(** 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, assume the existence of a function that maps 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 limited ideal uniprocessor 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 after their completion. *)
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(** Next, we assume that preemption points are defined by the
job-level model with limited preemptions. *)
Hypothesis H_valid_limited_preemptions_job_model:
valid_limited_preemptions_job_model arr_seq.
(** First, we prove a few auxiliary lemmas. *)
Section AuxiliaryLemmas.
(** Consider a job j. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
(** Recall that 0 is a preemption point. *)
Remark zero_in_preemption_points: 0 \in job_preemption_points j.
Proof. by apply H_valid_limited_preemptions_job_model. Qed.
(** Using the fact that [job_preemption_points] is a
non-decreasing sequence, we prove that the first element of
[job_preemption_points] is 0. *)
Lemma zero_is_first_element: first0 (job_preemption_points j) = 0.
Proof.
have F := zero_in_preemption_points.
destruct H_valid_limited_preemptions_job_model as [_ [_ C]]; specialize (C j H_j_arrives).
by apply nondec_seq_zero_first.
Qed.
(** We prove that the list of preemption points is not empty. *)
Lemma list_of_preemption_point_is_not_empty:
0 < size (job_preemption_points j).
Proof.
move: H_valid_limited_preemptions_job_model => [BEG [END _]].
apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; rewrite size_eq0 in CONTR.
specialize (BEG j H_j_arrives).
by rewrite /beginning_of_execution_in_preemption_points (eqbool_to_eqprop CONTR) in BEG.
Qed.
(** Next, we prove that the cost of a job is a preemption point. *)
Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.
Proof.
move: H_valid_limited_preemptions_job_model => [BEG [END _]].
move: (END _ H_j_arrives) => EQ.
rewrite -EQ; clear EQ.
rewrite /last0 -nth_last.
apply/(nthP 0).
exists ((size (job_preemption_points j)).-1); last by done.
rewrite -(leq_add2r 1) !addn1 prednK //.
by apply list_of_preemption_point_is_not_empty.
Qed.
(** As a corollary, we prove that the sequence of nonpreemptive
points of a job with poisitive cost contains at least 2
points. *)
Corollary number_of_preemption_points_at_least_two:
job_cost_positive j ->
2 <= size (job_preemption_points j).
Proof.
intros POS.
move: H_valid_limited_preemptions_job_model => [BEG [END _]].
have EQ: 2 = size [::0; job_cost j]; first by done.
rewrite EQ; clear EQ.
apply subseq_leq_size.
rewrite !cons_uniq.
{ apply/andP; split.
rewrite in_cons negb_or; apply/andP; split; last by done.
rewrite neq_ltn; apply/orP; left; eauto 2.
apply/andP; split; by done. }
intros t EQ; move: EQ; rewrite !in_cons.
move => /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
- by rewrite EQ; apply zero_in_preemption_points.
- by rewrite EQ; apply job_cost_in_nonpreemptive_points.
Qed.
(** Next we prove that "antidensity" property (from
preemption.util file) holds for [job_preemption_point j]. *)
Lemma antidensity_of_preemption_points:
forall (ρ : work),
ρ <= job_cost j ->
~~ (ρ \in job_preemption_points j) ->
first0 (job_preemption_points j) <= ρ < last0 (job_preemption_points j).
Proof.
intros ρ LE NotIN.
move: H_valid_limited_preemptions_job_model => [BEG [END NDEC]].
apply/andP; split.
- by rewrite zero_is_first_element.
- rewrite END; last by done.
rewrite ltn_neqAle; apply/andP; split; last by done.
apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
rewrite CONTR in NotIN.
move: NotIN => /negP NIN; apply: NIN.
by apply job_cost_in_nonpreemptive_points.
Qed.
(** We also prove that any work that doesn't belong to
preemption points of job j is placed strictly between two
neighboring preemption points. *)
Lemma work_belongs_to_some_nonpreemptive_segment:
forall (ρ : work),
ρ <= job_cost j ->
~~ (ρ \in job_preemption_points j)->
exists n,
n.+1 < size (job_preemption_points j) /\
nth 0 (job_preemption_points j) n < ρ < nth 0 (job_preemption_points j) n.+1.
Proof.
intros ρ LE NotIN.
case: (posnP (job_cost j)) => [ZERO|POS].
{ exfalso; move: NotIN => /negP NIN; apply: NIN.
move: LE. rewrite ZERO leqn0; move => /eqP ->.
by apply zero_in_preemption_points. }
move: (belonging_to_segment_of_seq_is_total
(job_preemption_points j) ρ (number_of_preemption_points_at_least_two POS)
(antidensity_of_preemption_points _ LE NotIN)) => [n [SIZE2 /andP [N1 N2]]].
exists n; split; first by done.
apply/andP; split; last by done.
move: N1; rewrite leq_eqVlt; move => /orP [/eqP EQ | G]; last by done.
exfalso.
move: NotIN => /negP CONTR; apply: CONTR.
rewrite -EQ; clear EQ.
rewrite mem_nth //.
by apply ltnW.
Qed.
(** Recall that file [job.parameters] also defines notion of
preemption poins. And note that
[job.parameters.job_preemption_points] cannot have a
duplicating preemption points. Therefore, we need additional
lemmas to relate [job.parameters.job_preemption_points] and
[limited.job_preemption_points]]. *)
(** First we show that the length of the last non-preemptive
segment of [job.parameters.job_preemption_points] is equal to
the length of the last non-empty non-preemptive segment of
[limited.job_preemption_points]. *)
Lemma job_parameters_last_np_to_job_limited:
last0 (distances (parameters.job_preemption_points j)) =
last0 (filter (fun x => 0 < x) (distances (job_preemption_points j))).
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
intros; rewrite distances_iota_filtered; eauto.
rewrite -A2 //.
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
Qed.
(** Next we show that the length of the max non-preemptive
segment of [job.parameters.job_preemption_points] is equal to
the length of the max non-preemptive segment of
[limited.job_preemption_points]. *)
Lemma job_parameters_max_np_to_job_limited:
max0 (distances (parameters.job_preemption_points j)) =
max0 (distances (job_preemption_points j)).
Proof.
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].
unfold parameters.job_preemption_points, job_preemptable, limited_preemptions_model.
intros; rewrite distances_iota_filtered; eauto 2.
rewrite max0_rem0 //.
rewrite -A2 //.
by intros; apply last_is_max_in_nondecreasing_seq; eauto 2.
Qed.
End AuxiliaryLemmas.
(** We prove that the [fixed_preemption_point_model] function
defines a valid preemption model. *)
Lemma valid_fixed_preemption_points_model_lemma:
valid_preemption_model arr_seq sched.
Proof.
intros j ARR; repeat split.
{ by apply zero_in_preemption_points. }
{ by apply job_cost_in_nonpreemptive_points. }
{ by move => t NPP; apply H_valid_schedule_with_limited_preemptions. }
{ intros t NSCHED SCHED.
have SERV: service sched j t = service sched j t.+1.
{ rewrite -[service sched j t]addn0 /service /service_during; apply/eqP.
rewrite big_nat_recr //=.
rewrite eqn_add2l eq_sym.
rewrite scheduled_at_def in NSCHED.
by rewrite eqb0. }
rewrite -[job_preemptable _ _]Bool.negb_involutive.
apply/negP; intros CONTR.
move: NSCHED => /negP NSCHED; apply: NSCHED.
apply H_valid_schedule_with_limited_preemptions; first by done.
by rewrite SERV.
}
Qed.
End ModelWithLimitedPreemptions.
Hint Resolve valid_fixed_preemption_points_model_lemma : 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 Require Import job task.
From rt.restructuring.model.schedule Require Import nonpreemptive.
From rt.restructuring.model.preemption Require Import
valid_model job.parameters job.instance.nonpreemptive rtc_threshold.valid_rtct.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Platform for Fully Non-Preemptive model *)
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the fully non-preemptive model indeed
defines a valid preemption model. *)
Section FullyNonPreemptiveModel.
(** Consider any type of jobs. *)
Context {Job : JobType}.
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 non-preemptive ideal 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.
(** For simplicity, let's define some local names. *)
Let job_pending := pending sched.
Let job_completed_by := completed_by sched.
Let job_scheduled_at := scheduled_at sched.
(** Then, we prove that fully_nonpreemptive_model is a valid preemption model. *)
Lemma valid_fully_nonpreemptive_model:
valid_preemption_model arr_seq sched.
Proof.
intros j; split; [by apply/orP; left | split; [by apply/orP; right | split]].
- move => t; rewrite /job_preemptable /fully_nonpreemptive_model Bool.negb_orb -lt0n; move => /andP [POS NCOMPL].
move: (incremental_service_during _ _ _ _ _ POS) => [ft [/andP [_ LT] [SCHED SERV]]].
apply H_nonpreemptive_sched with ft.
+ by apply ltnW.
+ by done.
+ rewrite /completed_by -ltnNge.
move: NCOMPL; rewrite neq_ltn; move => /orP [LE|GE]; [by done | exfalso].
move: GE; rewrite ltnNge; move => /negP GE; apply: GE.
apply completion.service_at_most_cost; eauto 2 with basic_facts.
- intros t NSCHED SCHED.
rewrite /job_preemptable /fully_nonpreemptive_model.
apply/orP; left.
apply/negP; intros CONTR; move: CONTR => /negP; rewrite -lt0n; intros POS.
move: (incremental_service_during _ _ _ _ _ POS) => [ft [/andP [_ LT] [SCHEDn SERV]]].
move: NSCHED => /negP NSCHED; apply: NSCHED.
apply H_nonpreemptive_sched with ft.
+ by rewrite -ltnS.
+ by done.
+ rewrite /completed_by -ltnNge.
apply leq_ltn_trans with (service sched j t.+1).
* by rewrite /service /service_during big_nat_recr //= leq_addr.
* rewrite -addn1; apply leq_trans with (service sched j t.+2).
have <-: (service_at sched j t.+1) = 1.
{ by apply/eqP; rewrite eqb1 -scheduled_at_def. }
by rewrite -big_nat_recr //=.
by apply completion.service_at_most_cost; eauto 2 with basic_facts.
Qed.
(** We also prove that under the fully non-preemptive model
[job_max_nonpreemptive_segment j] is equal to [job_cost j] ... *)
Lemma job_max_nps_is_job_cost:
forall j, job_max_nonpreemptive_segment j = job_cost j.
Proof.
intros.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_model.
case: (posnP (job_cost j)) => [ZERO|POS].
{ by rewrite ZERO; compute. }
have ->: forall n, n>0 -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].
{ clear; simpl; intros.
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
have ->: forall xs P1 P2, (forall x, x \in xs -> ~~ P1 x) -> [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
{ clear; intros.
apply eq_in_filter.
intros ? IN. specialize (H _ IN).
by destruct (P1 x), (P2 x).
}
rewrite filter_pred1_uniq; first by done.
- by apply iota_uniq.
- by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].
- intros x; rewrite mem_iota; move => /andP [POS _].
by rewrite -lt0n.
}
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
by done.
Qed.
(** ... and [job_last_nonpreemptive_segment j] is equal to [job_cost j]. *)
Lemma job_last_nps_is_job_cost:
forall j, job_last_nonpreemptive_segment j = job_cost j.
Proof.
intros.
rewrite /job_last_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_model.
case: (posnP (job_cost j)) => [ZERO|POS].
{ by rewrite ZERO; compute. }
have ->: forall n, n>0 -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].
{ clear; simpl; intros.
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
have ->: forall xs P1 P2, (forall x, x \in xs -> ~~ P1 x) -> [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
{ clear; intros.
apply eq_in_filter.
intros ? IN. specialize (H _ IN).
by destruct (P1 x), (P2 x).
}
rewrite filter_pred1_uniq; first by done.
- by apply iota_uniq.
- by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].
- intros x; rewrite mem_iota; move => /andP [POS _].
by rewrite -lt0n.
}
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
by done.
Qed.
End FullyNonPreemptiveModel.
Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model.preemption Require Import valid_model job.parameters task.parameters.
From rt.restructuring.model.preemption Require Import job.instance.preemptive.
(** * Preemptions in Fully Premptive Model *)
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the fully preemptive model indeed defines
a valid preemption model. *)
Section FullyPreemptiveModel.
(** Consider any type of jobs. *)
Context {Job : JobType}.
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.
(** Then, we prove that fully_preemptive_model is a valid preemption model. *)
Lemma valid_fully_preemptive_model:
valid_preemption_model arr_seq sched.
Proof.
by intros j ARR; repeat split; intros t CONTR.
Qed.
(** We also prove that under the fully preemptive model
[job_max_nonpreemptive_segment j] is equal to 0, when [job_cost
j = 0] ... *)
Lemma job_max_nps_is_0:
forall j,
job_cost j = 0 ->
job_max_nonpreemptive_segment j = 0.
Proof.
intros.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
by rewrite H2; compute.
Qed.
(** ... or ε when [job_cost j > 0]. *)
Lemma job_max_nps_is_ε:
forall j,
job_cost j > 0 ->
job_max_nonpreemptive_segment j = ε.
Proof.
intros ? POS.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
rewrite /job_preemptable /fully_preemptive_model.
rewrite filter_predT.
apply max0_of_uniform_set.
- rewrite /range /index_iota subn0.
rewrite [size _]pred_Sn -[in X in _ <= X]addn1 -size_of_seq_of_distances size_iota.
+ by rewrite -pred_Sn.
+ by rewrite ltnS.
- by apply distances_of_iota_ε.
Qed.
End FullyPreemptiveModel.
Hint Resolve valid_fully_preemptive_model : basic_facts.
\ No newline at end of file
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model.preemption Require Import job.parameters task.parameters.
(** Definition of a parameter relating a job
to the sequence of its preemption points. *)
Class JobPreemptionPoints (Job : JobType) :=
{
job_preemption_points : Job -> seq work
}.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we instantiate [job_preemptable] for the model
with limited preemptions and introduce a set of requirements for
function [job_preemption_points], so it is coherent with limited
preemptions model. *)
Section LimitedPreemptions.
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** In addition, assume the existence of a function that
maps a job to the sequence of its preemption points. *)
Context `{JobPreemptionPoints Job}.
(** In the model with limited preemptions a job can be preempted
if its progress is equal to one of the preemption points. *)
Global Instance limited_preemptions_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := ρ \in job_preemption_points j
}.
(** Next, we describe some structural properties that
a sequence of preemption points should satisfy. *)
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** We require the sequence of preemption points to contain the beginning ... *)
Definition beginning_of_execution_in_preemption_points :=
forall j, arrives_in arr_seq j -> 0 \in job_preemption_points j.
(** ... and the end of execution for any job j. *)
Definition end_of_execution_in_preemption_points :=
forall j, arrives_in arr_seq j -> last0 (job_preemption_points j) = job_cost j.
(** We require the sequence of preemption points to be a non-decreasing sequence. *)
Definition preemption_points_is_nondecreasing_sequence :=
forall j, arrives_in arr_seq j -> nondecreasing_sequence (job_preemption_points j).
(** We define a valid job-level model with limited preemptions
as a conjunction of the hypotheses above. *)
Definition valid_limited_preemptions_job_model :=
beginning_of_execution_in_preemption_points /\
end_of_execution_in_preemption_points /\
preemption_points_is_nondecreasing_sequence.
End LimitedPreemptions.
\ No newline at end of file
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model.preemption Require Import job.parameters.
(** * Platform for Fully Non-Preemptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
non-preemptive model. *)
Section FullyNonPreemptiveModel.
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobCost Job}.
(** We say that the model is fully non-preemptive iff no job
can be preempted until its completion. *)
Global Instance fully_nonpreemptive_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := (ρ == 0) || (ρ == job_cost j)
}.
End FullyNonPreemptiveModel.
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model.preemption Require Import job.parameters.
(** * Platform for Fully Premptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
preemptive model. *)
Section FullyPreemptiveModel.
(** Consider any type of jobs. *)
Context {Job : JobType}.
(** In the fully preemptive model any job can be preempted at any time. *)
Global Program Instance fully_preemptive_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := true
}.
End FullyPreemptiveModel.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment