Library rt.implementation.apa.arrival_sequence

(* We can reuse the.apa definition of periodic arrival sequence. *)
Require Import rt.util.all.
Require Import rt.model.apa.arrival_sequence rt.model.apa.job
               rt.model.apa.task rt.model.apa.task_arrival.
Require Import rt.implementation.apa.task rt.implementation.apa.job.
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.

Module ConcreteArrivalSequence.

  Import Job ArrivalSequence ConcreteTask ConcreteJob SporadicTaskset SporadicTaskArrival.

  Section PeriodicArrivals.

    Context {num_cpus: nat}.
    Variable ts: concrete_taskset num_cpus.

    (* At any time t, we release Some job of tsk if t is a multiple of the period,
       otherwise we release None. *)
    Definition add_job (t: time) (tsk: @concrete_task num_cpus) : option (@concrete_job _) :=
      if task_period tsk %| t then
        Some (Build_concrete_job (t %/ task_period tsk) (task_cost tsk) (task_deadline tsk) tsk)
      else
        None.

    (* The arrival sequence at any time t is simply the partial map of add_job. *)
    Definition periodic_arrival_sequence (t: time) := pmap (add_job t) ts.

  End PeriodicArrivals.

  Section Proofs.

    Context {num_cpus: nat}.

    (* Let ts be any concrete task set with valid parameters. *)
    Variable ts: concrete_taskset num_cpus.
    Hypothesis H_valid_task_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.

    (* Regarding the periodic arrival sequence built from ts, we prove that...*)
    Let arr_seq := periodic_arrival_sequence ts.

    (* ... every job comes from the task set, ... *)
    Theorem periodic_arrivals_all_jobs_from_taskset:
      ∀ (j: JobIn arr_seq),
        job_task (_job_in arr_seq j) ∈ ts. (* TODO: fix coercion. *)
    Proof.
      intros j.
      destruct j as [j arr ARRj]; simpl.
      unfold arr_seq, arrives_at, periodic_arrival_sequence in ×.
      rewrite mem_pmap in ARRj.
      move: ARRj ⇒ /mapP ARRj; destruct ARRj as [tsk IN SOME].
      by unfold add_job in *; desf.
    Qed.

    (* ..., jobs have valid parameters, ... *)
    Theorem periodic_arrivals_valid_job_parameters:
      ∀ (j: JobIn arr_seq),
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
    Proof.
      rename H_valid_task_parameters into PARAMS.
      unfold valid_sporadic_taskset, is_valid_sporadic_task in ×.
      intros j; destruct j as [j arr ARRj]; simpl.
      unfold arrives_at, arr_seq, periodic_arrival_sequence in ARRj.
      rewrite mem_pmap in ARRj; move: ARRj ⇒ /mapP [tsk IN SOME].
      unfold add_job in SOME; desf.
      specialize (PARAMS tsk IN); des.
      unfold valid_sporadic_job, valid_realtime_job, job_cost_positive.
      by repeat split; try (by done); apply leqnn.
    Qed.

    (* ... job arrivals satisfy the sporadic task model, ... *)
    Theorem periodic_arrivals_are_sporadic:
      sporadic_task_model task_period arr_seq job_task.
    Proof.
      unfold sporadic_task_model; move ⇒ j j' /eqP DIFF SAMEtsk LE.
      destruct j as [j arr ARR], j' as [j' arr' ARR']; simpl in ×.
      rewrite eqE /= /jobin_eqdef negb_and /= in DIFF.
      unfold arrives_at, arr_seq, periodic_arrival_sequence in ×.
      rewrite 2!mem_pmap in ARR ARR'.
      move: ARR ARR' ⇒ /mapP [tsk_j INj SOMEj] /mapP [tsk_j' INj' SOMEj'].
      unfold add_job in SOMEj, SOMEj'; desf; simpl in *;
      move: Heq0 Heq ⇒ /dvdnP [k DIV] /dvdnP [k' DIV'].
      {
        rewrite DIV DIV' -mulSnr.
        rewrite leq_eqVlt in LE; move: LE ⇒ /orP [/eqP EQ | LESS].
        {
          exfalso; move: DIFF ⇒ /negP DIFF; apply DIFF.
          by subst; rewrite EQ.
        }
        subst; rewrite leq_mul2r; apply/orP; right.
        by rewrite ltn_mul2r in LESS; move: LESS ⇒ /andP [_ LT].
      }
      {
        assert (LT: arr < arr'). by rewrite ltn_neqAle; apply/andP.
        clear LE DIFF; subst tsk_j' arr arr'.
        rewrite ltn_mul2r in LT; move: LT ⇒ /andP [_ LT].
        by apply leq_trans with (n := k.+1 × task_period tsk_j);
          [by rewrite mulSnr | by rewrite leq_mul2r; apply/orP; right].
      }
    Qed.

    (* ... and the arrival sequence has no duplicate jobs. *)
    Theorem periodic_arrivals_is_a_set:
      arrival_sequence_is_a_set arr_seq.
    Proof.
      intros t.
      unfold arr_seq, periodic_arrival_sequence.
      apply (pmap_uniq) with (g := job_task); last by destruct ts.
      by unfold add_job, ocancel; intro tsk; desf.
    Qed.

  End Proofs.

End ConcreteArrivalSequence.