Require Export prosa.analysis.facts.busy_interval.pi.
[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]

(** * Bounded Priority Inversion Due to Non-Preemptive Sections *)

(** In the following, we relate the maximum cumulative priority inversion with a
    given blocking bound, assuming that priority version is caused (only) by
    non-preemptive segments. *)
Section PriorityInversionIsBounded.

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

  (** In addition, we assume that each task has a maximal non-preemptive
    segment ... *)
  Context `{TaskMaxNonpreemptiveSegment Task}.

  (**  ... and any type of preemptable jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobPreemptable Job}.

  (** Consider any valid arrival sequence,... *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

  (** ... and any schedule of this arrival sequence. *)
  Context {PState : ProcessorState Job}.
  Variable sched : schedule PState.

  (** Consider a JLFP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.

  (** And assume that they define a valid preemption model with
      bounded nonpreemptive segments. *)
  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

  (** Further, allow for any work-bearing notion of job readiness. *)
  Context `{!JobReady Job PState}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

  (** We assume that the schedule is valid. *)
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

  (** Next, we assume that the schedule is a work-conserving schedule... *)
  Hypothesis H_work_conserving : work_conserving arr_seq sched.

  (** ...,it respects the scheduling policy at every preemption point,... *)
  Hypothesis H_respects_policy :
    respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.

  (** ... and complies with the preemption model. *)
  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.

  (** Now, we consider an arbitrary task set [ts]... *)
  Variable ts : seq Task.

  (** ... and assume that all jobs stem from tasks in this task set. *)
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

  (** Let [tsk] be any task in [ts] that is to be analyzed. *)
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

  (** Let [blocking_bound] be a bound on the priority inversion caused by jobs
      with lower priority. *)
  Variable blocking_bound: duration -> duration.

  (** The following argument assumes an ideal uniprocessor. *)
  Hypothesis H_uni : uniprocessor_model PState.
  Hypothesis H_unit : unit_service_proc_model PState.
  Hypothesis H_progress : ideal_progress_proc_model PState.

  (** We show that, if the maximum length of a priority inversion of a given job [j]
      is bounded by the blocking bound,... *)
  Hypothesis H_priority_inversion_is_bounded_by_blocking:
    forall j t1 t2,
      arrives_in arr_seq j ->
      job_of_task tsk j ->
      busy_interval_prefix arr_seq sched j t1 t2 ->
      max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound (job_arrival j - t1).

  (** ... then the priority inversion incurred by any job is bounded by the blocking bound. *)
  Lemma priority_inversion_is_bounded :
    priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
