Require Export prosa.analysis.definitions.blocking_bound.fp.
[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.busy_interval.pi.


(** * Lower-Priority Non-Preemptive Segment is Bounded *)
(** In this file, we prove that, under the FP scheduling policy, the
    length of the maximum non-preemptive segment of a lower-priority
    job (w.r.t. a job of a task [tsk]) is bounded by
    [blocking_bound]. *)
Section  MaxNPSegmentIsBounded.

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

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

  (** Consider any kind of processor state model. *)
  Context `{PState : ProcessorState Job}.

  (** Consider an FP policy. *)
  Context {FP : FP_policy Task}.

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

  (** ... and any schedule of this arrival sequence. *)
  Variable sched : schedule PState.

  (** In addition, we assume the existence of a function mapping jobs
      to their preemption points ... *)
  Context `{JobPreemptable Job}.

  (** ... and assume that it defines a valid preemption model with
      bounded non-preemptive segments. *)
  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

  (** Consider an arbitrary task set [ts], ... *)
  Variable ts : list Task.

  (** ... assume that all jobs come from the task set, ... *)
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

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

  (** Consider any job [j] of [tsk]. *)
  Variable j : Job.
  Hypothesis H_job_of_tsk : job_of_task tsk j.

  (** Then, the maximum length of a nonpreemptive segment among all
      lower-priority jobs (w.r.t. the given job [j]) arrived so far is
      bounded by [blocking_bound]. *)
  Lemma nonpreemptive_segments_bounded_by_blocking :
    forall t,
      max_lp_nonpreemptive_segment arr_seq j t <= blocking_bound ts tsk.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
forall t : instant,
max_lp_nonpreemptive_segment arr_seq j t <=
blocking_bound ts tsk
  Proof.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
forall t : instant,
max_lp_nonpreemptive_segment arr_seq j t <=
blocking_bound ts tsk
    move=> t; move: H_job_of_tsk => /eqP TSK.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
max_lp_nonpreemptive_segment arr_seq j t <=
blocking_bound ts tsk
    apply: leq_trans; first exact: max_np_job_segment_bounded_by_max_np_task_segment.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_job
                                               j_lp j &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) <=
blocking_bound ts tsk
    apply: (@leq_trans (\max_(j_lp <- arrivals_between arr_seq 0 t
                             | (~~ hep_task (job_task j_lp) tsk) && (0 < job_cost j_lp))
                         (task_max_nonpreemptive_segment (job_task j_lp) - ε))).
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_job
                                               j_lp j &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) <=
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_task
                                               (job_task
                                                 j_lp)
                                               tsk &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1)
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
\max_(j_lp <- 
arrivals_between arr_seq 0 t | 
~~ hep_task (job_task j_lp) tsk && 
(0 < job_cost j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) <=
blocking_bound ts tsk
    {
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_job
                                               j_lp j &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) <=
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_task
                                               (job_task
                                                 j_lp)
                                               tsk &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) rewrite /hep_job /FP_to_JLFP TSK.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_task
                                               (job_task
                                                 j_lp)
                                               tsk &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) <=
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_task
                                               (job_task
                                                 j_lp)
                                               tsk &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1)
      apply: leq_big_max => j' JINB NOTHEP.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk &&
(0 < job_cost j')
task_max_nonpreemptive_segment (job_task j') - 1 <=
task_max_nonpreemptive_segment (job_task j') - 1
      by rewrite leq_sub2r //. }
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_task
                                               (job_task
                                                 j_lp)
                                               tsk &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) <=
blocking_bound ts tsk
    {
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
\max_(j_lp <- arrivals_between arr_seq 0 t | ~~
                                             hep_task
                                               (job_task
                                                 j_lp)
                                               tsk &&
                                             (0 <
                                              job_cost
                                                j_lp))
   (task_max_nonpreemptive_segment (job_task j_lp) - 1) <=
blocking_bound ts tsk apply /bigmax_leq_seqP => j' JINB /andP[NOTHEP POS].
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk
POS: 0 < job_cost j'
task_max_nonpreemptive_segment (job_task j') - 1 <=
blocking_bound ts tsk
      apply leq_bigmax_cond_seq with
        (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1);
        last by done.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk
POS: 0 < job_cost j'
job_task j' \in ts
      apply: H_all_jobs_from_taskset.
Task: TaskType
H: TaskCost Task
H0: TaskMaxNonpreemptiveSegment Task
Job: JobType
H1: JobTask Job Task
H2: JobCost Job
PState: ProcessorState Job
FP: FP_policy Task
arr_seq: arrival_sequence Job
sched: schedule PState
H3: JobPreemptable Job
H_valid_model_with_bounded_nonpreemptive_segments: valid_model_with_bounded_nonpreemptive_segments
  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
j: Job
H_job_of_tsk: job_of_task tsk j
t: instant
TSK: job_task j = tsk
j': Job
JINB: j' \in arrivals_between arr_seq 0 t
NOTHEP: ~~ hep_task (job_task j') tsk
POS: 0 < job_cost j'
arrives_in arr_seq j'
      by apply: in_arrivals_implies_arrived (JINB). }
  Qed.

End MaxNPSegmentIsBounded.