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 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.

Results in the Current Version of Prosa

The following results are part of “modern Prosa,” the current, actively maintained branch of Prosa.

Optimality & Generality Results

Optimality of Earliest-Deadline-First (EDF) scheduling on an ideal uniprocessor:

prosa.results.optimality.edf

Generality of (Global) EDF-Like (GEL) scheduling:

prosa.results.generality.gel

Generality of EDF-Like within Fixed priorities (ELF) scheduling:

prosa.results.generality.elf

Transfer Schedulability

Prosa contains the mechanized proofs for Willemsen et al.’s EMSOFT’25 paper introducing the concept of transfer schedulability.

The general system model, definition of the transfer schedulability criterion, and the main proofs of necessity and sufficiency: prosa.results.transfer_schedulability.criterion
Instantiation of the general results for the more specific system model assumed in the paper: prosa.results.transfer_schedulability.paper_model

Response-Time Analyses (RTAs)

All RTAs support a quite general setting: sporadic tasks characterized by arbitrary arrival curves and with arbitrary deadlines.

Sporadic Tasks on an Ideal Uniprocessor

Scheduling Policy	Preemption Model	RTA in Prosa
FIFO	any	`prosa.results.rta.ideal.fifo.bounded_nps`
EDF	fully preemptive	`prosa.results.rta.ideal.edf.fully_preemptive`
EDF	floating non-preemptive sections	`prosa.results.rta.ideal.edf.floating_nonpreemptive`
EDF	segmented limited-preemptive	`prosa.results.rta.ideal.edf.limited_preemptive`
EDF	fully non-preemptive	`prosa.results.rta.ideal.edf.fully_nonpreemptive`
FP	fully preemptive	`prosa.results.rta.ideal.fp.fully_preemptive`
FP	floating non-preemptive sections	`prosa.results.rta.ideal.fp.floating_nonpreemptive`
FP	segmented limited-preemptive	`prosa.results.rta.ideal.fp.limited_preemptive`
FP	fully non-preemptive	`prosa.results.rta.ideal.fp.fully_nonpreemptive`

Sporadic Tasks on a Non-Ideal Uniprocessor Subject to Overheads

Scheduling Policy	Preemption Model	RTA in Prosa
FIFO	any	`prosa.results.rta.ovh.fifo.bounded_nps`
EDF	fully preemptive	`prosa.results.rta.ovh.edf.fully_preemptive`
EDF	floating non-preemptive sections	`prosa.results.rta.ovh.edf.floating_nonpreemptive`
EDF	segmented limited-preemptive	`prosa.results.rta.ovh.edf.limited_preemptive`
EDF	fully non-preemptive	`prosa.results.rta.ovh.edf.fully_nonpreemptive`
FP	fully preemptive	`prosa.results.rta.ovh.fp.fully_preemptive`
FP	floating non-preemptive sections	`prosa.results.rta.ovh.fp.floating_nonpreemptive`
FP	segmented limited-preemptive	`prosa.results.rta.ovh.fp.limited_preemptive`
FP	fully non-preemptive	`prosa.results.rta.ovh.fp.fully_nonpreemptive`

Sporadic Tasks on a Uniprocessor Subject to Execution-Time Exceedance

Scheduling Policy	Preemption Model	RTA in Prosa
FP	fully non-preemptive	`prosa.results.rta.exc.fp.fully_nonpreemptive`

Sporadic Tasks under the Periodic Resource Model

Scheduling Policy	Preemption Model	RTA in Prosa
FIFO	any	`prosa.results.rta.prm.fifo.bounded_nps`
EDF	fully preemptive	`prosa.results.rta.prm.edf.fully_preemptive`
EDF	floating non-preemptive sections	`prosa.results.rta.prm.edf.floating_nonpreemptive`
EDF	segmented limited-preemptive	`prosa.results.rta.prm.edf.limited_preemptive`
EDF	fully non-preemptive	`prosa.results.rta.prm.edf.fully_nonpreemptive`
FP	fully preemptive	`prosa.results.rta.prm.fp.fully_preemptive`
FP	floating non-preemptive sections	`prosa.results.rta.prm.fp.floating_nonpreemptive`
FP	segmented limited-preemptive	`prosa.results.rta.prm.fp.limited_preemptive`
FP	fully non-preemptive	`prosa.results.rta.prm.fp.fully_nonpreemptive`

Sporadic Tasks under the Average Resource Model

Also known as the Rate-Delay Model.