priority_inversion_is_bounded_by arr_seq sched tsk
  blocking_bound
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
priority_inversion_is_bounded_by arr_seq sched tsk
  blocking_bound
    move=> j ARR TSK POS t1 t2 PREF.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1)
    move: (PREF) => [_ [_ [_ /andP [T _]]]].
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1)
    move: H_valid_schedule => [COARR MBR].
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1)
    have [NEQ|NEQ] := boolP ((t2-t1) <= blocking_bound (job_arrival j - t1)).
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: t2 - t1 <= blocking_bound (job_arrival j - t1)
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1)
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1)
    {
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: t2 - t1 <= blocking_bound (job_arrival j - t1)
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1) apply leq_trans with (t2 -t1) => [|//].
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: t2 - t1 <= blocking_bound (job_arrival j - t1)
cumulative_priority_inversion arr_seq sched j t1 t2 <=
t2 - t1
      rewrite /cumulative_priority_inversion.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: t2 - t1 <= blocking_bound (job_arrival j - t1)
\sum_(t1 <= t < t2)
   priority_inversion arr_seq sched j t <= t2 - t1
      rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: t2 - t1 <= blocking_bound (job_arrival j - t1)
\sum_(t1 <= t < t2)
   priority_inversion arr_seq sched j t <=
\sum_(t1 <= i < t2) 1
      by rewrite leq_sum //; move=> t _; destruct (priority_inversion). }
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1)
    have [ppt [PPT' /andP[GE LE]]]: exists ppt : instant,
                                      preemption_time arr_seq sched ppt /\
                                      t1 <= ppt <=
                                      t1 + max_lp_nonpreemptive_segment arr_seq j t1
      by exact: preemption_time_exists.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
cumulative_priority_inversion arr_seq sched j t1 t2 <=
blocking_bound (job_arrival j - t1)
    apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 ppt).
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
cumulative_priority_inversion arr_seq sched j t1 t2 <=
cumulative_priority_inversion arr_seq sched j t1 ppt
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
cumulative_priority_inversion arr_seq sched j t1 ppt <=
blocking_bound (job_arrival j - t1)
    -
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
cumulative_priority_inversion arr_seq sched j t1 t2 <=
cumulative_priority_inversion arr_seq sched j t1 ppt by apply: priority_inversion_occurs_only_till_preemption_point =>//.
    -
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
cumulative_priority_inversion arr_seq sched j t1 ppt <=
blocking_bound (job_arrival j - t1) apply leq_trans with (ppt - t1).
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
cumulative_priority_inversion arr_seq sched j t1 ppt <=
ppt - t1
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
ppt - t1 <= blocking_bound (job_arrival j - t1)
      +
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
cumulative_priority_inversion arr_seq sched j t1 ppt <=
ppt - t1 rewrite /cumulative_priority_inversion -[X in _ <= X]addn0 -[ppt - t1]mul1n
                -iter_addn -big_const_nat.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
\sum_(t1 <= t < ppt)
   priority_inversion arr_seq sched j t <=
\sum_(t1 <= i < ppt) 1
        by rewrite leq_sum //; move=> t _; case: priority_inversion. 
      +
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
ppt - t1 <= blocking_bound (job_arrival j - t1) rewrite leq_subLR.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
ppt <= t1 + blocking_bound (job_arrival j - t1)
        apply leq_trans with (t1 + max_lp_nonpreemptive_segment arr_seq j t1) => [//|].
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobArrival Job
H3: JobCost Job
H4: JobPreemptable Job
arr_seq: arrival_sequence Job
H_valid_arrival_sequence: valid_arrival_sequence
  arr_seq
PState: ProcessorState Job
sched: schedule PState
JLFP: JLFP_policy Job
H_priority_is_reflexive: reflexive_job_priorities
  JLFP
H_priority_is_transitive: transitive_job_priorities
  JLFP
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  arr_seq sched
JobReady0: JobReady Job PState
H_job_ready: work_bearing_readiness arr_seq sched
H_valid_schedule: valid_schedule sched arr_seq
H_work_conserving: work_conserving arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched JLFP
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
ts: seq Task
H_all_jobs_from_taskset: all_jobs_from_taskset
  arr_seq ts
tsk: Task
H_tsk_in_ts: tsk \in ts
blocking_bound: duration -> duration
H_uni: uniprocessor_model PState
H_unit: unit_service_proc_model PState
H_progress: ideal_progress_proc_model PState
H_priority_inversion_is_bounded_by_blocking: forall (j : Job)
  (t1
   t2 : instant),
arrives_in
  arr_seq j ->
job_of_task tsk
  j ->
busy_interval_prefix
  arr_seq sched
  j t1 t2 ->
max_lp_nonpreemptive_segment
  arr_seq j t1 <=
blocking_bound
  (job_arrival j -
   t1)
j: Job
ARR: arrives_in arr_seq j
TSK: job_of_task tsk j
POS: 0 < job_cost j
t1, t2: instant
PREF: busy_interval_prefix arr_seq sched j t1 t2
T: t1 <= job_arrival j
COARR: jobs_come_from_arrival_sequence sched arr_seq
MBR: jobs_must_be_ready_to_execute sched
NEQ: ~~
(t2 - t1 <= blocking_bound (job_arrival j - t1))
ppt: instant
PPT': preemption_time arr_seq sched ppt
GE: t1 <= ppt
LE: ppt <=
t1 + max_lp_nonpreemptive_segment arr_seq j t1
t1 + max_lp_nonpreemptive_segment arr_seq j t1 <=
t1 + blocking_bound (job_arrival j - t1)
        by rewrite leq_add2l; apply: (H_priority_inversion_is_bounded_by_blocking j t1 t2).
  Qed.

End PriorityInversionIsBounded.