shifted_job_costs.v

Require Export prosa.analysis.facts.periodic.arrival_times.[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.analysis.facts.periodic.task_arrivals_size.
Require Export prosa.model.task.concept.
Require Export prosa.analysis.facts.hyperperiod.

(** In this file we define a new function for job costs
    in an observation interval and prove its validity. *)
Section ValidJobCostsShifted.

  (** Consider any type of periodic tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.
  Context `{TaskCost Task}.

  (** ... and any type of jobs. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobDeadline Job}.

  (** Consider a consistent arrival sequence with non-duplicate arrivals. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** Furthermore, assume that arrivals have valid job costs. *)
  Hypothesis H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq.

  (** Consider a periodic task set [ts] such that all tasks in
      [ts] have valid periods and offsets. *)
  Variable ts : TaskSet Task.
  Hypothesis H_periodic_taskset: taskset_respects_periodic_task_model arr_seq ts.
  Hypothesis H_valid_periods_in_taskset: valid_periods ts.
  Hypothesis H_valid_offsets_in_taskset: valid_offsets arr_seq ts.

  (** Consider a job [j] that stems from the arrival sequence. *)
  Variable j : Job.
  Hypothesis H_j_from_arrival_sequence: arrives_in arr_seq j.

  (** Let [O_max] denote the maximum task offset of all tasks in [ts] ... *)
  Let O_max := max_task_offset ts.
  (** ... and let [HP] denote the hyperperiod of all tasks in [ts]. *)
  Let HP := hyperperiod ts.

  (** We now define a new function for job costs in the observation interval. *)

  (** Given that job [j] arrives after [O_max], the cost of a job [j']
   that arrives in the interval <<[O_max + HP, O_max + 2HP)>> is defined to
   be the same as the job cost of its corresponding job in [j]'s hyperperiod. *)
  Definition job_costs_shifted (j' : Job) :=
    if (job_arrival j >= O_max) && (O_max + HP <= job_arrival j' < O_max + 2 * HP) then
      job_cost (corresponding_job_in_hyperperiod ts arr_seq j' (starting_instant_of_corresponding_hyperperiod ts j) (job_task j'))
    else job_cost j'.

  (** Assume that we have an infinite sequence of jobs. *)
  Hypothesis H_infinite_jobs: infinite_jobs arr_seq.

  (** Assume all jobs in the arrival sequence [arr_seq] belong to some task
   in [ts]. *)
  Hypothesis H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts.

  (** We assign the job costs as defined by the [job_costs_shifted] function. *)
  Instance job_costs_in_oi : JobCost Job :=
    job_costs_shifted.

  (** We show that the [job_costs_shifted] function is valid. *)
  Lemma job_costs_shifted_valid: arrivals_have_valid_job_costs arr_seq.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
arrivals_have_valid_job_costs arr_seq
  Proof.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
arrivals_have_valid_job_costs arr_seq
    rewrite /arrivals_have_valid_job_costs /valid_job_cost.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
forall j : Job,
arrives_in arr_seq j ->
job_cost j <= task_cost (job_task j)
    intros j' ARR.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
job_cost j' <= task_cost (job_task j')
    unfold job_cost; rewrite /job_costs_in_oi /job_costs_shifted.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
(if
  [&& O_max <= job_arrival j,
      O_max + HP <= job_arrival j'
    & job_arrival j' < O_max + 2 * HP]
 then
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod
          ts j) (job_task j'))
 else job_cost j') <= task_cost (job_task j')
    destruct (leqP O_max (job_arrival j)) as [A | B];
      last by apply H_arrivals_have_valid_job_costs => //.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
(if
  [&& true, O_max + HP <= job_arrival j'
    & job_arrival j' < O_max + 2 * HP]
 then
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod
          ts j) (job_task j'))
 else job_cost j') <= task_cost (job_task j')
    destruct (leqP (O_max + HP) (job_arrival j')) as [NEQ | NEQ];
      last by apply H_arrivals_have_valid_job_costs => //.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
(if [&& true, true & job_arrival j' < O_max + 2 * HP]
 then
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod
          ts j) (job_task j'))
 else job_cost j') <= task_cost (job_task j')
    destruct (leqP (O_max + 2 * HP) (job_arrival j')) as [LT | LT];
      first by apply H_arrivals_have_valid_job_costs => //.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP
(if [&& true, true & true]
 then
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod
          ts j) (job_task j'))
 else job_cost j') <= task_cost (job_task j')
    specialize (corresponding_jobs_have_same_task arr_seq ts j' j) => TSK.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP
TSK: job_task
  (corresponding_job_in_hyperperiod ts arr_seq
     j'
     (starting_instant_of_corresponding_hyperperiod
        ts j) 
     (job_task j')) = 
job_task j'
(if [&& true, true & true]
 then
  job_cost
    (corresponding_job_in_hyperperiod ts arr_seq j'
       (starting_instant_of_corresponding_hyperperiod
          ts j) (job_task j'))
 else job_cost j') <= task_cost (job_task j')
    rewrite -[in X in _ <= task_cost X]TSK.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP
TSK: job_task
  (corresponding_job_in_hyperperiod ts arr_seq
     j'
     (starting_instant_of_corresponding_hyperperiod
        ts j) 
     (job_task j')) = 
job_task j'
job_cost
  (corresponding_job_in_hyperperiod ts arr_seq j'
     (starting_instant_of_corresponding_hyperperiod ts
        j) (job_task j')) <=
task_cost
  (job_task
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod
           ts j) (job_task j')))
    have IN : job_task j' \in ts by apply H_jobs_from_taskset.Task: TaskType
H: TaskOffset Task
H0: PeriodicModel Task
H1: TaskCost Task
Job: JobType
H2: JobTask Job Task
H3: JobArrival Job
H4: JobCost Job
H5: JobDeadline Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs
  arr_seq
ts: TaskSet Task
H_periodic_taskset: taskset_respects_periodic_task_model
  arr_seq ts
H_valid_periods_in_taskset: valid_periods ts
H_valid_offsets_in_taskset: valid_offsets arr_seq ts
j: Job
H_j_from_arrival_sequence: arrives_in arr_seq j
O_max:= max_task_offset ts: nat
HP:= hyperperiod ts: duration
H_infinite_jobs: infinite_jobs arr_seq
H_jobs_from_taskset: all_jobs_from_taskset arr_seq ts
j': Job
ARR: arrives_in arr_seq j'
A: O_max <= job_arrival j
NEQ: O_max + HP <= job_arrival j'
LT: job_arrival j' < O_max + 2 * HP
TSK: job_task
  (corresponding_job_in_hyperperiod ts arr_seq
     j'
     (starting_instant_of_corresponding_hyperperiod
        ts j) 
     (job_task j')) = 
job_task j'
IN: job_task j' \in ts
job_cost
  (corresponding_job_in_hyperperiod ts arr_seq j'
     (starting_instant_of_corresponding_hyperperiod ts
        j) (job_task j')) <=
task_cost
  (job_task
     (corresponding_job_in_hyperperiod ts arr_seq j'
        (starting_instant_of_corresponding_hyperperiod
           ts j) (job_task j')))
    by apply H_arrivals_have_valid_job_costs, corresponding_job_arrives => //; lia.
  Qed.

End ValidJobCostsShifted.