# Library prosa.analysis.facts.suspension

Require Export prosa.model.readiness.suspension.

# Facts about Self-Suspensions

In this file, we establish some basic facts related to self-suspensions.
Section Suspensions.
Consider any kind of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Suppose that the jobs can exhibit self-suspensions.
Context `{JobSuspension Job}.
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.

## Basic Lemmas

First, we establish some basic lemmas regarding self-suspending jobs.
We show that a self-suspended job cannot be ready, ...
Lemma suspended_implies_job_not_ready :
∀ j t,
suspended sched j t →
~~ job_ready sched j t.
... which trivially implies that the job cannot be scheduled.
Lemma suspended_implies_not_scheduled :
∀ j t,
suspended sched j t →
~~ scheduled_at sched j t.
Next, we observe that a self-suspended job has already arrived.
Lemma suspended_implies_arrived :
∀ j t,
suspended sched j t →
has_arrived j t.
By definition, only pending jobs can be self-suspended.
Lemma suspended_implies_pending :
∀ j t,
suspended sched j t →
pending sched j t.
Next, we note that self-suspended jobs are not backlogged.
Lemma suspended_implies_not_backlogged :
∀ j t,
suspended sched j t →
~~ backlogged sched j t.
Further, we prove that if a job is pending and not self-suspended then it is ready.
Lemma pending_and_not_suspended_implies_ready :
∀ j t,
pending sched j t →
~~ suspended sched j t →
job_ready sched j t.

## Self-Suspension Bound at any Point During a Job's Execution

Next, we focus on bounding the self-suspension period of a job after receiving some amount of service.
Section SuspensionBoundedinInterval.
Consider any job j ...
Variable j : Job.
... and any time interval `[t1, t2)`.
Variable t1 t2 : instant.
Now consider any amount of work ρ.
Variable ρ : work.
Our aim is to prove a bound on the self-suspension period of j after receiving an amount of service ρ. Note that it is possible that the job may not self-suspend after receiving ρ amount of service in which case job_suspension j ρ = 0.
Additionally, it is also important to note that the job may self-suspend multiple times within an interval, and these self-suspension intervals are separated by an interval where the job gets serviced. We can refer each such self-suspension interval as a segment, and each such segment is characterized by the amount of service received by the job.
Essentially here we are establishing a bound on the length of the self-suspension segment of j characterized by ρ.

### Step 1

Note that we can have two cases here, either the job j starts a suspension segment within the interval `[t1, t2)`, or the job is already suspended at t1.
Section Step1.
Consider a point tf inside `[t1, t2)`.
Variable tf : instant.
Hypothesis INtf : t1 ≤ tf < t2.
Let tf be the first point in the interval `[t1, t2)` that is also inside the self-suspension segment.
Hypothesis H_suspended_tf : suspended sched j tf.
Hypothesis H_service_at_tf : service sched j tf = ρ.
Hypothesis H_before_tf :
∀ to,
t1 ≤ to < tf →
~~ (suspended sched j to && (service sched j to == ρ)).
First, we prove a trivial result that the total suspension before tf is zero.
Local Lemma suspension_zero_before :
\sum_(t1 ≤ t < tf | service sched j t == ρ) suspended sched j t = 0.
Next we consider the trivial case when the suspension period exceeds the interval `[tf, t2)`.
Lemma suspension_bounded_trivial :
t2 - tf ≤ job_suspension j ρ →
\sum_(tf ≤ t < t2 | service sched j t == ρ) suspended sched j t ≤ job_suspension j ρ.
Next, we consider the case when the suspension period is within the interval `[tf, t2)`.
Lemma suspension_bounded_longer_interval :
t2 - tf > job_suspension j ρ →
\sum_(tf ≤ t < t2 | service sched j t == ρ) suspended sched j t ≤ job_suspension j ρ.
Now we prove the required bound in case a point like tf exists. This helps to simplify our final proof.
Lemma suspension_bounded_in_interval_aux :
\sum_(t1 ≤ t < t2 | service sched j t == ρ) suspended sched j t ≤ job_suspension j ρ.
End Step1.

### Step 2

Now we prove that the point tf, as used in the above lemmas, always exists if suspended is true at some point inside `[t1, t2)`.
Lemma exists_some_point :
(exists2 t, t \in index_iota t1 t2 & (suspended sched j t && (service sched j t == ρ))) →
∃ t',
t1 ≤ t' < t2
∧ suspended sched j t'
∧ service sched j t' = ρ
∧ ∀ to, t1 ≤ to < t' →
~~ (suspended sched j to && (service sched j to == ρ)).

### Final Bound

Finally we prove the required result.
Lemma suspension_bounded_in_interval :
\sum_(t1 ≤ t < t2 | service sched j t == ρ) suspended sched j t ≤ job_suspension j ρ.
End SuspensionBoundedinInterval.
End Suspensions.