classical.v

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

(** * 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 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
        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
        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
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 by 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 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 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 => //.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 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 by eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
    Qed.

  End DecidableQuietTime.

End BusyIntervalJLFP.