backlogged.v

Require Export prosa.model.schedule.work_conserving.[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.arrivals.
Require Export prosa.analysis.definitions.readiness.

(** In this file, we establish basic facts about backlogged jobs. *)

Section BackloggedJobs.

  (** Consider any kind of jobs with arrival times and costs... *)
  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.

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

  (** ... and allow for any notion of job readiness. *)
  Context {jr : JobReady Job PState}.

  (** Given an arrival sequence and a schedule ... *)
  Variable arr_seq : arrival_sequence Job.
  Variable sched : schedule PState.

  (** ... with consistent arrival times, ... *)
  Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.

  (** ... we observe that any backlogged job is indeed in the set of backlogged
     jobs. *)
  Lemma mem_backlogged_jobs:
    forall j t,
      arrives_in arr_seq j ->
      backlogged sched j t ->
      j \in jobs_backlogged_at arr_seq sched t.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
j \in jobs_backlogged_at arr_seq sched t
  Proof.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
arrives_in arr_seq j ->
backlogged sched j t ->
j \in jobs_backlogged_at arr_seq sched t
    move=> j t ARRIVES BACKLOGGED.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
j \in jobs_backlogged_at arr_seq sched t
    rewrite /jobs_backlogged_at /arrivals_up_to.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
j
  \in [seq j <- arrivals_between arr_seq 0 t.+1
         | backlogged sched j t]
    rewrite mem_filter.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
backlogged sched j t &&
(j \in arrivals_between arr_seq 0 t.+1)
    apply /andP; split; first by exact.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
j \in arrivals_between arr_seq 0 t.+1
    apply arrived_between_implies_in_arrivals => //.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
arrived_between j 0 t.+1
    rewrite /arrived_between.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
0 <= job_arrival j < t.+1
    apply /andP; split => //.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
job_arrival j < t.+1
    rewrite ltnS -/(has_arrived _ _).Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged sched j t
has_arrived j t
    now apply (backlogged_implies_arrived sched).
  Qed.

  (** Trivially, it is also the case that any backlogged job comes from the
      respective arrival sequence. *)
  Lemma backlogged_job_arrives_in:
    forall j t,
      j \in jobs_backlogged_at arr_seq sched t ->
      arrives_in arr_seq j.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
j \in jobs_backlogged_at arr_seq sched t ->
arrives_in arr_seq j
  Proof.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
forall (j : Job) (t : instant),
j \in jobs_backlogged_at arr_seq sched t ->
arrives_in arr_seq j
    move=> j t.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
j \in jobs_backlogged_at arr_seq sched t ->
arrives_in arr_seq j
    rewrite  /jobs_backlogged_at mem_filter => /andP [_ IN].Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
IN: j \in arrivals_up_to arr_seq t
arrives_in arr_seq j
    move: IN.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
j \in arrivals_up_to arr_seq t -> arrives_in arr_seq j rewrite /arrivals_up_to.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
jr: JobReady Job PState
arr_seq: arrival_sequence Job
sched: schedule PState
H_consistent_arrival_times: consistent_arrival_times
  arr_seq
j: Job
t: instant
j \in arrivals_between arr_seq 0 t.+1 ->
arrives_in arr_seq j
    now apply in_arrivals_implies_arrived.
  Qed.

End BackloggedJobs.

(** In the following section, we make one more crucial assumption: namely, that
    the readiness model is non-clairvoyant, which allows us to relate
    backlogged jobs in schedules with a shared prefix. *)
Section NonClairvoyance.

  (** Consider any kind of jobs with arrival times and costs... *)
  Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.

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

  (** ... and allow for any non-clairvoyant notion of job readiness. *)
  Context {RM : JobReady Job PState}.
  Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

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

  (**  ... and two schedules  ... *)
  Variable sched sched': schedule PState.

  (** ... with a shared prefix to a fixed horizon. *)
  Variable h : instant.
  Hypothesis H_shared_prefix: identical_prefix sched sched' h.

  (** We observe that a job is backlogged at a time in the prefix in one
      schedule iff it is backlogged in the other schedule due to the
      non-clairvoyance of the notion of job readiness ... *)
  Lemma backlogged_prefix_invariance:
    forall t j,
      t < h ->
      backlogged sched j t = backlogged sched' j t.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
forall (t : nat) (j : Job),
t < h -> backlogged sched j t = backlogged sched' j t
  Proof.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
forall (t : nat) (j : Job),
t < h -> backlogged sched j t = backlogged sched' j t
    move=> t j IN_PREFIX.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: nat
j: Job
IN_PREFIX: t < h
backlogged sched j t = backlogged sched' j t
    rewrite /backlogged.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: nat
j: Job
IN_PREFIX: t < h
job_ready sched j t && ~~ scheduled_at sched j t =
job_ready sched' j t && ~~ scheduled_at sched' j t
    rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: nat
j: Job
IN_PREFIX: t < h
job_ready sched' j t && ~~ scheduled_at sched j t =
job_ready sched' j t && ~~ scheduled_at sched' j t
    by rewrite /scheduled_at H_shared_prefix.
  Qed.

  (** As a corollary, if we further know that j is not scheduled at time [h],
      we can expand the previous lemma to [t <= h]. *)
  Corollary backlogged_prefix_invariance':
    forall t j,
      ~~ scheduled_at sched  j t ->
      ~~ scheduled_at sched' j t ->
      t <= h ->
      backlogged sched j t = backlogged sched' j t.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
forall (t : instant) (j : Job),
~~ scheduled_at sched j t ->
~~ scheduled_at sched' j t ->
t <= h -> backlogged sched j t = backlogged sched' j t
  Proof.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
forall (t : instant) (j : Job),
~~ scheduled_at sched j t ->
~~ scheduled_at sched' j t ->
t <= h -> backlogged sched j t = backlogged sched' j t
    move=> t j NOT_SCHED NOT_SCHED'.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: instant
j: Job
NOT_SCHED: ~~ scheduled_at sched j t
NOT_SCHED': ~~ scheduled_at sched' j t
t <= h -> backlogged sched j t = backlogged sched' j t
    rewrite leq_eqVlt => /orP [/eqP EQ | LT]; last by apply backlogged_prefix_invariance.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: instant
j: Job
NOT_SCHED: ~~ scheduled_at sched j t
NOT_SCHED': ~~ scheduled_at sched' j t
EQ: t = h
backlogged sched j t = backlogged sched' j t
    rewrite /backlogged.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: instant
j: Job
NOT_SCHED: ~~ scheduled_at sched j t
NOT_SCHED': ~~ scheduled_at sched' j t
EQ: t = h
job_ready sched j t && ~~ scheduled_at sched j t =
job_ready sched' j t && ~~ scheduled_at sched' j t
    rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //;
            last by rewrite EQ.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: instant
j: Job
NOT_SCHED: ~~ scheduled_at sched j t
NOT_SCHED': ~~ scheduled_at sched' j t
EQ: t = h
job_ready sched' j t && ~~ scheduled_at sched j t =
job_ready sched' j t && ~~ scheduled_at sched' j t
    now rewrite NOT_SCHED NOT_SCHED'.
  Qed.

  (** ... and also lift this observation to the set of all backlogged jobs at
      any given time in the shared prefix. *)
  Lemma backlogged_jobs_prefix_invariance:
    forall t,
      t < h ->
      jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
forall t : nat,
t < h ->
jobs_backlogged_at arr_seq sched t =
jobs_backlogged_at arr_seq sched' t
  Proof.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
forall t : nat,
t < h ->
jobs_backlogged_at arr_seq sched t =
jobs_backlogged_at arr_seq sched' t
    move=> t IN_PREFIX.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: nat
IN_PREFIX: t < h
jobs_backlogged_at arr_seq sched t =
jobs_backlogged_at arr_seq sched' t
    rewrite /jobs_backlogged_at.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: nat
IN_PREFIX: t < h
[seq j <- arrivals_up_to arr_seq t
   | backlogged sched j t] =
[seq j <- arrivals_up_to arr_seq t
   | backlogged sched' j t]
    apply eq_filter.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: nat
IN_PREFIX: t < h
(backlogged sched)^~ t =1 (backlogged sched')^~ t
    rewrite /eqfun => j.Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
RM: JobReady Job PState
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness
  RM
arr_seq: arrival_sequence Job
sched, sched': schedule PState
h: instant
H_shared_prefix: identical_prefix sched sched' h
t: nat
IN_PREFIX: t < h
j: Job
backlogged sched j t = backlogged sched' j t
    now apply backlogged_prefix_invariance.
  Qed.

End NonClairvoyance.