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.

  Lemma jobs_must_arrive_to_be_ready:
    jobs_must_be_ready_to_execute sched →
    jobs_must_arrive_to_execute sched.

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.