prove existence of abstract busy interval

Proofs of existence for busy intervals are usually quite long. They
also depend on specific scheduling policy and preemption model. This
leads to some unnecessary duplication. This commit introduces a proof
of existence for abstract busy interval. The idea is to instantiate
this proof for specific policies removing the duplication.

analysis/abstract/busy_interval.v

-Require Export prosa.analysis.definitions.job_properties.
-Require Export prosa.analysis.facts.behavior.all.
-Require Export prosa.analysis.abstract.definitions.
 Require Export prosa.analysis.abstract.iw_auxiliary.
+Require Export prosa.analysis.facts.model.workload.
 
 (** * Lemmas About Abstract Busy Intervals *)
 
@@ -48,7 +46,55 @@ Section LemmasAboutAbstractBusyInterval.
   Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
   Hypothesis H_job_cost_positive : job_cost_positive j.
 
-  (** Consider a busy interval <<[t1, t2)>> of job [j]. *)
+  (** We first prove that any interval <<[t1, t2)>> is either a busy
+      interval of job [j] or not. *)
+  Lemma busy_interval_prefix_case :
+    forall t1 t2,
+      busy_interval_prefix sched j t1 t2 \/ ~ busy_interval_prefix sched j t1 t2.
+  Proof.
+    move=> t1 t2.
+    have [JA|NAT] := boolP (t1 <= job_arrival j < t2); last first.
+    { by right; move => PREF; move: NAT => /negP NQT; apply: NQT; apply PREF. }
+    have [QT1|NQT] := boolP (quiet_time sched j t1); last first.
+    { by right; move => PREF; move: NQT => /negP NQT; apply: NQT; apply PREF. }
+    have [AQT|NQT] := boolP (all (fun t => ~~ quiet_time sched j t) (index_iota t1.+1 t2)); last first.
+    { right; move=> PREF; move: NQT => /negP NQT; apply: NQT.
+      apply/allP => t IO; apply/negP.
+      by apply PREF; move: IO; rewrite mem_index_iota.
+    }
+    left; split; [by done | split] => //.
+    move => t NEQ; apply/negP; move: AQT => /allP AQT; apply: AQT.
+    by rewrite mem_index_iota.
+  Qed.
+
+  (** Consider two intervals <<[t1, t2)>> ⊆ <<[t1, t2')>>, where
+      <<[t1, t2)>> is a busy-interval prefix and <<[t1, t2')>> is not
+      a busy-interval prefix. Then there exists [t2''] such that
+      <<[t1, t2'')>> is a busy interval. *)
+  Lemma terminating_busy_prefix_is_busy_interval :
+    forall t1 t2 t2',
+      t2 <= t2' ->
+      busy_interval_prefix sched j t1 t2 ->
+      ~ busy_interval_prefix sched j t1 t2' ->
+      exists t2'', busy_interval sched j t1 t2''.
+  Proof.
+    move=> t1 t2 t2' LE BUSY NBUSY.
+    interval_to_duration t2 t2' δ.
+    induction δ as [ | δ IHδ].
+    { by exfalso; apply: NBUSY; rewrite addn0. }
+    have [BUSY'|NBUSY'] := busy_interval_prefix_case t1 (t2 + δ); last by apply IHδ in NBUSY'.
+    clear IHδ.
+    exists (t2 + δ); split => //.
+    apply negbNE; apply/negP => FF.
+    apply:NBUSY; split; first by move: BUSY => []; lia.
+    split; first by move: BUSY => []; lia.
+    move => t; rewrite addnS ltnS [_ <= t2  + δ]leq_eqVlt.
+    move => /andP [LT1 /orP [/eqP WDFW | VB]].
+    - by subst; apply/negP.
+    - by apply BUSY'; lia.
+  Qed.
+
+  (** Next, consider a busy interval <<[t1, t2)>> of job [j]. *)
   Variable t1 t2 : instant.
   Hypothesis H_busy_interval : busy_interval sched j t1 t2.
 
@@ -158,6 +204,339 @@ Section LemmasAboutAbstractBusyInterval.
 
 End LemmasAboutAbstractBusyInterval.
 
+(** In the following section, we derive a sufficient condition for the
+    existence of abstract busy intervals for unit-service
+    processors. *)
+Section AbstractBusyIntervalExists.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider any kind of of unit-service processor model. *)
+  Context {PState : ProcessorState Job}.
+  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload ... *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** ... that do not allow speculative execution. *)
+  Hypothesis H_no_speculative_exec : no_speculative_execution.
+
+  (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arrival_sequence_is_a_set : arrival_sequence_uniq arr_seq.
+
+  (** Consider an arbitrary task [tsk]. *)
+  Variable tsk : Task.
+
+  (** Next, consider any work-conserving (in the abstract sense)
+      schedule of this arrival sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** ... where jobs do not execute before their arrival or after completion. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+
+  (** Consider an arbitrary job [j] from task [tsk] with positive cost. *)
+  Variable j : Job.
+  Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
+  Hypothesis H_job_task : job_of_task tsk j.
+  Hypothesis H_job_cost_positive : job_cost_positive j.
+
+  (** In this section, we prove a fact that allows one to extend an
+      inequality between cumulative interference and interfering
+      workload from a busy-interval prefix <<[t1, t)>> to the whole
+      timeline <<[0, t)>>. *)
+  Section CumulativeIntIntWorkExtension.
+
+    (** Consider any busy-interval prefix of job [j]. *)
+    Variable t1 t_busy : instant.
+    Hypothesis H_is_busy_prefix : busy_interval_prefix sched j t1 t_busy.+1.
+
+      (** We assume that, for some positive [δ], the cumulative
+          interfering workload within interval <<[t1, t1 + δ)>> is
+          bounded by cumulative interference in the same interval. *)
+    Variable δ : duration.
+    Hypothesis H_iw_bounded :
+      cumulative_interfering_workload j t1 (t1 + δ) <= cumulative_interference j t1 (t1 + δ).
+
+    (** Then the cumulative interfering workload within interval <<[0,
+        t1 + δ)>> is bounded by the cumulative interference in the
+        same interval. *)
+      Local Lemma cumul_iw_bounded_by_cumul_i :
+        cumulative_interfering_workload j 0 (t1 + δ) <= cumulative_interference j 0 (t1 + δ).
+      Proof.
+        move: (H_iw_bounded) => LE.
+        rewrite /definitions.cumulative_interference
+                /definitions.cumulative_interfering_workload
+                /cumul_cond_interference.
+        rewrite (@big_cat_nat _ _ _ t1) //=; last by lia.
+        rewrite [in X in _ <= X](@big_cat_nat _ _ _ t1) //=; last by lia.
+        move: H_is_busy_prefix => [_  [/andP [/eqP DD KK ] ADD]].
+        rewrite /cumulative_interfering_workload in LE; rewrite (leqRW LE); clear LE.
+        rewrite leq_add2r.
+        rewrite /cumulative_interfering_workload in DD.
+        by rewrite -DD; clear DD.
+      Qed.
+
+  End CumulativeIntIntWorkExtension.
+
+  (** In the following section, we show that the busy interval is
+      bounded. More specifically, we show that the length of any
+      abstract busy interval is bounded, as long as there is enough
+      supply to accommodate the interfering workload.  *)
+  Section BoundingBusyInterval.
+
+    (** For simplicity, let us define some local names. *)
+    Let quiet_time t := quiet_time sched j t.
+    Let busy_interval_prefix := busy_interval_prefix sched j.
+    Let busy_interval := busy_interval sched j.
+
+    (** Suppose that job [j] is pending at time [t_busy]. *)
+    Variable t_busy : instant.
+    Hypothesis H_j_is_pending : pending sched j t_busy.
+
+    (** First, we show that there must exist a busy interval prefix. *)
+    Section LowerBound.
+
+      (** Since job [j] is pending at time [t_busy], there is a
+          (potentially unbounded) busy interval that starts no later
+          than with the arrival of [j]. *)
+      Lemma exists_busy_interval_prefix :
+        exists t1,
+          busy_interval_prefix t1 t_busy.+1 /\
+          t1 <= job_arrival j <= t_busy.
+      Proof.
+        rename H_j_is_pending into PEND.
+        destruct ([exists t:'I_t_busy.+1, quiet_time t]) eqn:EX.
+        { set (last0 := \max_(t < t_busy.+1 | quiet_time t) t).
+          move: EX => /existsP [t EX].
+          have PRED: quiet_time last0 by apply (bigmax_pred t_busy.+1 (quiet_time) t).
+          move: PRED => QUIET.
+          exists last0.
+          have JARRIN: last0 <= job_arrival j <= t_busy.
+          { move: PEND => /andP [ARR NCOM].
+            apply/andP; split => //. move: QUIET => /andP [_ PE]. 
+            move: PE; rewrite negb_and -leqNgt => /orP [ | /negPn COMPL] => //; exfalso.
+            apply completion_monotonic with (t' := t_busy) in COMPL.
+            - by move: NCOM => /negP.
+            - by rewrite -ltnS; eapply bigmax_ltn_ord.
+          }
+          repeat split; auto 2; try apply QUIET => //=.
+          move => t0 /andP [GTlast LTbusy] QUIET0.
+          move_neq_down GTlast.
+          by eapply (@leq_bigmax_cond
+                       _ (fun (x: 'I_t_busy.+1) => quiet_time x)
+                       (fun x => x) (Ordinal LTbusy)).
+        }
+        { apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
+          exists 0; split; last by apply/andP; split; last by move: PEND => /andP [ARR _].
+          repeat split.
+          - apply/andP; split => //; rewrite ltnS.
+            by move: PEND => /andP PEND; apply PEND.
+          - apply/andP; split;
+              first by rewrite /cumulative_interference /cumul_cond_interference /cumulative_interfering_workload !big_geq.
+            by apply not_pending_earlier_and_at_0.
+          - move => t /andP [GE LT] QUIET.
+            move: (ALL (Ordinal LT)) => /negP ALL'.
+            by apply ALL'.
+        }
+      Qed.
+
+    End LowerBound.
+
+    (** Next we prove that, if there is a point where the requested
+        workload is upper-bounded by the supply, then the busy
+        interval eventually ends. *)
+    Section UpperBound.
+
+      (** Consider any busy interval prefix of job [j]. *)
+      Variable t1 : instant.
+      Hypothesis H_is_busy_prefix : busy_interval_prefix t1 t_busy.+1.
+
+      (** We assume that for some positive [δ], the cumulative
+          interfering workload within interval <<[t1, t1 + δ)>> is
+          bounded by [δ]. *)
+      Variable δ : duration.
+      Hypothesis H_δ_positive : δ > 0.
+      Hypothesis H_workload_is_bounded :
+        workload_of_job arr_seq j t1 (t1 + δ)
+        + cumulative_interfering_workload j t1 (t1 + δ) <= δ.
+
+      (** If there is a quiet time by time [t1 + δ], it trivially
+          follows that the busy interval is bounded. Thus, let's
+          consider first the harder case where there is no quiet time,
+          which turns out to be impossible. *)
+      Section CannotBeBusyForSoLong.
+
+        (** Assume that there is no quiet time in the interval <<(t1, t1 + δ]>>. *)
+        Hypothesis H_no_quiet_time : forall t, t1 < t <= t1 + δ -> ~ quiet_time t.
+
+        (** We prove that the sum of cumulative service and cumulative
+            interference in the interval <<[t, t + δ)>> is equal to
+            [δ]. *)
+
+        (** Since the interval is always non-quiet, the processor is
+            always busy processing job [j] and the job's interference
+            and, hence, the sum of service of [j] and its cumulative
+            interference within the interval <<[t1, t1 + δ)>> is
+            greater than or equal to [δ]. *)
+        Lemma busy_interval_has_uninterrupted_service :
+          δ <= service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ).
+        Proof.
+          clear H_δ_positive H_workload_is_bounded H_j_is_pending.
+          rewrite /service_during /cumulative_interference /cumul_cond_interference  /cond_interference /service_at.
+          rewrite -big_split //= -{1}(sum_of_ones t1 δ).
+          rewrite big_nat [in X in _ <= X]big_nat.
+          apply leq_sum => x /andP[Lo Hi].
+          destruct (leqP (t1 + δ) (t_busy.+1)) as [LE|LT].
+          { move: (H_work_conserving j t1 t_busy.+1 x) => Workj.
+            feed_n 4 Workj; try done.
+            { by apply/andP; split; eapply leq_trans; eauto. }
+            destruct interference.
+            - by lia.
+            - by rewrite //= addn0; apply Workj.
+          }
+          { move: (H_work_conserving j t1 (t1 + δ) x) => Workj.
+            feed_n 4 Workj; try done.
+            - move: H_is_busy_prefix => [/andP [A1 A2] [QT NQT]]; split; [ | split].
+              + by apply/andP; split => //; rewrite (leqRW A2) -(leqRW LT).
+              + by apply QT.
+              + move => t /andP [A3 A4]; apply H_no_quiet_time.
+                by apply/andP; split; lia.
+            - by apply/andP; split; eapply leq_trans; eauto 2.
+            - destruct interference.
+              + by lia.
+              + by rewrite //= addn0; apply Workj.
+          }
+        Qed.
+
+        (** However, since the total workload is bounded (see
+            [H_workload_is_bounded]), the sum of [j]'s cost and its
+            interfering workload within the interval <<[t1, t1 + δ)>>
+            is bounded by [j]'s service and its interference within
+            the same time interval. *)
+        Lemma busy_interval_too_much_workload :
+          job_cost j + cumulative_interfering_workload j t1 (t1 + δ) <=
+          service_during sched j t1 (t1 + δ) + cumulative_interference j t1 (t1 + δ).
+        Proof.
+          replace (job_cost j) with (workload_of_job arr_seq j t1 (t1 + δ));
+            first by rewrite (leqRW H_workload_is_bounded)
+                     -(leqRW busy_interval_has_uninterrupted_service).
+          move: (H_is_busy_prefix) => [/andP [NEQ1 _] _].
+          erewrite workload_of_job_eq_job_arrival => //=.
+          rewrite NEQ1 Bool.andb_true_l.
+          have -> : job_arrival j < t1 + δ; last by done.
+          move_neq_up GE.
+          apply (H_no_quiet_time (t1 + δ)).
+          { by apply/andP; split; [rewrite -addn1 leq_add2l | done]. }
+          apply/andP; split.
+          - move: (H_workload_is_bounded); rewrite workload_of_job_eq_job_arrival //=.
+            rewrite NEQ1 Bool.andb_true_l [_ < _ + _]leqNgt ltnS GE //= add0n => LE.
+            rewrite eqn_leq; apply/andP; split.
+            + by apply H_no_speculative_exec.
+            + apply (cumul_iw_bounded_by_cumul_i _ t_busy) => //=; rewrite (leqRW LE).
+              eapply leq_trans; first apply busy_interval_has_uninterrupted_service.
+              by have -> : service_during sched j t1 (t1 + δ) = 0
+                by rewrite cumulative_service_before_job_arrival_zero.
+          - by rewrite /pending_earlier_and_at negb_and;
+              apply/orP; left; rewrite -ltnNge ltnS.
+        Qed.
+
+        (** The latter two lemmas imply that [t1 + δ] is a quiet time ... *)
+        Lemma t1δ_is_quiet : quiet_time (t1 + δ).
+        Proof.
+          have LW := busy_interval_too_much_workload.
+          have NEQ: forall a b c d, a >= c -> b >= d -> a + b <= c + d -> a = c /\ b = d by lia.
+          apply NEQ in LW; first destruct LW as [EQ1 EQ2].
+          - apply/andP; split.
+            + rewrite eqn_leq; apply/andP; split.
+              * by apply H_no_speculative_exec.
+              * by apply (cumul_iw_bounded_by_cumul_i _ t_busy) => //=; rewrite EQ2.
+            + rewrite negb_and Bool.negb_involutive; apply/orP; right.
+              rewrite /completed_by EQ1.
+              by erewrite <-(service_cat); [apply leq_addl | ]; lia.
+          - eapply leq_trans; last by apply service_at_most_cost => //=.
+            by erewrite <-(service_cat); [apply leq_addl | ]; lia.
+          - move: H_is_busy_prefix => [_ [/andP [/eqP D _] _]].
+            rewrite -(leq_add2l (definitions.cumulative_interference j 0 t1)) {2}D.
+            rewrite -(big_cat_nat) //=; last by lia.
+            by rewrite -(big_cat_nat) //=; last by lia.
+        Qed.
+
+        (** ... which is a contradiction with the initial
+            assumption. *)
+        Lemma t1δ_is_quiet_contra : False.
+        Proof.
+          eapply H_no_quiet_time; last by apply t1δ_is_quiet.
+          apply/andP; split; last by done.
+          by rewrite -addn1 leq_add2l.
+        Qed.
+
+      End CannotBeBusyForSoLong.
+
+      (** Since the interval cannot remain busy for so long, we prove
+          that the busy interval finishes at some point [t2 <= t1 +
+          δ]. *)
+      Lemma busy_interval_is_bounded :
+        exists t2,
+          t_busy < t2
+          /\ t2 <= t1 + δ
+          /\ busy_interval t1 t2.
+      Proof.
+        move: H_is_busy_prefix => [NEQ [QT NQT]].
+        destruct ([exists t2:'I_(t1 + δ).+1, (t2 > t1) && quiet_time t2]) eqn:EX.
+        { have EX': exists (t2 : instant), ((t1 < t2 <= t1 + δ) && quiet_time t2).
+          { move: EX => /existsP [t2 /andP [LE QUIET]].
+            exists t2; apply/andP; split => //;
+              by apply/andP; split; last (rewrite -ltnS; apply ltn_ord). }
+          move: (ex_minnP EX') => [t2 /andP [/andP [GT LE] QUIET] MIN]; clear EX EX'.
+          exists t2; split; [ | split; [ |split; [split; [ | split] | ] ]]; try done.
+          { move_neq_up NEQ2.
+            move: (H_is_busy_prefix) => [_ [_ NQ]]; apply:(NQ t2) => //.
+            by apply/andP; split => //.
+          }
+          { move: NEQ => /andP [IN1 IN2].
+            apply/andP; split => //.
+            apply leq_ltn_trans with t_busy; eauto 2.
+            rewrite ltnNge; apply/negP; intros CONTR.
+            apply NQT with t2 => //.
+            by apply/andP; split; last rewrite ltnS.
+          }
+          { move => t /andP [GT1 LT2] BUG.
+            feed (MIN t); first (apply/andP; split) => //.
+            { by apply/andP; split; last apply leq_trans with (n := t2); eauto using ltnW. }
+            { by lia. }
+          }
+        }
+        { apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL'.
+          have ALL: forall t, t1 < t <= t1 + δ -> ~ quiet_time t.
+          { move => t /andP [GTt LEt] QUIET; rewrite -ltnS in LEt.
+            specialize (ALL' (Ordinal LEt)); rewrite negb_and /= GTt orFb in ALL'. 
+            by move: ALL' => /negP ALL'; apply ALL'; clear ALL'.
+          }
+          by clear ALL'; exfalso; eapply t1δ_is_quiet_contra.
+        }
+      Qed.
+
+    End UpperBound.
+
+  End BoundingBusyInterval.
+
+End AbstractBusyIntervalExists.
+
+
 (** We add some facts into the "Hint Database" basic_rt_facts, so Coq will be
     able to apply them automatically where needed. *)
 Global Hint Resolve

analysis/facts/behavior/completion.v

@@ -150,6 +150,14 @@ Section CompletionFacts.
       completed_by sched j t -> ~~ scheduled_at sched j t.
   Proof. move=> ? /negPn; exact/contra/scheduled_implies_not_completed. Qed.
 
+  (** Job [j] cannot be pending before and at time [0]. *)
+  Remark not_pending_earlier_and_at_0 :
+    ~~ pending_earlier_and_at sched j 0.
+  Proof.
+    rewrite /pending_earlier_and_at negb_and; apply/orP; left.
+    by rewrite /arrived_before -ltnNge.
+  Qed.
+
 End CompletionFacts.
 
 (** In this section, we establish some facts that are really about service,