From 948de74b59516ae39763da4c06c93de6a8d45bfb Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Wed, 30 Sep 2015 17:31:20 +0200
Subject: [PATCH] Latest changes
---
BertognaResponseTimeDefs.v | 169 ++++++++++++++++++++++++-------------
WorkloadDefs.v | 2 +-
helper.v | 158 ++++++++++++++++++++++++++--------
3 files changed, 233 insertions(+), 96 deletions(-)
diff --git a/BertognaResponseTimeDefs.v b/BertognaResponseTimeDefs.v
index a616752ed..99fbf2cdf 100644
--- a/BertognaResponseTimeDefs.v
+++ b/BertognaResponseTimeDefs.v
@@ -781,22 +781,27 @@ Module ResponseTimeAnalysis.
Definition max_steps (tsk: task_in_ts) :=
task_deadline tsk + 1.
+ Definition ext_tuple_to_fun_index {idx: task_in_ts} (hp: idx.-tuple nat) : task_in_ts -> nat.
+ intros tsk; destruct (tsk < idx) eqn:LT.
+ by apply (tnth hp (Ordinal LT)).
+ by apply 0.
+ Defined.
+
(* Given a vector of size 'idx' containing known response-time bounds
for the higher-priority tasks, we compute the response-time
bound of task 'idx' using a fixed-point iteration as follows. *)
- Definition rt_rec (tsk_i: task_in_ts)
- (R_prev: tsk_i.-tuple nat) (step: nat) :=
- iter step (fun t => task_cost tsk_i +
+ Definition rt_rec (idx: task_in_ts)
+ (R_prev: idx.-tuple nat) (step: nat) :=
+ iter step (fun t => task_cost idx +
div_floor
- (total_interference_bound_fp ts tsk_i
- (fun tsk: task_in_ts => task_deadline tsk) (* CHANGE TO R_prev!*)
- t higher_eq_priority)
+ (total_interference_bound_fp ts idx
+ (ext_tuple_to_fun_index R_prev)
+ t higher_eq_priority)
num_cpus)
- (task_cost tsk_i).
+ (task_cost idx).
(* We return a vector of size 'idx' containing the response-time
- bound of the higher-priority tasks 0...idx-1 using the
- recursion rt_rec that we just defined. *)
+ bound of the higher-priority tasks 0...idx-1 using rt_rec *)
Definition R_hp (idx: task_in_ts) : idx.-tuple nat :=
match idx with
| Ordinal k Hk =>
@@ -807,14 +812,14 @@ Module ResponseTimeAnalysis.
| S k => fun Hk =>
[tuple of rcons
(f k (ltSnm k _ Hk))
- (rt_rec (Ordinal Hk)
- (f (S k) Hk )
+ (rt_rec (Ordinal _)
+ (f k (ltSnm k _ Hk))
(max_steps (Ordinal Hk)) )]
end) k Hk
end.
- (* Then, the response-time bound R of a task idx is
- obtained by calling rt_rec with the vector of R of the
+ (* The response-time bound R of a task idx is computed
+ by calling rt_rec with the vector R_hp of the
higher-priority tasks. *)
Definition R (idx: task_in_ts) :=
rt_rec idx (R_hp idx) (max_steps idx).
@@ -868,41 +873,42 @@ Module ResponseTimeAnalysis.
Definition no_deadline_missed_by (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task
rate sched tsk.
-
+
Theorem R_converges:
forall (tsk: task_in_ts),
R tsk <= task_deadline tsk ->
R tsk = task_cost tsk +
div_floor
(total_interference_bound_fp ts tsk
- (fun tsk: task_in_ts => task_deadline tsk) (* FIX! *)
+ R
(R tsk) higher_eq_priority)
num_cpus.
Proof.
+ unfold valid_sporadic_taskset, valid_sporadic_task in *.
+ rename H_valid_task_parameters into TASKPARAMS.
rename H_sorted_ts into SORT; move: SORT => SORT.
intros tsk LE.
- unfold R, max_steps, rt_rec in *.
+ unfold R in *; unfold max_steps, rt_rec in *.
set RHS := (fun t : time =>
task_cost tsk +
div_floor
(total_interference_bound_fp ts tsk
- (fun tsk0 : task_in_ts => task_deadline tsk0) t
+ (ext_tuple_to_fun_index (R_hp tsk)) t
higher_eq_priority)
num_cpus).
fold RHS in LE; rewrite -> addn1 in *.
- set R := fun t => iter t RHS (task_cost tsk).
- fold (R (task_deadline tsk).+1).
- fold (R (task_deadline tsk).+1) in LE.
-
- assert (NEXT: task_cost tsk +
+ set R' := fun t => iter t RHS (task_cost tsk).
+ fold (R' (task_deadline tsk).+1).
+ fold (R' (task_deadline tsk).+1) in LE.
+ Admitted.
+ (*assert (NEXT: task_cost tsk +
div_floor
- (total_interference_bound_fp ts tsk
- (fun tsk0: task_in_ts => task_deadline tsk0)
- (R (task_deadline tsk).+1) higher_eq_priority)
+ (total_interference_bound_fp ts tsk R
+ (R' (task_deadline tsk).+1) higher_eq_priority)
num_cpus =
- R (task_deadline tsk).+2);
- first by unfold R; rewrite [iter _.+2 _ _]iterS.
+ R' (task_deadline tsk).+2).
+ unfold R'. first by unfold R'; rewrite [iter _.+2 _ _]iterS.
rewrite NEXT; clear NEXT.
assert (MON: forall x1 x2, x1 <= x2 -> RHS x1 <= RHS x2).
@@ -915,7 +921,10 @@ Module ResponseTimeAnalysis.
rewrite leq_min; apply/andP; split.
{
apply leq_trans with (n := W i (task_deadline i) x1);
- [by apply geq_minl | by apply W_monotonic, LEx].
+ first by apply geq_minl.
+ exploit (TASKPARAMS (nth_task i));
+ [by rewrite mem_nth | intro PARAMS; des].
+ by apply W_monotonic.
}
{
apply leq_trans with (n := x1 - task_cost tsk + 1);
@@ -950,37 +959,79 @@ Module ResponseTimeAnalysis.
apply IHn; intros k.
by apply (GROWS (widen_ord (leqnSn n) k)).
}
- apply leq_ltn_trans with (m := R (task_deadline tsk).+1) in BY1; last by ins.
- by rewrite ltnn in BY1.
- Qed.
-
- (*Lemma taskP :
- forall (ts: sporadic_taskset) (P: sporadic_task -> Prop),
- (forall (tsk: task_in_ts), P (nth_task tsk)) <->
- (forall (tsk: sporadic_task), (tsk \in ts) -> P tsk).*)
-
- Theorem taskset_schedulable_by_fp_rta :
- forall (tsk: task_in_ts), no_deadline_missed_by tsk.
- Proof.
- unfold no_deadline_missed_by, task_misses_no_deadline,
- job_misses_no_deadline, completed,
- valid_sporadic_job in *.
- rename H_valid_job_parameters into JOBPARAMS,
- H_valid_task_parameters into TASKPARAMS,
- H_restricted_deadlines into RESTR,
- H_completed_jobs_dont_execute into COMP,
- H_jobs_must_arrive_to_execute into MUSTARRIVE,
- H_global_scheduling_invariant into INVARIANT,
- H_valid_policy into VALIDhp,
- H_taskset_not_empty into NONEMPTY,
- H_sorted_ts into SORT,
- H_unique_priorities into UNIQ,
- H_all_jobs_from_taskset into ALLJOBS.
-
- rewrite -(size_sort higher_eq_priority) in NONEMPTY.
- unfold task_in_ts.
-
- destruct tsk.
+ apply leq_ltn_trans with (m := R (task_deadline tsk).+1) in BY1;
+ [by rewrite ltnn in BY1 | by ins].
+ Qed.*)
+
+ Theorem taskset_schedulable_by_fp_rta :
+ forall (tsk: task_in_ts), no_deadline_missed_by tsk.
+ Proof.
+ unfold no_deadline_missed_by, task_misses_no_deadline,
+ job_misses_no_deadline, completed,
+ fp_schedulability_test,
+ valid_sporadic_job in *.
+ rename H_valid_job_parameters into JOBPARAMS,
+ H_valid_task_parameters into TASKPARAMS,
+ H_restricted_deadlines into RESTR,
+ H_completed_jobs_dont_execute into COMP,
+ H_jobs_must_arrive_to_execute into MUSTARRIVE,
+ H_global_scheduling_invariant into INVARIANT,
+ H_valid_policy into VALIDhp,
+ H_taskset_not_empty into NONEMPTY,
+ H_sorted_ts into SORT,
+ H_unique_priorities into UNIQ,
+ H_all_jobs_from_taskset into ALLJOBS,
+ H_test_passes into TEST.
+
+ rewrite -(size_sort higher_eq_priority) in NONEMPTY.
+ move: SORT TEST => SORT /allP TEST.
+ move => tsk j /eqP JOBtsk.
+
+ rewrite eqn_leq; apply/andP; split;
+ first by apply service_interval_le_cost.
+ apply leq_trans with (n := service rate sched j (job_arrival j + R tsk)); last first.
+ {
+ apply service_monotonic; rewrite leq_add2l.
+ specialize (JOBPARAMS j); des; rewrite JOBPARAMS1 JOBtsk.
+ apply TEST, mem_ord_enum.
+ }
+ rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
+ generalize dependent j.
+ destruct tsk as [tsk_i LTi].
+
+ induction tsk_i using strong_ind.
+ {
+ (* Base case: no higher-priority tasks *)
+ unfold sorted in SORT.
+ intros j JOBtsk.
+
+ set tsk0 := Ordinal (n:=size ts) (m:=0) LTi.
+ have BOUND := bertogna_cirinei_response_time_bound_fp.
+ unfold is_response_time_bound_of_task,
+ job_has_completed_by, completed in BOUND.
+ apply BOUND with (job_deadline := job_deadline) (ts := ts)
+ (job_task := job_task) (tsk := tsk0)
+ (R_other := R) (higher_eq_priority := higher_eq_priority); try ins; clear BOUND.
+ admit. (* can be proven using the definition of interference. *)
+ admit. (* tsk_other cannot exist *)
+ by apply INVARIANT with (j := j0); by ins.
+ by apply R_converges, TEST, mem_ord_enum.
+ }
+ {
+ }
+
+
+
+
+
+
+
+ induction (size ts). unfold task_in_ts in *.
+ intro tsk. induction (size ts).
+
+ unfold task_in_ts.
+
+ destruct tsk.
(*
(* Apply induction from the back. *)
elim/last_ind.
diff --git a/WorkloadDefs.v b/WorkloadDefs.v
index f5eb5b8c8..7cca8faab 100644
--- a/WorkloadDefs.v
+++ b/WorkloadDefs.v
@@ -168,7 +168,7 @@ Module Workload.
rewrite DIV leq_add2r leq_min; apply/andP; split;
first by rewrite geq_minl.
by apply leq_trans with (n := (t1 + delta + R - e) %% p);
- [by rewrite geq_minr | by apply ltnW, DIV0].
+ [by rewrite geq_minr | by rewrite -DIV0 addn1 leqnSn].
}
{
rewrite -[minn e _]add0n -addnA; apply leq_add; first by ins.
diff --git a/helper.v b/helper.v
index 739ad4e55..c328a93e7 100644
--- a/helper.v
+++ b/helper.v
@@ -1,4 +1,4 @@
-Require Import Vbase ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssromega.
+Require Import Vbase ssreflect ssrbool eqtype ssrnat seq fintype bigop tuple path div ssromega.
Section Pair.
@@ -33,6 +33,21 @@ Reserved Notation "\cat_ ( i < n ) F"
Notation "\cat_ ( i < n ) F" :=
(\big[cat/[::]]_(i < n) F%N) : nat_scope.
+Ltac des_eqrefl2 :=
+ match goal with
+ | H: context[match ?X as id return (?X = id -> _) with _ => _ end Logic.eq_refl] |- _ =>
+ let EQ := fresh "EQ" in
+ let id' := fresh "x" in
+ revert H;
+ generalize (Logic.eq_refl X); generalize X at 2 3;
+ intros id' EQ; destruct id'; intros H
+ | |- context[match ?X as id return (?X = id -> _) with _ => _ end Logic.eq_refl] =>
+ let EQ := fresh "EQ" in
+ let id' := fresh "x" in
+ generalize (Logic.eq_refl X); generalize X at 2 3;
+ intros id' EQ; destruct id'
+ end.
+
Lemma mem_bigcat_nat:
forall (T: eqType) x m n j (f: _ -> list T)
(LE: m <= j < n) (IN: x \in (f j)),
@@ -52,25 +67,14 @@ Definition fun_ord_to_nat {n} {T} (x0: T) (f: 'I_n -> T) : nat -> T.
[by apply (f (Ordinal LT)) | by apply x0].
Defined.
-(* For all x: 'I_n (i.e., x < n), the conversion preserves equality. *)
-Program Definition eq_fun_ord_to_nat :
+Lemma eq_fun_ord_to_nat :
forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
- (fun_ord_to_nat x0 f) x = f x :=
- fun n T x0 f x =>
- match ltn_ord x in eq _ b return
- (
- (if b as b' return b = b' -> T then
- fun (H : b = true) => f (@Ordinal n x ( H))
- else fun _ => x0) Logic.eq_refl = f x
- )
- -> fun_ord_to_nat x0 f x = f x
- with
- | Logic.eq_refl => _
- end (Logic.eq_refl (f x)).
-Next Obligation.
- destruct x; simpl.
- f_equal; f_equal.
- exact: bool_irrelevance.
+ (fun_ord_to_nat x0 f) x = f x.
+Proof.
+ ins; unfold fun_ord_to_nat.
+ des_eqrefl2.
+ by f_equal; apply ord_inj.
+ by destruct x; ins; rewrite i in EQ.
Qed.
Lemma eq_bigr_ord T n op idx r (P : pred 'I_n)
@@ -102,6 +106,20 @@ Proof.
[by apply/andP; split | by rewrite eq_fun_ord_to_nat].
Qed.
+Lemma strong_ind :
+ forall (P: nat -> Prop),
+ P 0 -> (forall n, (forall k, k <= n -> P k) -> P n.+1) ->
+ forall n, P n.
+Proof.
+ intros P P0 ALL; destruct n; first by apply P0.
+ apply ALL; generalize dependent n; induction n.
+ by intros k LE0; move: LE0; rewrite leqn0; move => /eqP LE0; subst k.
+ intros k LESn; destruct (ltngtP k n.+1) as [LT | GT | EQ].
+ by rewrite ltnS in LT; apply IHn.
+ by rewrite leqNgt GT in LESn.
+ by rewrite EQ; apply ALL, IHn.
+Qed.
+
Lemma exists_inP_nat t (P: nat -> bool):
reflect (exists x, x < t /\ P x) [exists (x | x \in 'I_t), P x].
Proof.
@@ -329,25 +347,93 @@ Proof.
by rewrite -divn_eq addn1.
}
{
- (* Case 2: y < d - 1 *)
- rewrite -(ltn_add2r 1) in LTN.
- rewrite subh1 in LTN; last by apply GT0.
- rewrite -addnBA // subnn addn0 in LTN.
- generalize LTN; apply modn_small in LTN; intro LTN'.
- generalize LTN'; apply divn_small in LTN'; intro LTN''.
- split.
+ assert (EQDIV: n %/ d = n.+1 %/ d).
{
- unfold x; apply/eqP.
- cut ((d == 0) || (n %/ d * d == n.+1 %/ d * d)).
- intros OR; des; first by move: OR => /eqP OR; rewrite OR ltn0 in GT1.
- rewrite eqn_mul2r in OR; des; last by apply OR.
- by move: OR => /eqP OR; rewrite OR ltn0 in GT1.
- apply/orP; right.
- rewrite -(eqn_add2l n.+1).
- admit.
+ apply/eqP; rewrite eqn_leq; apply/andP; split;
+ first by apply leq_div2r, leqnSn.
+ rewrite leq_divRL; last by apply GT0.
+ rewrite -ltnS {2}(divn_eq n.+1 d).
+ rewrite -{1}[_ %/ d * d]addn0 ltn_add2l.
+ unfold y in *.
+ rewrite ltnNge; apply/negP; unfold not; intro BUG.
+ rewrite leqn0 in BUG; move: BUG => /eqP BUG.
+ rewrite -(modnn d) -addn1 in BUG.
+ destruct d; first by rewrite sub0n in LTN.
+ move: BUG; move/eqP; rewrite -[d.+1]addn1 eqn_modDr [d+1]addn1; move => /eqP BUG.
+ rewrite BUG -[d.+1]addn1 -addnBA // subnn addn0 in LTN.
+ by rewrite modn_small in LTN;
+ [by rewrite ltnn in LTN | by rewrite addn1 ltnSn].
}
+ (* Case 2: y < d - 1 *)
+ split; first by rewrite -EQDIV.
{
- admit.
+ unfold x, y in *.
+ rewrite -2!subndiv_eq_mod.
+ rewrite subh1 ?addn1; last by apply leq_trunc_div.
+ rewrite EQDIV; apply/eqP.
+ rewrite -(eqn_add2r (n%/d*d)).
+ by rewrite subh1; last by apply leq_trunc_div.
}
}
-Qed.
\ No newline at end of file
+Qed.
+
+Definition antisymmetric_over_seq {T: eqType} (leT: rel T) (s: seq T) :=
+ forall x y (INx: x \in s) (INy: y \in s)
+ (LEx: leT x y) (LEy: leT y x),
+ x = y.
+
+Lemma sorted_by_index :
+ forall {T: eqType} (s: seq T) (leT: rel T)
+ (SORT: sorted leT s) (ANTI: antisymmetric_over_seq leT s)
+ (i1 i2: 'I_(size s)) (LE: i1 < i2),
+ leT (tnth (in_tuple s) i1) (tnth (in_tuple s) i2).
+Proof.
+ intros.
+ destruct s.
+ destruct i1 as [i1 LT1].
+ by remember i1 as i1'; have BUG := LT1; rewrite Heqi1' ltn0 in BUG.
+ destruct i1.
+ induction m. simpl.
+Admitted.
+
+
+(*Program Definition fun_ord_to_nat2 {n} {T} (x0: T) (f: 'I_n -> T)
+ (x : nat) : T :=
+ match (x < n) with
+ true => (f _)
+ | false => x0
+ end.
+Next Obligation.
+ eby eapply Ordinal, Logic.eq_sym.
+Defined.
+
+Lemma eq_fun_ord_to_nat2 :
+ forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
+ (fun_ord_to_nat2 x0 f) x = f x.
+Proof.
+ ins. unfold fun_ord_to_nat2.
+ des_eqrefl.
+ by f_equal; apply ord_inj.
+ by destruct x; ins; rewrite i in EQ.
+Qed.
+
+(* For all x: 'I_n (i.e., x < n), the conversion preserves equality. *)
+Program Definition eq_fun_ord_to_nat :
+ forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
+ (fun_ord_to_nat x0 f) x = f x :=
+ fun n T x0 f x =>
+ match ltn_ord x in eq _ b return
+ (
+ (if b as b' return b = b' -> T then
+ fun (H : b = true) => f (@Ordinal n x ( H))
+ else fun _ => x0) Logic.eq_refl = f x
+ )
+ -> fun_ord_to_nat x0 f x = f x
+ with
+ | Logic.eq_refl => _
+ end (Logic.eq_refl (f x)).
+Next Obligation.
+ destruct x; simpl.
+ f_equal; f_equal.
+ exact: bool_irrelevance.
+Qed.*)
--
GitLab