Library prosa.classic.model.arrival.basic.arrival_bounds
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.priority.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path div.
(* Properties of job arrival. *)
Module ArrivalBounds.
Import ArrivalSequence SporadicTaskset TaskArrival Priority.
Section Lemmas.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
(* In this section, we upper bound the number of jobs that can arrive in any interval. *)
Section BoundOnSporadicArrivals.
(* Assume that jobs are sporadic. *)
Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
(* Consider any time interval t1, t2)... *)
Variable t1 t2: time.
(* ...and let tsk be any task with period > 0. *)
Variable tsk: Task.
Hypothesis H_period_gt_zero: task_period tsk > 0.
(* Recall the jobs of tsk during t1, t2), along with the number of arrivals. *)
Let arriving_jobs := arrivals_of_task_between job_task arr_seq tsk t1 t2.
Let num_arrivals := num_arrivals_of_task job_task arr_seq tsk t1 t2.
(* We will establish an upper bound on the number of arriving jobs of tsk.
The proof follows by case analysis. *)
(* Case 1: Assume that no jobs of tsk arrive in the interval. *)
Section NoJobs.
(* If there are no arriving jobs in t1, t2), *)
Hypothesis... H_no_jobs: num_arrivals = 0.
(* ...then the arrival bound trivially holds. *)
Lemma sporadic_arrival_bound_no_jobs:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End NoJobs.
(* Case 2: Assume that a single job of tsk arrives in the interval. *)
Section OneJob.
(* First, note that since the interval is open at time t2,
t2 must be larger than t1. *)
Lemma sporadic_arrival_bound_more_than_one_point:
num_arrivals > 0 →
t1 < t2.
(* Therefore, if there is one job of tsk arriving during t1, t2), ... *)
Hypothesis H_no_jobs: num_arrivals = 1.
(* ...then (t2 - t1) > 0 and the arrival bound also holds. *)
Lemma sporadic_arrival_bound_one_job:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End OneJob.
(* Case 3: There are at least two arriving jobs. *)
Section AtLeastTwoJobs.
(* Assume that there are at least two jobs of tsk arriving in t1,t2). *)
Hypothesis H_at_least_two_jobs: num_arrivals ≥ 2.
(* We prove the arrival bound by contradiction. *)
Section DerivingContradiction.
(* Suppose that the number of arrivals is larger than the bound. *)
Hypothesis H_many_arrivals: div_ceil (t2 - t1) (task_period tsk) < num_arrivals.
(* Consider the list of 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.
(* Based on the notation for the n-th job in the sorted list of arrivals, ... *)
Variable elem: Job.
Let nth_job := nth elem sorted_jobs.
(* ...we identify the first and last jobs and their respective arrival times. *)
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.
(* Recall from task_arrival.v the properties of the n-th job ...*)
Corollary sporadic_arrival_bound_properties_of_nth:
∀ idx,
idx < num_arrivals →
t1 ≤ job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
(* ...and the distance between the first and last jobs. *)
Corollary sporadic_arrival_bound_distance_between_first_and_last:
a_last ≥ a_first + (num_arrivals-1) × task_period tsk.
(* Because the number of arrivals is larger than the ceiling term,
it follows that the first and last jobs are separated by at
least the length of the interval, ... *)
Lemma sporadic_arrival_bound_last_job_too_far:
a_first + t2 - t1 ≤ a_last.
(* ...which implies that the last job arrives after the interval. *)
Lemma sporadic_arrival_bound_last_arrives_too_late:
a_last ≥ t2.
(* However, the last job must lie within t1, t2). Contradiction! *)
Lemma sporadic_arrival_bound_case_3_contradiction: False.
End DerivingContradiction.
(* From the contradiction above, we prove that the arrival bound
is correct for case 3 (i.e., at least two arriving jobs). *)
Lemma sporadic_task_arrival_bound_at_least_two_jobs:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End AtLeastTwoJobs.
(* Using the case analysis, we prove that the number of job arrivals of tsk
can be upper-bounded using the length of the interval as follows. *)
Theorem sporadic_task_arrival_bound:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End BoundOnSporadicArrivals.
End Lemmas.
End ArrivalBounds.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.priority.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path div.
(* Properties of job arrival. *)
Module ArrivalBounds.
Import ArrivalSequence SporadicTaskset TaskArrival Priority.
Section Lemmas.
Context {Task: eqType}.
Variable task_period: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
(* In this section, we upper bound the number of jobs that can arrive in any interval. *)
Section BoundOnSporadicArrivals.
(* Assume that jobs are sporadic. *)
Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
(* Consider any time interval t1, t2)... *)
Variable t1 t2: time.
(* ...and let tsk be any task with period > 0. *)
Variable tsk: Task.
Hypothesis H_period_gt_zero: task_period tsk > 0.
(* Recall the jobs of tsk during t1, t2), along with the number of arrivals. *)
Let arriving_jobs := arrivals_of_task_between job_task arr_seq tsk t1 t2.
Let num_arrivals := num_arrivals_of_task job_task arr_seq tsk t1 t2.
(* We will establish an upper bound on the number of arriving jobs of tsk.
The proof follows by case analysis. *)
(* Case 1: Assume that no jobs of tsk arrive in the interval. *)
Section NoJobs.
(* If there are no arriving jobs in t1, t2), *)
Hypothesis... H_no_jobs: num_arrivals = 0.
(* ...then the arrival bound trivially holds. *)
Lemma sporadic_arrival_bound_no_jobs:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End NoJobs.
(* Case 2: Assume that a single job of tsk arrives in the interval. *)
Section OneJob.
(* First, note that since the interval is open at time t2,
t2 must be larger than t1. *)
Lemma sporadic_arrival_bound_more_than_one_point:
num_arrivals > 0 →
t1 < t2.
(* Therefore, if there is one job of tsk arriving during t1, t2), ... *)
Hypothesis H_no_jobs: num_arrivals = 1.
(* ...then (t2 - t1) > 0 and the arrival bound also holds. *)
Lemma sporadic_arrival_bound_one_job:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End OneJob.
(* Case 3: There are at least two arriving jobs. *)
Section AtLeastTwoJobs.
(* Assume that there are at least two jobs of tsk arriving in t1,t2). *)
Hypothesis H_at_least_two_jobs: num_arrivals ≥ 2.
(* We prove the arrival bound by contradiction. *)
Section DerivingContradiction.
(* Suppose that the number of arrivals is larger than the bound. *)
Hypothesis H_many_arrivals: div_ceil (t2 - t1) (task_period tsk) < num_arrivals.
(* Consider the list of 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.
(* Based on the notation for the n-th job in the sorted list of arrivals, ... *)
Variable elem: Job.
Let nth_job := nth elem sorted_jobs.
(* ...we identify the first and last jobs and their respective arrival times. *)
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.
(* Recall from task_arrival.v the properties of the n-th job ...*)
Corollary sporadic_arrival_bound_properties_of_nth:
∀ idx,
idx < num_arrivals →
t1 ≤ job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
(* ...and the distance between the first and last jobs. *)
Corollary sporadic_arrival_bound_distance_between_first_and_last:
a_last ≥ a_first + (num_arrivals-1) × task_period tsk.
(* Because the number of arrivals is larger than the ceiling term,
it follows that the first and last jobs are separated by at
least the length of the interval, ... *)
Lemma sporadic_arrival_bound_last_job_too_far:
a_first + t2 - t1 ≤ a_last.
(* ...which implies that the last job arrives after the interval. *)
Lemma sporadic_arrival_bound_last_arrives_too_late:
a_last ≥ t2.
(* However, the last job must lie within t1, t2). Contradiction! *)
Lemma sporadic_arrival_bound_case_3_contradiction: False.
End DerivingContradiction.
(* From the contradiction above, we prove that the arrival bound
is correct for case 3 (i.e., at least two arriving jobs). *)
Lemma sporadic_task_arrival_bound_at_least_two_jobs:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End AtLeastTwoJobs.
(* Using the case analysis, we prove that the number of job arrivals of tsk
can be upper-bounded using the length of the interval as follows. *)
Theorem sporadic_task_arrival_bound:
num_arrivals ≤ div_ceil (t2 - t1) (task_period tsk).
End BoundOnSporadicArrivals.
End Lemmas.
End ArrivalBounds.