Library prosa.classic.model.arrival.jitter.task_arrival
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path.
(* In this file, we provide definitions and lemmas about task arrivals
in jitter-aware schedules. *)
Module TaskArrivalWithJitter.
Import ArrivalSequenceWithJitter SporadicTaskset.
Export TaskArrival.
(* First, we identify the arrivals of a particular task. *)
Section NumberOfArrivals.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
(* Consider any job arrival sequence ...*)
Variable arr_seq: arrival_sequence Job.
(* ...and recall the list of jobs with actual arrival time in a given interval. *)
Let arrivals_between := actual_arrivals_between job_arrival job_jitter arr_seq.
(* Next, let tsk be any task. *)
Variable tsk: Task.
(* By checking the jobs spawned by tsk... *)
Definition is_job_of_tsk := is_job_of_task job_task tsk.
(* ...we identify the jobs of tsk that arrived in any interval t1, t2) ... *)
Definition actual_arrivals_of_task_between (t1 t2: time) :=
[seq j <- arrivals_between t1 t2 | is_job_of_tsk j].
(* ...and also count the number of such job arrivals. *)
Definition num_actual_arrivals_of_task (t1 t2: time) :=
size (actual_arrivals_of_task_between t1 t2).
End NumberOfArrivals.
(* Next, we prove properties about lists of actual arrivals
that are sorted by arrival time. *)
Section DistanceBetweenSporadicJobs.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
(* Consider any arrival sequence with consistent, duplicate-free arrivals, ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
(* ...where jobs are sporadic. *)
Hypothesis H_sporadic_jobs:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* For simplicity, let's define some local names. *)
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
(* Next, let tsk be any task to be scheduled. *)
Variable tsk: Task.
(* Consider any time interval t1, t2)... *)
Variable t1 t2: time.
(* ...and the associated actual arrivals of task tsk. *)
Let arriving_jobs := actual_arrivals_of_task_between job_arrival job_jitter
job_task arr_seq tsk t1 t2.
Let num_arrivals := num_actual_arrivals_of_task job_arrival job_jitter job_task arr_seq tsk t1 t2.
(* Then, consider the sequence of such jobs ordered by arrival times... *)
Let by_arrival_time j j' := job_arrival j ≤ job_arrival j'.
Let sorted_jobs := sort by_arrival_time arriving_jobs.
(* ...and let (nth_job i) denote the i-th job in the sorted sequence. *)
Variable elem: Job.
Let nth_job := nth elem sorted_jobs.
(* First, we recall some trivial properties about nth_job. *)
Remark sorted_arrivals_properties_of_nth:
∀ idx,
idx < num_arrivals →
t1 ≤ actual_job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
(* Next, we conclude that consecutive jobs are different. *)
Lemma sorted_arrivals_current_differs_from_next:
∀ idx,
idx < num_arrivals.-1 →
nth_job idx ≠ nth_job idx.+1.
(* Since the list is sorted, we prove that each job arrives at
least (task_period tsk) time units after the previous job. *)
Lemma sorted_arrivals_separated_by_period:
∀ idx,
idx < num_arrivals.-1 →
job_arrival (nth_job idx.+1) ≥ job_arrival (nth_job idx) + task_period tsk.
(* If the list of arrivals is not empty, we analyze the distance between
the first and last jobs. *)
Section FirstAndLastJobs.
(* Suppose that there is at least one job, ... *)
Hypothesis H_at_least_one_job:
num_arrivals ≥ 1.
(* ...in which case we identify the first and last jobs and their
respective arrival times (note that they could be the same job). *)
Let j_first := nth_job 0.
Let j_last := nth_job (num_arrivals.-1).
Let a_first := job_arrival j_first.
Let a_last := job_arrival j_last.
(* By induction, we prove that that each job with index 'idx' arrives at
least idx*(task_period tsk) units after the first job. *)
Lemma sorted_arrivals_distance_from_first_job:
∀ idx,
idx < num_arrivals →
job_arrival (nth_job idx) ≥ a_first + idx × task_period tsk.
(* Therefore, the first and last jobs are separated by at least
(num_arrivals - 1) periods. *)
Corollary sorted_arrivals_distance_between_first_and_last:
a_last ≥ a_first + (num_arrivals-1) × task_period tsk.
End FirstAndLastJobs.
End DistanceBetweenSporadicJobs.
End TaskArrivalWithJitter.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path.
(* In this file, we provide definitions and lemmas about task arrivals
in jitter-aware schedules. *)
Module TaskArrivalWithJitter.
Import ArrivalSequenceWithJitter SporadicTaskset.
Export TaskArrival.
(* First, we identify the arrivals of a particular task. *)
Section NumberOfArrivals.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
(* Consider any job arrival sequence ...*)
Variable arr_seq: arrival_sequence Job.
(* ...and recall the list of jobs with actual arrival time in a given interval. *)
Let arrivals_between := actual_arrivals_between job_arrival job_jitter arr_seq.
(* Next, let tsk be any task. *)
Variable tsk: Task.
(* By checking the jobs spawned by tsk... *)
Definition is_job_of_tsk := is_job_of_task job_task tsk.
(* ...we identify the jobs of tsk that arrived in any interval t1, t2) ... *)
Definition actual_arrivals_of_task_between (t1 t2: time) :=
[seq j <- arrivals_between t1 t2 | is_job_of_tsk j].
(* ...and also count the number of such job arrivals. *)
Definition num_actual_arrivals_of_task (t1 t2: time) :=
size (actual_arrivals_of_task_between t1 t2).
End NumberOfArrivals.
(* Next, we prove properties about lists of actual arrivals
that are sorted by arrival time. *)
Section DistanceBetweenSporadicJobs.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
(* Consider any arrival sequence with consistent, duplicate-free arrivals, ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
(* ...where jobs are sporadic. *)
Hypothesis H_sporadic_jobs:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* For simplicity, let's define some local names. *)
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
(* Next, let tsk be any task to be scheduled. *)
Variable tsk: Task.
(* Consider any time interval t1, t2)... *)
Variable t1 t2: time.
(* ...and the associated actual arrivals of task tsk. *)
Let arriving_jobs := actual_arrivals_of_task_between job_arrival job_jitter
job_task arr_seq tsk t1 t2.
Let num_arrivals := num_actual_arrivals_of_task job_arrival job_jitter job_task arr_seq tsk t1 t2.
(* Then, consider the sequence of such jobs ordered by arrival times... *)
Let by_arrival_time j j' := job_arrival j ≤ job_arrival j'.
Let sorted_jobs := sort by_arrival_time arriving_jobs.
(* ...and let (nth_job i) denote the i-th job in the sorted sequence. *)
Variable elem: Job.
Let nth_job := nth elem sorted_jobs.
(* First, we recall some trivial properties about nth_job. *)
Remark sorted_arrivals_properties_of_nth:
∀ idx,
idx < num_arrivals →
t1 ≤ actual_job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
(* Next, we conclude that consecutive jobs are different. *)
Lemma sorted_arrivals_current_differs_from_next:
∀ idx,
idx < num_arrivals.-1 →
nth_job idx ≠ nth_job idx.+1.
(* Since the list is sorted, we prove that each job arrives at
least (task_period tsk) time units after the previous job. *)
Lemma sorted_arrivals_separated_by_period:
∀ idx,
idx < num_arrivals.-1 →
job_arrival (nth_job idx.+1) ≥ job_arrival (nth_job idx) + task_period tsk.
(* If the list of arrivals is not empty, we analyze the distance between
the first and last jobs. *)
Section FirstAndLastJobs.
(* Suppose that there is at least one job, ... *)
Hypothesis H_at_least_one_job:
num_arrivals ≥ 1.
(* ...in which case we identify the first and last jobs and their
respective arrival times (note that they could be the same job). *)
Let j_first := nth_job 0.
Let j_last := nth_job (num_arrivals.-1).
Let a_first := job_arrival j_first.
Let a_last := job_arrival j_last.
(* By induction, we prove that that each job with index 'idx' arrives at
least idx*(task_period tsk) units after the first job. *)
Lemma sorted_arrivals_distance_from_first_job:
∀ idx,
idx < num_arrivals →
job_arrival (nth_job idx) ≥ a_first + idx × task_period tsk.
(* Therefore, the first and last jobs are separated by at least
(num_arrivals - 1) periods. *)
Corollary sorted_arrivals_distance_between_first_and_last:
a_last ≥ a_first + (num_arrivals-1) × task_period tsk.
End FirstAndLastJobs.
End DistanceBetweenSporadicJobs.
End TaskArrivalWithJitter.