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

Require Export prosa.model.job.properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.model.task.preemption.parameters.

Run-to-Completion Threshold

In this section, we provide a few basic properties of run-to-completion-threshold-compliant schedules.
Section RunToCompletionThreshold.

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.
  Hypothesis H_valid_preemption_model :
    valid_preemption_model arr_seq sched.

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.
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 ⇒ /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.
  Lemma preemption_points_nondecreasing :
    nondecreasing_sequence (job_preemption_points j).
  Proof. by apply increasing_implies_nondecreasing, iota_is_increasing_sequence. Qed.

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.

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.
    move⇒ t 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.