Library prosa.classic.analysis.apa.bertogna_edf_comp
Require Import prosa.classic.util.all.
Require Import prosa.classic.analysis.apa.bertogna_edf_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDF.
(* In this section, we define the algorithm corresponding to the APA-reduction
of Bertogna and Cirinei's RTA for EDF scheduling. *)
Section Analysis.
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_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* As input for each iteration of the algorithm, we consider pairs
of tasks and response-time bounds. *)
Let task_with_response_time := (sporadic_task × time)%type.
(* Consider a platform with num_cpus processors. *)
Variable num_cpus: nat.
(* Assume that every task has a processor affinity alpha. *)
Variable alpha: task_affinity sporadic_task num_cpus.
(* For the reduction to subproblems, consider a subaffinity alpha' for each task. *)
Variable alpha': task_affinity sporadic_task num_cpus.
(* First, recall the interference bound under EDF. Note that we use
subaffinity (alpha' tsk) when computing the set of interfering tasks. *)
Let I (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline alpha tsk
(alpha' tsk) (* Subproblem alpha' *)
rt_bounds delta.
(* Then, we define the response-time recurrence. Note that we divide the
interference by the cardinality of (alpha' tsk). *)
Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
task_cost tsk + div_floor (I rt_bounds tsk delta)
#|alpha' tsk|.
(* Also note that a response-time is only valid if it is no larger
than the deadline. *)
Definition R_le_deadline (pair: task_with_response_time) :=
let (tsk, R) := pair in
R ≤ task_deadline tsk.
(* Next, we define the fixed-point iteration for computing the
response-time bound of each task. *)
(* Given a sequence 'rt_bounds' of task and response-time bounds
from the previous iteration, we compute the response-time
bound of a single task using the RTA for EDF. *)
Definition update_bound (rt_bounds: seq task_with_response_time) pair :=
let '(tsk, R) := pair in
(tsk, edf_response_time_bound rt_bounds tsk R).
(* To compute the response-time bounds of the entire task set,
we start the iteration with a sequence of tasks and costs:
<(task1, cost1), (task2, cost2), ...>. *)
Let initial_state (ts: seq sporadic_task) :=
map (fun tsk ⇒ (tsk, task_cost tsk)) ts.
(* Then, we successively update the the response-time bounds based
on the slack computed in the previous iteration. *)
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
map (update_bound rt_bounds) rt_bounds.
(* To ensure that the procedure converges, we stop the iteration
after a "sufficient" number of times, which corresponds to
the time complexity of the procedure. *)
Let max_steps (ts: seq sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
(* This yields the following definition for the RTA. At the end
we check if all computed response-time bounds are less than
or equal to the deadline, in which case they are valid. *)
Definition edf_claimed_bounds (ts: seq sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then
Some R_values
else None.
(* The schedulability test simply checks if we got a list of
response-time bounds (i.e., if the computation did not fail). *)
Definition edf_schedulable (ts: seq sporadic_task) :=
edf_claimed_bounds ts != None.
(* In the following section, we prove several helper lemmas about the
list of tasks/response-time bounds. *)
Section SimpleLemmas.
(* Updating a single response-time bound does not modify the task. *)
Lemma edf_claimed_bounds_unzip1_update_bound :
∀ l rt_bounds,
unzip1 (map (update_bound rt_bounds) l) = unzip1 l.
(* At any point of the iteration, the tasks are the same. *)
Lemma edf_claimed_bounds_unzip1_iteration :
∀ l k,
unzip1 (iter k edf_rta_iteration (initial_state l)) = l.
(* The iteration preserves the size of the list. *)
Lemma edf_claimed_bounds_size :
∀ l k,
size (iter k edf_rta_iteration (initial_state l)) = size l.
(* If the analysis succeeds, the computed response-time bounds are no smaller
than the task cost. *)
Lemma edf_claimed_bounds_ge_cost :
∀ l k tsk R,
(tsk, R) \in (iter k edf_rta_iteration (initial_state l)) →
R ≥ task_cost tsk.
(* If the analysis suceeds, the computed response-time bounds are no larger
than the deadline. *)
Lemma edf_claimed_bounds_le_deadline :
∀ ts rt_bounds tsk R,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
(* The list contains a response-time bound for every task in the task set. *)
Lemma edf_claimed_bounds_has_R_for_every_task :
∀ ts rt_bounds tsk,
edf_claimed_bounds ts = Some rt_bounds →
tsk \in ts →
∃ R,
(tsk, R) \in rt_bounds.
End SimpleLemmas.
(* In this section, we prove the convergence of the RTA procedure.
Since we define the RTA procedure as the application of a function
a fixed number of times, this translates into proving that the value
of the iteration at (max_steps ts) is equal to the value at (max_steps ts) + 1. *)
Section Convergence.
(* Consider any sequence of tasks with valid parameters. *)
Variable ts: seq sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* To simplify, let f denote the RTA procedure. *)
Let f (k: nat) := iter k edf_rta_iteration (initial_state ts).
(* Since the iteration is applied directly to a list of tasks and response-times,
we define a corresponding relation "<=" over those lists. *)
(* Let 'all_le' be a binary relation over lists of tasks/response-time bounds.
It states that every element of list l1 has a response-time bound R that is less
than or equal to the corresponding response-time bound R' in list l2 (point-wise).
In addition, the relation states that the tasks of both lists are unchanged. *)
Let all_le := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
all (fun p ⇒ (snd (fst p)) ≤ (snd (snd p))) (zip l1 l2).
(* Similarly, we define a strict version of 'all_le' called 'one_lt', which states that
there exists at least one element whose response-time bound increases. *)
Let one_lt := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
has (fun p ⇒ (snd (fst p)) < (snd (snd p))) (zip l1 l2).
(* Next, we prove some basic properties about the relation all_le. *)
Section RelationProperties.
(* The relation is reflexive, ... *)
Lemma all_le_reflexive : reflexive all_le.
(* ... and transitive. *)
Lemma all_le_transitive: transitive all_le.
(* At any step of the iteration, the corresponding list
is larger than or equal to the initial state. *)
Lemma bertogna_edf_comp_iteration_preserves_minimum :
∀ step, all_le (initial_state ts) (f step).
(* The application of the function is inductive. *)
Lemma bertogna_edf_comp_iteration_inductive (P : seq task_with_response_time → Type) :
P (initial_state ts) →
(∀ k, P (f k) → P (f (k.+1))) →
P (f (max_steps ts)).
(* As a last step, we show that edf_rta_iteration preserves order, i.e., for any
list l1 no smaller than the initial state, and list l2 such that
l1 <= l2, we have (edf_rta_iteration l1) <= (edf_rta_iteration l2). *)
Lemma bertogna_edf_comp_iteration_preserves_order :
∀ l1 l2,
all_le (initial_state ts) l1 →
all_le l1 l2 →
all_le (edf_rta_iteration l1) (edf_rta_iteration l2).
(* It follows from the properties above that the iteration is monotonically increasing. *)
Lemma bertogna_edf_comp_iteration_monotonic: ∀ k, all_le (f k) (f k.+1).
End RelationProperties.
(* Knowing that the iteration is monotonically increasing (with respect to all_le),
we show that the RTA procedure converges to a fixed point. *)
(* First, note that when there are no tasks, the iteration trivially converges. *)
Lemma bertogna_edf_comp_f_converges_with_no_tasks :
size ts = 0 →
f (max_steps ts) = f (max_steps ts).+1.
(* Otherwise, if the iteration reached a fixed point before (max_steps ts), then
the value at (max_steps ts) is still at a fixed point. *)
Lemma bertogna_edf_comp_f_converges_early :
(∃ k, k ≤ max_steps ts ∧ f k = f k.+1) →
f (max_steps ts) = f (max_steps ts).+1.
(* Else, we derive a contradiction. *)
Section DerivingContradiction.
(* Assume that there are tasks. *)
Hypothesis H_at_least_one_task: size ts > 0.
(* Assume that the iteration continued to diverge. *)
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps ts → f k != f k.+1.
(* Since the iteration is monotonically increasing, it must be
strictly increasing. *)
Lemma bertogna_edf_comp_f_increases :
∀ k,
k ≤ max_steps ts → one_lt (f k) (f k.+1).
(* In the end, each response-time bound is so high that the sum
of all response-time bounds exceeds the sum of all deadlines.
Contradiction! *)
Lemma bertogna_edf_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps ts →
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
End DerivingContradiction.
(* Using the lemmas above, we prove that edf_rta_iteration reaches
a fixed point after (max_steps ts) step, ... *)
Lemma edf_claimed_bounds_finds_fixed_point_of_list :
∀ rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
valid_sporadic_taskset task_cost task_period task_deadline ts →
f (max_steps ts) = edf_rta_iteration (f (max_steps ts)).
(* ...and since there cannot be a vector of response-time bounds with values less than
the task costs, this solution is also the least fixed point. *)
Lemma edf_claimed_bounds_finds_least_fixed_point :
∀ v,
all_le (initial_state ts) v →
v = edf_rta_iteration v →
all_le (f (max_steps ts)) v.
(* Therefore, with regard to the response-time bound recurrence,
the individual response-time bounds (elements of the list) are
also fixed points. *)
Theorem edf_claimed_bounds_finds_fixed_point_for_each_bound :
∀ tsk R rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R = edf_response_time_bound rt_bounds tsk R.
End Convergence.
(* Now we prove the correctness of the response-time bounds. *)
Section MainProof.
(* Consider a task set ts where... *)
Variable ts: taskset_of sporadic_task.
(* ... all tasks have valid parameters ... *)
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ... and constrained deadlines. *)
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
(* Assume that alpha' is a non-empty subaffinity of alpha. *)
Hypothesis H_non_empty_affinity:
∀ tsk, tsk \in ts → #|alpha' tsk| > 0.
Hypothesis H_subaffinity:
∀ tsk, tsk \in ts → is_subaffinity (alpha' tsk) (alpha tsk).
(* Next, consider any arrival sequence such that...*)
Variable arr_seq: arrival_sequence Job.
(* ...all jobs come from task set ts, ...*)
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j → job_task j \in ts.
(* ...they have valid parameters,...*)
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* ... and satisfy the sporadic task model.*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Then, consider any schedule with at least one CPU such that...*)
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* ...jobs only execute after they arrived and no longer
than their execution costs,... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume a work-conserving APA scheduler that respects EDF policy. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_edf_policy:
respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task
arr_seq sched alpha (EDF job_arrival job_deadline).
(* To avoid a long list of parameters, we provide some local definitions. *)
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
(* In the following theorem, we prove that any response-time bound contained
in edf_claimed_bounds is safe. The proof follows by direct application of
the main Theorem from bertogna_edf_theory.v. *)
Theorem edf_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In edf_claimed_bounds ts →
response_time_bounded_by tsk R.
(* Therefore, if the schedulability test suceeds, ...*)
Hypothesis H_test_succeeds: edf_schedulable ts.
(*... no task misses its deadline. *)
Theorem taskset_schedulable_by_edf_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
(* For completeness, since all jobs of the arrival sequence
are spawned by the task set, we conclude that no job misses
its deadline. *)
Theorem jobs_schedulable_by_edf_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
End MainProof.
End Analysis.
End ResponseTimeIterationEDF.
Require Import prosa.classic.analysis.apa.bertogna_edf_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDF.
(* In this section, we define the algorithm corresponding to the APA-reduction
of Bertogna and Cirinei's RTA for EDF scheduling. *)
Section Analysis.
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_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* As input for each iteration of the algorithm, we consider pairs
of tasks and response-time bounds. *)
Let task_with_response_time := (sporadic_task × time)%type.
(* Consider a platform with num_cpus processors. *)
Variable num_cpus: nat.
(* Assume that every task has a processor affinity alpha. *)
Variable alpha: task_affinity sporadic_task num_cpus.
(* For the reduction to subproblems, consider a subaffinity alpha' for each task. *)
Variable alpha': task_affinity sporadic_task num_cpus.
(* First, recall the interference bound under EDF. Note that we use
subaffinity (alpha' tsk) when computing the set of interfering tasks. *)
Let I (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline alpha tsk
(alpha' tsk) (* Subproblem alpha' *)
rt_bounds delta.
(* Then, we define the response-time recurrence. Note that we divide the
interference by the cardinality of (alpha' tsk). *)
Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
task_cost tsk + div_floor (I rt_bounds tsk delta)
#|alpha' tsk|.
(* Also note that a response-time is only valid if it is no larger
than the deadline. *)
Definition R_le_deadline (pair: task_with_response_time) :=
let (tsk, R) := pair in
R ≤ task_deadline tsk.
(* Next, we define the fixed-point iteration for computing the
response-time bound of each task. *)
(* Given a sequence 'rt_bounds' of task and response-time bounds
from the previous iteration, we compute the response-time
bound of a single task using the RTA for EDF. *)
Definition update_bound (rt_bounds: seq task_with_response_time) pair :=
let '(tsk, R) := pair in
(tsk, edf_response_time_bound rt_bounds tsk R).
(* To compute the response-time bounds of the entire task set,
we start the iteration with a sequence of tasks and costs:
<(task1, cost1), (task2, cost2), ...>. *)
Let initial_state (ts: seq sporadic_task) :=
map (fun tsk ⇒ (tsk, task_cost tsk)) ts.
(* Then, we successively update the the response-time bounds based
on the slack computed in the previous iteration. *)
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
map (update_bound rt_bounds) rt_bounds.
(* To ensure that the procedure converges, we stop the iteration
after a "sufficient" number of times, which corresponds to
the time complexity of the procedure. *)
Let max_steps (ts: seq sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
(* This yields the following definition for the RTA. At the end
we check if all computed response-time bounds are less than
or equal to the deadline, in which case they are valid. *)
Definition edf_claimed_bounds (ts: seq sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then
Some R_values
else None.
(* The schedulability test simply checks if we got a list of
response-time bounds (i.e., if the computation did not fail). *)
Definition edf_schedulable (ts: seq sporadic_task) :=
edf_claimed_bounds ts != None.
(* In the following section, we prove several helper lemmas about the
list of tasks/response-time bounds. *)
Section SimpleLemmas.
(* Updating a single response-time bound does not modify the task. *)
Lemma edf_claimed_bounds_unzip1_update_bound :
∀ l rt_bounds,
unzip1 (map (update_bound rt_bounds) l) = unzip1 l.
(* At any point of the iteration, the tasks are the same. *)
Lemma edf_claimed_bounds_unzip1_iteration :
∀ l k,
unzip1 (iter k edf_rta_iteration (initial_state l)) = l.
(* The iteration preserves the size of the list. *)
Lemma edf_claimed_bounds_size :
∀ l k,
size (iter k edf_rta_iteration (initial_state l)) = size l.
(* If the analysis succeeds, the computed response-time bounds are no smaller
than the task cost. *)
Lemma edf_claimed_bounds_ge_cost :
∀ l k tsk R,
(tsk, R) \in (iter k edf_rta_iteration (initial_state l)) →
R ≥ task_cost tsk.
(* If the analysis suceeds, the computed response-time bounds are no larger
than the deadline. *)
Lemma edf_claimed_bounds_le_deadline :
∀ ts rt_bounds tsk R,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
(* The list contains a response-time bound for every task in the task set. *)
Lemma edf_claimed_bounds_has_R_for_every_task :
∀ ts rt_bounds tsk,
edf_claimed_bounds ts = Some rt_bounds →
tsk \in ts →
∃ R,
(tsk, R) \in rt_bounds.
End SimpleLemmas.
(* In this section, we prove the convergence of the RTA procedure.
Since we define the RTA procedure as the application of a function
a fixed number of times, this translates into proving that the value
of the iteration at (max_steps ts) is equal to the value at (max_steps ts) + 1. *)
Section Convergence.
(* Consider any sequence of tasks with valid parameters. *)
Variable ts: seq sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* To simplify, let f denote the RTA procedure. *)
Let f (k: nat) := iter k edf_rta_iteration (initial_state ts).
(* Since the iteration is applied directly to a list of tasks and response-times,
we define a corresponding relation "<=" over those lists. *)
(* Let 'all_le' be a binary relation over lists of tasks/response-time bounds.
It states that every element of list l1 has a response-time bound R that is less
than or equal to the corresponding response-time bound R' in list l2 (point-wise).
In addition, the relation states that the tasks of both lists are unchanged. *)
Let all_le := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
all (fun p ⇒ (snd (fst p)) ≤ (snd (snd p))) (zip l1 l2).
(* Similarly, we define a strict version of 'all_le' called 'one_lt', which states that
there exists at least one element whose response-time bound increases. *)
Let one_lt := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
has (fun p ⇒ (snd (fst p)) < (snd (snd p))) (zip l1 l2).
(* Next, we prove some basic properties about the relation all_le. *)
Section RelationProperties.
(* The relation is reflexive, ... *)
Lemma all_le_reflexive : reflexive all_le.
(* ... and transitive. *)
Lemma all_le_transitive: transitive all_le.
(* At any step of the iteration, the corresponding list
is larger than or equal to the initial state. *)
Lemma bertogna_edf_comp_iteration_preserves_minimum :
∀ step, all_le (initial_state ts) (f step).
(* The application of the function is inductive. *)
Lemma bertogna_edf_comp_iteration_inductive (P : seq task_with_response_time → Type) :
P (initial_state ts) →
(∀ k, P (f k) → P (f (k.+1))) →
P (f (max_steps ts)).
(* As a last step, we show that edf_rta_iteration preserves order, i.e., for any
list l1 no smaller than the initial state, and list l2 such that
l1 <= l2, we have (edf_rta_iteration l1) <= (edf_rta_iteration l2). *)
Lemma bertogna_edf_comp_iteration_preserves_order :
∀ l1 l2,
all_le (initial_state ts) l1 →
all_le l1 l2 →
all_le (edf_rta_iteration l1) (edf_rta_iteration l2).
(* It follows from the properties above that the iteration is monotonically increasing. *)
Lemma bertogna_edf_comp_iteration_monotonic: ∀ k, all_le (f k) (f k.+1).
End RelationProperties.
(* Knowing that the iteration is monotonically increasing (with respect to all_le),
we show that the RTA procedure converges to a fixed point. *)
(* First, note that when there are no tasks, the iteration trivially converges. *)
Lemma bertogna_edf_comp_f_converges_with_no_tasks :
size ts = 0 →
f (max_steps ts) = f (max_steps ts).+1.
(* Otherwise, if the iteration reached a fixed point before (max_steps ts), then
the value at (max_steps ts) is still at a fixed point. *)
Lemma bertogna_edf_comp_f_converges_early :
(∃ k, k ≤ max_steps ts ∧ f k = f k.+1) →
f (max_steps ts) = f (max_steps ts).+1.
(* Else, we derive a contradiction. *)
Section DerivingContradiction.
(* Assume that there are tasks. *)
Hypothesis H_at_least_one_task: size ts > 0.
(* Assume that the iteration continued to diverge. *)
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps ts → f k != f k.+1.
(* Since the iteration is monotonically increasing, it must be
strictly increasing. *)
Lemma bertogna_edf_comp_f_increases :
∀ k,
k ≤ max_steps ts → one_lt (f k) (f k.+1).
(* In the end, each response-time bound is so high that the sum
of all response-time bounds exceeds the sum of all deadlines.
Contradiction! *)
Lemma bertogna_edf_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps ts →
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
End DerivingContradiction.
(* Using the lemmas above, we prove that edf_rta_iteration reaches
a fixed point after (max_steps ts) step, ... *)
Lemma edf_claimed_bounds_finds_fixed_point_of_list :
∀ rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
valid_sporadic_taskset task_cost task_period task_deadline ts →
f (max_steps ts) = edf_rta_iteration (f (max_steps ts)).
(* ...and since there cannot be a vector of response-time bounds with values less than
the task costs, this solution is also the least fixed point. *)
Lemma edf_claimed_bounds_finds_least_fixed_point :
∀ v,
all_le (initial_state ts) v →
v = edf_rta_iteration v →
all_le (f (max_steps ts)) v.
(* Therefore, with regard to the response-time bound recurrence,
the individual response-time bounds (elements of the list) are
also fixed points. *)
Theorem edf_claimed_bounds_finds_fixed_point_for_each_bound :
∀ tsk R rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R = edf_response_time_bound rt_bounds tsk R.
End Convergence.
(* Now we prove the correctness of the response-time bounds. *)
Section MainProof.
(* Consider a task set ts where... *)
Variable ts: taskset_of sporadic_task.
(* ... all tasks have valid parameters ... *)
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ... and constrained deadlines. *)
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
(* Assume that alpha' is a non-empty subaffinity of alpha. *)
Hypothesis H_non_empty_affinity:
∀ tsk, tsk \in ts → #|alpha' tsk| > 0.
Hypothesis H_subaffinity:
∀ tsk, tsk \in ts → is_subaffinity (alpha' tsk) (alpha tsk).
(* Next, consider any arrival sequence such that...*)
Variable arr_seq: arrival_sequence Job.
(* ...all jobs come from task set ts, ...*)
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j → job_task j \in ts.
(* ...they have valid parameters,...*)
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* ... and satisfy the sporadic task model.*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Then, consider any schedule with at least one CPU such that...*)
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* ...jobs only execute after they arrived and no longer
than their execution costs,... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume a work-conserving APA scheduler that respects EDF policy. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_edf_policy:
respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task
arr_seq sched alpha (EDF job_arrival job_deadline).
(* To avoid a long list of parameters, we provide some local definitions. *)
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
(* In the following theorem, we prove that any response-time bound contained
in edf_claimed_bounds is safe. The proof follows by direct application of
the main Theorem from bertogna_edf_theory.v. *)
Theorem edf_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In edf_claimed_bounds ts →
response_time_bounded_by tsk R.
(* Therefore, if the schedulability test suceeds, ...*)
Hypothesis H_test_succeeds: edf_schedulable ts.
(*... no task misses its deadline. *)
Theorem taskset_schedulable_by_edf_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
(* For completeness, since all jobs of the arrival sequence
are spawned by the task set, we conclude that no job misses
its deadline. *)
Theorem jobs_schedulable_by_edf_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
End MainProof.
End Analysis.
End ResponseTimeIterationEDF.