Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export 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. *)
Section TaskRTCThresholdFullyNonPreemptive .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** We assume a fully non-preemptive task model. *)
#[local] Existing Instance fully_nonpreemptive_job_model .
#[local] Existing Instance fully_nonpreemptive_task_model .
#[local] Existing Instance fully_nonpreemptive_rtc_threshold .
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** Next, consider any non-preemptive unit-service schedule of the arrival sequence ... *)
Context {PState : ProcessorState Job}.
Hypothesis H_unit_service : unit_service_proc_model PState.
Variable sched : schedule PState.
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.
(** 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 :
forall j ,
job_cost j = 0 ->
job_rtct j = 0 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
move => j cj0.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 cj0 : job_cost j = 0
job_rtct j = 0
apply /eqP; rewrite eqn_leq; apply /andP; split => [|//].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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 cj0 : job_cost j = 0
job_rtct j <= 0
by rewrite /job_rtct cj0; compute .
Qed .
(** ... and ε otherwise. *)
Fact job_rtc_threshold_is_ε :
forall j ,
job_cost j > 0 ->
arrives_in arr_seq j ->
job_rtct j = ε.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 = 1
Proof .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 = 1
move => j ARRj POSj.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 jPOSj : arrives_in arr_seq j
job_rtct j = 1
unfold job_rtct.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 jPOSj : arrives_in arr_seq j
job_cost j - (job_last_nonpreemptive_segment j - 1 ) =
1
rewrite job_last_nps_is_job_cost.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 jPOSj : arrives_in arr_seq j
job_cost j - (job_cost j - 1 ) = 1
by rewrite subKn.
Qed .
(** Consider a task with a positive cost. *)
Variable tsk : Task.
Hypothesis H_positive_cost : 0 < task_cost tsk.
(** 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.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
intros ; split .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
by unfold task_rtc_bounded_by_cost.
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 tskj : Job ARR : arrives_in arr_seq j TSK : job_of_task tsk j
job_rtct j <= task_rtct tsk
move : TSK => /eqP <-; rewrite /fully_nonpreemptive_rtc_threshold.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 tskj : Job ARR : arrives_in arr_seq j
job_rtct j <= task_rtct (job_task j)
edestruct (posnP (job_cost j)) as [ZERO|POS].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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 tskj : Job ARR : arrives_in arr_seq j ZERO : job_cost j = 0
job_rtct j <= task_rtct (job_task j)
+ 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 tskj : Job ARR : arrives_in arr_seq j ZERO : job_cost j = 0
job_rtct j <= task_rtct (job_task j)
by rewrite job_rtc_threshold_is_0.
+ 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 tskj : Job ARR : arrives_in arr_seq j POS : 0 < job_cost j
job_rtct j <= task_rtct (job_task j)
by erewrite job_rtc_threshold_is_ε; eauto 2 .
Qed .
End TaskRTCThresholdFullyNonPreemptive .
Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_rt_facts.