# Library prosa.analysis.facts.readiness.backlogged

Require Export prosa.model.schedule.work_conserving.

Require Export prosa.analysis.facts.behavior.arrivals.

Require Export prosa.analysis.definitions.readiness.

Require Export prosa.analysis.facts.behavior.arrivals.

Require Export prosa.analysis.definitions.readiness.

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

Consider any kind of jobs with arrival times and costs...

... and any kind of processor model, ...

... and allow for any notion of job readiness.

Given an arrival sequence and a schedule ...

... with consistent arrival times, ...

... we observe that any backlogged job is indeed in the set of backlogged
jobs.

Lemma mem_backlogged_jobs:

∀ j t,

arrives_in arr_seq j →

backlogged sched j t →

j \in jobs_backlogged_at arr_seq sched t.

∀ j t,

arrives_in arr_seq j →

backlogged sched j t →

j \in jobs_backlogged_at arr_seq sched t.

Trivially, it is also the case that any backlogged job comes from the
respective arrival sequence.

Lemma backlogged_job_arrives_in:

∀ j t,

j \in jobs_backlogged_at arr_seq sched t →

arrives_in arr_seq j.

End BackloggedJobs.

∀ j t,

j \in jobs_backlogged_at arr_seq sched t →

arrives_in arr_seq j.

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.

Consider any kind of jobs with arrival times and costs...

... any kind of processor model, ...

... and allow for any non-clairvoyant notion of job readiness.

Context {RM : JobReady Job PState}.

Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.

Consider any arrival sequence ...

... and two schedules ...

... with a shared prefix to a fixed horizon.

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 ...

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':

∀ t j,

~~ scheduled_at sched j t →

~~ scheduled_at sched' j t →

t ≤ h →

backlogged sched j t = backlogged sched' j t.

∀ t j,

~~ scheduled_at sched j t →

~~ scheduled_at sched' j t →

t ≤ h →

backlogged sched j t = backlogged sched' j t.

... 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:

∀ t,

t < h →

jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t.

End NonClairvoyance.

∀ t,

t < h →

jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t.

End NonClairvoyance.