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.