Library prosa.classic.analysis.uni.basic.tdma_wcrt_analysis
Require Import Arith Nat.
Require Import prosa.classic.util.all.
Require Import 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.
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 WCRT_OneJobTDMA.
Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Schedulability.
Section WCRT_analysis.
Require Import prosa.classic.util.all.
Require Import 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.
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 WCRT_OneJobTDMA.
Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Schedulability.
Section WCRT_analysis.
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_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.
Variable j:Job.
Hypothesis H_job_task: job_task j =tsk.
Hypothesis job_in_arr_seq: arrives_in arr_seq j.
Hypothesis H_valid_job:
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Let time_slot:= task_time_slot tsk.
Let slot_offset:= Task_slot_offset ts slot_order tsk task_time_slot.
Let tdma_cycle:= TDMA_cycle ts task_time_slot.
Let is_scheduled_at t:=
scheduled_at sched j t.
Let in_time_slot_at t:=
Task_in_time_slot ts slot_order tsk task_time_slot t.
Let pending_at:=
pending job_arrival job_cost sched j.
Let job_end_time_predicate:= end_time_predicate sched j.
Let job_completes_at:=
completes_at job_arrival job_cost sched j.
Let from_start_of_slot t:=
( t + tdma_cycle- slot_offset %% tdma_cycle) %% tdma_cycle.
Let to_next_slot t:=
tdma_cycle - from_start_of_slot t.
Let duration_to_finish_from_start_of_slot_with c:duration :=
(div_ceil c time_slot -1) × (tdma_cycle - time_slot) + c.
Let to_end_of_slot t:=
time_slot - from_start_of_slot t.
Definition formula_rt (arr:instant) (c:duration):=
if c ==0 then 0 else
if in_time_slot_at arr then
if c ≤ to_end_of_slot arr then
c
else to_next_slot arr +
duration_to_finish_from_start_of_slot_with (c - to_end_of_slot arr)
else
to_next_slot arr + duration_to_finish_from_start_of_slot_with c.
Definition job_response_time_tdma_in_at_most_one_job_is_pending:=
formula_rt (job_arrival j) (job_cost j).
Hypothesis H_valid_time_slot: is_valid_time_slot tsk task_time_slot.
Hypothesis TDMA_policy:
Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.
Hypothesis all_previous_jobs_of_same_task_completed :
∀ j_other,
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).
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_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.
Variable j:Job.
Hypothesis H_job_task: job_task j =tsk.
Hypothesis job_in_arr_seq: arrives_in arr_seq j.
Hypothesis H_valid_job:
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Let time_slot:= task_time_slot tsk.
Let slot_offset:= Task_slot_offset ts slot_order tsk task_time_slot.
Let tdma_cycle:= TDMA_cycle ts task_time_slot.
Let is_scheduled_at t:=
scheduled_at sched j t.
Let in_time_slot_at t:=
Task_in_time_slot ts slot_order tsk task_time_slot t.
Let pending_at:=
pending job_arrival job_cost sched j.
Let job_end_time_predicate:= end_time_predicate sched j.
Let job_completes_at:=
completes_at job_arrival job_cost sched j.
Let from_start_of_slot t:=
( t + tdma_cycle- slot_offset %% tdma_cycle) %% tdma_cycle.
Let to_next_slot t:=
tdma_cycle - from_start_of_slot t.
Let duration_to_finish_from_start_of_slot_with c:duration :=
(div_ceil c time_slot -1) × (tdma_cycle - time_slot) + c.
Let to_end_of_slot t:=
time_slot - from_start_of_slot t.
Definition formula_rt (arr:instant) (c:duration):=
if c ==0 then 0 else
if in_time_slot_at arr then
if c ≤ to_end_of_slot arr then
c
else to_next_slot arr +
duration_to_finish_from_start_of_slot_with (c - to_end_of_slot arr)
else
to_next_slot arr + duration_to_finish_from_start_of_slot_with c.
Definition job_response_time_tdma_in_at_most_one_job_is_pending:=
formula_rt (job_arrival j) (job_cost j).
Hypothesis H_valid_time_slot: is_valid_time_slot tsk task_time_slot.
Hypothesis TDMA_policy:
Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.
Hypothesis all_previous_jobs_of_same_task_completed :
∀ j_other,
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).
First, we prove some basic lemmas about pending.
Section BasicLemmas.
Lemma at_most_one_job_is_pending:
∀ j_other (t : time),
arrives_in arr_seq j_other →
job_arrival j_other < job_arrival j →
pending job_arrival job_cost sched j t →
pending job_arrival job_cost sched j_other t →
job_task j = job_task j_other → j = j_other.
Lemma TDMA_policy_case_RT_le_Period:
∀ t,
pending_at t →
reflect (in_time_slot_at t) (is_scheduled_at t).
Lemma pendingArrival: pending_at (job_arrival j).
Lemma pendingSt:
∀ t,
pending_at t →
is_scheduled_at t = false →
pending_at t.+1.
Lemma pendingSt_Sched:
∀ t c,
pending_at t →
service sched j t + c.+2 =job_cost j →
is_scheduled_at t = true →
pending_at t.+1.
End BasicLemmas.
Lemma at_most_one_job_is_pending:
∀ j_other (t : time),
arrives_in arr_seq j_other →
job_arrival j_other < job_arrival j →
pending job_arrival job_cost sched j t →
pending job_arrival job_cost sched j_other t →
job_task j = job_task j_other → j = j_other.
Lemma TDMA_policy_case_RT_le_Period:
∀ t,
pending_at t →
reflect (in_time_slot_at t) (is_scheduled_at t).
Lemma pendingArrival: pending_at (job_arrival j).
Lemma pendingSt:
∀ t,
pending_at t →
is_scheduled_at t = false →
pending_at t.+1.
Lemma pendingSt_Sched:
∀ t c,
pending_at t →
service sched j t + c.+2 =job_cost j →
is_scheduled_at t = true →
pending_at t.+1.
End BasicLemmas.
Next, we prove some generic lemmas about the response time formula and the end time predicate.
Section formula_predicate_eq.
Lemma to_next_slot_pos:
∀ t, to_next_slot t>0.
Lemma lt_to_next_slot_1LR:
∀ a t,
a.+1 < to_next_slot t →
a < to_next_slot t.+1.
Lemma lt_to_next_slot_LR:
∀ b a t,
a+b < to_next_slot t →
a < to_next_slot (t+b).
Lemma S_t_not_sched:
∀ t, pending_at t →
is_scheduled_at t = false →
1 < to_next_slot t →
is_scheduled_at t.+1 = false.
Lemma duration_not_sched:
∀ t,
pending_at t →
is_scheduled_at t = false →
∀ d, d < to_next_slot t →
is_scheduled_at (t+d) = false ∧ pending_at (t+d).
Lemma pending_Nsched_sched:
∀ t,
pending_at t →
is_scheduled_at t = false →
pending_at (t+ to_next_slot t).
Lemma at_next_start_of_slot_schedulabe:
∀ t,
pending_at t →
is_scheduled_at t = false →
is_scheduled_at (t+to_next_slot t) = true.
Lemma formula_not_sched_St: ∀ t c, pending_at t →
is_scheduled_at t = false →
t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.+1.
Lemma formula_sched_St:
∀ t c,
is_scheduled_at t = true →
t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.
Lemma formula_not_sched_interval:
∀ t c,
pending_at t →
is_scheduled_at t = false →
∀ d, d < to_next_slot t →
t + formula_rt t c.+1 = t + d + formula_rt (t + d) c.+1.
Lemma formula_not_sched_to_next_slot:
∀ t c, pending_at t →
is_scheduled_at t = false →
t + formula_rt t c.+1 = t + to_next_slot t + formula_rt (t + to_next_slot t) c.+1.
Lemma job_not_sched_to_cunsume_1unit:
∀ t c, pending_at t →
is_scheduled_at t = false →
t + formula_rt t c.+1 = (t + to_next_slot t).+1 + formula_rt (t + to_next_slot t).+1 c.
Lemma end_time_predicate_not_sched_eq:
∀ d c t e ,
pending_at t →
is_scheduled_at t = false →
job_end_time_predicate t c.+1 e →
d < to_next_slot t →
job_end_time_predicate (t+d) c.+1 e.
Lemma end_time_predicate_not_sched_eq_rev:
∀ d c t e ,
pending_at t →
is_scheduled_at t = false →
job_end_time_predicate (t+d) (S c) e →
d < to_next_slot t →
job_end_time_predicate t (S c) e.
Lemma end_time_predicate_eq:
∀ t c e,
pending_at t →
is_scheduled_at t = false →
job_end_time_predicate t c.+1 e ↔
job_end_time_predicate ((t+to_next_slot t).+1) c e.
Lemma service_is_zero_in_Nsched_duration:
∀ d t,
pending_at t →
scheduled_at sched j t = false →
d ≤ to_next_slot t →
service sched j ( t + d) = service sched j t.
Lemma completes_at_end_time_pre:
∀ c t , pending_at t → service sched j t + c = job_cost j →
end_time_predicate sched j t c (t + formula_rt t c).
End formula_predicate_eq.
Lemma to_next_slot_pos:
∀ t, to_next_slot t>0.
Lemma lt_to_next_slot_1LR:
∀ a t,
a.+1 < to_next_slot t →
a < to_next_slot t.+1.
Lemma lt_to_next_slot_LR:
∀ b a t,
a+b < to_next_slot t →
a < to_next_slot (t+b).
Lemma S_t_not_sched:
∀ t, pending_at t →
is_scheduled_at t = false →
1 < to_next_slot t →
is_scheduled_at t.+1 = false.
Lemma duration_not_sched:
∀ t,
pending_at t →
is_scheduled_at t = false →
∀ d, d < to_next_slot t →
is_scheduled_at (t+d) = false ∧ pending_at (t+d).
Lemma pending_Nsched_sched:
∀ t,
pending_at t →
is_scheduled_at t = false →
pending_at (t+ to_next_slot t).
Lemma at_next_start_of_slot_schedulabe:
∀ t,
pending_at t →
is_scheduled_at t = false →
is_scheduled_at (t+to_next_slot t) = true.
Lemma formula_not_sched_St: ∀ t c, pending_at t →
is_scheduled_at t = false →
t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.+1.
Lemma formula_sched_St:
∀ t c,
is_scheduled_at t = true →
t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.
Lemma formula_not_sched_interval:
∀ t c,
pending_at t →
is_scheduled_at t = false →
∀ d, d < to_next_slot t →
t + formula_rt t c.+1 = t + d + formula_rt (t + d) c.+1.
Lemma formula_not_sched_to_next_slot:
∀ t c, pending_at t →
is_scheduled_at t = false →
t + formula_rt t c.+1 = t + to_next_slot t + formula_rt (t + to_next_slot t) c.+1.
Lemma job_not_sched_to_cunsume_1unit:
∀ t c, pending_at t →
is_scheduled_at t = false →
t + formula_rt t c.+1 = (t + to_next_slot t).+1 + formula_rt (t + to_next_slot t).+1 c.
Lemma end_time_predicate_not_sched_eq:
∀ d c t e ,
pending_at t →
is_scheduled_at t = false →
job_end_time_predicate t c.+1 e →
d < to_next_slot t →
job_end_time_predicate (t+d) c.+1 e.
Lemma end_time_predicate_not_sched_eq_rev:
∀ d c t e ,
pending_at t →
is_scheduled_at t = false →
job_end_time_predicate (t+d) (S c) e →
d < to_next_slot t →
job_end_time_predicate t (S c) e.
Lemma end_time_predicate_eq:
∀ t c e,
pending_at t →
is_scheduled_at t = false →
job_end_time_predicate t c.+1 e ↔
job_end_time_predicate ((t+to_next_slot t).+1) c e.
Lemma service_is_zero_in_Nsched_duration:
∀ d t,
pending_at t →
scheduled_at sched j t = false →
d ≤ to_next_slot t →
service sched j ( t + d) = service sched j t.
Lemma completes_at_end_time_pre:
∀ c t , pending_at t → service sched j t + c = job_cost j →
end_time_predicate sched j t c (t + formula_rt t c).
End formula_predicate_eq.
Then we prove that job j completes at instant (arrival + response time) by
(1) assuming that all its previous jobs have been completed by its arrival time and
(2) basing on the basic and generic lemmas above.
Lemma completes_at_end_time:
job_completes_at (job_arrival j + job_response_time_tdma_in_at_most_one_job_is_pending).
job_completes_at (job_arrival j + job_response_time_tdma_in_at_most_one_job_is_pending).
Finally, we prove that job can be finished within the formula WCRT.
Section ValidWCRT.
Let WCET := task_cost tsk.
Definition WCRT_formula cycle s wcet:=
(div_ceil wcet s)*(cycle - s) + wcet.
Definition WCRT:=
WCRT_formula tdma_cycle time_slot WCET.
Hypothesis H_job_cost_le_task_cost: job_cost_le_task_cost task_cost job_cost job_task j.
Lemma response_time_le_WCRT:
job_response_time_tdma_in_at_most_one_job_is_pending ≤ WCRT.
Lemma exists_WCRT:
job_cost j = WCET ∧ from_start_of_slot (job_arrival j)=time_slot →
job_response_time_tdma_in_at_most_one_job_is_pending = WCRT.
Let WCET := task_cost tsk.
Definition WCRT_formula cycle s wcet:=
(div_ceil wcet s)*(cycle - s) + wcet.
Definition WCRT:=
WCRT_formula tdma_cycle time_slot WCET.
Hypothesis H_job_cost_le_task_cost: job_cost_le_task_cost task_cost job_cost job_task j.
Lemma response_time_le_WCRT:
job_response_time_tdma_in_at_most_one_job_is_pending ≤ WCRT.
Lemma exists_WCRT:
job_cost j = WCET ∧ from_start_of_slot (job_arrival j)=time_slot →
job_response_time_tdma_in_at_most_one_job_is_pending = WCRT.
Main Theorem
Theorem job_completed_by_WCRT:
completed_by job_cost sched j (job_arrival j + WCRT).
End ValidWCRT.
End WCRT_analysis.
End WCRT_OneJobTDMA.
completed_by job_cost sched j (job_arrival j + WCRT).
End ValidWCRT.
End WCRT_analysis.
End WCRT_OneJobTDMA.