Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating
Require Import rt.restructuring.model.preemption.limited_preemptive.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Export rt.restructuring.analysis.basic_facts.preemption.task.floating.
Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Task's Run to Completion Threshold
In this section, we instantiate function task run to completion threshold for the model with floating non-preemptive regions.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
Consider any arrival sequence.
Assume that a job cost cannot be larger than a task cost.
Then, we prove that task_run_to_completion_threshold function
defines a valid task's run to completion threshold.
Lemma floating_preemptive_valid_task_run_to_completion_threshold:
∀ tsk, valid_task_run_to_completion_threshold arr_seq tsk.
Proof.
intros; split.
- by rewrite /task_run_to_completion_threshold_le_task_cost.
- intros j ARR TSK.
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
by rewrite-TSK; apply H_job_cost_le_task_cost.
Qed.
End TaskRTCThresholdFloatingNonPreemptiveRegions.
Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.
∀ tsk, valid_task_run_to_completion_threshold arr_seq tsk.
Proof.
intros; split.
- by rewrite /task_run_to_completion_threshold_le_task_cost.
- intros j ARR TSK.
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
by rewrite-TSK; apply H_job_cost_le_task_cost.
Qed.
End TaskRTCThresholdFloatingNonPreemptiveRegions.
Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.