Library prosa.analysis.facts.periodic.task_arrivals_size

Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.definitions.infinite_jobs.
Require Export prosa.analysis.facts.sporadic.arrival_sequence.

In this file we prove some properties concerning the size of task arrivals in context of the periodic model.

Section TaskArrivalsSize.

Consider any type of periodic tasks with an offset ...

  Context {Task : TaskType}.
  Context `{TaskOffset Task}.
  Context `{PeriodicModel Task}.

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

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

Consider any unique arrival sequence with consistent arrivals ...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any periodic task tsk with a valid offset and period.

  Variable tsk : Task.
  Hypothesis H_valid_offset : valid_offset arr_seq tsk.
  Hypothesis H_valid_period : valid_period tsk.
  Hypothesis H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk.

We show that if an instant t is not an "arrival time" for task tsk then task_arrivals_at arr_seq tsk t is an empty sequence.

  Lemma task_arrivals_size_at_non_arrival:
    ∀ t,
      (∀ n, t ≠ task_offset tsk + n × task_period tsk ) →
      task_arrivals_at arr_seq tsk t = [::].

We show that at any instant t, at most one job of task tsk can arrive (i.e. size of task_arrivals_at arr_seq tsk t is at most one).

  Lemma task_arrivals_at_size_cases:
    ∀ t,
      size (task_arrivals_at arr_seq tsk t) = 0 ∨
      size (task_arrivals_at arr_seq tsk t) = 1.

We show that the size of task arrivals (strictly) between two consecutive arrival times is zero.

  Lemma size_task_arrivals_between_eq0:
    ∀ n,
      let l := (task_offset tsk + n × task_period tsk ).+1 in
      let r := (task_offset tsk + n .+1 × task_period tsk) in
      size (task_arrivals_between arr_seq tsk l r) = 0.

In this section we show some properties of task arrivals in case of an infinite sequence of jobs.

Section TaskArrivalsInCaseOfInfiniteJobs.

Assume that we have an infinite sequence of jobs.

Hypothesis H_infinite_jobs : infinite_jobs arr_seq.

We show that for any number n, there exists a job j of task tsk such that job_index of j is equal to n and j arrives at task_offset tsk + n × task_period tsk.

    Lemma jobs_exists_later:
      ∀ n,
      ∃ j ,
        arrives_in arr_seq j ∧
        job_task j = tsk ∧
        job_arrival j = task_offset tsk + n × task_period tsk ∧
        job_index arr_seq j = n.

We show that the size of task arrivals at any arrival time is equal to one.

    Lemma task_arrivals_at_size:
      ∀ n,
        let l := (task_offset tsk + n × task_period tsk) in
        size (task_arrivals_at arr_seq tsk l) = 1.

We show that the size of task arrivals up to task_offset tsk is equal to one.

Lemma size_task_arrivals_up_to_offset:
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1.

We show that for any number n, the number of jobs released by task tsk up to task_offset tsk + n × task_period tsk is equal to n + 1.

    Lemma task_arrivals_up_to_size:
      ∀ n,
        let l := (task_offset tsk + n × task_period tsk) in
        let r := (task_offset tsk + n .+1 × task_period tsk) in
        size (task_arrivals_up_to arr_seq tsk l) = n + 1.

We show that the number of jobs released by task tsk at any instant t and t + n × task_period tsk is the same for any number n.

    Lemma eq_size_of_task_arrivals_seperated_by_period:
      ∀ n t,
        t ≥ task_offset tsk →
        size (task_arrivals_at arr_seq tsk t) =
        size (task_arrivals_at arr_seq tsk (t + n × task_period tsk)).

  End TaskArrivalsInCaseOfInfiniteJobs.

End TaskArrivalsSize.