Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.model.task.preemption.fully_nonpreemptive.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
 
(** * 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 ideal non-preemptive uniprocessor schedule of
      this arrival sequence ... *)
  Variable sched : schedule (ideal.processor_state Job).
  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
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.
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
    intros.
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.
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.
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.
  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
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.
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 = ε
    intros ? ARRj POSj; unfold ε in *.
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.
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.
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.
  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
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.
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
    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
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
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
    -
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
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 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
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
    -
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.
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_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
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
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
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
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
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
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
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
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
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
POS: 0 < job_cost j
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
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
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
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
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.