diff --git a/BertognaResponseTimeDefs.v b/BertognaResponseTimeDefs.v
index d1f1a8ea5bddbda4ab101a04c39af0e39397da30..7b2b26fa1708f731a06958bae68654257d4b8ff2 100644
--- a/BertognaResponseTimeDefs.v
+++ b/BertognaResponseTimeDefs.v
@@ -905,11 +905,11 @@ Module ResponseTimeAnalysis.
Section Proof.
- (* Assume that higher_eq_priority is an order relation. *)
+ (* Assume that higher_eq_priority is a total order over the task set. *)
Hypothesis H_reflexive: reflexive higher_eq_priority.
Hypothesis H_transitive: transitive higher_eq_priority.
- Hypothesis H_unique_priorities:
- antisymmetric_over_seq higher_eq_priority ts.
+ Hypothesis H_unique_priorities: antisymmetric higher_eq_priority.
+ Hypothesis H_total: total higher_eq_priority.
(* Assume the task set has no duplicates, ... *)
Hypothesis H_ts_is_a_set: uniq ts.
@@ -1115,7 +1115,9 @@ Module ResponseTimeAnalysis.
H_global_scheduling_invariant into INVARIANT,
H_valid_policy into VALIDhp,
H_sorted_ts into SORT,
+ H_transitive into TRANS,
H_unique_priorities into UNIQ,
+ H_total into TOTAL,
H_all_jobs_from_taskset into ALLJOBS,
H_test_passes into TEST.
@@ -1124,15 +1126,49 @@ Module ResponseTimeAnalysis.
move: TEST => /eqP TEST.
unfold R_list in TEST.
- clear SORT ALLJOBS H_reflexive UNIQ H_ts_is_a_set.
+ clear ALLJOBS H_reflexive H_ts_is_a_set.
have CONV := rt_rec_converges.
+
+ (*generalize dependent j.
+ generalize dependent tsk.
+ destruct ts as [| tsk0 hp_tasks]; first by intro t; rewrite in_nil.
+ desf; rename l into hp_bounds.
+
+ set R0 := per_task_rta tsk0 hp_bounds (max_steps tsk0).
+
+ assert (INbounds: forall hp_tsk,
+ hp_tsk \in ts ->
+ exists R_tsk,
+ (hp_tsk, R_tsk) \in R_list).
+ {
+ admit.
+ }
+
+ cut (
+ forall (hp_tsk : task_eqType) (R : nat_eqType),
+ (hp_tsk, R) \in (tsk0, R0) :: hp_bounds ->
+ forall j : JobIn arr_seq,
+ job_task j = hp_tsk ->
+ service rate sched j (job_arrival j + job_deadline j ) == job_cost j).
+ {
+ intros CUT; ins.
+ specialize (INbounds tsk INtsk); des.
+ by apply (CUT tsk R_tsk INbounds).
+ }
+
+ induction hp_bounds as [| (tsk_i, R_i) hp_tasks'].
+ {
+ (* Base case: lowest-priority task. *)
+ intros hp_tsk R; rewrite mem_seq1; move/eqP => EQ j JOBj.
+
+ }*)
+
generalize dependent j.
generalize dependent tsk.
induction ts as [| tsk_i hp_tasks].
{
- (* Base case: empty taskset. *)
by intros tsk; rewrite in_nil.
}
{
@@ -1140,13 +1176,25 @@ Module ResponseTimeAnalysis.
intros tsk INtsk; rewrite in_cons in INtsk.
move: INtsk => /orP INtsk; des; last first.
{
- desf; apply IHhp_tasks; last by ins.
+ desf; apply IHhp_tasks; try (by ins).
by red; ins; apply TASKPARAMS; rewrite in_cons; apply/orP; right.
by ins; apply RESTR; rewrite in_cons; apply/orP; right.
- ins. simpl in INVARIANT. apply INVARIANT. rewrite count_cons. capply INVARIANT. ins; exploit (TASKPARAMS tsk0); [ by rewrite in_cons; apply/orP; right | ins; des]. ins. apply TASKPARAMS. admit.
- admit.
- admit.
- admit.
+ {
+ intros tsk0 j t HP0 JOB0 BACK0.
+ ins; exploit (INVARIANT tsk0 j t); try (by ins);
+ [by rewrite in_cons; apply/orP; right | intro INV].
+ assert (NOINTERF: is_interfering_task_fp tsk0 higher_eq_priority tsk_i = false).
+ {
+ apply negbTE; rewrite negb_and; apply/orP; left.
+ move: SORT => SORT.
+ apply order_path_min in SORT;
+ first by move: SORT => /allP SORT; specialize (SORT tsk0 HP0).
+ by apply comp_relation_trans.
+ }
+ by rewrite NOINTERF andFb add0n in INV.
+ }
+ by simpl in SORT; apply path_sorted in SORT.
+ by ins; apply CONV; ins; rewrite in_cons; apply/orP; right.
}
move: INtsk => /eqP INtsk; subst tsk.
diff --git a/helper.v b/helper.v
index 26dea3d7697114b1a44205b2f82b299f46a6b968..4b02ae81632f3585e802d2836b6331146b2f02c5 100644
--- a/helper.v
+++ b/helper.v
@@ -425,6 +425,10 @@ Proof.
}
Qed.
+Definition total_over_seq {T: eqType} (leT: rel T) (s: seq T) :=
+ forall x y (INx: x \in s) (INy: y \in s),
+ leT x y \/ leT y x.
+
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),
@@ -513,6 +517,35 @@ Definition comp_relation {T} (R: rel T) : rel T :=
Definition reverse_sorted {T: eqType} (R: rel T) (s: seq T) :=
sorted (comp_relation R) s.
+Lemma revert_comp_relation:
+ forall {T: eqType} (R: rel T)
+ (ANTI: antisymmetric R)
+ (TOTAL: total R)
+ x y (DIFF: x != y),
+ ~~ R x y = R y x.
+Proof.
+ unfold comp_relation, antisymmetric, total.
+ ins; specialize (ANTI x y).
+ destruct (R x y) eqn:Rxy, (R y x) eqn:Ryx; try (by ins).
+ by exploit ANTI; ins; subst x; rewrite eq_refl in DIFF.
+ by specialize (TOTAL x y); move: TOTAL => /orP TOTAL; des; rewrite ?Rxy ?Ryx in TOTAL.
+Qed.
+
+Lemma comp_relation_trans:
+ forall {T: eqType} (R: rel T)
+ (ANTI: antisymmetric R)
+ (TOTAL: total R)
+ (TRANS: transitive R),
+ transitive (comp_relation R).
+Proof.
+ unfold comp_relation; ins; red; intros y x z XY YZ.
+ unfold transitive, total in *.
+ destruct (R x y) eqn:Rxy, (R y x) eqn:Ryx, (R x z) eqn:Rxz; try (by ins).
+ by apply TRANS with (x := y) in Rxz; [by rewrite Rxz in YZ | by ins].
+ by destruct (orP (TOTAL x y)) as [XY' | YX'];
+ [by rewrite Rxy in XY' | by rewrite Ryx in YX'].
+Qed.
+
Lemma leq_sum_subseq :
forall {I: eqType} r1 r2 (P : pred I) F
(SUB: subseq r1 r2),