Library prosa.classic.model.schedule.uni.jitter.schedule

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* In this file, we prove additional definitions and lemmas about jitter-aware schedules. *)
Module UniprocessorScheduleWithJitter.

  (* To formalize jitter, we import the original uniprocessor schedule and
     redefine some of the properties. *)

  Export ArrivalSequenceWithJitter UniprocessorSchedule.

  (* In this section we redefine properties that depend on the arrival time. *)
  Section RedefiningProperties.

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

    (* Consider any uniprocessor schedule. *)
    Variable arr_seq: arrival_sequence Job.
    Variable sched: schedule Job.

    (* First, we redefine some job properties. *)
    Section JobProperties.

      (* Let j be any job in the arrival sequence. *)
      Variable j: Job.

      (* Then, we say that job j is pending at time t iff the jitter has passed but
         j has not completed by time t. *)

      Definition pending (t: time) :=
        jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.

      (* Finally, we say that job j is backlogged at time t iff it is pending and not scheduled. *)
      Definition backlogged (t: time) :=
        pending t && ~~ scheduled_at sched j t.

    End JobProperties.

    (* Next, we define properties of a valid jitter-aware schedule. *)
    Section ValidSchedules.

      (* In any jitter-aware schedule, a job can only be scheduled after
         the jitter has passed. *)

      Definition jobs_execute_after_jitter :=
         j t,
          scheduled_at sched j t jitter_has_passed job_arrival job_jitter j t.

    End ValidSchedules.

    (* In this section, we prove some basic lemmas about jitter-aware schedules. *)
    Section Lemmas.

      (* For simplicity, let's define some local names. *)
      Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
      Let actual_job_arrival := actual_arrival job_arrival job_jitter.

      (* We begin by proving properties related to job arrivals. *)
      Section Arrival.

        (* Assume that jobs only execute after the jitter has passed. *)
        Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.

        (* First, we show that every job in the schedule only executes after its arrival time. *)
        Lemma jobs_with_jitter_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.
        Proof.
          intros j t SCHED.
          apply leq_trans with (n := actual_arrival job_arrival job_jitter j);
            first by apply leq_addr.
          by apply H_jobs_execute_after_jitter.
        Qed.

        (* Now, let j be any job. *)
        Variable j: Job.

        (* First, we show that if the jitter has passed, then the job must have arrived. *)
        Lemma jitter_has_passed_implies_arrived:
           t,
            has_actually_arrived j t
            has_arrived job_arrival j t.
        Proof.
          by intros t PASS; apply: leq_trans PASS; apply leq_addr.
        Qed.

        (* Now we prove that job j does not receive service at any time t before
           its actual arrival time. *)

        Lemma service_before_jitter_is_zero :
           t,
            t < actual_job_arrival j
            service_at sched j t = 0.
        Proof.
          rename H_jobs_execute_after_jitter into ARR; red in ARR; intros t LT.
          specialize (ARR j t).
          apply contra with (c := scheduled_at sched j t)
                            (b := jitter_has_passed job_arrival job_jitter j t) in ARR;
            last by rewrite -ltnNge.
          by apply/eqP; rewrite eqb0.
        Qed.

        (* Note that the same property applies to the cumulative service. *)
        Lemma cumulative_service_before_jitter_is_zero :
           t1 t2,
            t2 actual_job_arrival j
            \sum_(t1 i < t2) service_at sched j i = 0.
        Proof.
          intros t1 t2 LE; apply/eqP; rewrite -leqn0.
          apply leq_trans with (n := \sum_(t1 i < t2) 0);
            last by rewrite big_const_nat iter_addn mul0n addn0.
          rewrite big_nat_cond [\sum_(_ _ < _) 0]big_nat_cond.
          apply leq_sum; intro i; rewrite andbT; move ⇒ /andP LTi; des.
          rewrite service_before_jitter_is_zero; first by ins.
            by apply leq_trans with (n := t2); ins.
        Qed.

        (* Hence, one can ignore the service received by a job before the jitter. *)
        Lemma ignore_service_before_jitter:
           t1 t2,
            t1 actual_job_arrival j t2
            \sum_(t1 t < t2) service_at sched j t =
            \sum_(actual_job_arrival j t < t2) service_at sched j t.
        Proof.
          movet1 t2 /andP [LE1 GE2].
          rewritebig_cat_nat with (n := actual_job_arrival j); try (by done).
          by rewrite /= cumulative_service_before_jitter_is_zero; [rewrite add0n | apply leqnn].
        Qed.

      End Arrival.

      (* In this section, we prove properties about pending jobs. *)
      Section Pending.

        (* Assume that jobs only execute after the jitter has passed... *)
        Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.

        (* ...and that completed jobs do not execute. *)
        Hypothesis H_completed_jobs:
          completed_jobs_dont_execute job_cost sched.

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

        (* First, we show that if job j is scheduled, then it must be pending. *)
        Lemma scheduled_implies_pending:
           t,
            scheduled_at sched j t pending j t.
        Proof.
          rename H_jobs_execute_after_jitter into ARR,
          H_completed_jobs into COMP.
          unfold jobs_must_arrive_to_execute, completed_jobs_dont_execute in ×.
          intros t SCHED.
          unfold pending; apply/andP; split; first by apply ARR.
          apply/negP; unfold not; intro COMPLETED.
          have BUG := COMP j t.+1.
          rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply BUG.
          unfold service, service_during; rewrite -addn1 big_nat_recr // /=.
            by apply leq_add; last rewrite /service_at SCHED.
        Qed.

      End Pending.

    End Lemmas.

  End RedefiningProperties.

End UniprocessorScheduleWithJitter.