Library rt.model.arrival.jitter.arrival_bounds
Require Import rt.util.all.
Require Import rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.arrival.jitter.job
rt.model.arrival.jitter.arrival_sequence
rt.model.arrival.jitter.task_arrival.
(* In this file, we prove bounds on the number of actual task arrivals, i.e,
taking release jitter into account. *)
Module ArrivalBounds.
Import JobWithJitter ArrivalSequenceWithJitter SporadicTaskset Priority
TaskArrivalWithJitter.
Section BoundingActualArrivals.
Context {Task: eqType}.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: 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.
(* ...where the jitter of each job is bounded by the jitter of its task. *)
Hypothesis H_job_jitter_bounded:
∀ j,
arrives_in arr_seq j →
job_jitter_leq_task_jitter task_jitter job_jitter job_task j.
(* For simplicity, let's define some local names. *)
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
(* In this section, we prove an upper bound on the number of jobs with actual arrival time
in a given interval. *)
Section UpperBoundOn.
(* 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 with actual arrival time in [t1, t2), along with the corresponding
number of arrivals. *)
Let actual_arrivals := actual_arrivals_of_task_between job_arrival job_jitter
job_task arr_seq tsk t1 t2.
Let num_actual_arrivals := num_actual_arrivals_of_task job_arrival job_jitter job_task
arr_seq tsk t1 t2.
(* We will establish an upper bound on the number of actual arrivals of tsk.
The proof follows by case analysis. *)
(* Case 1: Assume that there are no jobs of tsk with actual arrival time in the interval. *)
Section NoJobs.
(* If there are no actual arrivals in [t1, t2), ...*)
Hypothesis H_no_jobs: num_actual_arrivals = 0.
(* ...then the arrival bound trivially holds. *)
Lemma sporadic_arrival_bound_no_jobs:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End NoJobs.
(* Case 2: Assume that a single job of tsk has actual arrival time 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_actual_arrivals > 0 →
t1 < t2.
(* Therefore, if there is one job of tsk with actual arrival time in [t1, t2), ... *)
Hypothesis H_no_jobs: num_actual_arrivals = 1.
(* ...then (t2 - t1) > 0 and the arrival bound also holds. *)
Lemma sporadic_arrival_bound_one_job:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End OneJob.
(* Case 3: There are at least two actual job arrivals. *)
Section AtLeastTwoJobs.
(* Assume that there are at least two jobs of tsk with actual arrival in [t1,t2). *)
Hypothesis H_at_least_two_jobs: num_actual_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 + task_jitter tsk - t1) (task_period tsk) < num_actual_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 actual_arrivals.
(* 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_actual_arrivals.-1).
Let a_first := job_arrival j_first.
Let a_last := job_arrival j_last.
(* Next, we recall from task_arrival.v the properties of the n-th job in
the sequence... *)
Corollary sporadic_arrival_bound_properties_of_nth:
∀ idx,
idx < num_actual_arrivals →
t1 ≤ actual_job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
(* ...and that the first and last jobs are separated by at least
(num_actual_arrivals - 1) periods. *)
Corollary sporadic_arrival_bound_distance_between_first_and_last:
a_last ≥ a_first + (num_actual_arrivals - 1) × task_period tsk.
(* Next, because the number of actual 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 plus the jitter of the task, ... *)
Lemma sporadic_arrival_bound_last_job_too_far:
a_first + t2 + task_jitter tsk - 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 actual arrival time of 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 actual arrivals). *)
Lemma sporadic_task_arrival_bound_at_least_two_jobs:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End AtLeastTwoJobs.
(* Using the case analysis above, we prove that the number of actual arrivals of tsk
can be upper-bounded using the length of the interval as follows. *)
Theorem sporadic_task_with_jitter_arrival_bound:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End UpperBoundOn.
End BoundingActualArrivals.
End ArrivalBounds.
Require Import rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.arrival.jitter.job
rt.model.arrival.jitter.arrival_sequence
rt.model.arrival.jitter.task_arrival.
(* In this file, we prove bounds on the number of actual task arrivals, i.e,
taking release jitter into account. *)
Module ArrivalBounds.
Import JobWithJitter ArrivalSequenceWithJitter SporadicTaskset Priority
TaskArrivalWithJitter.
Section BoundingActualArrivals.
Context {Task: eqType}.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: 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.
(* ...where the jitter of each job is bounded by the jitter of its task. *)
Hypothesis H_job_jitter_bounded:
∀ j,
arrives_in arr_seq j →
job_jitter_leq_task_jitter task_jitter job_jitter job_task j.
(* For simplicity, let's define some local names. *)
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
(* In this section, we prove an upper bound on the number of jobs with actual arrival time
in a given interval. *)
Section UpperBoundOn.
(* 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 with actual arrival time in [t1, t2), along with the corresponding
number of arrivals. *)
Let actual_arrivals := actual_arrivals_of_task_between job_arrival job_jitter
job_task arr_seq tsk t1 t2.
Let num_actual_arrivals := num_actual_arrivals_of_task job_arrival job_jitter job_task
arr_seq tsk t1 t2.
(* We will establish an upper bound on the number of actual arrivals of tsk.
The proof follows by case analysis. *)
(* Case 1: Assume that there are no jobs of tsk with actual arrival time in the interval. *)
Section NoJobs.
(* If there are no actual arrivals in [t1, t2), ...*)
Hypothesis H_no_jobs: num_actual_arrivals = 0.
(* ...then the arrival bound trivially holds. *)
Lemma sporadic_arrival_bound_no_jobs:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End NoJobs.
(* Case 2: Assume that a single job of tsk has actual arrival time 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_actual_arrivals > 0 →
t1 < t2.
(* Therefore, if there is one job of tsk with actual arrival time in [t1, t2), ... *)
Hypothesis H_no_jobs: num_actual_arrivals = 1.
(* ...then (t2 - t1) > 0 and the arrival bound also holds. *)
Lemma sporadic_arrival_bound_one_job:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End OneJob.
(* Case 3: There are at least two actual job arrivals. *)
Section AtLeastTwoJobs.
(* Assume that there are at least two jobs of tsk with actual arrival in [t1,t2). *)
Hypothesis H_at_least_two_jobs: num_actual_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 + task_jitter tsk - t1) (task_period tsk) < num_actual_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 actual_arrivals.
(* 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_actual_arrivals.-1).
Let a_first := job_arrival j_first.
Let a_last := job_arrival j_last.
(* Next, we recall from task_arrival.v the properties of the n-th job in
the sequence... *)
Corollary sporadic_arrival_bound_properties_of_nth:
∀ idx,
idx < num_actual_arrivals →
t1 ≤ actual_job_arrival (nth_job idx) < t2 ∧
job_task (nth_job idx) = tsk ∧
arrives_in arr_seq (nth_job idx).
(* ...and that the first and last jobs are separated by at least
(num_actual_arrivals - 1) periods. *)
Corollary sporadic_arrival_bound_distance_between_first_and_last:
a_last ≥ a_first + (num_actual_arrivals - 1) × task_period tsk.
(* Next, because the number of actual 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 plus the jitter of the task, ... *)
Lemma sporadic_arrival_bound_last_job_too_far:
a_first + t2 + task_jitter tsk - 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 actual arrival time of 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 actual arrivals). *)
Lemma sporadic_task_arrival_bound_at_least_two_jobs:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End AtLeastTwoJobs.
(* Using the case analysis above, we prove that the number of actual arrivals of tsk
can be upper-bounded using the length of the interval as follows. *)
Theorem sporadic_task_with_jitter_arrival_bound:
num_actual_arrivals ≤ div_ceil (t2 + task_jitter tsk - t1) (task_period tsk).
End UpperBoundOn.
End BoundingActualArrivals.
End ArrivalBounds.