Library prosa.analysis.facts.behavior.arrivals

Require Export prosa.behavior.all.
Require Export prosa.util.all.

Arrival Sequence

In this section, we relate job readiness to has_arrived.
Section Arrived.

Consider any kinds of jobs and any kind of processor state.
  Context {Job : JobType} {PState : Type}.
  Context `{ProcessorState Job PState}.

Consider any schedule...
  Variable sched : schedule PState.

...and suppose that jobs have a cost, an arrival time, and a notion of readiness.
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
  Context `{JobReady Job PState}.

First, we note that readiness models are by definition consistent w.r.t. pending.
  Lemma any_ready_job_is_pending:
     j t,
      job_ready sched j t pending sched j t.

Next, we observe that a given job must have arrived to be ready...
  Lemma ready_implies_arrived:
     j t, job_ready sched j t has_arrived j t.

...and lift this observation also to the level of whole schedules.
In this section, we establish useful facts about arrival sequence prefixes.
Assume that job arrival times are known.
  Context {Job: JobType}.
  Context `{JobArrival Job}.

Consider any job arrival sequence.
  Variable arr_seq: arrival_sequence Job.

We begin with basic lemmas for manipulating the sequences.
  Section Composition.

First, we show that the set of arriving jobs can be split into disjoint intervals.
    Lemma arrivals_between_cat:
       t1 t t2,
        t1 t
        t t2
        arrivals_between arr_seq t1 t2 =
        arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.

Second, the same observation applies to membership in the set of arrived jobs.
    Lemma arrivals_between_mem_cat:
       j t1 t t2,
        t1 t
        t t2
        j \in arrivals_between arr_seq t1 t2 =
        (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).

Third, we observe that we can grow the considered interval without "losing" any arrived jobs, i.e., membership in the set of arrived jobs is monotonic.
    Lemma arrivals_between_sub:
       j t1 t1' t2 t2',
        t1' t1
        t2 t2'
        j \in arrivals_between arr_seq t1 t2
        j \in arrivals_between arr_seq t1' t2'.

  End Composition.

Next, we relate the arrival prefixes with job arrival times.
  Section ArrivalTimes.

Assume that job arrival times are consistent.
First, we prove that if a job belongs to the prefix (jobs_arrived_before t), then it arrives in the arrival sequence.
    Lemma in_arrivals_implies_arrived:
       j t1 t2,
        j \in arrivals_between arr_seq t1 t2
        arrives_in arr_seq j.

Next, we prove that if a job belongs to the prefix (jobs_arrived_between t1 t2), then it indeed arrives between t1 and t2.
    Lemma in_arrivals_implies_arrived_between:
       j t1 t2,
        j \in arrivals_between arr_seq t1 t2
        arrived_between j t1 t2.

Similarly, if a job belongs to the prefix (jobs_arrived_before t), then it indeed arrives before time t.
    Lemma in_arrivals_implies_arrived_before:
       j t,
        j \in arrivals_before arr_seq t
        arrived_before j t.

Similarly, we prove that if a job from the arrival sequence arrives before t, then it belongs to the sequence (jobs_arrived_before t).
    Lemma arrived_between_implies_in_arrivals:
       j t1 t2,
        arrives_in arr_seq j
        arrived_between j t1 t2
        j \in arrivals_between arr_seq t1 t2.

Next, we prove that if the arrival sequence doesn't contain duplicate jobs, the same applies for any of its prefixes.
    Lemma arrivals_uniq :
      arrival_sequence_uniq arr_seq
       t1 t2, uniq (arrivals_between arr_seq t1 t2).

Also note there can't by any arrivals in an empty time interval.
    Lemma arrivals_between_geq:
       t1 t2,
        t1 t2
        arrivals_between arr_seq t1 t2 = [::].

  End ArrivalTimes.

End ArrivalSequencePrefix.