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

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.
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.
Next, consider any ideal uniprocessor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Consider an arbitrary task set ts.
  Variable ts : seq Task.

Assume that a job cost cannot be larger than a task cost.
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.
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).
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.

End TaskRTCThresholdLimitedPreemptions.
Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_rt_facts.