Scheduling Policy	Preemption Model	RTA in Prosa
FIFO	any	`prosa.results.rta.arm.fifo.bounded_nps`
EDF	fully preemptive	`prosa.results.rta.arm.edf.fully_preemptive`
EDF	floating non-preemptive sections	`prosa.results.rta.arm.edf.floating_nonpreemptive`
EDF	segmented limited-preemptive	`prosa.results.rta.arm.edf.limited_preemptive`
EDF	fully non-preemptive	`prosa.results.rta.arm.edf.fully_nonpreemptive`
FP	fully preemptive	`prosa.results.rta.arm.fp.fully_preemptive`
FP	floating non-preemptive sections	`prosa.results.rta.arm.fp.floating_nonpreemptive`
FP	segmented limited-preemptive	`prosa.results.rta.arm.fp.limited_preemptive`
FP	fully non-preemptive	`prosa.results.rta.arm.fp.fully_nonpreemptive`

Sporadic Tasks on Uniprocessors Subject to Arbitrary Supply Restrictions

Scheduling Policy	Preemption Model	RTA in Prosa
FIFO	any	`prosa.results.rta.rs.fifo.bounded_nps`
EDF	fully preemptive	`prosa.results.rta.rs.edf.fully_preemptive`
EDF	floating non-preemptive sections	`prosa.results.rta.rs.edf.floating_nonpreemptive`
EDF	segmented limited-preemptive	`prosa.results.rta.rs.edf.limited_preemptive`
EDF	fully non-preemptive	`prosa.results.rta.rs.edf.fully_nonpreemptive`
FP	fully preemptive	`prosa.results.rta.rs.fp.fully_preemptive`
FP	floating non-preemptive sections	`prosa.results.rta.rs.fp.floating_nonpreemptive`
FP	segmented limited-preemptive	`prosa.results.rta.rs.fp.limited_preemptive`
FP	fully non-preemptive	`prosa.results.rta.rs.fp.fully_nonpreemptive`
ELF	fully preemptive	`prosa.results.rta.rs.elf.fully_preemptive`
ELF	floating non-preemptive sections	`prosa.results.rta.rs.elf.floating_nonpreemptive`
ELF	segmented limited-preemptive	`prosa.results.rta.rs.elf.limited_preemptive`
ELF	fully non-preemptive	`prosa.results.rta.rs.elf.fully_nonpreemptive`

Results in Classic Prosa

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

Uniprocessor Scheduling

Response-time analysis of time-partitioned scheduling (i.e., table-driven scheduling or TDMA) on an ideal uniprocessor assuming sporadic tasks (without release jitter): prosa.classic.analysis.uni.basic.tdma_rta_theory and tdma_wcrt_analysis
Response-time analysis of FP scheduling with release jitter on an ideal uniprocessor assuming sporadic tasks: prosa.classic.analysis.uni.jitter.fp_rta_theory and fp_rta_comp
Suspension-oblivious response-time analysis of FP scheduling assuming sporadic tasks with dynamic self-suspensions on an ideal uniprocessor: prosa.classic.analysis.uni.susp.dynamic.oblivious
Suspension-aware response-time analysis of FP scheduling assuming sporadic tasks with dynamic self-suspensions on an ideal uniprocessor, by reduction to a jitter-aware response-time analysis: prosa.classic.analysis.uni.susp.dynamic.jitter.rta_by_reduction
Weak sustainability of job costs and varying suspension times in the dynamic suspension model: prosa.classic.analysis.uni.susp.sustainability.allcosts.main_claim

Multiprocessor Scheduling

Response-time analysis of Global EDF (G-EDF) on an ideal identical multiprocessor for…
1. sequential sporadic tasks without release jitter: prosa.classic.analysis.global.basic.bertogna_edf_theory and bertogna_edf_comp
2. sequential sporadic tasks with release jitter: prosa.classic.analysis.global.jitter.bertogna_edf_theory and bertogna_edf_comp
3. parallel sporadic tasks (without jitter): prosa.classic.analysis.global.parallel.bertogna_edf_theory and bertogna_edf_comp
Response-time analysis of Global FP (G-FP) on an ideal identical multiprocessor for…
1. sequential sporadic tasks without release jitter: prosa.classic.analysis.global.basic.bertogna_fp_theory and bertogna_fp_comp
2. sequential sporadic tasks with release jitter: prosa.classic.analysis.global.jitter.bertogna_fp_theory and bertogna_fp_comp
3. parallel sporadic tasks (without jitter): prosa.classic.analysis.global.parallel.bertogna_fp_theory and bertogna_fp_comp
Response-time analysis of Arbitrary Processor Affinity (APA) scheduling for sequential sporadic tasks without release jitter, with job priorities determined according to…
1. EDF: prosa.classic.analysis.apa.bertogna_edf_theory and bertogna_edf_comp
2. FP: prosa.classic.analysis.apa.bertogna_fp_theory and bertogna_fp_comp