# A Foundation for Formally Proven Schedulability Analysis

## What is Prosa?

Prosa is a repository of definitions and proofs for real-time schedulability analysis. To ensure full correctness, Prosa is built and verified with Coq, a powerful and mature proof assistant with support for higher-order logic and computations. Prosa’s distinguishing characteristic is that Prosa prioritizes readability over all other concerns to ensure that specifications remain accessible to readers without a background in formal proofs. (A background in real-time scheduling is assumed.)

See the Prosa paper for an in-depth introduction.

## News

• December 2021: New work-in-progress paper by Maida et al. on the automatic generation of proof-carrying response-time bounds — check it out (PDF).
• August 2021: New paper by Guo et al. on certified schedulability analysis in RT-CertiKOS — check it out (PDF).
• July 2020: Bozhko and Brandenburg win an Outstanding Paper Award at ECRTS’20 for their paper on abstract response-time analysis in Prosa — check it out (PDF).
• December 2019: Prosa 0.4 released, a completely refactored version of Prosa.
• October 2019: Fourth RT-PROOFS meeting @ Inria in Paris, France.
• July 2019: New paper by Guo et al. on a connection between CertiKOS and Prosa — check it out (PDF).
• June 2019: Up-to-date coqdoc documentation for the master branch and work-in-progress branches is now available at https://prosa.mpi-sws.org/branches.
• April 2019: New paper by Fradet et al. on CertiCAN, a tool for certified CAN analysis — check it out (PDF).
• April 2019: Third RT-PROOFS meeting @ TUBS in Braunschweig, Germany.
• December 2018: New paper by Fradet et al. on a generic proof of typical worst-case analysis at RTSS’18 — check it out (PDF).
• October 2018: New paper by Fradet et al. on generalized digraph models at RTNS’18 — check it out (PDF).
• September 2018: Second RT-PROOFS meeting @ MPI-SWS in Kaiserslautern, Germany.
• July 2018: Prosa 0.3 released, including a formalization of sustainability theory and self-suspending tasks.
• July 2018: New work-in-progress paper by Riffard et al. on support for synchronization protocols in Prosa — check it out (PDF)!
• July 2018: Cerqueira et al. win an Outstanding Paper Award at ECRTS’18 for their paper on strong and weak sustainability, with proofs checked in Prosa — check it out (PDF)!
• January 2018: First RT-PROOFS meeting @ ONERA in Toulouse, France.
• December 2017: New work-in-progress paper by Xiaojie Guo et al. on certified schedulability analysis tools — check it out (PDF)!
• October 2017: The French-German RT-PROOFS project, which leverages and seeks to improve Prosa, is funded by ANR and DFG for three years (≈660k EUR).
• July 2016: Cerqueira et al. win the ECRTS’16 Best Paper Award for their paper introducing Prosa.
• June 2016: Prosa 0.2 released, with support for arbitrary processor affinities (APA).
• May 2016: Prosa 0.1 released.

## Why should I use Prosa?

Prosa is a framework for developing schedulability analysis backed by mechanized proofs, i.e., formal proofs that are developed using a proof assistant (e.g., Coq, Isabelle, Agda, etc.). The mechanization process provides three main benefits:

• Guaranteed correctness: since proofs are machine-checked, they are bug-free and can be easily checked by third parties.

• Trustworthy extensions: localized changes in the task model (e.g., to introduce jitter, blocking, or system overheads) or other assumptions can be factored in systematically, without compromising correctness. If a change in assumptions breaks a proof, it will be flagged by the proof assistant.

• Safe composition: schedulability analyses that are individually correct can be safely composed without the risk of implicit or mismatching assumptions. In Prosa, all assumptions are explicit, and any differences in assumptions will be flagged by the proof assistant.

One of the distinguishing features of Prosa is its emphasis on making the specification readable and accessible to the community at large. In the long term, as the formal specification gains widespread acceptance by the real-time community, Prosa will allow us to develop schedulability analysis with the highest-possible degree of confidence, matching the requirements of safety-critical applications.

## What does Prosa look like?

Prosa is nothing more than a collection of definitions, hypotheses, and theorems, with extensive commentary in between. To provide a taste of what it looks like, we provide a short example of a simple lemma. For the sake of brevity, we don’t provide the full context of the specification.

Example: Assume that jobs are sequential, i.e., any single job cannot be scheduled on multiple processors in parallel.

(* Assume that jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.

Explanation: this fragment introduces an assumption, named H_sequential_jobs for later reference, that states that, in any considered schedule sched (defined previously in the context, not shown here), all jobs execute sequentially (with the sequential_jobs predicate, definition not shown here). In Prosa, all assumptions are made explicitly using this Hypothesis syntax, which greatly aids readability.

Then, let $j$ be any job in the arrival sequence.

(* Let j be any job in the arrival sequence. *)
Variable j: JobIn arr_seq.

Explanation: this fragment introduces a new variable, named j, to denote an arbitrary job of a sporadic task. The type of the variable is JobIn arr_seq, which means that job j stems from the arrival sequence arr_seq, where arr_seq is an arbitrary legal arrival sequence (definition not shown here).

Using the job sequentiality assumption, we prove that the instantaneous service received by job $j$ at any time $t$ is at most one time unit.

(* The service received by any job j at any time t is at most 1. *)
Lemma service_at_most_one :
t, service_at sched j t 1.
[Show Proof]

Explanation: there are two parts to this fragment. The first part is the lemma statement (i.e., the claim). In Prosa, lemma claims are kept intentionally simple to make sure that they can be understood without a deep knowledge of Coq. For instance, in this example, the lemma quite literally states that, at any time t, the job j receives at most one time unit of processor service, which follows from the assumption that jobs are sequential.

The second part is the justification of the claim, which is a low-level proof script that instructs Coq how to construct a formal proof (technically, a proof term) for the claim. In contrast to the specification (definitions and claims), proof scripts are not intended for human consumption and require significant Coq expertise (and use of the proof assistant) to be understood.

This highlights the Prosa goals and principles:

• the specification and claims should be accessible to, and understood by, anyone with a background in real-time scheduling, whereas

• the development of new proofs is necessarily a task that requires more specialized Coq knowledge.

However, even non-experts can easily verify that the provided proofs are correct by downloading Prosa and running the Coq proof checker.