# 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.
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.
End TotalSuspensionBounded.