# 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).
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.
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 - ε.
End TaskRTCThresholdLimitedPreemptions.
Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_rt_facts.