Library prosa.analysis.facts.model.exceedance.SBF

In this file, we instantiate the supply-bound function for ideal uniprocessors with exceedance.

Let us state the definition first.

Section SBFDefinition.

Let e be the bound on exceedance in any busy window.

Variable e : work.

Then, the SBF is defined as follows.

Definition eps_sbf (Δ : nat) : work := Δ - e.

End SBFDefinition.

Next, we establish some facts about the above-defined SBF.

Section SBFFacts.

Consider tasks characterized by nominal execution times ...

Context {Task : TaskType} `{TaskCost Task}.

... and their associated jobs with costs and arrival times.

Context {Job : JobType} `{JobTask Job Task}
`{JobCost Job} `{JobArrival Job}.

Consider any JLFP policy.

Context `{JLFP_policy Job}.

Assume an arrival sequence ...

... and a corresponding ideal uniprocessor schedule subject to exceedance.

Assume e is the bound on exceedance in a busy interval ...

Variable e : work.

... of a given task tsk.

Variable tsk : Task.

Let us state the exceedance using Instance to make it locally available to the typeclasses database.

Let us formally state the assumption that the total exceedance inside the busy interval of tsk is bounded by e.

Since we model exceedance as blackouts, we trivially have that the blackouts are bounded by e.

Using the above, we can prove that our definition of SBF is valid.

Finally, we prove that our SBF only takes steps of one unit.