Library prosa.analysis.facts.model.overheads.sbf.fifo

In this section, we define an SBF for the FIFO scheduling policy in the presence of overheads.

Consider any type of tasks,...

... an arbitrary task set ts, ...

... and bounds DB, CSB, and CRPDB on dispatch overhead, context-switch overhead, and preemption-related overhead, respectively.

We define the blackout bound for FIFO in an interval of length Δ as the number of jobs that can arrive in Δ, plus one, multiplied by the sum of all overhead bounds. The "+1" accounts for the fact that n arrivals can result in up to n + 1 segments without a schedule change, and thus up to n + 1 intervals wherein overhead duration is bounded by DB + CSB + CRPDB. Unlike JLFP and FP, FIFO does not require doubling the arrivals, because all jobs are treated uniformly and there are no preemptions caused by higher-priority jobs.

First, we define the FIFO SBF as the interval length minus the FIFO blackout bound.

Next, we define the "slowed-down" version of the FIFO SBF as the interval length minus the slowed-down blackout bound. The slowdown ensures that the resulting SBF is monotone and unit-growth, which is necessary to obtain response-time bounds using aRSA. This slowed-down FIFO SBF is used internally in the analysis, while the unmodified FIFO SBF is used to state the top-level analysis result.

In the following section, we show that the SBF defined above is indeed a valid SBF.

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Consider a FIFO priority policy that indicates a higher-or-equal priority relation.

Consider any valid arrival sequence...

... and any explicit-overhead uni-processor schedule without superfluous preemptions of this arrival sequence.

Assume that the schedule respects the JLFP policy.

Assume that the preemption model is valid.

We consider an arbitrary task set ts ...

... and assume that all jobs stem from tasks in this task set.

We assume that max_arrivals is a family of valid arrival curves that constrains the arrival sequence arr_seq, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and ...

... (2) a monotone function that equals 0 for the empty interval delta = 0.

We assume that all jobs have positive cost. This restriction is not fundamental to the analysis, but rather an artifact of the current proof structure in the library.

Finally, we assume that the schedule respects a valid overhead resource model with dispatch overhead DB, context-switch overhead CSB, and preemption-related overhead CRPDB.

We show that the slowed SBF is monotone.

In addition, we note that fifo_blackout_bound is monotone as well.

The slowed SBF is also a unit-supply SBF.

Lastly, we prove that the slowed SBF is valid.