Built with Alectryon, running Coq+SerAPI v8.16.0+0.16.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ predI _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ predU _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ predD _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ predC _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ preim _ of _ ]" 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)>>. *)
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
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
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
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
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
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
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)
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))
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]. *)
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
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.