Library prosa.implementation.facts.maximal_arrival_sequence

Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.implementation.definitions.maximal_arrival_sequence.

Recall that, given an arrival curve max_arrivals and a job-generating function generate_jobs_at, the function concrete_arrival_sequence generates an arrival sequence. In this section, we prove a few properties of this function.

Section MaximalArrivalSequence.

Consider any type of tasks ...

Context {Task : TaskType}.
Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.

  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider a task set ts with non-duplicate tasks.

Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.

Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.

Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.

Further assume we are given a function that generates the required number of jobs of a given task at a given instant of time.

Variable generate_jobs_at : Task → nat → instant → seq Job.

First, we assume that generate_jobs_at tsk n t generates n jobs.

Hypothesis H_job_generation_valid_number:
∀ (tsk : Task) (n : nat) (t : instant), tsk \in ts → size (generate_jobs_at tsk n t) = n.

Second, we assume that generate_jobs_at tsk n t generates jobs of task tsk that arrive at time t.

  Hypothesis H_job_generation_valid_jobs:
    ∀ (tsk : Task) (n : nat) (t : instant) (j : Job),
      (j \in generate_jobs_at tsk n t ) →
      job_task j = tsk
      ∧ job_arrival j = t
      ∧ job_cost j ≤ task_cost tsk.

Finally, we assume that all jobs generated by generate_jobs_at are unique.

  Hypothesis H_jobs_unique:
    ∀ (t1 t2 : instant),
      uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2).

Assuming such a well-behaved "constructor" generate_jobs_at, we prove a few validity claims about an arrival sequence generated by concrete_arrival_sequence.

Section ValidityClaims.

We start by showing that the obtained arrival sequence is a set.

Lemma arr_seq_is_a_set :
arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts).

Next, we show that all jobs in the arrival sequence come from ts.

Lemma concrete_all_jobs_from_taskset :
all_jobs_from_taskset (concrete_arrival_sequence generate_jobs_at ts) ts.

Further, we note that the jobs in the arrival sequence have consistent arrival times.

Lemma arrival_times_are_consistent :
consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts).

Lastly, we observe that the jobs in the arrival sequence have valid job costs.

    Lemma concrete_valid_job_cost :
      arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts).

  End ValidityClaims.

In this section, we prove a series of facts regarding the maximal arrival sequence, leading up to the main theorem that all arrival-curve constraints are respected.

Section Facts.

Let tsk be any task in ts that is to be analyzed.

Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.

First, we show that the arrivals at time t are indeed generated by generate_jobs_at applied at time t.

    Lemma task_arrivals_at_eq_generate_jobs_at:
      ∀ t,
        task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t
        = generate_jobs_at tsk (max_arrivals_at tsk t) t.

Next, we show that the number of arrivals at time t always matches max_arrivals_at applied at time t.

    Lemma task_arrivals_at_eq:
      ∀ t,
        size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
        = max_arrivals_at tsk t.

We then generalize the previous result to an arbitrary interval [t1,t2).

    Lemma number_of_task_arrivals_eq :
      ∀ t1 t2,
        number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2
        = \sum_(t1 ≤ t < t2 ) max_arrivals_at tsk t.

We further show that, starting from an empty prefix and applying extend_arrival_prefix t times, we end up with a prefix of size t...

    Lemma extend_horizon_size :
      ∀ t,
        size (iter t (extend_arrival_prefix tsk) [::]) = t.

...and that the arrival sequence prefix up to an arbitrary horizon t is a sequence of t+1 elements.

    Lemma prefix_up_to_size :
      ∀ t,
        size (maximal_arrival_prefix tsk t) = t .+1.

Next, we prove prefix inclusion for maximal_arrival_prefix when the horizon is expanded by one...

    Lemma n_arrivals_at_prefix_inclusion1 :
      ∀ t h,
        t ≤ h →
        nth 0 (maximal_arrival_prefix tsk h) t
        = nth 0 (maximal_arrival_prefix tsk h .+1) t.

...and we generalize the previous result to two arbitrary horizons h1 ≤ h2.

    Lemma n_arrivals_at_prefix_inclusion :
      ∀ t h1 h2,
        t ≤ h1 ≤ h2 →
        nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.

Next, we prove that, for any positive time instant t, max_arrivals_at indeed matches the arrivals of next_max_arrival applied at t-1.

    Lemma max_arrivals_at_next_max_arrivals_eq:
      ∀ t,
        0 < t →
        max_arrivals_at tsk t
        = next_max_arrival tsk (maximal_arrival_prefix tsk t .-1).

Given a time instant t and and interval Δ, we show that max_arrivals_at applied at time t is always less-or-equal to max_arrivals applied to Δ+1, even when each value of max_arrivals_at in the interval [t-Δ, t) is subtracted from it.

    Lemma n_arrivals_at_leq :
      ∀ t Δ,
        Δ ≤ t →
        max_arrivals_at tsk t
        ≤ max_arrivals tsk Δ .+1 - \sum_(t - Δ ≤ i < t ) max_arrivals_at tsk i.
  End Facts.

Finally, we prove our main result, that is, the proposed maximal arrival sequence instantiation indeed respects all arrival-curve constraints.

Theorem concrete_is_arrival_curve :
taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts.
End MaximalArrivalSequence.