Library rt.analysis.basic.bertogna_fp_theory
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.constrained_deadlines
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.response_time rt.model.basic.interference.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_fp.
Module ResponseTimeAnalysisFP.
Export Job SporadicTaskset ScheduleOfSporadicTask Workload Interference
InterferenceBoundFP Platform Schedulability ResponseTime
Priority SporadicTaskArrival WorkloadBound ConstrainedDeadlines.
(* In this section, we prove that any fixed point in Bertogna and
Cirinei's RTA for FP scheduling is a safe response-time bound.
This analysis can be found in Chapter 18.2 of Baruah et al.'s
book Multiprocessor Scheduling for Real-time Systems. *)
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Assume that we have a task set where all tasks have valid
parameters and constrained deadlines, ... *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk ∈ ts → task_deadline tsk ≤ task_period tsk.
(* ... and that all jobs in the arrival sequence come from the task set. *)
Hypothesis H_all_jobs_from_taskset:
∀ (j: JobIn arr_seq), job_task j ∈ ts.
(* Next, consider any schedule such that...*)
Variable num_cpus: nat.
Variable sched: schedule num_cpus arr_seq.
(* ...jobs are sequential and do not execute before their
arrival times nor longer than their execution costs. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that there exists at least one processor. *)
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Consider a given FP policy, ... *)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is a work-conserving
schedule that enforces this policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_enforces_FP_policy:
enforces_FP_policy job_cost job_task sched higher_eq_priority.
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Next, we consider the response-time recurrence.
Let tsk be a task in ts that is to be analyzed. *)
Variable tsk: sporadic_task.
Hypothesis task_in_ts: tsk ∈ ts.
(* Let is_hp_task denote whether a task is a higher-priority task
(with respect to tsk). *)
Let is_hp_task := higher_priority_task higher_eq_priority tsk.
(* Assume a response-time bound is known... *)
Let task_with_response_time := (sporadic_task × time)%type.
Variable hp_bounds: seq task_with_response_time.
Hypothesis H_response_time_of_interfering_tasks_is_known:
∀ hp_tsk R,
(hp_tsk, R) ∈ hp_bounds →
response_time_bounded_by hp_tsk R.
(* ... for every higher-priority task. *)
Hypothesis H_hp_bounds_has_interfering_tasks:
∀ hp_tsk,
hp_tsk ∈ ts →
is_hp_task hp_tsk →
∃ R, (hp_tsk, R) ∈ hp_bounds.
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
∀ hp_tsk R,
(hp_tsk, R) ∈ hp_bounds → R ≥ task_cost hp_tsk.
(* Assume that no deadline is missed by any higher-priority task. *)
Hypothesis H_interfering_tasks_miss_no_deadlines:
∀ hp_tsk R,
(hp_tsk, R) ∈ hp_bounds → R ≤ task_deadline hp_tsk.
(* Let R be the fixed point of Bertogna and Cirinei's recurrence, ...*)
Variable R: time.
Hypothesis H_response_time_recurrence_holds :
R = task_cost tsk +
div_floor
(total_interference_bound_fp task_cost task_period tsk hp_bounds R)
num_cpus.
(* ... and assume that R is no larger than the deadline of tsk.*)
Hypothesis H_response_time_no_larger_than_deadline:
R ≤ task_deadline tsk.
(* In order to prove that R is a response-time bound, we first provide some lemmas. *)
Section Lemmas.
(* Consider any job j of tsk. *)
Variable j: JobIn arr_seq.
Hypothesis H_job_of_tsk: job_task j = tsk.
(* Assume that job j is the first job of tsk not to complete by the response time bound. *)
Hypothesis H_j_not_completed: ¬ completed job_cost sched j (job_arrival j + R).
Hypothesis H_previous_jobs_of_tsk_completed :
∀ (j0: JobIn arr_seq),
job_task j0 = tsk →
job_arrival j0 < job_arrival j →
completed job_cost sched j0 (job_arrival j0 + R).
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference job_cost job_task sched j tsk_other
(job_arrival j) (job_arrival j + R).
(* ...and X the total interference incurred by job j due to any task. *)
Let X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
(* Recall Bertogna and Cirinei's workload bound. *)
Let workload_bound (tsk_other: sporadic_task) (R_other: time) :=
W task_cost task_period tsk_other R_other R.
(* Let hp_tasks denote the set of higher-priority tasks. *)
Let hp_tasks := [seq tsk_other <- ts | is_hp_task tsk_other].
(* Now we establish results about the higher-priority tasks. *)
Section LemmasAboutHPTasks.
(* Let (tsk_other, R_other) be any pair of higher-priority task and
response-time bound computed in previous iterations. *)
Variable tsk_other: sporadic_task.
Variable R_other: time.
Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) ∈ hp_bounds.
(* Since tsk_other cannot interfere more than it executes, we show that
the interference caused by tsk_other is no larger than workload bound W. *)
Lemma bertogna_fp_workload_bounds_interference :
x tsk_other ≤ workload_bound tsk_other R_other.
End LemmasAboutHPTasks.
(* Next we prove some lemmas that help to derive a contradiction.*)
Section DerivingContradiction.
(* 0) Since job j did not complete by its response time bound, it follows that
the total interference X >= R - e_k + 1. *)
Lemma bertogna_fp_too_much_interference : X ≥ R - task_cost tsk + 1.
(* 1) Next, we prove that during the scheduling window of j, any job that is
scheduled while j is backlogged comes from a different task.
This follows from the fact that j is the first job not to complete
by its response-time bound, so previous jobs of j's task must have
completed by their periods and cannot be pending. *)
Lemma bertogna_fp_interference_by_different_tasks :
∀ t j_other,
job_arrival j ≤ t < job_arrival j + R →
backlogged job_cost sched j t →
scheduled sched j_other t →
job_task j_other ≠ tsk.
(* Let's define a predicate to identify the other tasks that are scheduled. *)
Let other_scheduled_task (t: time) (tsk_other: sporadic_task) :=
task_is_scheduled job_task sched tsk_other t ∧
is_hp_task tsk_other.
(* 2) Now we prove that, at all times that j is backlogged, the number
of tasks other than tsk that are scheduled is exactly the number
of processors in the system. This is required to prove lemma (3). *)
Lemma bertogna_fp_all_cpus_are_busy:
∀ t,
job_arrival j ≤ t < job_arrival j + R →
backlogged job_cost sched j t →
count (other_scheduled_task t) ts = num_cpus.
(* 3) Now we prove that, at all times that j is backlogged, the number
of tasks other than tsk that are scheduled is exactly the number
of processors in the system. This is required to prove lemma (4). *)
Lemma bertogna_fp_interference_on_all_cpus :
\sum_(tsk_k <- hp_tasks) x tsk_k = X × num_cpus.
(* Before stating the next lemma, let (num_tasks_exceeding delta) be the
number of interfering tasks whose interference x is larger than delta. *)
Let num_tasks_exceeding delta := count (fun i ⇒ x i ≥ delta) (hp_tasks).
(* 4) Now we prove that, for any delta, if (num_task_exceeding delta > 0), then the
cumulative interference caused by the complementary set of interfering tasks fills
the remaining, not-completely-full (num_cpus - num_tasks_exceeding delta)
processors. *)
Lemma bertogna_fp_interference_in_non_full_processors :
∀ delta,
0 < num_tasks_exceeding delta < num_cpus →
\sum_(i <- hp_tasks | x i < delta) x i ≥ delta × (num_cpus - num_tasks_exceeding delta).
(* 5) Based on lemma (4), we prove that, for any interval delta, if the sum of per-task
interference exceeds (delta * num_cpus), the same applies for the
sum of the minimum of the interference and delta. *)
Lemma bertogna_fp_minimum_exceeds_interference :
∀ delta,
\sum_(tsk_k <- hp_tasks) x tsk_k ≥ delta × num_cpus →
\sum_(tsk_k <- hp_tasks) minn (x tsk_k) delta ≥
delta × num_cpus.
(* 6) Next, using lemmas (0), (3) and (5) we prove that the reduction-based
interference bound is not enough to cover the sum of the minima over all tasks
(artifact of the proof by contradiction). *)
Lemma bertogna_fp_sum_exceeds_total_interference:
\sum_((tsk_k, R_k) <- hp_bounds)
minn (x tsk_k) (R - task_cost tsk + 1) >
total_interference_bound_fp task_cost task_period tsk hp_bounds R.
(* 7) After concluding that the sum of the minima exceeds (R - e_i + 1),
we prove that there exists a tuple (tsk_k, R_k) that satisfies
min (x_k, R - e_i + 1) > min (W_k, R - e_i + 1).
This implies that x_k > W_k, which is of course a contradiction,
since W_k is a valid task interference bound. *)
Lemma bertogna_fp_exists_task_that_exceeds_bound :
∃ tsk_k R_k,
(tsk_k, R_k) ∈ hp_bounds ∧
(minn (x tsk_k) (R - task_cost tsk + 1) >
minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
End DerivingContradiction.
End Lemmas.
(* Using the lemmas above, we prove that R bounds the response time of task tsk. *)
Theorem bertogna_cirinei_response_time_bound_fp :
response_time_bounded_by tsk R.
End ResponseTimeBound.
End ResponseTimeAnalysisFP.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
rt.model.basic.schedule rt.model.basic.platform rt.model.basic.constrained_deadlines
rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
rt.model.basic.response_time rt.model.basic.interference.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_fp.
Module ResponseTimeAnalysisFP.
Export Job SporadicTaskset ScheduleOfSporadicTask Workload Interference
InterferenceBoundFP Platform Schedulability ResponseTime
Priority SporadicTaskArrival WorkloadBound ConstrainedDeadlines.
(* In this section, we prove that any fixed point in Bertogna and
Cirinei's RTA for FP scheduling is a safe response-time bound.
This analysis can be found in Chapter 18.2 of Baruah et al.'s
book Multiprocessor Scheduling for Real-time Systems. *)
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Assume that we have a task set where all tasks have valid
parameters and constrained deadlines, ... *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk ∈ ts → task_deadline tsk ≤ task_period tsk.
(* ... and that all jobs in the arrival sequence come from the task set. *)
Hypothesis H_all_jobs_from_taskset:
∀ (j: JobIn arr_seq), job_task j ∈ ts.
(* Next, consider any schedule such that...*)
Variable num_cpus: nat.
Variable sched: schedule num_cpus arr_seq.
(* ...jobs are sequential and do not execute before their
arrival times nor longer than their execution costs. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that there exists at least one processor. *)
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Consider a given FP policy, ... *)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is a work-conserving
schedule that enforces this policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_enforces_FP_policy:
enforces_FP_policy job_cost job_task sched higher_eq_priority.
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Next, we consider the response-time recurrence.
Let tsk be a task in ts that is to be analyzed. *)
Variable tsk: sporadic_task.
Hypothesis task_in_ts: tsk ∈ ts.
(* Let is_hp_task denote whether a task is a higher-priority task
(with respect to tsk). *)
Let is_hp_task := higher_priority_task higher_eq_priority tsk.
(* Assume a response-time bound is known... *)
Let task_with_response_time := (sporadic_task × time)%type.
Variable hp_bounds: seq task_with_response_time.
Hypothesis H_response_time_of_interfering_tasks_is_known:
∀ hp_tsk R,
(hp_tsk, R) ∈ hp_bounds →
response_time_bounded_by hp_tsk R.
(* ... for every higher-priority task. *)
Hypothesis H_hp_bounds_has_interfering_tasks:
∀ hp_tsk,
hp_tsk ∈ ts →
is_hp_task hp_tsk →
∃ R, (hp_tsk, R) ∈ hp_bounds.
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
∀ hp_tsk R,
(hp_tsk, R) ∈ hp_bounds → R ≥ task_cost hp_tsk.
(* Assume that no deadline is missed by any higher-priority task. *)
Hypothesis H_interfering_tasks_miss_no_deadlines:
∀ hp_tsk R,
(hp_tsk, R) ∈ hp_bounds → R ≤ task_deadline hp_tsk.
(* Let R be the fixed point of Bertogna and Cirinei's recurrence, ...*)
Variable R: time.
Hypothesis H_response_time_recurrence_holds :
R = task_cost tsk +
div_floor
(total_interference_bound_fp task_cost task_period tsk hp_bounds R)
num_cpus.
(* ... and assume that R is no larger than the deadline of tsk.*)
Hypothesis H_response_time_no_larger_than_deadline:
R ≤ task_deadline tsk.
(* In order to prove that R is a response-time bound, we first provide some lemmas. *)
Section Lemmas.
(* Consider any job j of tsk. *)
Variable j: JobIn arr_seq.
Hypothesis H_job_of_tsk: job_task j = tsk.
(* Assume that job j is the first job of tsk not to complete by the response time bound. *)
Hypothesis H_j_not_completed: ¬ completed job_cost sched j (job_arrival j + R).
Hypothesis H_previous_jobs_of_tsk_completed :
∀ (j0: JobIn arr_seq),
job_task j0 = tsk →
job_arrival j0 < job_arrival j →
completed job_cost sched j0 (job_arrival j0 + R).
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference job_cost job_task sched j tsk_other
(job_arrival j) (job_arrival j + R).
(* ...and X the total interference incurred by job j due to any task. *)
Let X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
(* Recall Bertogna and Cirinei's workload bound. *)
Let workload_bound (tsk_other: sporadic_task) (R_other: time) :=
W task_cost task_period tsk_other R_other R.
(* Let hp_tasks denote the set of higher-priority tasks. *)
Let hp_tasks := [seq tsk_other <- ts | is_hp_task tsk_other].
(* Now we establish results about the higher-priority tasks. *)
Section LemmasAboutHPTasks.
(* Let (tsk_other, R_other) be any pair of higher-priority task and
response-time bound computed in previous iterations. *)
Variable tsk_other: sporadic_task.
Variable R_other: time.
Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) ∈ hp_bounds.
(* Since tsk_other cannot interfere more than it executes, we show that
the interference caused by tsk_other is no larger than workload bound W. *)
Lemma bertogna_fp_workload_bounds_interference :
x tsk_other ≤ workload_bound tsk_other R_other.
End LemmasAboutHPTasks.
(* Next we prove some lemmas that help to derive a contradiction.*)
Section DerivingContradiction.
(* 0) Since job j did not complete by its response time bound, it follows that
the total interference X >= R - e_k + 1. *)
Lemma bertogna_fp_too_much_interference : X ≥ R - task_cost tsk + 1.
(* 1) Next, we prove that during the scheduling window of j, any job that is
scheduled while j is backlogged comes from a different task.
This follows from the fact that j is the first job not to complete
by its response-time bound, so previous jobs of j's task must have
completed by their periods and cannot be pending. *)
Lemma bertogna_fp_interference_by_different_tasks :
∀ t j_other,
job_arrival j ≤ t < job_arrival j + R →
backlogged job_cost sched j t →
scheduled sched j_other t →
job_task j_other ≠ tsk.
(* Let's define a predicate to identify the other tasks that are scheduled. *)
Let other_scheduled_task (t: time) (tsk_other: sporadic_task) :=
task_is_scheduled job_task sched tsk_other t ∧
is_hp_task tsk_other.
(* 2) Now we prove that, at all times that j is backlogged, the number
of tasks other than tsk that are scheduled is exactly the number
of processors in the system. This is required to prove lemma (3). *)
Lemma bertogna_fp_all_cpus_are_busy:
∀ t,
job_arrival j ≤ t < job_arrival j + R →
backlogged job_cost sched j t →
count (other_scheduled_task t) ts = num_cpus.
(* 3) Now we prove that, at all times that j is backlogged, the number
of tasks other than tsk that are scheduled is exactly the number
of processors in the system. This is required to prove lemma (4). *)
Lemma bertogna_fp_interference_on_all_cpus :
\sum_(tsk_k <- hp_tasks) x tsk_k = X × num_cpus.
(* Before stating the next lemma, let (num_tasks_exceeding delta) be the
number of interfering tasks whose interference x is larger than delta. *)
Let num_tasks_exceeding delta := count (fun i ⇒ x i ≥ delta) (hp_tasks).
(* 4) Now we prove that, for any delta, if (num_task_exceeding delta > 0), then the
cumulative interference caused by the complementary set of interfering tasks fills
the remaining, not-completely-full (num_cpus - num_tasks_exceeding delta)
processors. *)
Lemma bertogna_fp_interference_in_non_full_processors :
∀ delta,
0 < num_tasks_exceeding delta < num_cpus →
\sum_(i <- hp_tasks | x i < delta) x i ≥ delta × (num_cpus - num_tasks_exceeding delta).
(* 5) Based on lemma (4), we prove that, for any interval delta, if the sum of per-task
interference exceeds (delta * num_cpus), the same applies for the
sum of the minimum of the interference and delta. *)
Lemma bertogna_fp_minimum_exceeds_interference :
∀ delta,
\sum_(tsk_k <- hp_tasks) x tsk_k ≥ delta × num_cpus →
\sum_(tsk_k <- hp_tasks) minn (x tsk_k) delta ≥
delta × num_cpus.
(* 6) Next, using lemmas (0), (3) and (5) we prove that the reduction-based
interference bound is not enough to cover the sum of the minima over all tasks
(artifact of the proof by contradiction). *)
Lemma bertogna_fp_sum_exceeds_total_interference:
\sum_((tsk_k, R_k) <- hp_bounds)
minn (x tsk_k) (R - task_cost tsk + 1) >
total_interference_bound_fp task_cost task_period tsk hp_bounds R.
(* 7) After concluding that the sum of the minima exceeds (R - e_i + 1),
we prove that there exists a tuple (tsk_k, R_k) that satisfies
min (x_k, R - e_i + 1) > min (W_k, R - e_i + 1).
This implies that x_k > W_k, which is of course a contradiction,
since W_k is a valid task interference bound. *)
Lemma bertogna_fp_exists_task_that_exceeds_bound :
∃ tsk_k R_k,
(tsk_k, R_k) ∈ hp_bounds ∧
(minn (x tsk_k) (R - task_cost tsk + 1) >
minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
End DerivingContradiction.
End Lemmas.
(* Using the lemmas above, we prove that R bounds the response time of task tsk. *)
Theorem bertogna_cirinei_response_time_bound_fp :
response_time_bounded_by tsk R.
End ResponseTimeBound.
End ResponseTimeAnalysisFP.