Overview of Verified Results

In addition to a specification of real-time scheduling, various task and system models, and a large library of utility lemmas, Prosa also contains several higher-level theorems of general interest to the real-time systems community, which we refer to as the main results.

For ease of reference, this page provides an overview of the main results formalized and proven correct in Prosa to date.

Earliest-Deadline-First (EDF) Scheduling

Under the classic EDF scheduling policy, each task is associated with a relative deadline, and each job derives its absolute deadline by adding its task’s relative deadline to the its arrival time. Jobs are then scheduled in order of non-decreasing absolute deadlines.

Prosa provides the following results about EDF scheduling:

First-In First-Out (FIFO) Scheduling

Under the trivial FIFO scheduling policy, jobs are scheduled in order of non-decreasing arrival times.

Prosa provides the following result about FIFO scheduling:

As FIFO scheduling is inherently non-preemptive, the above result applies to any preemption model (e.g., fully preemptive, fully non-preemptive, limited-preemptive, …). Therefore, unlike in the case of EDF scheduling above, no further instantiations to specific preemption models are required.

Fixed-Priority (FP) Scheduling

Under fixed-priority (FP) scheduling, also known as static-priority (SP) scheduling, each task is assigned an unchanging priority ahead of time, and jobs are scheduled at runtime in order of decreasing task priorities (with any ties in priority broken arbitrarily). Rate-monotonic (RM) scheduling is a particularly well-known case of FP scheduling.

Prosa provides the following results, which are applicable to any FP policy (i.e., to RM scheduling, but also to any other priority assignment scheme).

EDF-Like Scheduling (GEL)

EDF-Like (EL) scheduling, due to its origins also called Global-EDF-Like (GEL) scheduling, generalizes the idea behind EDF by associating with each task a (relative) priority point (analogous to a relative deadline), from which each job derives its absolute priority point (analogous to an absolute deadline). Jobs are then scheduled in order of non-decreasing absolute priority points. GEL scheduling generalizes both EDF and FIFO scheduling, and under some assumptions (Günzel et al., RTSS’22), also FP scheduling.

As in the cases of FP and EDF scheduling above, the bounded-PI GEL analysis could be instantiated to bounded non-preemptive sections (NPS), and from there to various preemption models. These instantiations have not yet been carried out, however. Patches welcome… :-)

Results in Classic Prosa

Additionally, the following results may be found in classic Prosa, an earlier version of Prosa developed until 2020.

Uniprocessor Scheduling

Multiprocessor Scheduling

legal imprint | data protection notice