Library prosa.classic.model.schedule.uni.susp.suspension_intervals

Require Import prosa.classic.util.all.

Require Import prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.susp.last_execution.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module SuspensionIntervals.

  Export Job UniprocessorSchedule Suspension LastExecution.

  (* In this section we define job suspension intervals in a schedule. *)
  Section DefiningSuspensionIntervals.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.

    (* Consider any job suspension times... *)
    Variable next_suspension: job_suspension Job.

    (* ...and any uniprocessor schedule. *)
    (*Context {arr_seq: arrival_sequence Job}.*)
    Variable sched: schedule Job.

    (* For simplicity, let's define some local names. *)
    Let job_scheduled_at := scheduled_at sched.
    Let job_completed_by := completed_by job_cost sched.

    (* Based on the time after the last execution of a job, we define next
       whether a job is suspended. *)

    Section JobSuspension.

      (* Let j be any job. *)
      Variable j: Job.

      Section DefiningSuspension.

        (* We are going to define whether job j is suspended at time t. *)
        Variable t: time.

        (* First, we define the beginning of the latest self suspension as the
           time following the last execution of job j in the interval 0, t). (Note that suspension_start can return time t itself.) *)

        Let suspension_start := time_after_last_execution job_arrival sched j t.

        (* Next, using the service received by j in the interval 0, suspension_start*)
        Let),... current_service := service sched j suspension_start.

        (* ... we recall the duration of the suspension expected for job j after having
           received that amount of service. *)

        Definition suspension_duration := next_suspension j current_service.

        (* Then, we say that job j is suspended at time t iff j has not completed
           by time t and t lies in the latest suspension interval.
           (Also note that the suspension interval can have duration 0, in which
            case suspended_at will be trivially false.)                         *)

        Definition suspended_at :=
          ~~ completed_by job_cost sched j t &&
          (suspension_start t < suspension_start + suspension_duration).

      End DefiningSuspension.

      (* Based on the notion of suspension, we also define the cumulative
         suspension time of job j in any interval t1, t2)... *)

      Definition cumulative_suspension_during (t1 t2: time) :=
        \sum_(t1 t < t2) (suspended_at t).

      (* ...and the cumulative suspension time in any interval 0, t). *)
      Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.

    End JobSuspension.

    (* Next, we define whether the schedule respects self-suspensions. *)
    Section SuspensionAwareSchedule.

      (* We say that the schedule respects self-suspensions iff suspended
         jobs are never scheduled. *)

      Definition respects_self_suspensions :=
         j t,
          job_scheduled_at j t ¬ suspended_at j t.

    End SuspensionAwareSchedule.

    (* In this section, we prove several results related to job suspensions. *)
    Section Lemmas.

      (* First, we prove that at any time within any suspension interval, 
         a job is always suspended. *)

      Section InsideSuspensionInterval.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

        (* Let j be any job. *)
        Variable j: Job.

        (* Consider any time t after the arrival of j... *)
        Variable t: time.
        Hypothesis H_has_arrived: has_arrived job_arrival j t.

        (* ...and recall the latest suspension interval of job j relative to time t. *)
        Let suspension_start := time_after_last_execution job_arrival sched j t.
        Let duration := suspension_duration j t.

        (* First, we analyze the service received during a suspension interval. *)
        Section SameService.

          (* Let t_in be any time in the suspension interval relative to time t. *)
          Variable t_in: time.
          Hypothesis H_within_suspension_interval:
            suspension_start t_in suspension_start + duration.

          (* Then, we show that the service received before time t_in
             equals the service received before the beginning of the
             latest suspension interval (if exists). *)

          Lemma same_service_in_suspension_interval:
            service sched j t_in = service sched j suspension_start.
          Proof.
            rename H_within_suspension_interval into BETWEEN,
                   H_respects_self_suspensions into SUSP, t_in into i.
            generalize dependent i.
            suff SAME:
               delta,
                delta duration
                service sched j (suspension_start + delta) =
                service sched j suspension_start.
            {
              movei /andP [GE LT].
              feed (SAME (i-suspension_start)); first by rewrite leq_subLR.
              by rewrite addnBA // addKn in SAME.
            }
            induction delta; first by rewrite addn0.
            intros LT.
            feed IHdelta; first by apply ltnW.
            rewrite addnS -[service _ _ suspension_start]addn0.
            rewrite /service /service_during big_nat_recr //=.
            f_equal; first by done.
            apply/eqP; rewrite eqb0; apply/negP; intro SCHED.
            move: (SCHED) ⇒ SCHED'.
            apply SUSP in SCHED; apply SCHED; clear SCHED.
            rewrite /suspended_at /suspension_duration.
            case: (boolP (completed_by _ _ _ _)) ⇒ [COMP | NOTCOMP];
              first by apply completed_implies_not_scheduled in COMP;
                first by rewrite SCHED' in COMP.
            rewrite andTb (same_service_implies_same_last_execution _ _ _ _
                                                                    suspension_start) //.
            rewrite /suspension_start last_execution_idempotent //.
            apply/andP; split; first by apply leq_addr.
            by rewrite ltn_add2l.
          Qed.

        End SameService.

        (* Next, we infer that the job is suspended at all times during
           the suspension interval. *)

        Section JobSuspendedAtAllTimes.

          (* Let t_in be any time before the completion of job j. *)
          Variable t_in: time.
          Hypothesis H_not_completed: ~~ job_completed_by j t_in.

          (* If t_in lies in the suspension interval relative to time t, ...*)
          Hypothesis H_within_suspension_interval:
            suspension_start t_in < suspension_start + duration.

          (* ...then job j is suspended at time t_in. More precisely, the suspension
             interval relative to time t_in is included in the suspension interval
             relative to time t. *)

          Lemma suspended_in_suspension_interval:
            suspended_at j t_in.
          Proof.
            rename H_within_suspension_interval into BETWEEN.
            move: BETWEEN ⇒ /andP [GE LT].
            have ARR: has_arrived job_arrival j t_in.
            {
              apply leq_trans with (n := suspension_start); last by done.
              rewrite -/(has_arrived job_arrival j suspension_start).
              by apply last_execution_after_arrival.
            }
            apply/andP; split; first by done.
            apply/andP; split;
              first by apply last_execution_bounded_by_identity.
            apply (leq_trans LT).
            have SAME: time_after_last_execution job_arrival sched j t =
                       time_after_last_execution job_arrival sched j t_in.
            {
              set b := _ _ t.
              rewrite [_ _ t_in](same_service_implies_same_last_execution _ _ _ _ b);
                first by rewrite last_execution_idempotent.
              apply same_service_in_suspension_interval.
              by apply/andP; split; last by apply ltnW.
            }
            rewrite /suspension_start SAME leq_add2l.
            by rewrite /duration /suspension_duration SAME.
          Qed.

        End JobSuspendedAtAllTimes.

      End InsideSuspensionInterval.

      (* Next, we prove lemmas about the state of a suspended job. *)
      Section StateOfSuspendedJob.

        (* Assume that jobs do not execute before they arrived. *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* Let j be any job. *)
        Variable j: Job.

        (* Assume that j is suspended at time t. *)
        Variable t: time.
        Hypothesis H_j_is_suspended: suspended_at j t.

        (* First, we show that j must have arrived by time t. *)
        Lemma suspended_implies_arrived: has_arrived job_arrival j t.
        Proof.
          rename H_j_is_suspended into SUSP.
          move: SUSP ⇒ /andP [_ SUSP].
          rewrite -[_ && _]negbK in SUSP; move: SUSP ⇒ /negP SUSP.
          rewrite /has_arrived leqNgt; apply/negP; intro LT.
          apply SUSP; clear SUSP.
          rewrite negb_and; apply/orP; left.
          rewrite -ltnNge.
          apply: (leq_trans LT); clear LT.
          rewrite /time_after_last_execution.
          case EX: [ _, _]; last by apply leqnn.
          set t' := \max_(_ < _ | _)_.
          move: EX ⇒ /existsP [t0 EX].
          apply bigmax_pred in EX; rewrite -/t' /job_scheduled_at in EX.
          apply leq_trans with (n := t'); last by apply leq_addr.
          rewrite leqNgt; apply/negP; intro LT.
          have NOTSCHED: ~~ scheduled_at sched j t'.
          {
            rewrite -eqb0; apply/eqP.
            by eapply service_before_job_arrival_zero; first by eauto.
          }
          by rewrite EX in NOTSCHED.
        Qed.

        (* By the definition of suspension, it also follows that j cannot
           have completed by time t. *)

        Corollary suspended_implies_not_completed:
          ~~ completed_by job_cost sched j t.
        Proof.
          by move: H_j_is_suspended ⇒ /andP [NOTCOMP _].
        Qed.

      End StateOfSuspendedJob.

      (* Next, we establish a bound on the cumulative suspension time of any job. *)
      Section BoundOnCumulativeSuspension.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

        (* Let j be any job. *)
        Variable j: Job.

        (* Recall the total suspension of job j as given by the dynamic suspension model. *)
        Let cumulative_suspension_of_j :=
          cumulative_suspension_during j.
        Let total_suspension_of_j :=
          total_suspension job_cost next_suspension j.

        (* We prove that the cumulative suspension time of job j in any
           interval is upper-bounded by the total suspension time. *)

        Lemma cumulative_suspension_le_total_suspension:
           t1 t2,
            cumulative_suspension_of_j t1 t2 total_suspension_of_j.
        Proof.
          unfold cumulative_suspension_of_j, cumulative_suspension_during,
                 total_suspension_of_j, total_suspension.
          intros t1 t2.
          apply leq_trans with (n := \sum_(0 s < job_cost j)
                            \sum_(t1 t < t2 | service sched j t == s) suspended_at j t).
          { rewrite (exchange_big_dep_nat (fun xtrue)) //=.
            apply leq_sum; intros s _.
            destruct (boolP (suspended_at j s)) as [SUSP | NOTSUSP]; last by done.
            rewrite (big_rem (service sched j s)); first by rewrite eq_refl.
            rewrite mem_index_iota; apply/andP; split; first by done.
            rewrite ltn_neqAle; apply/andP; split;
              last by apply cumulative_service_le_job_cost.
            apply suspended_implies_not_completed in SUSP.
            rewrite neq_ltn; apply/orP; left.
              by rewrite ltnNge.
          }
          { apply leq_sum_nat; moves /andP [_ LT] _.
            destruct (boolP [ t:'I_t2, (tt1)&& (service sched j t==s)]) as [EX|ALL];
              last first.
            {
              rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.
              rewrite big_nat_cond big1 //.
              movei /andP [/andP [GEi LTi] SERV].
              by specialize (ALL (Ordinal LTi)); rewrite /= SERV GEi andbT in ALL.
            }
            move: EX ⇒ /existsP [t' /andP [GE' /eqP SERV]].
            unfold suspended_at, suspension_duration.
            set b := time_after_last_execution job_arrival sched j.
            set n := next_suspension j s.
            apply leq_trans with (n := \sum_(t1 t < t2 | b t' t < b t' + n) 1).
            {
              rewrite big_mkcond [\sum_(_ _ < _ | b t' _ < _) _]big_mkcond /=.
              apply leq_sum_nat; intros t LEt _.
              case: (boolP (completed_by _ _ _ _)) ⇒ [COMP | NOTCOMP];
                [by case (_ == _) | simpl].
              case EQ: (service _ _ _ == _); last by done.
              move: EQ ⇒ /eqP EQ. rewrite /n -EQ.
              case INT: (_ _ < _); last by done.
              apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
              move: INT ⇒ /andP [GEt LTt].
              rewrite (same_service_in_suspension_interval _ _ _ _ t') //.
              {
                rewrite -/b [b t'](same_service_implies_same_last_execution _ _ _ _ t);
                  last by rewrite SERV EQ.
                by apply/andP; split.
              }
              {
                rewrite /suspension_duration -/b.
                rewrite [b t'](same_service_implies_same_last_execution _ _ _ _ t);
                  last by rewrite SERV EQ.
                by apply/andP; split; last by apply ltnW.
              }
            }
            apply leq_trans with (n := \sum_(b t' t < b t' + n) 1);
              last by simpl_sum_const; rewrite addKn.
            by apply leq_sum1_smaller_range; movei [LE LE']; split.
          }
        Qed.

      End BoundOnCumulativeSuspension.

      (* Next, we show that when a job completes, it must have suspended
         as long as the total suspension time. *)

      Section SuspendsForTotalSuspension.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

        (* Let j be any job. *)
        Variable j: Job.

        (* Assume that j has completed by time t. *)
        Variable t: time.
        Hypothesis H_j_has_completed: completed_by job_cost sched j t.

        (* Then, we prove that the cumulative suspension time must be
           exactly equal to the total suspension time of the job. *)

        Lemma cumulative_suspension_eq_total_suspension:
          cumulative_suspension j t = total_suspension job_cost next_suspension j.
        Proof.
          rename H_j_has_completed into COMP, H_jobs_must_arrive_to_execute into ARR.
          have EARLIER := exists_last_execution_with_smaller_service job_arrival
                                                           job_cost sched ARR j t COMP.
          apply/eqP; rewrite eqn_leq; apply/andP; split;
            first by apply cumulative_suspension_le_total_suspension.
          rewrite /total_suspension /cumulative_suspension /cumulative_suspension_during.
          move: COMP ⇒ /eqP COMP.
          apply leq_trans with (n := \sum_(0 s < job_cost j)
                           \sum_(0 t0 < t | service sched j t0 == s) suspended_at j t0);
            last first.
          {
            rewrite (exchange_big_dep_nat (fun xtrue)) //=.
            apply leq_sum_nat; movet0 /andP [_ LT] _.
            case (boolP [ s: 'I_(job_cost j), service sched j t0 == s]) ⇒ [EX | ALL].
            {
              move: EX ⇒ /existsP [s /eqP EQs].
              rewrite big_mkcond /=.
              rewrite (bigD1_seq (nat_of_ord s)); [simpl | | by apply iota_uniq];
                last by rewrite mem_index_iota; apply/andP;split; last by apply ltn_ord.
              rewrite EQs eq_refl big1; first by rewrite addn0.
              by movei /negbTE NEQ; rewrite eq_sym NEQ.
            }
            {
              rewrite big_nat_cond big1; first by done.
              movei /andP [/andP [_ LTi] /eqP SERV].
              rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.
              by specialize (ALL (Ordinal LTi)); rewrite /= SERV eq_refl in ALL.
            }
          }
          {
            apply leq_sum_nat; moves /andP [_ LTs] _.
            rewrite /suspended_at /suspension_duration.
            set b := time_after_last_execution job_arrival sched j.
            set n := next_suspension j.

            move: (EARLIER s LTs) ⇒ [t' EQ'].
            apply leq_trans with (n := \sum_(0 t0 < t | (service sched j t0 == s) &&
                          (b t' t0 < b t' + n (service sched j (b t')))) 1); last first.
            { rewrite big_mkcond [\sum_(_ _ < _ | _ == s)_]big_mkcond.
              apply leq_sum_nat; movei /andP [_ LTi] _.
              case EQi: (service sched j i == s); [rewrite andTb | by rewrite andFb].
              case LE: (_ _ _); last by done.
              rewrite lt0n eqb0 negbK.
              apply suspended_in_suspension_interval with (t := t'); try (by done).
              rewrite -ltnNge.
                by apply: (leq_ltn_trans _ LTs); apply eq_leq; apply/eqP.
            }
            { apply leq_trans with (n := \sum_(b t' t0< b t'+ n (service sched j (b t')) |
                                            (0 t0 < t) && (service sched j t0 == s)) 1).
              {
                apply leq_trans with (n := \sum_(b t' t0 < b t'
                                                         + n (service sched j (b t'))) 1);
                  first by simpl_sum_const; rewrite addKn -EQ'.
                rewrite [in X in _ X]big_mkcond /=.
                apply leq_sum_nat; movei /andP [LEi GTi] _.
                apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
                apply/andP; split.
                {
                  have SUSPi: suspended_at j i.
                  {
                    apply: (suspended_in_suspension_interval _ _ _ _ t');
                      try (by done); last by apply/andP; split.
                    rewrite -ltnNge.
                    rewrite (same_service_in_suspension_interval _ _ _ _ t') //;
                      first by rewrite EQ'.
                    by apply/andP; split; last by apply ltnW.
                  }
                  apply contraT; rewrite -leqNgt; intro LE.
                  apply suspended_implies_not_completed in SUSPi.
                  exfalso; move: SUSPi ⇒ /negP COMPi; apply COMPi.
                  try ( apply completion_monotonic with (t0 := t); try (by done) ) ||
                  apply completion_monotonic with (t := t); try (by done).
                  by apply/eqP.
                }
                {
                  rewrite -EQ'; apply/eqP.
                  apply same_service_in_suspension_interval; try (by done).
                  by apply/andP; split; last by apply ltnW.
                }
              }
              {
                apply leq_sum1_smaller_range.
                by movei [LEb /andP [LE EQs]]; split;
                  last by apply/andP; split.
              }
            }
          }
        Qed.

      End SuspendsForTotalSuspension.

      (* In this section, we prove that a job executes just before it starts suspending.  *)
      Section ExecutionBeforeSuspension.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

        (* Let j be any job... *)
        Variable j: Job.

        (* ...that has arrived by some time t. *)
        Variable t: time.
        Hypothesis H_arrived: has_arrived job_arrival j t.

        (* If job j is not suspended at time t, but starts to suspend at time t + 1, ... *)
        Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
        Hypothesis H_begins_suspension: suspended_at j t.+1.

        (* ...then j must be scheduled at time t. *)
        Lemma executes_before_suspension:
          scheduled_at sched j t.
        Proof.
          rename H_not_suspended_at_t into NOTSUSPs, H_begins_suspension into SUSPs'.
          move: SUSPs' ⇒ /andP [NOTCOMP' /andP [GE LT]].
          apply contraT; intro NOTSCHED.
          suff BUG: suspended_at j t by rewrite BUG in NOTSUSPs.
          apply suspended_in_suspension_interval with (t := t.+1); try done.
          {
            apply contraT; rewrite negbK; intro COMP.
            suff COMP': completed_by job_cost sched j t.+1 by rewrite COMP' in NOTCOMP'.
            try ( by apply completion_monotonic with (t0 := t) ) ||
            by apply completion_monotonic with (t := t).
          }
          apply/andP; split; last by apply: (leq_ltn_trans _ LT).
          apply leq_trans with (n := time_after_last_execution job_arrival sched j t);
            last by apply last_execution_bounded_by_identity.
          apply eq_leq, same_service_implies_same_last_execution.
          rewrite /service /service_during big_nat_recr //= /service_at.
          by apply negbTE in NOTSCHED; rewrite NOTSCHED addn0.
        Qed.

      End ExecutionBeforeSuspension.

    End Lemmas.

  End DefiningSuspensionIntervals.

End SuspensionIntervals.