Library prosa.analysis.facts.preemption.rtc_threshold.job_preemptable

Run-to-Completion Threshold

In this section, we provide a few basic properties of run-to-completion-threshold-compliant schedules.
Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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

Consider any kind of processor state model, ...
  Context {PState : ProcessorState Job}.

... any job arrival sequence, ...
  Variable arr_seq: arrival_sequence Job.

... and any given schedule.
  Variable sched: schedule PState.

Assume that the preemption model is valid.
Consider an arbitrary job j from the arrival sequence.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.

First we prove a few auxiliary lemmas about job_preemption_points.
  Section AuxiliaryLemmas.

We prove that the sequence of preemption points of a zero-cost job consists of one element -- 0.
    Lemma preemption_points_of_zero_cost_job:
      job_cost j = 0
      job_preemption_points j = [::0].
    Proof.
      intros ZERO.
      destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
      unfold job_preemption_points; rewrite ZERO; simpl.
      simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
        by rewrite A1.
    Qed.

For a positive-cost job, 0 ...
    Lemma zero_in_preemption_points:
      0 < job_cost j
      0 \in job_preemption_points j.
    Proof.
      intros POS.
      unfold job_preemption_points, range.
      destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
      unfold job_cannot_become_nonpreemptive_before_execution in ×.
      by rewrite index_iota_lt_step//= A1 in_cons eq_refl.
    Qed.

... and job_cost are in preemption points.
    Lemma job_cost_in_preemption_points:
      0 < job_cost j
      job_cost j \in job_preemption_points j.
    Proof.
      intros POS.
      unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.
      rewrite iotaD add0n filter_cat mem_cat.
      apply/orP; right; simpl.
      destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
      unfold job_cannot_be_nonpreemptive_after_completion in ×.
        by rewrite A2 in_cons eq_refl.
    Qed.

