Library rt.model.jitter.schedule

Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Definition, properties and lemmas about schedules. *)
Module ScheduleWithJitter.

  (* We import the original schedule module and redefine whatever is required. *)
  Require Export rt.model.basic.schedule.
  Export ArrivalSequence Schedule.

  (* We need to redefine the properties of a job that depend on the arrival time. *)
  Section ArrivalDependentProperties.

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

    (* Given an arrival sequence, ... *)
    Context {arr_seq: arrival_sequence Job}.

    (* ... we define the following properties for job j in schedule sched. *)
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    Section JobProperties.

      Variable j: JobIn arr_seq.

      (* The actual arrival of job j occurs after the jitter. *)
      Definition actual_arrival := job_arrival j + job_jitter j.

      (* Whether job j's jitter has passed by time t. *)
      Definition jitter_has_passed (t: time) := actual_arrival t.

      (* Whether job j actually arrived before time t. *)
      Definition actual_arrival_before (t: time) := actual_arrival < t.

      (* Job j is pending at time t iff the jitter has passed but j has not completed. *)
      Definition pending (t: time) := jitter_has_passed t ¬ completed job_cost sched j t.

      (* Job j is backlogged at time t iff it is pending and not scheduled. *)
      Definition backlogged (t: time) := pending t ¬ scheduled sched j t.

      (* Job j is carry-in in interval t1, t2) iff it arrives before t1 and is not complete at time t1 *)
      Definition carried_in (t1: time) := actual_arrival_before t1 ¬ completed job_cost sched j t1.

      (* Job j is carry-out in interval t1, t2) iff it arrives after t1 and is not complete at time t2 *)
      Definition carried_out (t1 t2: time) := actual_arrival_before t2 ¬ completed job_cost sched j t2.

    End JobProperties.

    Section ScheduleProperties.

      (* A job can only be scheduled after the jitter has passed. *)
      Definition jobs_execute_after_jitter :=
         j t,
          scheduled sched j t jitter_has_passed j t.

    End ScheduleProperties.

    Section BasicLemmas.

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

      Section Pending.

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

        (* Then, if job j is scheduled, it must be pending. *)
        Lemma scheduled_implies_pending:
           j t,
            scheduled sched j t
            pending j t.
        Proof.
          rename H_jobs_execute_after_jitter into JITTER,
                 H_completed_jobs into COMP.
          unfold jobs_execute_after_jitter, completed_jobs_dont_execute in ×.
          intros j t SCHED.
          unfold pending; apply/andP; split; first by apply JITTER.
          apply/negP; unfold not; intro COMPLETED.
          have BUG := COMP j t.+1.
          rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply BUG.
          unfold service; rewrite -addn1 big_nat_recr // /=.
          apply leq_add;
            first by move: COMPLETED ⇒ /eqP COMPLETED; rewrite -COMPLETED.
          rewrite lt0n; apply/eqP; red; move ⇒ /eqP NOSERV.
          rewrite -not_scheduled_no_service in NOSERV.
          by rewrite SCHED in NOSERV.
        Qed.

      End Pending.

      Section Service.

        (* If a job only executes after the jitter, it also only
           executes after its arrival time. *)

        Lemma arrival_before_jitter :
          jobs_must_arrive_to_execute sched.
          Proof.
            unfold jobs_execute_after_jitter, jobs_must_arrive_to_execute.
            intros j t SCHED; unfold ArrivalSequence.has_arrived.

            rewrite -(leq_add2r (job_jitter j)).
            by apply leq_trans with (n := t);
              [by apply H_jobs_execute_after_jitter | by apply leq_addr].
          Qed.

        Lemma service_before_jitter_zero :
           j t,
            t < job_arrival j + job_jitter j
            service_at sched j t = 0.
        Proof.
          rename H_jobs_execute_after_jitter into AFTER; intros j t LT.
          apply/eqP; rewrite -not_scheduled_no_service; apply/negP; red; intro SCHED.
          by apply AFTER, (leq_trans LT) in SCHED; rewrite ltnn in SCHED.
        Qed.

        Lemma cumulative_service_before_jitter_zero :
           j t1 t2,
            t2 job_arrival j + job_jitter j
            \sum_(t1 t < t2) service_at sched j t = 0.
        Proof.
          intros j t1 t2 LE.
          apply/eqP; rewrite -leqn0.
          apply leq_trans with (n := \sum_(t1 t < t2) 0);
            last by rewrite big_const_nat iter_addn mul0n addn0.
          rewrite big_nat_cond [\sum_(_ _ < _)_]big_nat_cond.
          apply leq_sum; movet /andP [/andP [_ LT] _].
          rewrite leqn0; apply/eqP; apply service_before_jitter_zero.
          by apply (leq_trans LT).
        Qed.

      End Service.

    End BasicLemmas.

  End ArrivalDependentProperties.

End ScheduleWithJitter.

(* Specific properties of a schedule of sporadic jobs. *)
Module ScheduleOfSporadicTaskWithJitter.

  Import SporadicTask Job.
  Export ScheduleWithJitter.

  Section ScheduledJobs.

    Context {sporadic_task: eqType}.
    Context {Job: eqType}.
    Variable job_task: Job sporadic_task.

    (* Consider any schedule. *)
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    (* Given a task tsk, ...*)
    Variable tsk: sporadic_task.

    (* ..., we we can state that tsk is scheduled on cpu at time t as follows. *)
    Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
      if (sched cpu t) is Some j then
        (job_task j = tsk)
      else false.

    (* Likewise, we can state that tsk is scheduled on some processor. *)
      Definition task_is_scheduled (t: time) :=
        [ cpu, task_scheduled_on cpu t].

    (* We also define the list of jobs scheduled during t1, t2). *)
    Definition jobs_of_task_scheduled_between (t1 t2: time) :=
      filter (fun (j: JobIn arr_seq) ⇒ job_task j = tsk)
             (jobs_scheduled_between sched t1 t2).

  End ScheduledJobs.

  Section ScheduleProperties.

    Context {sporadic_task: eqType}.
    Context {Job: eqType}.
    Variable job_cost: Job time.
    Variable job_jitter: Job time.
    Variable job_task: Job sporadic_task.

    (* Consider any schedule. *)
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    (* Next we define intra-task parallelism. *)
    Definition jobs_of_same_task_dont_execute_in_parallel :=
       (j j': JobIn arr_seq) t,
        job_task j = job_task j'
        scheduled sched j t scheduled sched j' t j = j'.

  End ScheduleProperties.

  Section BasicLemmas.

    (* Assume the job cost and task are known. *)
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_deadline: sporadic_task time.

    Context {Job: eqType}.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.

    (* Then, in a valid schedule of sporadic tasks ...*)
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    (* ...such that jobs do not execute after completion, ...*)
    Hypothesis jobs_dont_execute_after_completion :
       completed_jobs_dont_execute job_cost sched.

    Variable tsk: sporadic_task.

    Variable j: JobIn arr_seq.
    Hypothesis H_job_of_task: job_task j = tsk.
    Hypothesis valid_job:
      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    (* Remember that for any job of tsk, service <= task_cost tsk *)
    Lemma cumulative_service_le_task_cost :
         t t',
          service_during sched j t t' task_cost tsk.
    Proof.
      rename valid_job into VALID; unfold valid_sporadic_job in *; ins; des.
      apply leq_trans with (n := job_cost j);
        last by rewrite -H_job_of_task; apply VALID0.
      by apply cumulative_service_le_job_cost.
    Qed.

  End BasicLemmas.

End ScheduleOfSporadicTaskWithJitter.