# 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 /limited_preemptions_rtc_threshold /task_rtct
/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 /limited_preemptions_rtc_threshold /task_rtct.
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.