Library prosa.analysis.facts.behavior.arrivals

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

Arrival Sequence

First, we relate the stronger to the weaker arrival predicates.

Section ArrivalPredicates.

Consider any kinds of jobs with arrival times.

Context {Job : JobType} `{JobArrival Job}.

A job that arrives in some interval [t1, t2) certainly arrives before time t2.

  Lemma arrived_between_before:
    ∀ j t1 t2,
      arrived_between j t1 t2 →
      arrived_before j t2.

A job that arrives before a time t certainly has arrived by time t.

  Lemma arrived_before_has_arrived:
    ∀ j t,
      arrived_before j t →
      has_arrived j t.

End ArrivalPredicates.

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.

  Lemma jobs_must_arrive_to_be_ready:
    jobs_must_be_ready_to_execute sched →
    jobs_must_arrive_to_execute sched.

Since backlogged jobs are by definition ready, any backlogged job must have arrived.

  Corollary backlogged_implies_arrived:
    ∀ j t,
      backlogged sched j t → has_arrived j t.

End Arrived.

In this section, we establish useful facts about arrival sequence prefixes.

Section ArrivalSequencePrefix.

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.

Hypothesis H_consistent_arrival_times:
consistent_arrival_times arr_seq.

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.