busy_interval.v

Require Export prosa.model.priority.classes.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]
Require Export prosa.analysis.facts.behavior.completion.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 "[ 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]

(** * Busy Interval for JLFP-models *)
(** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
Section BusyIntervalJLFP.
  
  (** Consider any type of jobs. *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.    

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

  (** Consider any arrival sequence with consistent arrivals ... *)
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
  
  (** ... and a schedule of this arrival sequence. *)
  Variable sched : schedule PState.
  
  (** Assume a given JLFP policy. *)
  Context `{JLFP_policy Job}. 

  (** In this section, we define the notion of a busy interval. *)
  Section BusyInterval.
    
    (** Consider any job j. *)
    Variable j : Job.
    Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
    
    (** We say that [t] is a quiet time for [j] iff every higher-priority job from
         the arrival sequence that arrived before [t] has completed by that time. *)
    Definition quiet_time (t : instant) :=
      forall (j_hp : Job),
        arrives_in arr_seq j_hp ->
        hep_job j_hp j ->
        arrived_before j_hp t ->
        completed_by sched j_hp t.
    
    (** Based on the definition of quiet time, we say that interval
         <<[t1, t_busy)>> is a (potentially unbounded) busy-interval prefix
         iff the interval starts with a quiet time where a higher or equal 
         priority job is released and remains non-quiet. We also require
         job [j] to be released in the interval. *)    
    Definition busy_interval_prefix (t1 t_busy : instant) :=
      t1 < t_busy /\
      quiet_time t1 /\
      (forall t, t1 < t < t_busy -> ~ quiet_time t) /\
      t1 <= job_arrival j < t_busy.

    (** Next, we say that an interval <<[t1, t2)>> is a busy interval iff
        <<[t1, t2)>> is a busy-interval prefix and [t2] is a quiet time. *)
    Definition busy_interval (t1 t2 : instant) :=
      busy_interval_prefix t1 t2 /\
      quiet_time t2.

  End BusyInterval.

  (** In this section we define the computational
      version of the notion of quiet time. *)
  Section DecidableQuietTime.

    (** We say that t is a quiet time for [j] iff every higher-priority job from
        the arrival sequence that arrived before [t] has completed by that time. *)
    Definition quiet_time_dec (j : Job) (t : instant) :=
      all
        (fun j_hp => hep_job j_hp j ==> (completed_by sched j_hp t))
        (arrivals_before arr_seq t).

    (** We also show that the computational and propositional definitions are equivalent. *)
    Lemma quiet_time_P :
      forall j t, reflect (quiet_time j t) (quiet_time_dec j t).Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
forall (j : Job) (t : instant),
reflect (quiet_time j t) (quiet_time_dec j t)
    Proof.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
forall (j : Job) (t : instant),
reflect (quiet_time j t) (quiet_time_dec j t)
      intros; apply/introP.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
quiet_time_dec j t -> quiet_time j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t
      -Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
quiet_time_dec j t -> quiet_time j t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t intros QT s ARRs HPs BEFs.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time_dec j t
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t
        move: QT => /allP QT.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: {in arrivals_before arr_seq t,
  forall x : Job,
  hep_job x j ==> completed_by sched x t}
completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t
        specialize (QT s); feed QT.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: s \in arrivals_before arr_seq t ->
(fun x : Job =>
 is_true (hep_job x j ==> completed_by sched x t))
  s
s \in arrivals_before arr_seq t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: (fun x : Job =>
 is_true (hep_job x j ==> completed_by sched x t))
  s
completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t
        eapply arrived_between_implies_in_arrivals; eauto 2.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
s: Job
ARRs: arrives_in arr_seq s
HPs: hep_job s j
BEFs: arrived_before s t
QT: (fun x : Job =>
 is_true (hep_job x j ==> completed_by sched x t))
  s
completed_by sched s t
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t
          by move: QT => /implyP Q; apply Q in HPs.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t
      -Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
~~ quiet_time_dec j t -> ~ quiet_time j t move => /negP DEC; intros QT; apply: DEC.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
quiet_time_dec j t
        apply/allP; intros s ARRs.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
hep_job s j ==> completed_by sched s t
        apply/implyP; intros HPs.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
completed_by sched s t
        apply QT; try done.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
arrives_in arr_seq s
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
arrived_before s t
        +Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
arrives_in arr_seq s
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
arrived_before s t by apply in_arrivals_implies_arrived in ARRs.Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
arrived_before s t
        +Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
H_arrival_times_are_consistent: consistent_arrival_times
  arr_seq
sched: schedule PState
H1: JLFP_policy Job
j: Job
t: instant
QT: quiet_time j t
s: Job
ARRs: s \in arrivals_before arr_seq t
HPs: hep_job s j
arrived_before s t by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
    Qed.

  End DecidableQuietTime.

End BusyIntervalJLFP.