Library prosa.analysis.facts.preemption.rtc_threshold.preemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Furthermore, we assume the fully preemptive task model.
Require Import prosa.model.preemption.fully_preemptive.
Require Import prosa.model.task.preemption.fully_preemptive.
Require Import prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Import prosa.model.task.preemption.fully_preemptive.
Require Import prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Task's Run to Completion Threshold
In this section, we prove that instantiation of function [task run to completion threshold] to the fully preemptive model indeed defines a valid run-to-completion threshold function.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Next, consider any arrival sequence ...
... and assume that a job cost cannot be larger than a task cost.
Then, we prove that [task_rtct] function
defines a valid task's run to completion threshold.
Lemma fully_preemptive_valid_task_run_to_completion_threshold:
∀ tsk, valid_task_run_to_completion_threshold arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 647)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
============================
forall tsk : Task, valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 650)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
============================
task_rtc_bounded_by_cost tsk
subgoal 2 (ID 651) is:
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- by rewrite /task_rtc_bounded_by_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 651)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
============================
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- intros j ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 662)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_rtct j <= task_rtct tsk
----------------------------------------------------------------------------- *)
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 666)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_cost j <= task_rtct tsk
----------------------------------------------------------------------------- *)
by rewrite-TSK; apply H_valid_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdFullyPreemptiveModel.
Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.
∀ tsk, valid_task_run_to_completion_threshold arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 647)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
============================
forall tsk : Task, valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 650)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
============================
task_rtc_bounded_by_cost tsk
subgoal 2 (ID 651) is:
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- by rewrite /task_rtc_bounded_by_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 651)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
============================
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- intros j ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 662)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_rtct j <= task_rtct tsk
----------------------------------------------------------------------------- *)
apply leq_trans with (job_cost j); eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 666)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobCost Job
arr_seq : arrival_sequence Job
H_valid_job_cost : arrivals_have_valid_job_costs arr_seq
tsk : Task
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_cost j <= task_rtct tsk
----------------------------------------------------------------------------- *)
by rewrite-TSK; apply H_valid_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdFullyPreemptiveModel.
Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.