Library prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
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_rtct j = 0] ...
Fact job_rtc_threshold_is_0:
∀ j,
job_cost j = 0 →
job_rtct j = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
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_rtct j = 0
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
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_rtct j = 0
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 130)
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_rtct j <= 0
----------------------------------------------------------------------------- *)
unfold job_rtct.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
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_rtct j = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 43)
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_rtct j = 0
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
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_rtct j = 0
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 130)
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_rtct j <= 0
----------------------------------------------------------------------------- *)
unfold job_rtct.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
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_rtct j = ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 54)
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_rtct j = ε
----------------------------------------------------------------------------- *)
Proof.
intros ? ARRj POSj; unfold ε in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
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_rtct j = 1
----------------------------------------------------------------------------- *)
unfold job_rtct.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
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 67)
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_rtct j = ε.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 54)
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_rtct j = ε
----------------------------------------------------------------------------- *)
Proof.
intros ? ARRj POSj; unfold ε in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
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_rtct j = 1
----------------------------------------------------------------------------- *)
unfold job_rtct.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
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 67)
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_rtct] 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 65)
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 67)
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 68) is:
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- by unfold task_rtc_bounded_by_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
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 73)
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_rtct j <= task_rtct tsk
----------------------------------------------------------------------------- *)
rewrite -TSK /fully_nonpreemptive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
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_rtct j <= task_rtct (job_task j)
----------------------------------------------------------------------------- *)
edestruct (posnP (job_cost j)) as [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 103)
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_rtct j <= task_rtct (job_task j)
subgoal 2 (ID 104) is:
job_rtct j <= task_rtct (job_task j)
----------------------------------------------------------------------------- *)
+ by rewrite job_rtc_threshold_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 104)
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_rtct j <= task_rtct (job_task j)
----------------------------------------------------------------------------- *)
+ by erewrite job_rtc_threshold_is_ε; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdFullyNonPreemptive.
Global 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 65)
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 67)
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 68) is:
job_respects_task_rtc arr_seq tsk
----------------------------------------------------------------------------- *)
- by unfold task_rtc_bounded_by_cost.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
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 73)
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_rtct j <= task_rtct tsk
----------------------------------------------------------------------------- *)
rewrite -TSK /fully_nonpreemptive.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
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_rtct j <= task_rtct (job_task j)
----------------------------------------------------------------------------- *)
edestruct (posnP (job_cost j)) as [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 103)
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_rtct j <= task_rtct (job_task j)
subgoal 2 (ID 104) is:
job_rtct j <= task_rtct (job_task j)
----------------------------------------------------------------------------- *)
+ by rewrite job_rtc_threshold_is_0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 104)
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_rtct j <= task_rtct (job_task j)
----------------------------------------------------------------------------- *)
+ by erewrite job_rtc_threshold_is_ε; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskRTCThresholdFullyNonPreemptive.
Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.