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.
Set Bullet Behavior "Strict Subproofs".
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.
Set Bullet Behavior "Strict Subproofs".
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) ).
Proof.
intros j [t ARR]. generalize dependent j.
induction t as [ t IHt ] using (well_founded_induction lt_wf).
case t eqn:GT;intros.
- have INJ: arrives_in arr_seq j by ∃ 0.
(( try ( apply completion_monotonic with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk ) ) || apply completion_monotonic with (t:=job_arrival j + WCRT task_cost task_time_slot ts tsk ) )
;trivial;try by rewrite leq_add2l H); ( try ( apply job_completed_by_WCRT
with (task_deadline0:=task_deadline)
(arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
(job_task0:=job_task)(slot_order0:=slot_order) ) || apply job_completed_by_WCRT
with (task_deadline:=task_deadline)
(arr_seq:=arr_seq)(job_deadline:=job_deadline)
(job_task:=job_task)(slot_order:=slot_order) );eauto 2.
intros. apply H_arrival_times_are_consistent in ARR. ssrlia.
- have INJ: arrives_in arr_seq j by ∃ n.+1.
try ( apply completion_monotonic
with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto ) ||
apply completion_monotonic
with (t:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto.
by rewrite leq_add2l H. try ( apply job_completed_by_WCRT
with (task_deadline0:=task_deadline)
(arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
(job_task0:=job_task)(slot_order0:=slot_order);auto ) ||
apply job_completed_by_WCRT
with (task_deadline:=task_deadline)
(arr_seq:=arr_seq)(job_deadline:=job_deadline)
(job_task:=job_task)(slot_order:=slot_order);auto.
intros.
have PERIOD: job_arrival j_other + task_period (job_task j_other)≤ job_arrival j.
apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
have JO:job_arrival j_other = job_arrival j by f_equal. ssrlia.
try ( apply completion_monotonic with (t0:= job_arrival j_other +
task_period (job_task j_other)); auto ) ||
apply completion_monotonic with (t:= job_arrival j_other +
task_period (job_task j_other)); auto.
have ARRJ: job_arrival j = n.+1 by auto.
apply (IHt (job_arrival j_other));auto. ssrlia.
destruct H0 as [tj AAJO]. have CONSIST: job_arrival j_other =tj by auto.
by subst. by subst.
Qed.
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).
Proof.
intros.
have PERIOD: job_arrival j_other + task_period (job_task j_other)≤ job_arrival j.
apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
have JO:job_arrival j_other = job_arrival j by f_equal. ssrlia.
apply completion_monotonic with (t:=job_arrival j_other + task_period (job_task j_other));auto.
apply any_job_completed_before_period;auto. by subst.
Qed.
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
completed_by job_cost sched j (job_arrival j + task_period (job_task j) ).
Proof.
intros j [t ARR]. generalize dependent j.
induction t as [ t IHt ] using (well_founded_induction lt_wf).
case t eqn:GT;intros.
- have INJ: arrives_in arr_seq j by ∃ 0.
(( try ( apply completion_monotonic with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk ) ) || apply completion_monotonic with (t:=job_arrival j + WCRT task_cost task_time_slot ts tsk ) )
;trivial;try by rewrite leq_add2l H); ( try ( apply job_completed_by_WCRT
with (task_deadline0:=task_deadline)
(arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
(job_task0:=job_task)(slot_order0:=slot_order) ) || apply job_completed_by_WCRT
with (task_deadline:=task_deadline)
(arr_seq:=arr_seq)(job_deadline:=job_deadline)
(job_task:=job_task)(slot_order:=slot_order) );eauto 2.
intros. apply H_arrival_times_are_consistent in ARR. ssrlia.
- have INJ: arrives_in arr_seq j by ∃ n.+1.
try ( apply completion_monotonic
with (t0:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto ) ||
apply completion_monotonic
with (t:=job_arrival j + WCRT task_cost task_time_slot ts tsk);auto.
by rewrite leq_add2l H. try ( apply job_completed_by_WCRT
with (task_deadline0:=task_deadline)
(arr_seq0:=arr_seq)(job_deadline0:=job_deadline)
(job_task0:=job_task)(slot_order0:=slot_order);auto ) ||
apply job_completed_by_WCRT
with (task_deadline:=task_deadline)
(arr_seq:=arr_seq)(job_deadline:=job_deadline)
(job_task:=job_task)(slot_order:=slot_order);auto.
intros.
have PERIOD: job_arrival j_other + task_period (job_task j_other)≤ job_arrival j.
apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
have JO:job_arrival j_other = job_arrival j by f_equal. ssrlia.
try ( apply completion_monotonic with (t0:= job_arrival j_other +
task_period (job_task j_other)); auto ) ||
apply completion_monotonic with (t:= job_arrival j_other +
task_period (job_task j_other)); auto.
have ARRJ: job_arrival j = n.+1 by auto.
apply (IHt (job_arrival j_other));auto. ssrlia.
destruct H0 as [tj AAJO]. have CONSIST: job_arrival j_other =tj by auto.
by subst. by subst.
Qed.
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).
Proof.
intros.
have PERIOD: job_arrival j_other + task_period (job_task j_other)≤ job_arrival j.
apply H_sporadic_tasks;auto. case (j==j_other)eqn: JJ;move/eqP in JJ;last auto.
have JO:job_arrival j_other = job_arrival j by f_equal. ssrlia.
apply completion_monotonic with (t:=job_arrival j_other + task_period (job_task j_other));auto.
apply any_job_completed_before_period;auto. by subst.
Qed.
Main Theorem
Theorem uniprocessor_response_time_bound_TDMA: response_time_bounded_by tsk BOUND.
Proof.
intros j arr_seq_j JobTsk.
apply completion_monotonic with (t:=job_arrival j + RT j); try done.
- rewrite leq_add2l /BOUND.
(try ( apply (response_time_le_WCRT)
with (task_cost0:=task_cost) (task_deadline0:=task_deadline)(sched0:=sched)
(job_arrival0:=job_arrival)(job_cost0:=job_cost)(job_deadline0:=job_deadline)
(job_task0:=job_task)(ts0:=ts)(arr_seq0:=arr_seq)
(slot_order0:=slot_order)(Job0:=Job)(tsk0:=tsk) ) ||
apply (response_time_le_WCRT)
with (task_cost:=task_cost) (task_deadline:=task_deadline)(sched:=sched)
(job_arrival:=job_arrival)(job_cost:=job_cost)(job_deadline:=job_deadline)
(job_task:=job_task)(ts:=ts)(arr_seq:=arr_seq)
(slot_order:=slot_order)(Job:=Job)(tsk:=tsk)); try done;auto;try (intros;
by apply all_previous_jobs_of_same_task_completed).
- ( try ( apply completed_by_end_time
with (sched0:=sched)(job_arrival0:=job_arrival)
(job_cost0:=job_cost) ) ||
apply completed_by_end_time
with (sched:=sched)(job_arrival:=job_arrival)
(job_cost:=job_cost)); first exact.
( try ( apply completes_at_end_time
with
(job_arrival0:=job_arrival)(task_cost0:=task_cost)(arr_seq0:=arr_seq)
(job_task0:=job_task)(job_deadline0:=job_deadline)(task_deadline0:=task_deadline)
(sched0:=sched)(ts0:=ts)(slot_order0:=slot_order)
(tsk0:=tsk) (j0:=j) ) ||
apply completes_at_end_time
with
(job_arrival:=job_arrival)(task_cost:=task_cost)(arr_seq:=arr_seq)
(job_task:=job_task)(job_deadline:=job_deadline)(task_deadline:=task_deadline)
(sched:=sched)(ts:=ts)(slot_order:=slot_order)
(tsk:=tsk) (j:=j)); try auto;try (intros;
by apply all_previous_jobs_of_same_task_completed).
Qed.
Proof.
intros j arr_seq_j JobTsk.
apply completion_monotonic with (t:=job_arrival j + RT j); try done.
- rewrite leq_add2l /BOUND.
(try ( apply (response_time_le_WCRT)
with (task_cost0:=task_cost) (task_deadline0:=task_deadline)(sched0:=sched)
(job_arrival0:=job_arrival)(job_cost0:=job_cost)(job_deadline0:=job_deadline)
(job_task0:=job_task)(ts0:=ts)(arr_seq0:=arr_seq)
(slot_order0:=slot_order)(Job0:=Job)(tsk0:=tsk) ) ||
apply (response_time_le_WCRT)
with (task_cost:=task_cost) (task_deadline:=task_deadline)(sched:=sched)
(job_arrival:=job_arrival)(job_cost:=job_cost)(job_deadline:=job_deadline)
(job_task:=job_task)(ts:=ts)(arr_seq:=arr_seq)
(slot_order:=slot_order)(Job:=Job)(tsk:=tsk)); try done;auto;try (intros;
by apply all_previous_jobs_of_same_task_completed).
- ( try ( apply completed_by_end_time
with (sched0:=sched)(job_arrival0:=job_arrival)
(job_cost0:=job_cost) ) ||
apply completed_by_end_time
with (sched:=sched)(job_arrival:=job_arrival)
(job_cost:=job_cost)); first exact.
( try ( apply completes_at_end_time
with
(job_arrival0:=job_arrival)(task_cost0:=task_cost)(arr_seq0:=arr_seq)
(job_task0:=job_task)(job_deadline0:=job_deadline)(task_deadline0:=task_deadline)
(sched0:=sched)(ts0:=ts)(slot_order0:=slot_order)
(tsk0:=tsk) (j0:=j) ) ||
apply completes_at_end_time
with
(job_arrival:=job_arrival)(task_cost:=task_cost)(arr_seq:=arr_seq)
(job_task:=job_task)(job_deadline:=job_deadline)(task_deadline:=task_deadline)
(sched:=sched)(ts:=ts)(slot_order:=slot_order)
(tsk:=tsk) (j:=j)); try auto;try (intros;
by apply all_previous_jobs_of_same_task_completed).
Qed.
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.
Proof.
( try ( apply task_completes_before_deadline with (task_deadline0:=task_deadline) (R:=BOUND) ) ||
apply task_completes_before_deadline with (task_deadline:=task_deadline) (R:=BOUND) )
;try done.
move ⇒ j arr_seqJ.
- by apply H_valid_job_parameters.
- apply uniprocessor_response_time_bound_TDMA.
Qed.
Theorem jobs_schedulable_by_tdma_rta :
∀ j,
arrives_in arr_seq j ∧ job_task j =tsk →
no_deadline_missed_by_job j.
Proof.
intros j [arr_seqJ Jtsk].
by apply taskset_schedulable_by_tdma.
Qed.
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.
Proof.
( try ( apply task_completes_before_deadline with (task_deadline0:=task_deadline) (R:=BOUND) ) ||
apply task_completes_before_deadline with (task_deadline:=task_deadline) (R:=BOUND) )
;try done.
move ⇒ j arr_seqJ.
- by apply H_valid_job_parameters.
- apply uniprocessor_response_time_bound_TDMA.
Qed.
Theorem jobs_schedulable_by_tdma_rta :
∀ j,
arrives_in arr_seq j ∧ job_task j =tsk →
no_deadline_missed_by_job j.
Proof.
intros j [arr_seqJ Jtsk].
by apply taskset_schedulable_by_tdma.
Qed.
End AnalysisIsSufficient.
End ResponseTimeBound.
End ResponseTimeAnalysisTDMA.