Library prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Furthermore, we assume the fully non-preemptive task model.
Require Import prosa.model.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_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 ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost 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.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Next, consider any ideal non-preemptive uniprocessor schedule of
this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule 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.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
First we prove that if the cost of a job j is equal to 0, then
[job_run_to_completion_threshold j = 0] ...
Fact job_rtc_threshold_is_0:
∀ j,
job_cost j = 0 →
job_run_to_completion_threshold j = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 659)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
============================
forall j : Job, job_cost j = 0 -> job_run_to_completion_threshold j = 0
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 661)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
H3 : job_cost j = 0
============================
job_run_to_completion_threshold j = 0
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 746)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
H3 : job_cost j = 0
============================
job_run_to_completion_threshold j <= 0
----------------------------------------------------------------------------- *)
unfold job_run_to_completion_threshold.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 749)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
H3 : job_cost j = 0
============================
job_cost j - (job_last_nonpreemptive_segment j - ε) <= 0
----------------------------------------------------------------------------- *)
by rewrite H3; compute.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ j,
job_cost j = 0 →
job_run_to_completion_threshold j = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 659)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
============================
forall j : Job, job_cost j = 0 -> job_run_to_completion_threshold j = 0
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 661)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
H3 : job_cost j = 0
============================
job_run_to_completion_threshold j = 0
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 746)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
H3 : job_cost j = 0
============================
job_run_to_completion_threshold j <= 0
----------------------------------------------------------------------------- *)
unfold job_run_to_completion_threshold.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 749)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
H3 : job_cost j = 0
============================
job_cost j - (job_last_nonpreemptive_segment j - ε) <= 0
----------------------------------------------------------------------------- *)
by rewrite H3; compute.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... and ε otherwise.
Fact job_rtc_threshold_is_ε:
∀ j,
job_cost j > 0 →
arrives_in arr_seq j →
job_run_to_completion_threshold j = ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
============================
forall j : Job,
0 < job_cost j ->
arrives_in arr_seq j -> job_run_to_completion_threshold j = ε
----------------------------------------------------------------------------- *)
Proof.
intros ? ARRj POSj; unfold ε in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
ARRj : 0 < job_cost j
POSj : arrives_in arr_seq j
============================
job_run_to_completion_threshold j = 1
----------------------------------------------------------------------------- *)
unfold job_run_to_completion_threshold.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 678)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
ARRj : 0 < job_cost j
POSj : arrives_in arr_seq j
============================
job_cost j - (job_last_nonpreemptive_segment j - ε) = 1
----------------------------------------------------------------------------- *)
rewrite job_last_nps_is_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 685)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
ARRj : 0 < job_cost j
POSj : arrives_in arr_seq j
============================
job_cost j - (job_cost j - ε) = 1
----------------------------------------------------------------------------- *)
by rewrite subKn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ j,
job_cost j > 0 →
arrives_in arr_seq j →
job_run_to_completion_threshold j = ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
============================
forall j : Job,
0 < job_cost j ->
arrives_in arr_seq j -> job_run_to_completion_threshold j = ε
----------------------------------------------------------------------------- *)
Proof.
intros ? ARRj POSj; unfold ε in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 676)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
ARRj : 0 < job_cost j
POSj : arrives_in arr_seq j
============================
job_run_to_completion_threshold j = 1
----------------------------------------------------------------------------- *)
unfold job_run_to_completion_threshold.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 678)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
ARRj : 0 < job_cost j
POSj : arrives_in arr_seq j
============================
job_cost j - (job_last_nonpreemptive_segment j - ε) = 1
----------------------------------------------------------------------------- *)
rewrite job_last_nps_is_job_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 685)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
j : Job
ARRj : 0 < job_cost j
POSj : arrives_in arr_seq j
============================
job_cost j - (job_cost j - ε) = 1
----------------------------------------------------------------------------- *)
by rewrite subKn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Consider a task with a positive cost.
Then, we prove that [task_run_to_completion_threshold] 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 682)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
============================
valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 684)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
============================
task_rtc_bounded_by_cost tsk
subgoal 2 (ID 685) is:
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- by unfold task_rtc_bounded_by_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 685)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
============================
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- intros j ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 691)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
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
----------------------------------------------------------------------------- *)
rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 701)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_run_to_completion_threshold j <= ε
----------------------------------------------------------------------------- *)
edestruct (posnP (job_cost j)) as [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 726)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
ZERO : job_cost j = 0
============================
job_run_to_completion_threshold j <= ε
subgoal 2 (ID 727) is:
job_run_to_completion_threshold j <= ε
----------------------------------------------------------------------------- *)
+ by rewrite job_rtc_threshold_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 727)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
POS : 0 < job_cost j
============================
job_run_to_completion_threshold j <= ε
----------------------------------------------------------------------------- *)
+ by erewrite job_rtc_threshold_is_ε; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdFullyNonPreemptive.
Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.
valid_task_run_to_completion_threshold arr_seq tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 682)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
============================
valid_task_run_to_completion_threshold arr_seq tsk
----------------------------------------------------------------------------- *)
Proof.
intros; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 684)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
============================
task_rtc_bounded_by_cost tsk
subgoal 2 (ID 685) is:
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- by unfold task_rtc_bounded_by_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 685)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
============================
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- intros j ARR TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 691)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
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
----------------------------------------------------------------------------- *)
rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 701)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
============================
job_run_to_completion_threshold j <= ε
----------------------------------------------------------------------------- *)
edestruct (posnP (job_cost j)) as [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 726)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
ZERO : job_cost j = 0
============================
job_run_to_completion_threshold j <= ε
subgoal 2 (ID 727) is:
job_run_to_completion_threshold j <= ε
----------------------------------------------------------------------------- *)
+ by rewrite job_rtc_threshold_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 727)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
H_positive_cost : 0 < task_cost tsk
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
POS : 0 < job_cost j
============================
job_run_to_completion_threshold j <= ε
----------------------------------------------------------------------------- *)
+ by erewrite job_rtc_threshold_is_ε; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdFullyNonPreemptive.
Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.