Library prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive

Task's Run to Completion Threshold

In this section, we prove that instantiation of function task run to completion threshold to the fully non-preemptive model indeed defines a valid run-to-completion threshold function.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

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

We assume a fully non-preemptive task model.
  #[local] Existing Instance fully_nonpreemptive_job_model.
  #[local] Existing Instance fully_nonpreemptive_task_model.
  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.

Consider any arrival sequence with consistent arrivals.
Next, consider any ideal non-preemptive uniprocessor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
First we prove that if the cost of a job j is equal to 0, then job_rtct j = 0 ...
  Fact job_rtc_threshold_is_0:
     j,
      job_cost j = 0
      job_rtct j = 0.

... and ε otherwise.
  Fact job_rtc_threshold_is_ε:
     j,
      job_cost j > 0
      arrives_in arr_seq j
      job_rtct j = ε.

Consider a task with a positive cost.
  Variable tsk : Task.
  Hypothesis H_positive_cost : 0 < task_cost tsk.

Then, we prove that task_rtct function defines a valid task's run to completion threshold.
  Lemma fully_nonpreemptive_valid_task_run_to_completion_threshold:
    valid_task_run_to_completion_threshold arr_seq tsk.

End TaskRTCThresholdFullyNonPreemptive.
Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_rt_facts.