Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.task.preemption.parameters.

(** * Run-to-Completion Threshold *) 
(** In this section, we provide a few basic properties 
    of run-to-completion-threshold-compilant 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
      maping jobs to theirs preemption points. *)
  Context `{JobPreemptable Job}.

  (** Consider any kind of processor state model, ... *)
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

  (** ... 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]. *)
  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 *.
      rewrite index_iota_lt_step; last by done.
        by simpl; rewrite 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 iota_add 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]); last by done.
      apply subseq_leq_size.
      - apply/andP; split. rewrite !in_cons Bool.negb_orb.
        + apply/andP; split. by rewrite neq_ltn POS. by done.
        + apply/andP; split; by done. 
      - 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 done.
    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 iota_add; destruct (iota 0 (job_cost j)). 
      + unfold range, index_iota; rewrite subn0 -addn1.
          by rewrite iota_add last0_cat //. 
      + by apply A2.
    Qed.
    
    (** Last nonpreemptive 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; first by done. 
        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.
        rewrite prednK ?ltnS; first by done. 
          by rewrite ltnW //; apply 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_run_to_completion_threshold j.
  Proof.
    intros COST; unfold job_run_to_completion_threshold, ε.
    have N1 := job_last_nonpreemptive_segment_positive COST.
    have N2 := job_last_nonpreemptive_segment_le_job_cost.
    ssromega.
  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_run_to_completion_threshold 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:
    forall (ρ : duration), 
      job_run_to_completion_threshold j <= ρ < job_cost j ->
      ~~ job_preemptable j ρ.
  Proof.
    move => ρ /andP [GE LT].
    apply/negP; intros C.
    have POS : 0 < job_cost j; first by ssromega.
    rewrite /job_run_to_completion_threshold subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
    rewrite -subh1 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; first by done.
      rewrite prednK; first by rewrite -last0_nth.
      rewrite -(leq_add2r 1) !addn1 prednK.
      - by apply size_of_preemption_points.
      - by eapply leq_trans; last apply size_of_preemption_points.
    }
    move: EQ => /negP EQ; apply: EQ.
    apply conversion_preserves_equivalence; try done.
    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: 
    forall t t',
      t <= t' ->
      job_run_to_completion_threshold j <= service sched j t ->
      ~~ completed_by sched j t' ->
      scheduled_at sched j t'.
  Proof.
    intros ? ? LE TH COM.
    apply H_valid_preemption_model; first by done.
    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_facts, so Coq 
    will be able to apply them automatically. *)   
Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.