RTA for FIFO Scheduling on Restricted-Supply Uniprocessors

In the following, we derive a response-time analysis for FIFO schedulers, assuming a workload of sporadic real-time tasks characterized by arbitrary arrival curves executing upon a uniprocessor with arbitrary supply restrictions. To this end, we instantiate the abstract Restricted-Supply Response-Time Analysis (aRSA) as provided in the prosa.analysis.abstract.restricted_supply module.

Defining the System Model

Before any formal claims can be stated, an initial setup is needed to define the system model under consideration. To this end, we next introduce and define the following notions using Prosa's standard definitions and behavioral semantics:

• processor model,
• tasks, jobs, and their parameters,
• the sequence of job arrivals,
• worst-case execution time (WCET) and the absence of self-suspensions,
• the task under analysis,
• an arbitrary schedule of the task set, and finally,
• a supply-bound function.

Processor Model

Consider a restricted-supply uniprocessor model.

Tasks and Jobs

Consider any type of tasks, each characterized by a WCET task_cost, an arrival curve max_arrivals, a run-to-completion threshold task_rtct, and a bound on the the task's longest non-preemptive segment task_max_nonpreemptive_segment ...

... and any type of jobs associated with these tasks, where each job has a task job_task, a cost job_cost, an arrival time job_arrival, and a predicate indicating when the job is preemptable job_preemptable.

The Job Arrival Sequence

Consider any arrival sequence arr_seq with consistent, non-duplicate arrivals.

Absence of Self-Suspensions and WCET Compliance

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

We further require that a job's cost cannot exceed its task's stated WCET.

The Task Set

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 monotonic function that equals 0 for the empty interval delta = 0.

The Schedule

Consider any arbitrary, work-conserving, valid restricted-supply uni-processor schedule of the given arrival sequence arr_seq (and hence the given task set ts) ...

... and assume that the schedule respects the FIFO policy.

We assume a valid preemption model with bounded non-preemptive segments.

The Task Under Analysis

Let tsk be any task in ts that is to be analyzed.

We assume that tsk is described by a valid task run-to-completion threshold. That is, there exists a task parameter task_rtct such that task_rtct tsk is

• (1) no larger than tsk's WCET, and
• (2) for any job of task tsk, the job's run-to-completion threshold job_rtct is bounded by task_rtct tsk.

Supply-Bound Function

Assume the minimum amount of supply that any job of task tsk receives is defined by a monotone unit-supply-bound function SBF.

Next, we assume that SBF properly characterizes all busy intervals (w.r.t. task tsk) in sched. That is, (1) SBF 0 = 0 and (2) for any duration Δ, at least SBF Δ supply is available in any busy-interval prefix of length Δ.

Length of Busy Interval

The next step is to establish a bound on the maximum busy-window length, which aRSA requires to be given. To this end, let L be any positive fixed point of the busy-interval recurrence. As the busy_intervals_are_bounded_rs_jlfp lemma shows, under any preemptive JLFP scheduling policy, this is sufficient to guarantee that all busy intervals are bounded by L.

Response-Time Bound

Having established all necessary preliminaries, it is finally time to state the claimed response-time bound R. A value R is an RTA-recurrence solution if, for any given offset A in the search space, the response-time bound recurrence has a solution F not exceeding R.

Finally, using the abstract restricted-supply analysis, we establish that any R that satisfies the stated equation is a sound response-time bound for the FIFO scheduling with arbitrary supply restrictions.