Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import job task.
From rt.restructuring.model.preemption Require Import
job.parameters task.parameters rtc_threshold.valid_rtct
job.instance.limited task.instance.floating rtc_threshold.instance.floating.
From rt.restructuring.analysis.basic_facts.preemption Require Import
job.limited task.floating 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 47)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
============================
forall tsk : Task, valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 50)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
============================
task_run_to_completion_threshold_le_task_cost tsk
subgoal 2 (ID 51) is:
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
arr_seq tsk
----------------------------------------------------------------------------- *)
- by rewrite /task_run_to_completion_threshold_le_task_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
============================
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
arr_seq tsk
----------------------------------------------------------------------------- *)
- intros j ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_cost j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
by rewrite-TSK; apply H_job_cost_le_task_cost.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 47)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
============================
forall tsk : Task, valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 50)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
============================
task_run_to_completion_threshold_le_task_cost tsk
subgoal 2 (ID 51) is:
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
arr_seq tsk
----------------------------------------------------------------------------- *)
- by rewrite /task_run_to_completion_threshold_le_task_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
============================
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
arr_seq tsk
----------------------------------------------------------------------------- *)
- intros j ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
H2 : JobPreemptable Job
arr_seq : arrival_sequence Job
H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_cost j <= task_run_to_completion_threshold tsk
----------------------------------------------------------------------------- *)
by rewrite-TSK; apply H_job_cost_le_task_cost.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdFloatingNonPreemptiveRegions.
Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.