Require Export analysis.abstract.ideal.iw_instantiation.
[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]

(** In this file, we prove some inequalities that always
    hold inside the busy interval of a job. Throughout this file we
    assume the ideal uniprocessor model. *)
Section BusyIntervalInequalities.

  (** Consider any kind of tasks and their jobs, each characterized by
      an arrival time, a cost, and an arbitrary notion of readiness. *)
  Context {Task : TaskType} {Job : JobType} `{JobTask Job Task}.
  Context `{JobArrival Job} `{JobCost Job} {JR :JobReady Job (ideal.processor_state Job)}.

  (** Consider a JLFP policy that is reflexive and respects sequential tasks. *)
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_policy_is_reflexive : reflexive_job_priorities JLFP.
  Hypothesis H_policy_respecsts_sequential_tasks : policy_respects_sequential_tasks JLFP.

  (** Consider a consistent arrival sequence that does not contain duplicates. *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** Consider any valid ideal uniprocessor schedule defined over this arrival sequence. *)
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_valid_schedule : valid_schedule sched  arr_seq.

  (** Consider a set of tasks [ts] that contains all the jobs in the
      arrival sequence. *)
  Variable ts : list Task.
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

  (** Consider a task [tsk]. *)
  Variable tsk : Task.

  (** Consider a job [j] of the task [tsk] that has a positive job cost. *)
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_of_task tsk j.
  Hypothesis H_job_cost_positive: job_cost_positive j.

  (** Consider the ideal JLFP definitions of interference and
      interfering workload. *)
  #[local] Instance ideal_jlfp_interference : Interference Job :=
    ideal_jlfp_interference arr_seq sched.

  #[local] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
    ideal_jlfp_interfering_workload arr_seq sched.

  (** Consider the busy interval for j is given by <<[t1,t2)>>. *)
  Variable t1 t2 : duration.
  Hypothesis H_busy_interval : definitions.busy_interval sched j t1 t2.

  (** Let us denote the relative arrival time by [A]. *)
  Let A := job_arrival j - t1.

  (** Consider any arbitrary time [Δ] inside the busy interval. *)
  Variable  Δ : duration.
  Hypothesis H_Δ_in_busy : t1 + Δ <= t2.

  (** First, we prove that if the priority inversion is bounded then,
      the cumulative priority inversion is also bounded. *)
  Section PIBound.

    (** Consider the priority inversion in any given interval
        is bounded by a constant. *)
    Variable priority_inversion_bound : duration -> duration.
    Hypothesis H_priority_inversion_is_bounded :
      priority_inversion_is_bounded_by arr_seq sched tsk priority_inversion_bound.

    (** Then, the cumulative priority inversion in any interval
        is also bounded. *)
    Lemma cumulative_priority_inversion_is_bounded:
      cumulative_priority_inversion arr_seq sched j t1 (t1 + Δ)
      <= priority_inversion_bound (job_arrival j - t1).
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
cumulative_priority_inversion arr_seq sched j t1
  (t1 + Δ) <=
priority_inversion_bound (job_arrival j - t1)
    Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
cumulative_priority_inversion arr_seq sched j t1
  (t1 + Δ) <=
priority_inversion_bound (job_arrival j - t1)
      apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 t2).
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
cumulative_priority_inversion arr_seq sched j t1
  (t1 + Δ) <=
cumulative_priority_inversion arr_seq sched j t1 t2
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
cumulative_priority_inversion arr_seq sched j t1 t2 <=
priority_inversion_bound (job_arrival j - t1)
      -
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
cumulative_priority_inversion arr_seq sched j t1
  (t1 + Δ) <=
cumulative_priority_inversion arr_seq sched j t1 t2 rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1  + Δ)) //=; try by lia.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
cumulative_priority_inversion arr_seq sched j t1
  (t1 + Δ) <=
\sum_(t1 <= i < t1 + Δ)
   priority_inversion arr_seq sched j i +
\sum_(t1 + Δ <= i < t2)
   priority_inversion arr_seq sched j i
        by rewrite /priority_inversion leq_addr.
      -
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
cumulative_priority_inversion arr_seq sched j t1 t2 <=
priority_inversion_bound (job_arrival j - t1) apply: H_priority_inversion_is_bounded => //.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
priority_inversion_bound: duration -> duration
H_priority_inversion_is_bounded: priority_inversion_is_bounded_by
  arr_seq sched tsk
  priority_inversion_bound
busy_interval_prefix arr_seq sched j t1 t2
        by move: H_busy_interval; rewrite -instantiated_busy_interval_equivalent_busy_interval // =>  -[PREF _].
    Qed.

  End PIBound.

  (** Let [jobs] denote the arrivals in the interval [Δ]. *)
  Let jobs := arrivals_between arr_seq t1 (t1 + Δ).

  (** Next, we prove that the cumulative interference from higher priority
      jobs of other tasks in an interval is bounded by the total service
      received by the higher priority jobs of those tasks. *)
  Lemma cumulative_interference_is_bounded_by_total_service:
    cumulative_another_task_hep_job_interference arr_seq sched j t1 (t1 + Δ)
    <= service_of_jobs sched (fun jo => another_task_hep_job jo j) jobs t1 (t1 + Δ).
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + Δ) <=
service_of_jobs sched (another_task_hep_job^~ j) jobs
  t1 (t1 + Δ)
  Proof.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + Δ) <=
service_of_jobs sched (another_task_hep_job^~ j) jobs
  t1 (t1 + Δ)
    move: (H_busy_interval) => [[/andP [JINBI JINBI2] [QT _]] _].
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
JINBI: t1 <= job_arrival j
JINBI2: job_arrival j < t2
QT: definitions.quiet_time sched j t1
cumulative_another_task_hep_job_interference arr_seq
  sched j t1 (t1 + Δ) <=
service_of_jobs sched (another_task_hep_job^~ j) jobs
  t1 (t1 + Δ)
    rewrite cumulative_i_thep_eq_service_of_othep => //.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
JINBI: t1 <= job_arrival j
JINBI2: job_arrival j < t2
QT: definitions.quiet_time sched j t1
quiet_time arr_seq sched j t1
    have /eqP TSK := H_job_of_tsk.
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobArrival Job
H1: JobCost Job
JR: JobReady Job (ideal.processor_state Job)
JLFP: JLFP_policy Job
H_policy_is_reflexive: reflexive_job_priorities JLFP
H_policy_respecsts_sequential_tasks: policy_respects_sequential_tasks
  JLFP
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
sched: schedule (ideal.processor_state Job)
H_valid_schedule: valid_schedule sched arr_seq
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
j: Job
H_j_arrives: arrives_in arr_seq j
H_job_of_tsk: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
t1, t2: duration
H_busy_interval: definitions.busy_interval sched j t1
  t2
A:= job_arrival j - t1: nat
Δ: duration
H_Δ_in_busy: t1 + Δ <= t2
jobs:= arrivals_between arr_seq t1 (t1 + Δ): seq Job
JINBI: t1 <= job_arrival j
JINBI2: job_arrival j < t2
QT: definitions.quiet_time sched j t1
TSK: job_task j = tsk
quiet_time arr_seq sched j t1
    by rewrite instantiated_quiet_time_equivalent_quiet_time.
  Qed.

End BusyIntervalInequalities.