Library prosa.analysis.facts.model.preemption

In this section, we establish two basic facts about preemption times.
Section PreemptionTimes.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

In addition, we assume the existence of a function mapping a job and its progress to a boolean value saying whether this job is preemptable at its current point of execution.
  Context `{JobPreemptable Job}.

Consider any valid arrival sequence
Allow for any uniprocessor model.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uniproc : uniprocessor_model PState.

Next, consider any schedule of the arrival sequence...
  Variable sched : schedule PState.

... where jobs come from the arrival sequence and don't execute before their arrival time.
Consider a valid preemption model.
We start with a trivial fact that, given a time interval [t1, t2)>>, the interval either contains a preemption time t or it does not.
  Lemma preemption_time_interval_case :
     t1 t2,
      ( t, t1 t < t2 ~~ preemption_time arr_seq sched t)
       ( t,
            t1 t < t2
             preemption_time arr_seq sched t
             t', t1 t' preemption_time arr_seq sched t' t t').
  Proof. by apply earliest_pred_element_exists_case. Qed.

An idle instant is a preemption time.
  Lemma idle_time_is_pt :
     t,
      is_idle arr_seq sched t
      preemption_time arr_seq sched t.
  Proof. by movet; rewrite is_idle_iff /preemption_time ⇒ /eqP →. Qed.

We show that time 0 is a preemption time.
  Lemma zero_is_pt: preemption_time arr_seq sched 0.
  Proof.
    rewrite /preemption_time.
    case SCHED: (scheduled_job_at _ _ 0) ⇒ [j|//].
    have ARR: arrives_in arr_seq j.
    { apply: H_jobs_come_from_arrival_sequence.
      rewrite -(scheduled_job_at_scheduled_at arr_seq) //; exact/eqP/SCHED. }
    rewrite /service /service_during big_geq //.
    by move: (H_valid_preemption_model j ARR) ⇒ [PP _].
  Qed.

Also, we show that the first instant of execution is a preemption time.
  Lemma first_moment_is_pt:
     j prt,
      arrives_in arr_seq j
      ~~ scheduled_at sched j prt
      scheduled_at sched j prt.+1
      preemption_time arr_seq sched prt.+1.
  Proof.
    moves pt ARR NSCHED SCHED.
    move: (SCHED); rewrite /preemption_time -(scheduled_job_at_scheduled_at arr_seq) // ⇒ /eqP →.
    by move: (H_valid_preemption_model s ARR) ⇒ [_ [_ [_ P]]]; apply P.
  Qed.

If a job is scheduled at a point in time that is not a preemption time, then it was previously scheduled.
  Lemma neg_pt_scheduled_at :
     j t,
      scheduled_at sched j t.+1
      ~~ preemption_time arr_seq sched t.+1
      scheduled_at sched j t.
  Proof.
    movej t sched_at_next.
    apply contraNTNSCHED.
    exact: (first_moment_is_pt j).
  Qed.

If a job is scheduled at time t-1 and time t is not a preemption time, then the job is scheduled at time t as well.
  Lemma neg_pt_scheduled_before :
     j t,
      ~~ preemption_time arr_seq sched t
      scheduled_at sched j t.-1
      scheduled_at sched j t.
  Proof.
    movej t NP SCHED; apply negbNE; apply/negPNSCHED.
    have [Z|POS] := posnP t.
    { by move: SCHED; subst ⇒ //= ⇒ SCHED; rewrite SCHED in NSCHED. }
    { edestruct scheduled_at_cases as [IDLE| [s SCHEDs]] ⇒ //.
      { move: NP ⇒ /negP NP; apply: NP; rewrite /preemption_time.
        by rewrite is_idle_iff in IDLE; move: IDLE ⇒ /eqP →. }
      { instantiate (1 := t) in SCHEDs.
        destruct t as [ | t]; [by done | rewrite -pred_Sn in SCHED].
        move: (SCHEDs) ⇒ SCHEDst; eapply neg_pt_scheduled_at in SCHEDs ⇒ //.
        have EQ : s = j by apply: H_uniproc; [apply SCHEDs | apply SCHED].
        by subst; rewrite SCHEDst in NSCHED. } }
  Qed.

We extend the previous lemma to a time interval. That is, assume that there is no preemption time in an interval [t1, t2), then if a job is scheduled at time t ∈ [t1, t2), then the same job is scheduled at another time t' ∈ [t1, t2).
  Lemma neg_pt_scheduled_continuous :
     j t1 t2 t t',
      t1 t < t2
      t1 t' < t2
      ( t, t1 t < t2 ~~ preemption_time arr_seq sched t)
      scheduled_at sched j t
      scheduled_at sched j t'.
  Proof.
    movej t1 t2 t t' NEQ1 NEQ2 NP SCHED.
    have NEQ3 : t1 < t2 by lia.
    interval_to_duration t1 t2 δ.
    generalize dependent t; generalize dependent t'.
    induction δ as [ | δ IHδ]; first by movet' NEQ; exfalso; lia.
    feed IHδ; first by movet NEQ; apply: NP; lia.
    movet NEQ t'; move: NEQ.
    rewrite addnS !ltnS [_ t1 + δ]leq_eqVlt [t' t1 + δ]leq_eqVlt.
    move ⇒ /andP [LE1 /orP [/eqP EQ1 | LT1]] /andP [LE2 /orP [/eqP EQ2 | LT2]]; subst.
    { by done. }
    { moveSCHED; apply IHδ with (t' := (t1 + δ).-1) in SCHED; try lia.
      by apply: neg_pt_scheduled_before ⇒ //; apply NP; lia. }
    { have POS: t1 + δ > 0 by lia.
      moveSCHED; apply IHδ with (t := (t1 + δ).-1); try lia.
      apply: neg_pt_scheduled_at ⇒ //.
      { by rewrite (@ltn_predK 0) //. }
      { by rewrite (@ltn_predK 0) //; apply NP; lia. }
    }
    { by apply IHδ; lia. }
  Qed.

If we observe two different jobs scheduled at two points in time, then there necessarily is a preemption time in between.
  Lemma neq_scheduled_at_pt :
     j t,
      scheduled_at sched j t
       j' t',
        scheduled_at sched j' t'
        j != j'
        t t'
        exists2 pt, preemption_time arr_seq sched pt & t < pt t'.
  Proof.
    movej t SCHED j'.
    elim.
    { moveSCHED' NEQ /[!leqn0]/eqP EQ.
      exfalso; apply/neqP; [exact: NEQ|].
      apply: H_uniproc.
      - exact: SCHED.
      - by rewrite EQ. }
    { movet' IH SCHED' NEQ.
      rewrite leq_eqVlt ⇒ /orP [/eqP EQ|LT //].
      - exfalso; apply/neqP; [exact: NEQ|].
        by rewrite -EQ in SCHED'; exact: (H_uniproc _ _ _ _ SCHED SCHED').
      - have [PT|NPT] := boolP (preemption_time arr_seq sched t'.+1);
          first by t'.+1 ⇒ //; apply/andP; split.
        have [pt PT /andP [tpt ptt']] :
          exists2 pt, preemption_time arr_seq sched pt & t < pt t'.
        { apply: IH ⇒ //.
          by apply: neg_pt_scheduled_at. }
        by pt ⇒ //; apply/andP; split. }
  Qed.

End PreemptionTimes.

In this section, we prove a lemma relating scheduling and preemption times.
Section PreemptionFacts.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.

Allow for any uniprocessor model.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uniproc : uniprocessor_model PState.

  Context `{@JobReady Job PState Cost Arrival}.

