Library prosa.classic.analysis.uni.basic.tdma_rta_theory
Require Import Arith.
Require Import prosa.classic.util.all
prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.schedule.uni.schedulability
prosa.classic.model.schedule.uni.schedule_of_task
prosa.classic.model.schedule.uni.response_time
prosa.classic.analysis.uni.basic.tdma_wcrt_analysis.
Require Import prosa.classic.model.schedule.uni.basic.platform_tdma
prosa.classic.model.schedule.uni.end_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module ResponseTimeAnalysisTDMA.
Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Schedulability
WCRT_OneJobTDMA.
(* In this section, we establish that the computed value WCRT of the exact response-time analysis
yields an upper bound on the response time of a task under TDMA scheduling policy on an uniprocessor,
assuming that such value is no larger than the task period. *)
Section ResponseTimeBound.
Require Import prosa.classic.util.all
prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.schedule.uni.schedulability
prosa.classic.model.schedule.uni.schedule_of_task
prosa.classic.model.schedule.uni.response_time
prosa.classic.analysis.uni.basic.tdma_wcrt_analysis.
Require Import prosa.classic.model.schedule.uni.basic.platform_tdma
prosa.classic.model.schedule.uni.end_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module ResponseTimeAnalysisTDMA.
Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Schedulability
WCRT_OneJobTDMA.
(* In this section, we establish that the computed value WCRT of the exact response-time analysis
yields an upper bound on the response time of a task under TDMA scheduling policy on an uniprocessor,
assuming that such value is no larger than the task period. *)
Section ResponseTimeBound.
System model
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.
(* Consider any arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* ...and any uniprocessor... *)
Variable sched: schedule Job.
(* ... where jobs do not execute before their arrival times nor after completion. *)
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.
(* Consider any TDMA slot assignment... *)
Variable task_time_slot: TDMA_slot sporadic_task.
(* ... and any slot order. *)
Variable slot_order: TDMA_slot_order sporadic_task.
(* Consider any task set ts. *)
Variable ts: {set sporadic_task}.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* Consider any task in task set. *)
Variable tsk:sporadic_task.
Hypothesis H_task_in_task_set: tsk \in ts.
(* For simplicity, let us use local names for some definitions and refer them to local variables. *)
(* Recall definition: whether a job can be scheduled at time t *)
Let is_scheduled_at j t:=
scheduled_at sched j t.
(* Recall definition: whether a task is in its own time slot at time t *)
Let in_time_slot_at j t:=
Task_in_time_slot ts slot_order (job_task j) task_time_slot t.
(* Recall the definition of response-time bound. *)
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
(* Let (RT j) denote the computed response-time of job j according to the TDMA analysis.
Note that this computation assumes that there is only one pending job of each task.
Still, this assumption doesn't break the generality of the proof. There cannot be
multiple jobs of the same task because:
(a) assumption: the computed value WCRT is bounded by its task's period; and
(b) the lemma: "jobs_finished_before_WCRT" in file tdma_wcrt_analysis.v. *)
Hypothesis WCRT_le_period:
WCRT task_cost task_time_slot ts tsk ≤ task_period tsk.
Let RT j:= job_response_time_tdma_in_at_most_one_job_is_pending job_arrival job_cost
task_time_slot slot_order ts tsk j.
(* Next, recall the definition of deadline miss of tasks and jobs. *)
Let no_deadline_missed_by_task :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
(* Then, we define a valid TDMA bound. *)
(* Bound is valid bound iff it is less than or equal to task's deadline *)
Definition is_valid_tdma_bound bound :=
(bound ≤ task_deadline tsk).
(* Now, let's assume that the schedule respects TDMA scheduling policy... *)
Hypothesis TDMA_policy:
Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.
(* ..., that task time slot is valid... *)
Hypothesis H_valid_time_slot:
is_valid_time_slot tsk task_time_slot.
(* ... and that any job in arrival sequence is a valid job. *)
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.
(* Assume that job cost is less than or equal to its task cost. *)
Hypothesis H_job_cost_le_task_cost:
∀ j, arrives_in arr_seq j →
job_cost_le_task_cost task_cost job_cost job_task j.
(* Let BOUND be the computed WCRT of tsk. *)
Let BOUND := WCRT task_cost task_time_slot ts tsk.
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.
(* Consider any arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* ...and any uniprocessor... *)
Variable sched: schedule Job.
(* ... where jobs do not execute before their arrival times nor after completion. *)
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.
(* Consider any TDMA slot assignment... *)
Variable task_time_slot: TDMA_slot sporadic_task.
(* ... and any slot order. *)
Variable slot_order: TDMA_slot_order sporadic_task.
(* Consider any task set ts. *)
Variable ts: {set sporadic_task}.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* Consider any task in task set. *)
Variable tsk:sporadic_task.
Hypothesis H_task_in_task_set: tsk \in ts.
(* For simplicity, let us use local names for some definitions and refer them to local variables. *)
(* Recall definition: whether a job can be scheduled at time t *)
Let is_scheduled_at j t:=
scheduled_at sched j t.
(* Recall definition: whether a task is in its own time slot at time t *)
Let in_time_slot_at j t:=
Task_in_time_slot ts slot_order (job_task j) task_time_slot t.
(* Recall the definition of response-time bound. *)
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
(* Let (RT j) denote the computed response-time of job j according to the TDMA analysis.
Note that this computation assumes that there is only one pending job of each task.
Still, this assumption doesn't break the generality of the proof. There cannot be
multiple jobs of the same task because:
(a) assumption: the computed value WCRT is bounded by its task's period; and
(b) the lemma: "jobs_finished_before_WCRT" in file tdma_wcrt_analysis.v. *)
Hypothesis WCRT_le_period:
WCRT task_cost task_time_slot ts tsk ≤ task_period tsk.
Let RT j:= job_response_time_tdma_in_at_most_one_job_is_pending job_arrival job_cost
task_time_slot slot_order ts tsk j.
(* Next, recall the definition of deadline miss of tasks and jobs. *)
Let no_deadline_missed_by_task :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
(* Then, we define a valid TDMA bound. *)
(* Bound is valid bound iff it is less than or equal to task's deadline *)
Definition is_valid_tdma_bound bound :=
(bound ≤ task_deadline tsk).
(* Now, let's assume that the schedule respects TDMA scheduling policy... *)
Hypothesis TDMA_policy:
Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.
(* ..., that task time slot is valid... *)
Hypothesis H_valid_time_slot:
is_valid_time_slot tsk task_time_slot.
(* ... and that any job in arrival sequence is a valid job. *)
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.
(* Assume that job cost is less than or equal to its task cost. *)
Hypothesis H_job_cost_le_task_cost:
∀ j, arrives_in arr_seq j →
job_cost_le_task_cost task_cost job_cost job_task j.
(* Let BOUND be the computed WCRT of tsk. *)
Let BOUND := WCRT task_cost task_time_slot ts tsk.
Two basic lemmas
(* Having assumed that the computed BOUND <= task_period tsk, we first prove that
any job of task tsk must have completed by its period. *)
Lemma any_job_completed_before_period:
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
completed_by job_cost sched j (job_arrival j + task_period (job_task j) ).
(* Based on the lemma above and the fact that jobs arrive sporadically, we can conclude that
all the previous jobs of task tsk must have completed before the analyzed job j. *)
Lemma all_previous_jobs_of_same_task_completed :
∀ j j_other,
arrives_in arr_seq j →
job_task j = tsk →
arrives_in arr_seq j_other →
job_task j = job_task j_other →
job_arrival j_other < job_arrival j →
completed_by job_cost sched j_other (job_arrival j).
any job of task tsk must have completed by its period. *)
Lemma any_job_completed_before_period:
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
completed_by job_cost sched j (job_arrival j + task_period (job_task j) ).
(* Based on the lemma above and the fact that jobs arrive sporadically, we can conclude that
all the previous jobs of task tsk must have completed before the analyzed job j. *)
Lemma all_previous_jobs_of_same_task_completed :
∀ j j_other,
arrives_in arr_seq j →
job_task j = tsk →
arrives_in arr_seq j_other →
job_task j = job_task j_other →
job_arrival j_other < job_arrival j →
completed_by job_cost sched j_other (job_arrival j).
Main Theorem
(* Therefore, we proved that the reponse time of task tsk is bouned by the
BOUND i.e., the computed value WCRT according to TDMA scheduling policy on an uniprocessor.
( for more details, see
response_time_le_WCRT: .
completed_by_end_time: model/schedule/uni/end_time.v
completes_at_end_time: model/schedule/uni/end_time.v
) *)
Theorem uniprocessor_response_time_bound_TDMA: response_time_bounded_by tsk BOUND.
BOUND i.e., the computed value WCRT according to TDMA scheduling policy on an uniprocessor.
( for more details, see
response_time_le_WCRT: .
completed_by_end_time: model/schedule/uni/end_time.v
completes_at_end_time: model/schedule/uni/end_time.v
) *)
Theorem uniprocessor_response_time_bound_TDMA: response_time_bounded_by tsk BOUND.
Sufficient Analysis
(* Finally, we show that the RTA is a sufficient schedulability analysis. *)
Section AnalysisIsSufficient.
(* Assume that BOUND is a valid tdma bound *)
Hypothesis H_is_valid_bound:
is_valid_tdma_bound BOUND.
(* We can prove the theorem: there is no deadline miss of task tsk *)
Theorem taskset_schedulable_by_tdma : no_deadline_missed_by_task tsk.
(* Based on the theorem above, we can prove that
any job of the arrival sequence are spawned by task tsk won't miss its deadline. *)
Theorem jobs_schedulable_by_tdma_rta :
∀ j,
arrives_in arr_seq j ∧ job_task j =tsk →
no_deadline_missed_by_job j.
End AnalysisIsSufficient.
End ResponseTimeBound.
End ResponseTimeAnalysisTDMA.
Section AnalysisIsSufficient.
(* Assume that BOUND is a valid tdma bound *)
Hypothesis H_is_valid_bound:
is_valid_tdma_bound BOUND.
(* We can prove the theorem: there is no deadline miss of task tsk *)
Theorem taskset_schedulable_by_tdma : no_deadline_missed_by_task tsk.
(* Based on the theorem above, we can prove that
any job of the arrival sequence are spawned by task tsk won't miss its deadline. *)
Theorem jobs_schedulable_by_tdma_rta :
∀ j,
arrives_in arr_seq j ∧ job_task j =tsk →
no_deadline_missed_by_job j.
End AnalysisIsSufficient.
End ResponseTimeBound.
End ResponseTimeAnalysisTDMA.