Library prosa.analysis.definitions.busy_interval


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.behavior.completion.

Throughout this file, we assume ideal uniprocessor schedules.
Require Import prosa.model.processor.ideal.

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 : Type}.
  Context `{ProcessorState Job PState}.

Consider any arrival sequence with consistent arrivals ...
... 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) :=
       (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
      ( 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_hphep_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 :
       j t, reflect (quiet_time j t) (quiet_time_dec j t).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 638)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : JLFP_policy Job
  ============================
  forall (j : Job) (t : instant),
  reflect (quiet_time j t) (quiet_time_dec j t)

----------------------------------------------------------------------------- *)


    Proof.
      intros; apply/introP.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 2) (ID 767)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : JLFP_policy Job
  j : Job
  t : instant
  ============================
  quiet_time_dec j t -> quiet_time j t

subgoal 2 (ID 768) is:
 ~~ quiet_time_dec j t -> ~ quiet_time j t

----------------------------------------------------------------------------- *)


      - intros QT s ARRs HPs BEFs.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 1) (ID 774)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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

subgoal 2 (ID 768) is:
 ~~ quiet_time_dec j t -> ~ quiet_time j t

----------------------------------------------------------------------------- *)


        move: QT ⇒ /allP QT.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 1) (ID 810)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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

subgoal 2 (ID 768) is:
 ~~ quiet_time_dec j t -> ~ quiet_time j t

----------------------------------------------------------------------------- *)


        specialize (QT s); feed QT.

(* ----------------------------------[ coqtop ]---------------------------------

3 focused subgoals
(shelved: 1) (ID 813)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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

subgoal 2 (ID 818) is:
 completed_by sched s t
subgoal 3 (ID 768) is:
 ~~ quiet_time_dec j t -> ~ quiet_time j t

----------------------------------------------------------------------------- *)


        eapply arrived_between_implies_in_arrivals; eauto 2.

(* ----------------------------------[ coqtop ]---------------------------------

2 focused subgoals
(shelved: 1) (ID 818)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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

subgoal 2 (ID 768) is:
 ~~ quiet_time_dec j t -> ~ quiet_time j t

----------------------------------------------------------------------------- *)


          by move: QT ⇒ /implyP Q; apply Q in HPs.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 768)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : JLFP_policy Job
  j : Job
  t : instant
  ============================
  ~~ quiet_time_dec j t -> ~ quiet_time j t

----------------------------------------------------------------------------- *)


      - move ⇒ /negP DEC; intros QT; apply: DEC.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 893)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : JLFP_policy Job
  j : Job
  t : instant
  QT : quiet_time j t
  ============================
  quiet_time_dec j t

----------------------------------------------------------------------------- *)


        apply/allP; intros s ARRs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 924)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 949)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 950)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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

subgoal 2 (ID 952) is:
 arrived_before s t

----------------------------------------------------------------------------- *)


        + by apply in_arrivals_implies_arrived in ARRs.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 952)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule PState
  H2 : 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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End DecidableQuietTime.

End BusyIntervalJLFP.