Commit 258edf49 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Formalization of Weakly Sustainable Policy

1) Formalize the notion of weakly sustainable policy, along with
its contrapositive, and prove the equivalence between the two.

2) Establish weak sustainability of self-suspending tasks w.r.t.
execution times and variable suspension times, based on the
transformation we had formalized.
parent 9aa57786
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
......@@ -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 *)
......
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.
}