Library prosa.analysis.facts.model.sbf.average

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.average.

SBF for Average Resource Model in Valid

In this file, we prove that the SBF defined in the file prosa.analysis.definitions.sbf.average is valid under the average resource model.
Section AverageResourceModelValidSBF.

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 processor state.
  Context {PState : ProcessorState Job}.

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 the average resource model with a resource period Π, resource allocation time Θ, and supply delay ν.
  Variable Π Θ ν : duration.
  Hypothesis H_average_resource_model : average_resource_model Π Θ ν sched.

We show that sbf is monotone.
  Lemma arm_sbf_monotone : sbf_is_monotone (arm_sbf Π Θ ν).

The introduced SBF is also a unit-supply SBF.
  Lemma arm_sbf_unit : unit_supply_bound_function (arm_sbf Π Θ ν).

Finally, we show that the defined sbf is a valid SBF.
  Lemma arm_sbf_valid :
    valid_supply_bound_function arr_seq sched (arm_sbf Π Θ ν).

End AverageResourceModelValidSBF.