Therefore, for a positive-cost job size of the sequence of preemption points is at least two.
    Lemma size_of_preemption_points:
      0 < job_cost j
      2 size (job_preemption_points j).
    Proof.
      intros POS.
      replace 2 with (size [::0; job_cost j]) ⇒ [|//].
      apply subseq_leq_size.
      - apply/andP; split.
        + rewrite !in_cons Bool.negb_orb.
          by apply/andP; split; [rewrite neq_ltn POS|].
        + by [].
      - intros ρ; rewrite !in_cons; move ⇒ /orP [/eqP EQ| /orP [/eqP Cost | C]].
        + by subst; apply zero_in_preemption_points.
        + by subst; apply job_cost_in_preemption_points.
        + by [].
    Qed.

Next we show that the sequence of preemption points is a non-decreasing sequence.
Next, we prove that the last element of the sequence of preemption points is job_cost.
    Lemma job_cost_is_last_element_of_preemption_points:
      job_cost j = last0 (job_preemption_points j).
    Proof.
      unfold job_preemption_points.
      edestruct H_valid_preemption_model as [A1 [A2 [A3 A4]]]; eauto 2.
      erewrite last0_filter.
      + by apply/eqP; apply eq_refl.
      + unfold range, index_iota; rewrite subn0 -addn1.
          by rewrite iotaD; destruct (iota 0 (job_cost j)).
      + unfold range, index_iota; rewrite subn0 -addn1.
          by rewrite iotaD last0_cat //.
      + by apply A2.
    Qed.

Last non-preemptive segment of a positive-cost job has positive length.
    Lemma job_last_nonpreemptive_segment_positive:
      job_cost_positive j
      0 < job_last_nonpreemptive_segment j.
    Proof.
      intros COST. unfold job_last_nonpreemptive_segment.
      rewrite last0_nth function_of_distances_is_correct subn_gt0.
      rewrite [size _]pred_Sn -addn1-addn1.
      rewrite -size_of_seq_of_distances ?addn1; last by apply size_of_preemption_points.
      rewrite prednK; last first.
      { rewrite -(leq_add2r 1) !addn1 prednK.
        - apply size_of_preemption_points; eauto.
        - rewrite ltnW //; apply size_of_preemption_points; eauto.
      }
      apply iota_is_increasing_sequence; apply/andP; split.
      - rewrite -(leq_add2r 2) !addn2.
        rewrite prednK//.
        rewrite -(leq_add2r 1) !addn1.
        rewrite prednK.
        + by apply size_of_preemption_points.
        + by rewrite ltnW //; apply size_of_preemption_points.
      - rewrite -(leq_add2r 1) !addn1.
        unfold job_preemption_points, range.
        by rewrite prednK ?ltnS// ltnW// size_of_preemption_points.
    Qed.

Max nonpreemptive segment of a positive-cost job has positive length.
    Lemma job_max_nonpreemptive_segment_positive:
      job_cost_positive j
      0 < job_max_nonpreemptive_segment j.
    Proof.
      intros COST.
      eapply leq_trans.
      - by apply job_last_nonpreemptive_segment_positive.
      - by apply last_of_seq_le_max_of_seq.
    Qed.

Next we show that max nonpreemptive segment is at most the cost of a job.
    Lemma job_max_nonpreemptive_segment_le_job_cost:
      job_max_nonpreemptive_segment j job_cost j.
    Proof.
      eapply leq_trans.
      - apply max_distance_in_seq_le_last_element_of_seq; apply preemption_points_nondecreasing.
      - destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
      case: (posnP (job_cost j)) ⇒ [ZERO|POSt].
      { unfold job_preemption_points; rewrite ZERO.
        simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
          by rewrite A1.
      }
      { eapply leq_trans; first apply last_of_seq_le_max_of_seq.
        rewrite job_cost_is_last_element_of_preemption_points.
        apply last_is_max_in_nondecreasing_seq; first by apply preemption_points_nondecreasing.
        apply max0_in_seq.
        have LL := size_of_preemption_points POSt.
          by destruct (job_preemption_points j).
      }
    Qed.

We also show that last nonpreemptive segment is at most the cost of a job.
    Lemma job_last_nonpreemptive_segment_le_job_cost:
      job_last_nonpreemptive_segment j job_cost j.
    Proof.
      eapply leq_trans.
      - apply last_of_seq_le_max_of_seq.
      - apply job_max_nonpreemptive_segment_le_job_cost.
    Qed.

  End AuxiliaryLemmas.

We prove that the run-to-completion threshold is positive for any job with positive cost. I.e., in order to become non-preemptive a job must receive at least one unit of service.
  Lemma job_run_to_completion_threshold_positive:
    job_cost_positive j
    0 < job_rtct j.
  Proof.
    intros COST; unfold job_rtct.
    have N1 := job_last_nonpreemptive_segment_positive COST.
    have N2 := job_last_nonpreemptive_segment_le_job_cost.
    lia.
  Qed.

Next we show that the run-to-completion threshold is at most the cost of a job.
  Lemma job_run_to_completion_threshold_le_job_cost:
    job_rtct j job_cost j.
  Proof. by apply leq_subr. Qed.

We prove that a job cannot be preempted during execution of the last segment.
  Lemma job_cannot_be_preempted_within_last_segment:
     (ρ : duration),
      job_rtct j ρ < job_cost j
      ~~ job_preemptable j ρ.
  Proof.
    move ⇒ ρ /andP [GE LT].
    apply/negP; intros C.
    have POS : 0 < job_cost j; first by lia.
    rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
    rewrite -addnBAC in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
    rewrite job_cost_is_last_element_of_preemption_points in LT, GE.
    rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.
    have EQ := antidensity_of_nondecreasing_seq.
    specialize (EQ (job_preemption_points j) ρ (size (job_preemption_points j)).-2 ).
    feed_n 2 EQ; first by apply preemption_points_nondecreasing.
    { apply/andP; split⇒ [//|].
      rewrite prednK; first by rewrite -last0_nth.
      rewrite -(leq_add2r 1) !addn1 prednK.
      - exact: size_of_preemption_points.
      - by eapply leq_trans; last apply size_of_preemption_points.
    }
    move: EQ ⇒ /negP EQ; apply: EQ.
    apply conversion_preserves_equivalence ⇒ //.
    eapply leq_trans; first by apply ltnW; exact LT.
    by rewrite job_cost_is_last_element_of_preemption_points.
  Qed.

In order to get a consistent schedule, the scheduler should respect the notion of run-to-completion threshold. We assume that, after a job reaches its run-to-completion threshold, it cannot be preempted until its completion.
  Lemma job_nonpreemptive_after_run_to_completion_threshold:
     t t',
      t t'
      job_rtct j service sched j t
      ~~ completed_by sched j t'
      scheduled_at sched j t'.
  Proof.
    movet t' LE TH COM.
    apply H_valid_preemption_model ⇒ [//|].
    apply job_cannot_be_preempted_within_last_segment; apply/andP; split.
    - by apply leq_trans with (service sched j t); last apply service_monotonic.
    - by rewrite ltnNge.
  Qed.

End RunToCompletionThreshold.

We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically.
Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_rt_facts.