Library prosa.classic.model.schedule.uni.sustainability
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.schedulability.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Sustainability.
Import ArrivalSequence UniprocessorSchedule Schedulability.
Section SustainabilityDefs.
Context {Job: eqType}.
Section DefiningParameters.
Require Import prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.schedulability.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Sustainability.
Import ArrivalSequence UniprocessorSchedule Schedulability.
Section SustainabilityDefs.
Context {Job: eqType}.
Section DefiningParameters.
Defining Parameter Type
Section ParameterType.
Inductive parameter_label :=
| JOB_ARRIVAL
| JOB_COST
| JOB_DEADLINE
| JOB_JITTER
| JOB_SUSPENSION.
Scheme Equality for parameter_label.
Lemma eqlabelP: Equality.axiom parameter_label_beq.
Proof.
intros x y.
by destruct x; destruct y; try (by apply ReflectT); try (by apply ReflectF).
Qed.
Canonical label_eqMixin := EqMixin eqlabelP.
Canonical label_eqType := Eval hnf in EqType parameter_label label_eqMixin.
Definition type_of_label (l: parameter_label) : Type :=
match l with
| JOB_ARRIVAL ⇒ Job → instant
| JOB_COST ⇒ Job → time
| JOB_DEADLINE ⇒ Job → time
| JOB_JITTER ⇒ Job → time
| JOB_SUSPENSION ⇒ Job → time → duration
end.
Definition default_val (l : parameter_label) : type_of_label l :=
match l with
| JOB_ARRIVAL ⇒ fun _ ⇒ 0
| JOB_COST ⇒ fun _ ⇒ 0
| JOB_DEADLINE ⇒ fun _ ⇒ 0
| JOB_JITTER ⇒ fun _ ⇒ 0
| JOB_SUSPENSION ⇒ fun _ _ ⇒ 0
end.
Record job_parameter := param
{
p_label : parameter_label;
p_function : type_of_label p_label
}.
Variable example_job_cost: Job → time.
Variable example_job_suspension: Job → time → duration.
Let example_params :=
[:: param JOB_COST example_job_cost; param JOB_SUSPENSION example_job_suspension].
End ParameterType.
Inductive parameter_label :=
| JOB_ARRIVAL
| JOB_COST
| JOB_DEADLINE
| JOB_JITTER
| JOB_SUSPENSION.
Scheme Equality for parameter_label.
Lemma eqlabelP: Equality.axiom parameter_label_beq.
Proof.
intros x y.
by destruct x; destruct y; try (by apply ReflectT); try (by apply ReflectF).
Qed.
Canonical label_eqMixin := EqMixin eqlabelP.
Canonical label_eqType := Eval hnf in EqType parameter_label label_eqMixin.
Definition type_of_label (l: parameter_label) : Type :=
match l with
| JOB_ARRIVAL ⇒ Job → instant
| JOB_COST ⇒ Job → time
| JOB_DEADLINE ⇒ Job → time
| JOB_JITTER ⇒ Job → time
| JOB_SUSPENSION ⇒ Job → time → duration
end.
Definition default_val (l : parameter_label) : type_of_label l :=
match l with
| JOB_ARRIVAL ⇒ fun _ ⇒ 0
| JOB_COST ⇒ fun _ ⇒ 0
| JOB_DEADLINE ⇒ fun _ ⇒ 0
| JOB_JITTER ⇒ fun _ ⇒ 0
| JOB_SUSPENSION ⇒ fun _ _ ⇒ 0
end.
Record job_parameter := param
{
p_label : parameter_label;
p_function : type_of_label p_label
}.
Variable example_job_cost: Job → time.
Variable example_job_suspension: Job → time → duration.
Let example_params :=
[:: param JOB_COST example_job_cost; param JOB_SUSPENSION example_job_suspension].
End ParameterType.
Looking up parameters
Section ParameterLookup.
Definition find_param (l : parameter_label) (s : seq job_parameter) :=
nth (param l (default_val l)) s
(find (fun x ⇒ p_label x == l) s).
Let convert_parameter_type (p: job_parameter) (l: parameter_label)
(EQ_PROOF: p_label p = l) :=
eq_rect (p_label p) (fun x ⇒ type_of_label x) (p_function p) l EQ_PROOF.
Definition get_param_function (l: parameter_label) (p: job_parameter) : type_of_label l :=
if (parameter_label_eq_dec (p_label p) l) is left EQ_PROOF then
convert_parameter_type p l EQ_PROOF
else (default_val l).
Definition return_param (l: parameter_label) (s: seq job_parameter) : type_of_label l :=
get_param_function l (find_param l s).
Variable example_job_cost: Job → time.
Variable example_job_suspension: Job → time → duration.
Let example_params :=
[:: param JOB_COST example_job_cost; param JOB_SUSPENSION example_job_suspension].
Example return_param_works1:
return_param JOB_COST example_params = example_job_cost.
Proof. by done. Qed.
Example return_param_works2:
return_param JOB_SUSPENSION example_params = example_job_suspension.
Proof. by done. Qed.
End ParameterLookup.
Definition find_param (l : parameter_label) (s : seq job_parameter) :=
nth (param l (default_val l)) s
(find (fun x ⇒ p_label x == l) s).
Let convert_parameter_type (p: job_parameter) (l: parameter_label)
(EQ_PROOF: p_label p = l) :=
eq_rect (p_label p) (fun x ⇒ type_of_label x) (p_function p) l EQ_PROOF.
Definition get_param_function (l: parameter_label) (p: job_parameter) : type_of_label l :=
if (parameter_label_eq_dec (p_label p) l) is left EQ_PROOF then
convert_parameter_type p l EQ_PROOF
else (default_val l).
Definition return_param (l: parameter_label) (s: seq job_parameter) : type_of_label l :=
get_param_function l (find_param l s).
Variable example_job_cost: Job → time.
Variable example_job_suspension: Job → time → duration.
Let example_params :=
[:: param JOB_COST example_job_cost; param JOB_SUSPENSION example_job_suspension].
Example return_param_works1:
return_param JOB_COST example_params = example_job_cost.
Proof. by done. Qed.
Example return_param_works2:
return_param JOB_SUSPENSION example_params = example_job_suspension.
Proof. by done. Qed.
End ParameterLookup.
Additional properties of parameter lists
Section Properties.
Definition differ_only_by (variable_labels: seq parameter_label) (s1 s2: seq job_parameter) :=
∀ (param param': job_parameter),
List.In param s1 →
List.In param' s2 →
p_label param = p_label param' →
p_label param \notin variable_labels →
param = param'.
Definition labels_of (params: seq job_parameter) := [seq p_label p | p <- params].
Definition has_unique_labels (params: seq job_parameter) := uniq (labels_of params).
Definition corresponding_labels (params: seq job_parameter) (labels: seq parameter_label) :=
∀ l, l \in labels_of params ↔ l \in labels.
Lemma found_param_label:
∀ (params: seq job_parameter) (p: job_parameter) (label: parameter_label),
has_unique_labels params →
List.In p params →
p_label p = label →
p = param label (return_param label params).
Proof.
induction params as [| p0 params']; first by done.
move ⇒ p label /= /andP [NOTIN UNIQ] IN EQ /=.
move: IN ⇒ [EQ0 | IN].
{
subst p0; rewrite /return_param /find_param /= EQ eq_refl /=.
by destruct p, label; simpl in *; subst.
}
{
rewrite /return_param /find_param /=.
case EQ': (_ == _); last by apply IHparams'.
move: EQ' ⇒ /eqP EQ'; rewrite EQ' in NOTIN.
move: NOTIN ⇒ /negP NOTIN; exfalso; apply NOTIN.
by apply/mapP2; ∃ p.
}
Qed.
End Properties.
End DefiningParameters.
Definition differ_only_by (variable_labels: seq parameter_label) (s1 s2: seq job_parameter) :=
∀ (param param': job_parameter),
List.In param s1 →
List.In param' s2 →
p_label param = p_label param' →
p_label param \notin variable_labels →
param = param'.
Definition labels_of (params: seq job_parameter) := [seq p_label p | p <- params].
Definition has_unique_labels (params: seq job_parameter) := uniq (labels_of params).
Definition corresponding_labels (params: seq job_parameter) (labels: seq parameter_label) :=
∀ l, l \in labels_of params ↔ l \in labels.
Lemma found_param_label:
∀ (params: seq job_parameter) (p: job_parameter) (label: parameter_label),
has_unique_labels params →
List.In p params →
p_label p = label →
p = param label (return_param label params).
Proof.
induction params as [| p0 params']; first by done.
move ⇒ p label /= /andP [NOTIN UNIQ] IN EQ /=.
move: IN ⇒ [EQ0 | IN].
{
subst p0; rewrite /return_param /find_param /= EQ eq_refl /=.
by destruct p, label; simpl in *; subst.
}
{
rewrite /return_param /find_param /=.
case EQ': (_ == _); last by apply IHparams'.
move: EQ' ⇒ /eqP EQ'; rewrite EQ' in NOTIN.
move: NOTIN ⇒ /negP NOTIN; exfalso; apply NOTIN.
by apply/mapP2; ∃ p.
}
Qed.
End Properties.
End DefiningParameters.
Definition of sustainability for scheduling policies.
Section SustainabilityPolicy.
Variable all_labels: seq parameter_label.
Variable is_schedulable:
seq job_parameter → schedule Job → Job → bool.
Variable belongs_to_task_model:
seq job_parameter → arrival_sequence Job → schedule Job → Prop.
Variable sustainable_param: parameter_label.
Variable has_better_params: (type_of_label sustainable_param) →
(type_of_label sustainable_param) → Prop.
Definition sustainable_param_becomes_better (params params': seq job_parameter) :=
let P := return_param sustainable_param params in
let P' := return_param sustainable_param params' in
has_better_params P P'.
Section VaryingParameters.
Variable variable_params: seq parameter_label.
Definition sustainable_and_varying_params_in (params: seq job_parameter) :=
∀ label,
label \in sustainable_param :: variable_params →
label \in labels_of params.
Definition has_consistent_labels (params: seq job_parameter) :=
has_unique_labels params ∧
corresponding_labels params all_labels ∧
sustainable_and_varying_params_in params.
Definition jobs_are_schedulable_with (params: seq job_parameter) :=
∀ arr_seq sched j,
belongs_to_task_model params arr_seq sched →
is_schedulable params sched j.
Definition jobs_are_V_schedulable_with (params: seq job_parameter) :=
∀ (similar_params: seq job_parameter),
has_consistent_labels similar_params →
differ_only_by variable_params params similar_params →
jobs_are_schedulable_with similar_params.
Definition weakly_sustainable :=
∀ (params better_params: seq job_parameter),
has_consistent_labels params →
has_consistent_labels better_params →
differ_only_by [::sustainable_param] params better_params →
sustainable_param_becomes_better params better_params →
jobs_are_V_schedulable_with params →
jobs_are_schedulable_with better_params.
Section AlternativeDefinition.
Definition sustainable_param_becomes_worse (params params': seq job_parameter) :=
let P := return_param sustainable_param params in
let P' := return_param sustainable_param params' in
has_better_params P' P.
Definition jobs_are_not_schedulable_with (params: seq job_parameter) :=
∃ arr_seq sched j,
belongs_to_task_model params arr_seq sched ∧
~~ is_schedulable params sched j.
Definition weakly_sustainable_contrapositive :=
∀ params params_worse,
has_consistent_labels params →
has_consistent_labels params_worse →
jobs_are_not_schedulable_with params →
differ_only_by [:: sustainable_param] params params_worse →
sustainable_param_becomes_worse params params_worse →
∃ params_worse',
has_consistent_labels params_worse' ∧
differ_only_by variable_params params_worse params_worse' ∧
jobs_are_not_schedulable_with params_worse'.
Hypothesis H_classical_forall_exists:
∀ (T: Type) (P: T → Prop),
¬ (∀ x, ¬ P x) → ∃ x, P x.
Hypothesis H_classical_and_or:
∀ (P Q: Prop), ¬ (P ∧ Q) → ¬ P ∨ ¬ Q.
Theorem weak_sustainability_equivalence:
weakly_sustainable ↔ weakly_sustainable_contrapositive.
Proof.
rename H_classical_forall_exists into NOTALL, H_classical_and_or into ANDOR.
split.
{
intros WEAK params params_worse CONS CONSworse NOTSCHED DIFF WORSE.
apply NOTALL; intro ALL.
unfold weakly_sustainable in ×.
specialize (WEAK params_worse params CONSworse CONS).
feed WEAK.
{
intros p p' IN IN' EQ NOTIN; symmetry.
apply DIFF; try by done.
by rewrite -EQ.
}
feed WEAK; first by done.
feed WEAK.
{
intros params' CONS' DIFF'; specialize (ALL params').
apply ANDOR in ALL; move: ALL ⇒ [BUG | ALL] //.
apply ANDOR in ALL; move: ALL ⇒ [BUG | ALL] //.
unfold jobs_are_not_schedulable_with in ×.
intros arr_seq sched j BELONGS; apply contraT; intro NOTSCHED'.
by exfalso; apply ALL; ∃ arr_seq, sched, j.
}
unfold jobs_are_schedulable_with, jobs_are_not_schedulable_with in ×.
clear -WEAK NOTSCHED.
move: NOTSCHED ⇒ [arr_seq [sched [j [BELONGS NOTSCHED]]]].
specialize (WEAK arr_seq sched j BELONGS).
by rewrite WEAK in NOTSCHED.
}
{
intros WEAK params better_params CONS CONSbetter DIFF BETTER VSCHED.
intros arr_seq sched j BELONGS; apply contraT; intros NOTSCHED.
unfold weakly_sustainable_contrapositive in ×.
feed (WEAK better_params params); first by done.
feed WEAK; first by done.
feed WEAK; first by ∃ arr_seq, sched, j.
feed WEAK.
{
intros p p' IN IN' EQ NOTIN; symmetry.
apply DIFF; try by done.
by rewrite -EQ.
}
feed WEAK; first by done.
move: WEAK ⇒ [params_worse' [CONS' [DIFF' NOTSCHED']]].
unfold jobs_are_V_schedulable_with in ×.
specialize (VSCHED params_worse' CONS' DIFF').
move: NOTSCHED' ⇒ [arr_seq' [sched' [j' [BELONGS' NOTSCHED']]]].
specialize (VSCHED arr_seq' sched' j' BELONGS').
by rewrite VSCHED in NOTSCHED'.
}
Qed.
End AlternativeDefinition.
End VaryingParameters.
Definition strongly_sustainable := weakly_sustainable [::].
End SustainabilityPolicy.
End SustainabilityDefs.
Global Arguments job_parameter: clear implicits.
End Sustainability.
Variable all_labels: seq parameter_label.
Variable is_schedulable:
seq job_parameter → schedule Job → Job → bool.
Variable belongs_to_task_model:
seq job_parameter → arrival_sequence Job → schedule Job → Prop.
Variable sustainable_param: parameter_label.
Variable has_better_params: (type_of_label sustainable_param) →
(type_of_label sustainable_param) → Prop.
Definition sustainable_param_becomes_better (params params': seq job_parameter) :=
let P := return_param sustainable_param params in
let P' := return_param sustainable_param params' in
has_better_params P P'.
Section VaryingParameters.
Variable variable_params: seq parameter_label.
Definition sustainable_and_varying_params_in (params: seq job_parameter) :=
∀ label,
label \in sustainable_param :: variable_params →
label \in labels_of params.
Definition has_consistent_labels (params: seq job_parameter) :=
has_unique_labels params ∧
corresponding_labels params all_labels ∧
sustainable_and_varying_params_in params.
Definition jobs_are_schedulable_with (params: seq job_parameter) :=
∀ arr_seq sched j,
belongs_to_task_model params arr_seq sched →
is_schedulable params sched j.
Definition jobs_are_V_schedulable_with (params: seq job_parameter) :=
∀ (similar_params: seq job_parameter),
has_consistent_labels similar_params →
differ_only_by variable_params params similar_params →
jobs_are_schedulable_with similar_params.
Definition weakly_sustainable :=
∀ (params better_params: seq job_parameter),
has_consistent_labels params →
has_consistent_labels better_params →
differ_only_by [::sustainable_param] params better_params →
sustainable_param_becomes_better params better_params →
jobs_are_V_schedulable_with params →
jobs_are_schedulable_with better_params.
Section AlternativeDefinition.
Definition sustainable_param_becomes_worse (params params': seq job_parameter) :=
let P := return_param sustainable_param params in
let P' := return_param sustainable_param params' in
has_better_params P' P.
Definition jobs_are_not_schedulable_with (params: seq job_parameter) :=
∃ arr_seq sched j,
belongs_to_task_model params arr_seq sched ∧
~~ is_schedulable params sched j.
Definition weakly_sustainable_contrapositive :=
∀ params params_worse,
has_consistent_labels params →
has_consistent_labels params_worse →
jobs_are_not_schedulable_with params →
differ_only_by [:: sustainable_param] params params_worse →
sustainable_param_becomes_worse params params_worse →
∃ params_worse',
has_consistent_labels params_worse' ∧
differ_only_by variable_params params_worse params_worse' ∧
jobs_are_not_schedulable_with params_worse'.
Hypothesis H_classical_forall_exists:
∀ (T: Type) (P: T → Prop),
¬ (∀ x, ¬ P x) → ∃ x, P x.
Hypothesis H_classical_and_or:
∀ (P Q: Prop), ¬ (P ∧ Q) → ¬ P ∨ ¬ Q.
Theorem weak_sustainability_equivalence:
weakly_sustainable ↔ weakly_sustainable_contrapositive.
Proof.
rename H_classical_forall_exists into NOTALL, H_classical_and_or into ANDOR.
split.
{
intros WEAK params params_worse CONS CONSworse NOTSCHED DIFF WORSE.
apply NOTALL; intro ALL.
unfold weakly_sustainable in ×.
specialize (WEAK params_worse params CONSworse CONS).
feed WEAK.
{
intros p p' IN IN' EQ NOTIN; symmetry.
apply DIFF; try by done.
by rewrite -EQ.
}
feed WEAK; first by done.
feed WEAK.
{
intros params' CONS' DIFF'; specialize (ALL params').
apply ANDOR in ALL; move: ALL ⇒ [BUG | ALL] //.
apply ANDOR in ALL; move: ALL ⇒ [BUG | ALL] //.
unfold jobs_are_not_schedulable_with in ×.
intros arr_seq sched j BELONGS; apply contraT; intro NOTSCHED'.
by exfalso; apply ALL; ∃ arr_seq, sched, j.
}
unfold jobs_are_schedulable_with, jobs_are_not_schedulable_with in ×.
clear -WEAK NOTSCHED.
move: NOTSCHED ⇒ [arr_seq [sched [j [BELONGS NOTSCHED]]]].
specialize (WEAK arr_seq sched j BELONGS).
by rewrite WEAK in NOTSCHED.
}
{
intros WEAK params better_params CONS CONSbetter DIFF BETTER VSCHED.
intros arr_seq sched j BELONGS; apply contraT; intros NOTSCHED.
unfold weakly_sustainable_contrapositive in ×.
feed (WEAK better_params params); first by done.
feed WEAK; first by done.
feed WEAK; first by ∃ arr_seq, sched, j.
feed WEAK.
{
intros p p' IN IN' EQ NOTIN; symmetry.
apply DIFF; try by done.
by rewrite -EQ.
}
feed WEAK; first by done.
move: WEAK ⇒ [params_worse' [CONS' [DIFF' NOTSCHED']]].
unfold jobs_are_V_schedulable_with in ×.
specialize (VSCHED params_worse' CONS' DIFF').
move: NOTSCHED' ⇒ [arr_seq' [sched' [j' [BELONGS' NOTSCHED']]]].
specialize (VSCHED arr_seq' sched' j' BELONGS').
by rewrite VSCHED in NOTSCHED'.
}
Qed.
End AlternativeDefinition.
End VaryingParameters.
Definition strongly_sustainable := weakly_sustainable [::].
End SustainabilityPolicy.
End SustainabilityDefs.
Global Arguments job_parameter: clear implicits.
End Sustainability.