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.

Furthermore, we assume the task model with fixed preemption points.

Require Import prosa.model.preemption.limited_preemptive.
Require Import 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}.

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 ideal uniprocessor schedule of this arrival sequence ...

  Variable sched : schedule (ideal.processor_state Job).
  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_run_to_completion_threshold 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.
Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.