diff --git a/analysis/uni/susp/sustainability/allcosts/main_claim.v b/analysis/uni/susp/sustainability/allcosts/main_claim.v
new file mode 100644
index 0000000000000000000000000000000000000000..44d78e7ee59b74143fca70654e2fc64300b0a7aa
--- /dev/null
+++ b/analysis/uni/susp/sustainability/allcosts/main_claim.v
@@ -0,0 +1,165 @@
+Require Import rt.util.all.
+Require Import rt.model.priority rt.model.suspension.
+Require Import rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.response_time
+ rt.model.schedule.uni.sustainability.
+Require Import rt.model.schedule.uni.susp.suspension_intervals
+ rt.model.schedule.uni.susp.schedule
+ rt.model.schedule.uni.susp.valid_schedule
+ rt.model.schedule.uni.susp.build_suspension_table
+ rt.model.schedule.uni.susp.platform.
+Require Import rt.analysis.uni.susp.sustainability.allcosts.reduction
+ rt.analysis.uni.susp.sustainability.allcosts.reduction_properties.
+Require Import rt.model.schedule.uni.transformation.construction.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+(* In this file, we use the reduction we derived to show the weak sustainability with
+ job costs and varying suspension times in the dynamic suspension model. *)
+Module SustainabilityAllCostsProperty.
+
+ Import ScheduleWithSuspensions Suspension Priority SuspensionIntervals
+ PlatformWithSuspensions ResponseTime Sustainability
+ ValidSuspensionAwareSchedule.
+
+ Module reduction := SustainabilityAllCosts.
+ Module reduction_prop := SustainabilityAllCostsProperties.
+
+ Section SustainabilityProperty.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+
+ (** Defining the task model *)
+
+ Variable higher_eq_priority: JLDP_policy Job.
+ Hypothesis H_priority_reflexive: JLDP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_transitive: JLDP_is_transitive higher_eq_priority.
+
+ Variable job_task: Job -> Task.
+ Variable task_suspension_bound: Task -> duration.
+
+ (* First, we state all properties about suspension, ... *)
+ Let satisfies_suspension_properties (params: seq (job_parameter Job)) :=
+ dynamic_suspension_model (return_param JOB_COST params) job_task
+ (return_param JOB_SUSPENSION params) task_suspension_bound.
+
+ (* ...all properties of the schedule, ... *)
+ Let satisfies_schedule_properties (params: seq (job_parameter Job)) (arr_seq: arrival_sequence Job)
+ (sched: schedule Job) :=
+ let job_arrival := return_param JOB_ARRIVAL params in
+ let job_cost := return_param JOB_COST params in
+ let job_suspension_duration := return_param JOB_SUSPENSION params in
+ jobs_come_from_arrival_sequence sched arr_seq /\
+ jobs_must_arrive_to_execute job_arrival sched /\
+ completed_jobs_dont_execute job_cost sched /\
+ work_conserving job_arrival job_cost job_suspension_duration arr_seq sched /\
+ respects_JLDP_policy job_arrival job_cost job_suspension_duration arr_seq
+ sched higher_eq_priority /\
+ respects_self_suspensions job_arrival job_cost job_suspension_duration sched.
+
+ (* ...and all properties of the arrival sequence. *)
+ Let satisfies_arrival_sequence_properties (params: seq (job_parameter Job))
+ (arr_seq: arrival_sequence Job) :=
+ arrival_times_are_consistent (return_param JOB_ARRIVAL params) arr_seq /\
+ JLDP_is_total arr_seq higher_eq_priority.
+
+ (* Then, we define the task model as the combination of such properties. *)
+ Let belongs_to_task_model (params: seq (job_parameter Job))
+ (arr_seq: arrival_sequence Job) (sched: schedule Job) :=
+ satisfies_arrival_sequence_properties params arr_seq /\
+ satisfies_schedule_properties params arr_seq sched /\
+ satisfies_suspension_properties params.
+
+ (** Sustainability Claim *)
+
+ (* We use as schedulability property the notion of response-time bound, i.e., we are
+ going to show that improving job parameters leads to "no worse response times". *)
+ Variable R: time.
+ Let response_time_bounded_by_R (params: seq (job_parameter Job)) (sched: schedule Job) (j: Job) :=
+ is_response_time_bound_of_job (return_param JOB_ARRIVAL params)
+ (return_param JOB_COST params) sched j R.
+
+ (* Next, we recall the definition of weakly-sustainable policy with job costs
+ and varying suspension times... *)
+ Let all_params := [:: JOB_ARRIVAL; JOB_COST; JOB_SUSPENSION].
+ Let sustainable_param := JOB_COST.
+ Let variable_params := [:: JOB_SUSPENSION].
+ Let has_better_sustainable_param (cost cost': Job -> time) := forall j, cost j >= cost' j.
+
+ Let weakly_sustainable_with_job_costs_and_variable_suspension_times :=
+ weakly_sustainable all_params response_time_bounded_by_R belongs_to_task_model
+ sustainable_param has_better_sustainable_param variable_params.
+
+ (* ...and prove that it holds for this scheduling policy and task model. *)
+ Theorem policy_is_weakly_sustainable:
+ weakly_sustainable_with_job_costs_and_variable_suspension_times.
+ Proof.
+ intros params good_params CONS CONS' ONLY BETTER VSCHED good_arr_seq good_sched good_j BELONGS.
+ split_conj BELONGS; split_conj BELONGS; split_conj BELONGS0; split_conj BELONGS1.
+ set job_arrival := return_param JOB_ARRIVAL good_params.
+ unfold differ_only_by in *.
+ have EQarr: job_arrival = return_param JOB_ARRIVAL params.
+ {
+ move: CONS CONS' => [UNIQ [IFF _]] [UNIQ' [IFF' _]].
+ have ARR: JOB_ARRIVAL \in labels_of params by apply IFF.
+ have ARR': JOB_ARRIVAL \in labels_of good_params by apply IFF'.
+ move: ARR ARR' => /mapP2 [p IN EQ] => /mapP2 [p' IN' EQ'].
+ symmetry in EQ; symmetry in EQ'.
+ have EQp := found_param_label params p JOB_ARRIVAL UNIQ IN EQ.
+ have EQp' := found_param_label good_params p' JOB_ARRIVAL UNIQ' IN' EQ'.
+ specialize (ONLY p p' IN IN').
+ feed_n 2 ONLY; [by rewrite EQ | by rewrite EQ |].
+ rewrite ONLY EQp' in EQp.
+ by inversion EQp.
+ }
+ set good_cost := return_param JOB_COST good_params.
+ set bad_cost := return_param JOB_COST params.
+ set good_suspension := return_param JOB_SUSPENSION good_params.
+ set bad_sched := reduction.sched_new job_arrival good_cost good_arr_seq higher_eq_priority
+ good_sched bad_cost good_j R.
+ set reduced_suspension_duration := reduction.reduced_suspension_duration job_arrival good_cost
+ good_arr_seq higher_eq_priority good_sched good_suspension bad_cost good_j R.
+ set bad_params := [:: param JOB_ARRIVAL job_arrival; param JOB_COST bad_cost;
+ param JOB_SUSPENSION reduced_suspension_duration].
+ apply reduction_prop.sched_new_response_time_of_job_j with (arr_seq := good_arr_seq)
+ (higher_eq_priority0 := higher_eq_priority) (inflated_job_cost := bad_cost);
+ try done.
+ feed (VSCHED bad_params).
+ {
+ split; first by done.
+ split; first by intros l; split;
+ move => IN; rewrite /= 2!in_cons mem_seq1 in IN;
+ move: IN => /orP [/eqP EQ | /orP [/eqP EQ | /eqP EQ]]; rewrite EQ.
+ intros l IN; move: CONS => [_ [IFF CONS]].
+ specialize (CONS l IN); apply IFF in CONS.
+ rewrite 2!in_cons mem_seq1 in CONS.
+ by move: CONS => /orP [/eqP EQ | /orP [/eqP EQ | /eqP EQ]]; rewrite EQ.
+ }
+ rewrite -/bad_sched.
+ apply VSCHED with (arr_seq := good_arr_seq).
+ {
+ intros P1 P2 IN1 IN2 EQ NOTIN; simpl in IN2.
+ move: CONS CONS' => [UNIQ _] [UNIQ' [IN' _]].
+ move: IN2 => [EQ2a | [EQ2c | [EQ2s | BUG]]]; try done; first last.
+ - by rewrite EQ -EQ2s in NOTIN.
+ - by rewrite -EQ2c; apply found_param_label; rewrite // EQ -EQ2c.
+ - by rewrite -EQ2a EQarr; apply found_param_label; rewrite // EQ -EQ2a.
+ }
+ {
+ repeat split; try (by done).
+ - by apply reduction_prop.sched_new_jobs_come_from_arrival_sequence.
+ - by apply reduction_prop.sched_new_jobs_must_arrive_to_execute.
+ - by apply reduction_prop.sched_new_completed_jobs_dont_execute.
+ - by apply reduction_prop.sched_new_work_conserving.
+ - by apply reduction_prop.sched_new_respects_policy.
+ - by apply reduction_prop.sched_new_respects_self_suspensions.
+ intros j0.
+ apply leq_trans with (n := total_suspension good_cost good_suspension j0); last by done.
+ by apply reduction_prop.sched_new_has_shorter_total_suspension.
+ }
+ Qed.
+
+ End SustainabilityProperty.
+
+End SustainabilityAllCostsProperty.
\ No newline at end of file
diff --git a/analysis/uni/susp/sustainability/allcosts/reduction_properties.v b/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
index 506e5b834048149933c88160215fb9691cb10fc9..068b2e0dd9e7cd8a6f9ba992b5549b1d6f9206ea 100644
--- a/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
+++ b/analysis/uni/susp/sustainability/allcosts/reduction_properties.v
@@ -24,7 +24,6 @@ Module SustainabilityAllCostsProperties.
Section ReductionProperties.
- Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
@@ -638,9 +637,9 @@ Module SustainabilityAllCostsProperties.
Let cumulative_suspension_in_sched_new :=
cumulative_suspension job_arrival inflated_job_cost reduced_suspension_duration sched_new.
- (* To conclude, we prove that the suspension durations in the new schedule are no
- longer than in the original schedule. *)
- Lemma sched_new_has_shorter_suspensions:
+ (* To conclude, we prove that the cumulative suspension in the new schedule is no
+ larger than in the original schedule,... *)
+ Lemma sched_new_has_shorter_suspension:
forall any_j t,
cumulative_suspension_in_sched_new any_j t
<= cumulative_suspension_in_sched_susp any_j t.
@@ -665,6 +664,65 @@ Module SustainabilityAllCostsProperties.
}
Qed.
+ (* ... which implies that the total suspension is also no larger. *)
+ Corollary sched_new_has_shorter_total_suspension:
+ forall any_j,
+ total_suspension inflated_job_cost reduced_suspension_duration any_j <=
+ total_suspension job_cost job_suspension_duration any_j.
+ Proof.
+ intros any_j.
+ apply leq_trans with (n := cumulative_suspension_in_sched_new any_j (arr_j + R)).
+ {
+ unfold total_suspension, reduced_suspension_duration, reduction.reduced_suspension_duration,
+ build_suspension_duration.
+ rewrite -/sched_new.
+ set SUSP_new := _ job_arrival job_cost _ _ _ _ _ _ _.
+ set cost' := inflated_job_cost.
+ set arr := job_arrival j.
+ apply leq_trans with (n := \sum_(0 <= t < cost' any_j) \sum_(0 <= t0 < arr + R)
+ if (service sched_new any_j t0 == t) then SUSP_new any_j t0 else false);
+ first by apply leq_sum; ins; rewrite big_mkcond; apply leq_sum; ins; case: (_ == _).
+ rewrite exchange_big /=.
+ apply leq_sum_nat; move => i /= LT _.
+ case COMP: (completed_in_sched_new any_j i).
+ {
+ apply leq_trans with (n := 0); last by done.
+ rewrite big_nat_cond big1 //; move => s /= LTs.
+ case EQ: (_ == _); last by done.
+ move: EQ => /eqP EQ; rewrite andbT -EQ {EQ} in LTs.
+ by move: COMP => /eqP COMP; rewrite ltn_neqAle COMP eq_refl in LTs.
+ }
+ {
+ apply negbT in COMP; rewrite /completed_in_sched_new /completed_by in COMP.
+ set s := service sched_new any_j i; rewrite -/s neq_ltn in COMP.
+ move: COMP => /orP [LTs | GTs]; last first.
+ {
+ suff BUG': inflated_job_cost any_j >= s by rewrite ltnNge BUG' in GTs.
+ apply cumulative_service_le_job_cost.
+ by apply sched_new_completed_jobs_dont_execute.
+ }
+ rewrite -> big_cat_nat with (n := s); [simpl | by done | by apply ltnW].
+ rewrite -> big_cat_nat with (m := s) (n := s.+1); [simpl | by done | by done].
+ rewrite big_nat_cond big1; last first.
+ {
+ move => i0; rewrite andbT; move => /= LT0.
+ by case EQ: (_ == _) => //; move: EQ => /eqP EQ; subst; rewrite ltnn in LT0.
+ }
+ rewrite add0n big_nat_recr //= eq_refl big_geq // add0n.
+ rewrite big_nat_cond big1; [rewrite addn0 |]; last first.
+ {
+ move => i0; rewrite andbT; move => /andP [LT0 _].
+ rewrite ltn_neqAle in LT0; move: LT0 => /andP [NEQ _].
+ by apply negbTE in NEQ; rewrite NEQ.
+ }
+ by rewrite -sched_new_suspension_matches.
+ }
+ }
+ apply leq_trans with (n := cumulative_suspension_in_sched_susp any_j (arr_j + R));
+ first by apply sched_new_has_shorter_suspension.
+ by apply cumulative_suspension_le_total_suspension.
+ Qed.
+
End SuspensionTable.
(** Suspension-Related Schedule Properties *)
diff --git a/model/schedule/uni/sustainability.v b/model/schedule/uni/sustainability.v
new file mode 100644
index 0000000000000000000000000000000000000000..fe76fa4c7f7dbfa0f0ac2f1b99c3ccb34d131f75
--- /dev/null
+++ b/model/schedule/uni/sustainability.v
@@ -0,0 +1,359 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.arrival_sequence
+ rt.model.schedule.uni.schedule
+ rt.model.schedule.uni.schedulability.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module Sustainability.
+
+ Import ArrivalSequence UniprocessorSchedule Schedulability.
+
+ Section SustainabilityDefs.
+
+ (* Consider any job type. *)
+ Context {Job: eqType}.
+
+ Section DefiningParameters.
+
+ (** Defining Parameter Type *)
+ Section ParameterType.
+
+ (* We begin by defining the set of possible parameter labels, ... *)
+ Inductive parameter_label :=
+ | JOB_ARRIVAL
+ | JOB_COST
+ | JOB_DEADLINE
+ | JOB_JITTER
+ | JOB_SUSPENSION.
+
+ (* ...which can be compared with the built-in decidable equality. *)
+ 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.
+
+ (* Next, we associate to each label a type of function over jobs. *)
+ 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.
+
+ (* For each function type, we also define a default value to simplify lookups. *)
+ 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.
+
+ (* Finally, we define a job parameter as a pair containing a label and a function. *)
+ Record job_parameter := param
+ {
+ p_label : parameter_label;
+ p_function : type_of_label p_label
+ }.
+
+ (* With the definitions above, we can declare parameter lists as follows. *)
+ 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.
+
+ (* By comparing labels, we define a function that finds a parameter in a list. *)
+ 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).
+
+ (* Next, we define a function that converts a given parameter p to the
+ type of label l, given a proof EQ that the labels are the same. *)
+ 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.
+
+ (* This allows returning the function of (type_of_label l) from a parameter p.
+ (If the label of p is not l, we return a dummy default value instead.) *)
+ 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).
+
+ (* To conclude, we define a function that returns the function with label l from a parameter list. *)
+ Definition return_param (l: parameter_label) (s: seq job_parameter) : type_of_label l :=
+ get_param_function l (find_param l s).
+
+ (* To illustrate how these functions work, consider this simple parameter list. *)
+ 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].
+
+ (* In that case, JOB_COST returns the function example_job_cost, ...*)
+ Example return_param_works1:
+ return_param JOB_COST example_params = example_job_cost.
+ Proof. by done. Qed.
+
+ (* ...and JOB_SUSPENSION_DURATION returns the function example_job_suspension. *)
+ 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.
+
+ (* Given a set of labels, we define whether two parameter lists differ only
+ by the parameters with those labels.
+ Note: This predicate assumes that both lists have similar, unique labels. *)
+ Definition differ_only_by (variable_labels: seq parameter_label) (s1 s2: seq job_parameter) :=
+ forall (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'.
+
+ (* Next, we define a function that returns the labels of a parameter list. *)
+ Definition labels_of (params: seq job_parameter) := [seq p_label p | p <- params].
+
+ (* Next, we define whether a parameter list has unique labels. *)
+ Definition has_unique_labels (params: seq job_parameter) := uniq (labels_of params).
+
+ (* We also define whether a parameter list corresponds to a given set of labels. *)
+ Definition corresponding_labels (params: seq job_parameter) (labels: seq parameter_label) :=
+ forall l, l \in labels_of params <-> l \in labels.
+
+ (* Finally, we prove that in any list of unique parameters, return_param always
+ returns the corresponding parameter. *)
+ Lemma found_param_label:
+ forall (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; exists p.
+ }
+ Qed.
+
+ End Properties.
+
+ End DefiningParameters.
+
+ (** Definition of sustainability for scheduling policies. *)
+ Section SustainabilityPolicy.
+
+ (* First, we define the set of possible labels for the job parameters. *)
+ Variable all_labels: seq parameter_label.
+
+ (* Next, let's consider any good schedulability property of a job, such as
+ "no deadline miss" or "response time bounded by R".
+ Given a sequence of job parameters, a schedule and a job j in this schedule,
+ the predicate indicates whether j satisfies the schedulability property. *)
+ Variable is_schedulable:
+ seq job_parameter -> schedule Job -> Job -> bool.
+
+ (* Also, consider any predicate that, given a parameter list, states whether the arrival
+ sequence and schedule belong to a certain task model. *)
+ Variable belongs_to_task_model:
+ seq job_parameter -> arrival_sequence Job -> schedule Job -> Prop.
+
+ (* Let sustainable_param denote the label of the parameter for which we claim sustainability. *)
+ Variable sustainable_param: parameter_label.
+
+ (* Let better_params denote any total order relation over the old and new values of the
+ sustainable parameter, i.e., it indicates: "the second parameter is better than the first".
+ For example, in many task models, lower job costs lead to better schedules, so a valid
+ predicate would be: (fun job_cost job_cost' => forall j, job_cost j >= job_cost' j). *)
+ Variable has_better_params: (type_of_label sustainable_param) ->
+ (type_of_label sustainable_param) -> Prop.
+
+ (* Next, we define whether the sustainable parameter becomes better when moving from list
+ params to params'. *)
+ 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.
+
+ (* Let variable_params denote the set of parameters that are allowed to vary. *)
+ Variable variable_params: seq parameter_label.
+
+ (* Now we define whether both the sustainable and the variable parameters belong to a parameter list. *)
+ Definition sustainable_and_varying_params_in (params: seq job_parameter) :=
+ forall label,
+ label \in sustainable_param :: variable_params ->
+ label \in labels_of params.
+
+ (* Next, we define whether a parameter list has consistent labels. Since
+ we'll have to quantify over many parameter lists, this prevents issues
+ with empty/invalid parameter lists. *)
+ Definition has_consistent_labels (params: seq job_parameter) :=
+ has_unique_labels params /\
+ corresponding_labels params all_labels /\
+ sustainable_and_varying_params_in params.
+
+ (* Next, we define whether all jobs sets with given params are schedulable... *)
+ Definition jobs_are_schedulable_with (params: seq job_parameter) :=
+ forall arr_seq sched j,
+ belongs_to_task_model params arr_seq sched ->
+ is_schedulable params sched j.
+
+ (* ...and also define whether the job sets that only differ from the given params
+ by the 'set of variable parameters' are all schedulable. *)
+ Definition jobs_are_V_schedulable_with (params: seq job_parameter) :=
+ forall (similar_params: seq job_parameter),
+ has_consistent_labels similar_params ->
+ differ_only_by variable_params params similar_params ->
+ jobs_are_schedulable_with similar_params.
+
+ (* Then, we say that the scheduling policy is weakly-sustainable with sustainable_param
+ and variable_params iff the following holds:
+ if jobs are V-schedulable with the original parameters, then they are also
+ schedulable with better parameters (according to the has_better_params relation). *)
+ Definition weakly_sustainable :=
+ forall (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.
+
+ (* Next, using the contrapositive of weakly_sustainable, we provide
+ an alternative definition of weak sustainability. *)
+ Section AlternativeDefinition.
+
+ (* First, let's define whether the sustainable parameter becomes
+ worse when switching from params to params'. *)
+ 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.
+
+ (* Next, we define whether jobs are not schedulable with a given set of parameters. *)
+ Definition jobs_are_not_schedulable_with (params: seq job_parameter) :=
+ exists arr_seq sched j,
+ belongs_to_task_model params arr_seq sched /\
+ ~~ is_schedulable params sched j.
+
+ (* Based on that, we formalize the alternative definition of weakly sustainable. *)
+ Definition weakly_sustainable_contrapositive :=
+ forall 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 ->
+ exists params_worse',
+ has_consistent_labels params_worse' /\
+ differ_only_by variable_params params_worse params_worse' /\
+ jobs_are_not_schedulable_with params_worse'.
+
+ (* Assume De Morgan's law for propositional and predicate logic. *)
+ Hypothesis H_classical_forall_exists:
+ forall (T: Type) (P: T -> Prop),
+ ~ (forall x, ~ P x) -> exists x, P x.
+ Hypothesis H_classical_and_or:
+ forall (P Q: Prop), ~ (P /\ Q) -> ~ P \/ ~ Q.
+
+ (* Then, we can prove the equivalence of the two definitions. *)
+ 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; exists 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 exists 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.
+
+ (* Also, we say that the scheduling policy is strongly-sustainable
+ with sustainable_param iff it is weakly-sustainable with
+ sustainable_param and the set of variable parameters is empty. *)
+ Definition strongly_sustainable := weakly_sustainable [::].
+
+ End SustainabilityPolicy.
+
+ End SustainabilityDefs.
+
+ Global Arguments job_parameter: clear implicits.
+
+End Sustainability.
\ No newline at end of file
diff --git a/model/suspension.v b/model/suspension.v
index 88c142b3f8c363429ce5510180e960c3138bbd78..cce479f9d3f943fa8ef242a7f0df50748838fa9b 100644
--- a/model/suspension.v
+++ b/model/suspension.v
@@ -15,9 +15,9 @@ Module Suspension.
(* We define job suspension as a function that takes a job in the arrival
sequence and its current service and returns how long the job must
suspend next. *)
- Definition job_suspension := Job -> (* job *)
- time -> (* current service *)
- time. (* duration of next suspension *)
+ Definition job_suspension := Job -> (* job *)
+ time -> (* current service *)
+ duration. (* duration of next suspension *)
End SuspensionTimes.
@@ -25,7 +25,7 @@ Module Suspension.
Section TotalSuspensionTime.
Context {Job: eqType}.
- Variable job_cost: Job -> time.
+ Variable job_cost: Job -> time.
(* Consider any job suspension function. *)
Variable next_suspension: job_suspension Job.
@@ -56,7 +56,7 @@ Module Suspension.
Let total_job_suspension := total_suspension job_cost next_suspension.
(* Next, assume that for each task a suspension bound is known. *)
- Variable suspension_bound: Task -> time.
+ Variable suspension_bound: Task -> duration.
(* Then, we say that the arrival sequence satisfies the dynamic
suspension model iff the total suspension time of each job is no