Require Export prosa.analysis.definitions.priority_inversion.
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]

(** * Lemma about Priority Inversion for arbitrary processors *)
(** In this section, we prove a lemma about the notion of priority
    inversion for arbitrary processors. *)
Section PIGenericProcessorModelLemma.

  (** 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}.

  (** Next, consider _any_ kind of processor state model, ... *)
  Context {PState : ProcessorState Job}.

  (** ... any arrival sequence, ... *)
  Variable arr_seq : arrival_sequence Job.

  (** ... and any schedule. *)
  Variable sched : schedule PState.

  (** Assume a given JLFP policy. *)
  Context `{JLFP_policy Job}.

  (** Consider an arbitrary job. *)
  Variable j : Job.


  (** Then we prove that cumulative priority inversion (CPI) that job
      [j] incurs in an interval <<[t1, t2)>> is equal to the sum of
      CPI in an interval <<[t1, t_mid)>> and CPI in an interval
      <<[t_mid, t2)>>. *)
  Lemma cumulative_priority_inversion_cat:
    forall (t_mid t1 t2 : instant),
      t1 <= t_mid ->
      t_mid <= t2 ->
      cumulative_priority_inversion arr_seq sched j t1 t2 =
        cumulative_priority_inversion arr_seq sched j t1 t_mid
        + cumulative_priority_inversion arr_seq sched j t_mid t2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
forall t_mid t1 t2 : instant,
t1 <= t_mid ->
t_mid <= t2 ->
cumulative_priority_inversion arr_seq sched j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t_mid +
cumulative_priority_inversion arr_seq sched j t_mid t2
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
forall t_mid t1 t2 : instant,
t1 <= t_mid ->
t_mid <= t2 ->
cumulative_priority_inversion arr_seq sched j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t_mid +
cumulative_priority_inversion arr_seq sched j t_mid t2
    intros * LE1 LE2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
t_mid, t1, t2: instant
LE1: t1 <= t_mid
LE2: t_mid <= t2
cumulative_priority_inversion arr_seq sched j t1 t2 =
cumulative_priority_inversion arr_seq sched j t1 t_mid +
cumulative_priority_inversion arr_seq sched j t_mid t2
    rewrite /cumulative_priority_inversion -big_cat //=.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
t_mid, t1, t2: instant
LE1: t1 <= t_mid
LE2: t_mid <= t2
\sum_(t1 <= t < t2)
   priority_inversion_dec arr_seq sched j t =
\sum_(i <- (index_iota t1 t_mid ++ index_iota t_mid t2))
   priority_inversion_dec arr_seq sched j i
    replace (index_iota t1 t_mid ++ index_iota t_mid t2) with (index_iota t1 t2); first by reflexivity.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
t_mid, t1, t2: instant
LE1: t1 <= t_mid
LE2: t_mid <= t2
index_iota t1 t2 =
index_iota t1 t_mid ++ index_iota t_mid t2
    interval_to_duration t1 t_mid δ1.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
t1, t2: instant
δ1: nat
LE2: t1 + δ1 <= t2
index_iota t1 t2 =
index_iota t1 (t1 + δ1) ++ index_iota (t1 + δ1) t2
    interval_to_duration (t1 + δ1) t2 δ2.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
t1: instant
δ1, δ2: nat
index_iota t1 (t1 + δ1 + δ2) =
index_iota t1 (t1 + δ1) ++
index_iota (t1 + δ1) (t1 + δ1 + δ2)
    rewrite -!addnA /index_iota.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
t1: instant
δ1, δ2: nat
iota t1 (t1 + (δ1 + δ2) - t1) =
iota t1 (t1 + δ1 - t1) ++
iota (t1 + δ1) (t1 + (δ1 + δ2) - (t1 + δ1))
    erewrite iotaD_impl with (n_le := δ1); last by lia.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
t1: instant
δ1, δ2: nat
iota t1 δ1 ++
iota (t1 + δ1) (t1 + (δ1 + δ2) - t1 - δ1) =
iota t1 (t1 + δ1 - t1) ++
iota (t1 + δ1) (t1 + (δ1 + δ2) - (t1 + δ1))
    by rewrite !addKn addnA addKn.
  Qed.

  (** Assume that [j] is scheduled at time [t], then there is no
      priority inversion at time [t]. *)
  Lemma sched_itself_implies_no_priority_inversion :
    forall t,
      scheduled_at sched j t ->
      priority_inversion_dec arr_seq sched j t = false.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
forall t : instant,
scheduled_at sched j t ->
priority_inversion_dec arr_seq sched j t = false
  Proof.
Task: TaskType
H: TaskCost Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JLFP_policy Job
j: Job
forall t : instant,
scheduled_at sched j t ->
priority_inversion_dec arr_seq sched j t = false by move => t SCHED; rewrite /priority_inversion_dec SCHED. Qed.

End PIGenericProcessorModelLemma.