Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive
Require Export rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Require Import rt.restructuring.model.preemption.fully_nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
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 : is_nonpreemptive_schedule sched.
Hypothesis H_nonpreemptive_sched : is_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.
Proof.
intros.
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
unfold job_run_to_completion_threshold.
by rewrite H3; compute.
Qed.
∀ j,
job_cost j = 0 →
job_run_to_completion_threshold j = 0.
Proof.
intros.
apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
unfold job_run_to_completion_threshold.
by rewrite H3; compute.
Qed.
... and ε otherwise.
Fact job_rtc_threshold_is_ε:
∀ j,
job_cost j > 0 →
arrives_in arr_seq j →
job_run_to_completion_threshold j = ε.
Proof.
intros ? ARRj POSj; unfold ε in ×.
unfold job_run_to_completion_threshold.
rewrite job_last_nps_is_job_cost.
by rewrite subKn.
Qed.
∀ j,
job_cost j > 0 →
arrives_in arr_seq j →
job_run_to_completion_threshold j = ε.
Proof.
intros ? ARRj POSj; unfold ε in ×.
unfold job_run_to_completion_threshold.
rewrite job_last_nps_is_job_cost.
by rewrite subKn.
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.
Proof.
intros; split.
- by unfold task_run_to_completion_threshold_le_task_cost.
- intros j ARR TSK.
rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
edestruct (posnP (job_cost j)) as [ZERO|POS].
+ by rewrite job_rtc_threshold_is_0.
+ by erewrite job_rtc_threshold_is_ε; eauto 2.
Qed.
End TaskRTCThresholdFullyNonPreemptive.
Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.
valid_task_run_to_completion_threshold arr_seq tsk.
Proof.
intros; split.
- by unfold task_run_to_completion_threshold_le_task_cost.
- intros j ARR TSK.
rewrite -TSK /task_run_to_completion_threshold /fully_nonpreemptive.
edestruct (posnP (job_cost j)) as [ZERO|POS].
+ by rewrite job_rtc_threshold_is_0.
+ by erewrite job_rtc_threshold_is_ε; eauto 2.
Qed.
End TaskRTCThresholdFullyNonPreemptive.
Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.