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.
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.
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.
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.
Variable sched: schedule Job.
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.
Variable task_time_slot: TDMA_slot sporadic_task.
Variable slot_order: TDMA_slot_order sporadic_task.
Variable ts: {set sporadic_task}.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Variable tsk:sporadic_task.
Hypothesis H_task_in_task_set: tsk \in ts.
Let is_scheduled_at j t:=
scheduled_at sched j t.
Let in_time_slot_at j t:=
Task_in_time_slot ts slot_order (job_task j) task_time_slot t.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
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.
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.
Definition is_valid_tdma_bound bound :=
(bound ≤ task_deadline tsk).
Hypothesis TDMA_policy:
Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.
Hypothesis H_valid_time_slot:
is_valid_time_slot tsk task_time_slot.
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.
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 := 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.
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.
Variable sched: schedule Job.
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.
Variable task_time_slot: TDMA_slot sporadic_task.
Variable slot_order: TDMA_slot_order sporadic_task.
Variable ts: {set sporadic_task}.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Variable tsk:sporadic_task.
Hypothesis H_task_in_task_set: tsk \in ts.
Let is_scheduled_at j t:=
scheduled_at sched j t.
Let in_time_slot_at j t:=
Task_in_time_slot ts slot_order (job_task j) task_time_slot t.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
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.
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.
Definition is_valid_tdma_bound bound :=
(bound ≤ task_deadline tsk).
Hypothesis TDMA_policy:
Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.
Hypothesis H_valid_time_slot:
is_valid_time_slot tsk task_time_slot.
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.
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 := WCRT task_cost task_time_slot ts tsk.
Two basic lemmas
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) ).
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).
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
completed_by job_cost sched j (job_arrival j + task_period (job_task 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
Sufficient Analysis
Section AnalysisIsSufficient.
Hypothesis H_is_valid_bound:
is_valid_tdma_bound BOUND.
Theorem taskset_schedulable_by_tdma : no_deadline_missed_by_task tsk.
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.
Hypothesis H_is_valid_bound:
is_valid_tdma_bound BOUND.
Theorem taskset_schedulable_by_tdma : no_deadline_missed_by_task tsk.
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.