# Library prosa.analysis.definitions.sbf.periodic

Require Export prosa.analysis.definitions.sbf.sbf.
Require Export prosa.model.processor.supply.

# Periodic Resource Model

In this file, we define the classical periodic resource model and the corresponding SBF, as introduced by Shin & Lee in their paper "Periodic Resource Model for Compositional Real-Time Guarantees" (RTSS 2003).
Section PeriodicResourceModel.
Consider any kind of jobs and any kind of processor state.
Context {Job : JobType} {PState : ProcessorState Job}.
The supply is distributed according to the periodic resource model with a resource period Π and a resource allocation time γ if, for any interval `[Π⋅k, Π⋅(k+1))`, the processor provides at least γ units of supply.
Definition periodic_resource_model (Π γ : duration) (sched : schedule PState) :=
Π > 0
∧ Π ≥ γ
∧ ∀ (k : nat),
supply_during sched (Π × k) (Π × (k + 1)) ≥ γ.
End PeriodicResourceModel.

# SBF for Periodic Resource Model

In this section, we define an SBF for the periodic resource model.
Section PeriodicResourceModelSBF.
Given a periodic resource model with a resource period Π and resource allocation time γ, ...
Variable Π γ : duration.
... we define the corresponding SBF as introduced in "Periodic Resource Model for Compositional Real-Time Guarantees" by Shin & Lee (RTSS 2003).
Definition prm_sbf : SupplyBoundFunction :=
{|
supply_bound_function Δ :=
let blackout := Π - γ in
let n_full_periods := (Δ - blackout) %/ Π in
let supply_in_full_periods := n_full_periods × γ in
let duration_of_full_periods := n_full_periods × Π in
supply_in_full_periods + (Δ - 2 × blackout - duration_of_full_periods)
|}.
End PeriodicResourceModelSBF.