# Library prosa.analysis.facts.model.dynamic_suspension

Require Export prosa.analysis.facts.suspension.
Require Export prosa.model.task.suspension.dynamic.
Require Export prosa.analysis.facts.model.arrival_curves.
In this file, we prove some facts related to the dynamic self-suspension model.
Section TotalSuspensionBounded.
Consider any type of tasks each characterized by a WCET task_cost, an arrival curve max_arrivals, and a bound on the maximum total self-suspension duration exhibited by any job of the task task_total_suspension.
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{TaskTotalSuspension Task}.
Consider any kind of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Here we consider that the jobs can exhibit self-suspensions.
Context `{JobSuspension Job}.
Assume that all jobs respect the bound on the maximum total self-suspension duration.
Hypothesis H_valid_dynamic_suspensions : valid_dynamic_suspensions.
Consider any valid arrival sequence of jobs ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and assume the notion of readiness for self-suspending jobs.
#[local] Existing Instance suspension_ready_instance.
Consider any kind of processor model.
Context `{PState : ProcessorState Job}.
Consider any valid schedule.
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Let tsk be any task.
Variable tsk : Task.
Consider any arbitrary time interval `[t1, t1 + Δ)`.
Variable t1 : instant.
Variable Δ : duration.
We first prove a bound on the total self-suspension duration of a job.
Section JobSuspensionBounded.
Consider any job j of tsk.
Variable j : Job.
Hypothesis H_job_tsk : job_of_task tsk j.
Now we prove an upper bound on the total duration a job remains suspended in the interval `[t1, t1 + Δ)`.
Lemma job_suspension_bounded :
\sum_(t1 ≤ t < t1 + Δ) suspended sched j t ≤ task_total_suspension tsk.
Proof.
move: H_job_tsk; rewrite /job_of_task ⇒ /eqP <-.
apply: leq_trans; last by apply H_valid_dynamic_suspensions.
rewrite /total_suspension.
apply leq_trans with (n := \sum_(0 ≤ r < service sched j (t1 + Δ) + 1)
\sum_(t1 ≤ t < (t1 + Δ) | service sched j t == r) suspended sched j t).
{ apply: sum_over_partitions_le ⇒ [t INt _].
rewrite mem_index_iota in INt.
rewrite mem_index_iota; apply /andP; split ⇒ //=.
have ->: service sched j (t1 + Δ) = service sched j t + service_during sched j t (t1 + Δ)
by rewrite service_cat; lia.
by lia. }
have [GEQ | LT] := boolP(service sched j (t1 + Δ) + 1 ≥ job_cost j).
{ erewrite big_cat_nat with (n := job_cost j) ⇒ //=.
have ->: \sum_(job_cost j ≤ r < service sched j (t1 + Δ) + 1)
\sum_(t1 ≤ t < t1 + Δ | service sched j t == r) suspended sched j t = 0.
{ apply /eqP; rewrite sum_nat_eq0_nat.
apply /allP ⇒ [r INr].
move: INr; rewrite mem_filter andTb mem_index_iota ⇒ INr.
rewrite sum_nat_eq0_nat; apply /allP ⇒ [to INto].
move: INto; rewrite mem_filter ⇒ /andP[/eqP SERVto INto].
rewrite /suspended.
have /negPf ->: ~~ pending sched j to; last by rewrite andbF.
rewrite /pending negb_and negbK; apply /orP; right.
rewrite /completed_by; by lia. }
rewrite addn0.
rewrite leq_sum_seq //= ⇒ r _ _.
by apply : suspension_bounded_in_interval. }
{ apply leq_trans with (n := \sum_(0 ≤ r < job_cost j)
\sum_(t1 ≤ t < t1 + Δ | service sched j t == r) suspended sched j t).
{ rewrite -ltnNge in LT.
rewrite [in leqRHS](@big_cat_nat _ _ _ (service sched j (t1 + Δ) + 1)) ⇒ //=.
by lia. }
rewrite leq_sum_seq //= ⇒ r _ _.
by apply: suspension_bounded_in_interval.
}
Qed.
End JobSuspensionBounded.
Next, assume that tsk respects the arrival curve defined by max_arrivals.
Hypothesis H_tsk_respects_max_arrivals : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
Now we establish a bound on the total duration the jobs of task tsk remain suspended in the interval `[t1, t2)`.
Lemma suspension_of_task_bounded :
\sum_(t1 ≤ t < t1 + Δ) \sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) suspended sched j t
≤ max_arrivals tsk Δ × task_total_suspension tsk.
Proof.
apply leq_trans with
(n := number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) × task_total_suspension tsk); last first.
{ rewrite leq_mul2r; apply /orP; right.
rewrite -{2}[Δ](addKn t1).
exact: H_tsk_respects_max_arrivals. }
rewrite /number_of_task_arrivals -sum1_size big_distrl //=.
rewrite exchange_big_idem //=.
apply leq_sum_seq ⇒ jo INjo _; rewrite mul1n.
apply job_suspension_bounded.
by move: INjo; rewrite mem_filter ⇒ /andP[? ?].
Qed.
End TotalSuspensionBounded.