Library prosa.analysis.facts.readiness.sequential

Require Export prosa.model.readiness.sequential.
Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.task_arrivals.

In this section, we show some useful properties of the sequential task readiness model.
Section SequentialTasksReadiness.

Consider any type of job associated with any type of tasks ...
  Context {Job : JobType}.
  Context {Task : TaskType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

... and any kind of processor state.
  Context {PState : ProcessorState Job}.

Consider any arrival sequence with consistent arrivals.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Assume a basic sequential readiness model, wherein a pending job is ready exactly when all prior jobs from the same task have completed.
  Context {RM : JobReady Job PState}.
  Hypothesis H_basic_sequential_readiness : basic_sequential_readiness RM arr_seq.

First, we observe that the sequential readiness model indeed lives up to its name.
  Fact sequential_readiness_is_sequential :
    sequential_readiness RM arr_seq.
  Proof.
    by move⇒ sched j t; rewrite H_basic_sequential_readiness ⇒ /andP [_ PRIOR].
  Qed.

Consider any valid schedule of arr_seq.
  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

Consider an FP policy that indicates a reflexive higher-or-equal priority relation.
  Context {FP : FP_policy Task}.
  Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.

We show that a sequential readiness model is non-clairvoyant.
  Fact sequential_readiness_nonclairvoyance :
    nonclairvoyant_readiness RM.
  Proof.
    intros sched1 sched2 j h ID t LE.
    rewrite !H_basic_sequential_readiness.
    erewrite identical_prefix_pending; eauto 2.
    destruct (boolP (pending sched2 j t)) as [_ | _] ⇒ //=.
    destruct (boolP (prior_jobs_complete arr_seq sched2 j t)) as [ALL | NOT_ALL]; apply/eqP.
    - rewrite eqb_id; apply/allP; intros x IN.
      move: ALL ⇒ /allP ALL; specialize (ALL x IN).
      by erewrite identical_prefix_completed_by; eauto 2.
    - move: NOT_ALL ⇒ /allPn [x IN NCOMP].
      rewrite eqbF_neg; apply/allPn; ∃ x ⇒ //.
      by erewrite identical_prefix_completed_by; eauto 2.
  Qed.

Next, we show that the sequential readiness model ensures that tasks are sequential. That is, that jobs of the same task execute in order of their arrival.
  Lemma sequential_readiness_implies_sequential_tasks :
    sequential_tasks arr_seq sched.
  Proof.
    intros j1 j2 t ARR1 ARR2 SAME LT SCHED.
    destruct (boolP (job_ready sched j2 t)) as [READY | NREADY].
    - move: READY; rewrite H_basic_sequential_readiness ⇒ /andP [PEND /allP ALL].
      apply: ALL.
      rewrite mem_filter; apply/andP; split⇒ [//|].
      exact: arrived_between_implies_in_arrivals.
    - by exfalso; apply/(negP NREADY)/job_scheduled_implies_ready.
  Qed.

Finally, we show that the sequential readiness model is a work-bearing readiness model. That is, if a job j is pending but not ready at a time instant t, then there exists another (earlier) job of the same task that is pending and ready at time t.
  Lemma sequential_readiness_implies_work_bearing_readiness :
    work_bearing_readiness RM arr_seq sched.
  Proof.
    intros j.
    have EX: ∃ k, job_arrival j ≤ k by (∃ (job_arrival j)).
    destruct EX as [k LE]; move: j LE.
    elim: k ⇒ [|k IHk] j LE t ARR PEND.
    { destruct (boolP (job_ready sched j t)) as [READY | NREADY].
      { ∃ j; repeat split ⇒ //.
        by rewrite /hep_job /fp_to_jlfp; apply: H_priority_is_reflexive. }
      { move: NREADY; rewrite H_basic_sequential_readiness PEND Bool.andb_true_l ⇒ /allPn [jhp IN NCOMP].
        apply arrives_in_task_arrivals_before_implies_arrives_before in IN ⇒ [|//].
        by exfalso; move: LE; rewrite leqn0 ⇒ /eqP EQ; rewrite EQ in IN.
      }
    }
    { move: LE; rewrite leq_eqVlt ltnS ⇒ /orP [/eqP EQ | LE]; last by apply IHk.
      destruct (boolP (job_ready sched j t)) as [READY | NREADY].
      { ∃ j; repeat split ⇒ //.
        by rewrite /hep_job /fp_to_jlfp; apply: H_priority_is_reflexive. }
      { move: NREADY; rewrite H_basic_sequential_readiness PEND Bool.andb_true_l ⇒ /allPn [j' IN NCOMP].
        have LE' : job_arrival j' ≤ k.
        { by apply arrives_in_task_arrivals_before_implies_arrives_before in IN; rewrite // -ltnS -EQ. }
        have ARR' : arrives_in arr_seq j'.
        { by eapply arrives_in_task_arrivals_implies_arrived; eauto 2. }
        have PEND' : pending sched j' t.
        { apply/andP; split⇒ [|//].
          move: PEND ⇒ /andP [LE _].
          by unfold has_arrived in *; lia.
        }
        specialize (IHk j' LE' t ARR' PEND').
        destruct IHk as [j'' [ARR'' [READY'' HEP'']]].
        ∃ j''; repeat split; auto.
        clear EQ; apply arrives_in_task_arrivals_implies_job_task in IN; move: IN ⇒ /eqP EQ.
        by rewrite /hep_job /fp_to_jlfp -EQ.
      }
    }
  Qed.

End SequentialTasksReadiness.