# Library prosa.analysis.facts.model.sbf.periodic

Require Export prosa.model.priority.classes.
Require Export prosa.model.processor.supply.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.definitions.sbf.plain.
Require Export prosa.analysis.definitions.sbf.periodic.

# SBF for Periodic Resource Model in Valid

In this file, we prove that the SBF defined in the paper "Periodic Resource Model for Compositional Real-Time Guarantees" by Shin & Lee (RTSS 2003) is valid under the periodic resource model.
Section PeriodicResourceModelValidSBF.
Consider any type of tasks ...
Context {Task : TaskType}.
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of unit-supply processor state model.
Context {PState : ProcessorState Job}.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Consider a JLFP policy, ...
Context `{JLFP_policy Job}.
... any arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
... and any schedule.
Variable sched : schedule PState.
Assume a periodic resource model with a resource period Π and resource allocation time γ.
Variable Π γ : duration.
Hypothesis H_periodic_resource_model : periodic_resource_model Π γ sched.
Next, we prove a few properties required by aRSA-based analyses, in particular that the SBF is valid.
We show that sbf is monotone.
Lemma prm_sbf_monotone : sbf_is_monotone (prm_sbf Π γ).
The introduced SBF is also a unit-supply SBF.
Lemma prm_sbf_unit : unit_supply_bound_function (prm_sbf Π γ).
In the following, we prove that the introduced SBF is valid.
We prove the validity claim via a case analysis on the interval for which the SBF is computed. First, we consider an interval that falls completely within a period `[kΠ, (k + 1)Π)` for some k.
Section Case1.
Consider a constant k and two durations q1, q2 < Π.
Variable (k : nat) (q1 q2 : duration).
Hypothesis H_q1_small : q1 < Π.
Hypothesis H_q2_small : q2 < Π.
We show that, in this case, supply during the interval is lower-bounded by (q2 - q1) - (Π - Θ).
Local Lemma prm_sbf_valid_aux_11 :
(q2 - q1) - (Π - γ) ≤ supply_during sched (k × Π + q1) (k × Π + q2).
Let `[t1, t2)` := `[kΠ + q1, kΠ + q2)` be the interval under analysis.
Let t1 := k × Π + q1.
Let t2 := k × Π + q2.
By unfolding the expression for sbf and using the above inequalities, we show that the supply during `[t1, t2)` is indeed lower-bounded by sbf (t2-t1).
Lemma prm_sbf_valid_aux_1 :
prm_sbf Π γ (t2 - t1) ≤ supply_during sched t1 t2.
End Case1.
For the second case, consider an interval that touches at least two periods. That is, consider an interval `[k1 Π + q1, k2 Π + q2)` for some k1 < k2.
Section Case2.
Consider two constants k1, k2 such that k1 < k2 and two durations q1, q2 < Π.
Variables (k1 k2 : nat) (q1 q2 : duration).
Hypothesis H_q1_small : q1 < Π.
Hypothesis H_q2_small : q2 < Π.
Hypothesis H_k1_lt_k2 : k1 < k2.
First, we show that the interval can be split into three sub-intervals: `[k1 Π + q1, (k1 + 1) Π + q1)`, `[(k1 + 1) Π + q1, k2 Π)`, and `[k2 Π, k2 Π + q2)`.
Lemma prm_sbf_valid_aux_21 :
supply_during sched (k1 × Π + q1) (k2 × Π + q2)
= supply_during sched (k1 × Π + q1) ((k1 + 1) × Π)
+ supply_during sched ((k1 + 1) × Π) (k2 × Π)
+ supply_during sched (k2 × Π) (k2 × Π + q2).
In the following, we simply lower-bound the supply in each of the three sub-intervals.
Supply in the interval `[k1 Π + q1, (k1 + 1) Π + q1)` is lower-bounded by (Π - q1) - (Π - Θ).
Lemma prm_sbf_valid_aux_22 :
(Π - q1) - (Π - γ) ≤ supply_during sched (k1 × Π + q1) ((k1 + 1) × Π).
Supply in the interval `[(k1 + 1) Π + q1, k2 Π)` is lower-bounded by (k2 - (k1 + 1)) × Θ.
Lemma prm_sbf_valid_aux_23 :
(k2 - (k1 + 1)) × γ ≤ supply_during sched ((k1 + 1) × Π) (k2 × Π).
Supply in the interval `[k2 Π, k2 Π + q2)` is lower-bounded by q2 - (Π - Θ).
Lemma prm_sbf_valid_aux_24 :
q2 - (Π - γ) ≤ supply_during sched (k2 × Π) (k2 × Π + q2).
Let `[t1, t2)` := `[k1 Π + q1, k2 Π + q2)` be the interval under analysis.
Let t1 := k1 × Π + q1.
Let t2 := k2 × Π + q2.
By unfolding the expression for sbf and using the above inequalities, we show that the supply during `[t1, t2)` is indeed lower-bounded by sbf (t2-t1).
Lemma prm_sbf_valid_aux_2 :
prm_sbf Π γ (t2 - t1) ≤ supply_during sched t1 t2.
End Case2.
By using the two auxiliary lemmas above, we prove that sbf is a valid SBF.
Lemma prm_sbf_valid :
valid_supply_bound_function arr_seq sched (prm_sbf Π γ).
End PeriodicResourceModelValidSBF.