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]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_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 j
POSj: 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 j
POSj: 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 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. *)
  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
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 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 tsk
j: 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 tsk
j: 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 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.