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.
[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] ... *)
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
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
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
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. *)
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
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
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 j
POSj: arrives_in arr_seq j

job_rtct j = 1
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 j
POSj: arrives_in arr_seq j

job_cost j - (job_last_nonpreemptive_segment j - 1) = 1
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 j
POSj: 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. *)
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
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
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
job_respects_task_rtc 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

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
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
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j

job_rtct j <= task_rtct 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
j: Job
ARR: arrives_in arr_seq j

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 tsk
j: 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 tsk
j: Job
ARR: arrives_in arr_seq j
POS: 0 < job_cost j
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 tsk
j: 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 tsk
j: 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.