Library prosa.analysis.facts.preemption.rtc_threshold.limited

Require Export prosa.analysis.facts.preemption.task.limited.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.model.task.preemption.limited_preemptive.

Task's Run to Completion Threshold

In this section, we prove that instantiation of function task run to completion threshold to the model with limited preemptions indeed defines a valid run-to-completion threshold function.
Section TaskRTCThresholdLimitedPreemptions.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskPreemptionPoints Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobPreemptionPoints Job}.

We assume a task model with fixed preemption points.
  #[local] Existing Instance limited_preemptive_job_model.
  #[local] Existing Instance limited_preemptions_rtc_threshold.

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

Next, consider any preemption-aware schedule of this arrival sequence...
  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.
  Hypothesis H_schedule_respects_preemption_model:
    schedule_respects_preemption_model arr_seq sched.

... where jobs do not execute before their arrival or after completion.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Consider an arbitrary task set ts.
  Variable ts : seq Task.

Assume that a job cost cannot be larger than a task cost.
  Hypothesis H_valid_job_cost:
    arrivals_have_valid_job_costs arr_seq.

Consider the model with fixed preemption points. I.e., each task is divided into a number of non-preemptive segments by inserting statically predefined preemption points.
  Hypothesis H_valid_fixed_preemption_points_model:
    valid_fixed_preemption_points_model arr_seq ts.

And consider any task from task set ts with positive cost.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.
  Hypothesis H_positive_cost : 0 < task_cost tsk.

We start by proving an auxiliary lemma. Note that since tsk has a positive cost, task_preemption_points tsk contains 0 and task_cost tsk. Thus, 2 ≤ size (task_preemption_points tsk).
  Remark number_of_preemption_points_in_task_at_least_two: 2 ≤ size (task_preemption_points tsk).
  Proof.
    move: (H_valid_fixed_preemption_points_model) ⇒ [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
    have Fact2: 0 < size (task_preemption_points tsk).
    { apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR ⇒ /eqP CONTR.
      move: (END _ H_tsk_in_ts) ⇒ EQ.
      move: EQ; rewrite /last0 -nth_last nth_default; last by rewrite CONTR.
      by move⇒ EQ; move: (H_positive_cost); rewrite EQ ltnn.
    }
    have EQ: 2 = size [::0; task_cost tsk] by [].
    rewrite EQ; clear EQ.
    apply subseq_leq_size.
    - rewrite !cons_uniq.
      apply/andP; split⇒ [|//].
      rewrite in_cons negb_or; apply/andP; split⇒ [|//].
      by rewrite neq_ltn; apply/orP; left.
    - intros t EQ; move: EQ; rewrite !in_cons.
      move ⇒ /orP[/eqP EQ | /orP[/eqP EQ|//]].
      + rewrite EQ; clear EQ.
        move: (BEG _ H_tsk_in_ts) ⇒ EQ.
        rewrite -EQ; clear EQ.
        rewrite /first0 -nth0.
        apply/(nthP 0).
        by ∃ 0.
      + rewrite EQ; clear EQ.
        move: (END _ H_tsk_in_ts) ⇒ EQ.
        rewrite -EQ; clear EQ.
        rewrite /last0 -nth_last.
        apply/(nthP 0).
        ∃ ((size (task_preemption_points tsk)).-1) ⇒ [|//].
        by rewrite -(leq_add2r 1) !addn1 prednK.
  Qed.

Then, we prove that task_rtct function defines a valid task's run to completion threshold.
  Lemma limited_valid_task_run_to_completion_threshold:
    valid_task_run_to_completion_threshold arr_seq tsk.
  Proof.
    split; first by rewrite /task_rtc_bounded_by_cost leq_subr.
    intros j ARR__j TSK__j. move: (H_valid_fixed_preemption_points_model) ⇒ [LJ LT].
    move: (LJ) (LT) ⇒ [ZERO__job [COST__job SORT__job]] [ZERO__task [COST__task [SORT__task [T4 [T5 T6]]]]].
    rewrite /job_rtct /task_rtct /limited_preemptions_rtc_threshold
            /job_last_nonpreemptive_segment /task_last_nonpr_segment /lengths_of_segments.
    case: (posnP (job_cost j)) ⇒ [Z|POS]; first by rewrite Z; compute.
    have J_RTCT__pos : 0 < job_last_nonpreemptive_segment j
      by eapply job_last_nonpreemptive_segment_positive; eauto using valid_fixed_preemption_points_model_lemma.
    have T_RTCT__pos : 0 < task_last_nonpr_segment tsk.
    { unfold job_respects_segment_lengths, task_last_nonpr_segment in ×.
      rewrite last0_nth; apply T6; eauto 2.
      have F: 1 ≤ size (distances (task_preemption_points tsk)).
      { apply leq_trans with (size (task_preemption_points tsk) - 1).
        - have F := number_of_preemption_points_in_task_at_least_two; lia.
        - rewrite [in X in X - 1]size_of_seq_of_distances; [lia | apply number_of_preemption_points_in_task_at_least_two].
      } lia.
    }
    have J_RTCT__le : job_last_nonpreemptive_segment j ≤ job_cost j
      by eapply job_last_nonpreemptive_segment_le_job_cost; eauto using valid_fixed_preemption_points_model_lemma.
    have T_RTCT__le : task_last_nonpr_segment tsk ≤ task_cost tsk.
    { unfold task_last_nonpr_segment. rewrite -COST__task //.
      eapply leq_trans; last by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
        by apply last_of_seq_le_max_of_seq.
    }
    rewrite subnBA // subnBA // -addnBAC // -addnBAC // !addn1 ltnS.
    erewrite job_parameters_last_np_to_job_limited; eauto 2.
    rewrite distances_positive_undup//.
    have → : job_cost j = last0 (undup (job_preemptive_points j)) by rewrite last0_undup; [rewrite -COST__job | apply SORT__job].
    rewrite last_seq_minus_last_distance_seq; last by apply nondecreasing_sequence_undup, SORT__job.
    apply leq_trans with( nth 0 (job_preemptive_points j) ((size (job_preemptive_points j)).-2)); first by apply undup_nth_le; eauto 2.
    have → : task_cost tsk = last0 (task_preemption_points tsk) by rewrite COST__task.
    rewrite last_seq_minus_last_distance_seq; last by apply SORT__task.
    move: TSK__j ⇒ /eqP TSK__j; rewrite -TSK__j.
    rewrite T4//.
    apply domination_of_distances_implies_domination_of_seq; try eauto 2.
    - erewrite zero_is_first_element; eauto.
    - eapply number_of_preemption_points_at_least_two; eauto 2.
    - by rewrite TSK__j; eapply number_of_preemption_points_in_task_at_least_two.
    - by apply SORT__task; rewrite TSK__j.
  Qed.

We show that the last non-preemptive segment of a task can be easily expressed in terms of the task cost and the task run-to-completion threshold.
  Lemma last_segment_eq_cost_minus_rtct :
    task_cost tsk - task_rtct tsk = task_last_nonpr_segment tsk - ε.
  Proof.
    move: (H_valid_fixed_preemption_points_model) ⇒ [MLP [BEG [END [INCR _]]]].
    rewrite /task_last_nonpr_segment /task_rtct /limited_preemptions_rtc_threshold.
    rewrite subKn // -[leqRHS]subn0 leq_sub //.
    apply leq_trans with (task_max_nonpreemptive_segment tsk).
    - by apply last_of_seq_le_max_of_seq.
    - rewrite -END; last by done.
      by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
  Qed.

End TaskRTCThresholdLimitedPreemptions.
Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_rt_facts.