Get Prosa

There are three main ways to use Prosa: either read the specification online (recommended for novices and researchers with a casual interest), download and check a specific release, or clone the Prosa repository (recommended for development).

Read the Prosa Specification

The recommended way to read Prosa is by looking at the specification with low-level proofs omitted:

For reference, the specification with proofs and the full Coq source code are made available here:

See the getting started guide for a brief intro to essential Coq syntax.

Checking the Proofs

To independently verify the correctness of the proofs, the full development can be downloaded, compiled, and validated with the Coq proof checker. This process is intentionally very simple and does not require any prior Coq knowledge.

For a short tutorial on how to check the proofs in Prosa, please follow the ECRTS’16 artifact evaluation instructions.

The Prosa Repository

To start a new proof development or to contribute patches, it’s best to work with the Prosa git repository, which is publicly available on the MPI-SWS GitLab server.

To clone the repository, use the following command.

git clone https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git

For a tutorial on how to compile Prosa, please follow the setup instructions.

Releases

We periodically provide stable releases, which may be found below. Note that these releases are primarily intended as stable snapshots for ease of reference (e.g., to refer to a specific proof in a paper). For new developments and general improvements, please base your work on the current version (as found in the git repository).

The current releases of Prosa are based on Coq 8.5. For a step-by-step guide on how to install Prosa and its dependencies, please check out the setup instructions.

Prosa 0.3

Released on July 17th, 2018. Tested with Coq 8.7.0 and mathcomp 1.6.4.

Prosa v0.3 introduces the new classification of strong and weak sustainable policies. It also includes a proof that uniprocessor JLFP scheduling of self-suspending tasks is weakly sustainable with respect to execution times and variable suspension times. See the overview page for more information.

Prosa 0.2

Released on June 6th, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.

Prosa v0.2 incorporates the reduction-based response-time analysis (RTA) for real-time scheduling with arbitrary processor affinities (APA). See the overview page for more information.

Prosa 0.1

Released on May 5th, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.

Prosa v0.1 formalizes Bertogna and Cirinei’s response-time analysis (RTA) for global FP and EDF scheduling, along with extensions for release jitter and parallel jobs. For additional information, please follow the ECRTS’16 artifact evaluation instructions.