Consider any valid arrival sequence.
Next, consider any valid schedule of this arrival sequence.
  Variable sched : schedule PState.
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.

In addition, we assume the existence of a function mapping jobs to their preemption points ...
  Context `{JobPreemptable Job}.

... and assume that it defines a valid preemption model.
We prove that every nonpreemptive segment always begins with a preemption time.
  Lemma scheduling_of_any_segment_starts_with_preemption_time:
     j t,
      scheduled_at sched j t
       pt,
        job_arrival j pt t
          preemption_time arr_seq sched pt
          ( t', pt t' t scheduled_at sched j t').
  Proof.
    intros s t SCHEDst.
    have EX: t', (t' t) && (scheduled_at sched s t')
                   && (all (fun t''scheduled_at sched s t'') (index_iota t' t.+1 )).
    { t. apply/andP; split; [ by apply/andP; split | ].
      apply/allP; intros t'.
      by rewrite mem_index_iota ltnS -eqn_leq; move ⇒ /eqP <-.
    }
    have MATE : jobs_must_arrive_to_execute sched by [].
    move : (H_sched_valid) ⇒ [COME_ARR READY].
    have MIN := ex_minnP EX.
    move: MIN ⇒ [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
    destruct mpt as [|mpt].
    - 0; repeat split.
      + by apply/andP; split ⇒ //; apply MATE.
      + eapply (zero_is_pt arr_seq); eauto 2.
      + by intros; apply ALL; rewrite mem_iota subn0 add0n ltnS.
    - have NSCHED: ~~ scheduled_at sched s mpt.
      { apply/negP; intros SCHED.
        enough (F : mpt < mpt); first by rewrite ltnn in F.
        apply MIN.
        apply/andP; split; [by apply/andP; split; [ apply ltnW | ] | ].
        apply/allP; intros t'.
        rewrite mem_index_iota; move ⇒ /andP [GE LE].
        move: GE; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ| LT].
        - by subst t'.
        - by apply ALL; rewrite mem_index_iota; apply/andP; split.
      }
      have PP: preemption_time arr_seq sched mpt.+1
        by eapply (first_moment_is_pt arr_seq) with (j := s); eauto 2.
       mpt.+1; repeat split⇒ //.
      + by apply/andP; split⇒ [|//]; apply MATE in SCHEDsmpt.
      + movet' /andP [GE LE].
        by apply ALL; rewrite mem_index_iota; apply/andP; split.
  Qed.

End PreemptionFacts.