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).
The recommended way to read Prosa is by looking at the HTML specification with low-level proofs hidden (available on demand by clicking “Proof” under each lemma/theorem):
If you are unsure where to start, then read the specifications in the module prosa.behavior first, followed by those in prosa.model. The release overview provides further information on the organization of the Prosa library.
Note: if the specification appears to be missing all comments, try reloading the page with your ad-blocker disabled; there are some false-positive issues with coqdoc and certain blockers.
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.
git clone https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git.Makefile by running ./create_makefile.sh. For further information on this poin, see also the compilation instructions).make validate.The last step should report that there are no unproven or admitted theorems, nor any nonstandard axioms. For a short tutorial on how to interpret the output, please consult the ECRTS’16 artifact evaluation instructions.
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.
Up-to-date documentation for all branches is generated automatically.
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.
We infrequently 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, general improvements, or simply getting to know Prosa, please base your work on the current version (as found in the git repository).
The current releases of Prosa are usually based on the latest versions of Coq and the Mathematical Components library (mathcomp). For a step-by-step guide on how to install Prosa and its dependencies, please check out the setup instructions.
Released on November 7, 2022. Tested with Coq 8.16.0 and mathcomp 1.15.0.
view specification (with show-on-click proof scripts, recommended)
view specification (without proof scripts)
Released on December 21, 2019. Tested with Coq 8.10.0 and mathcomp 1.9.0.
view specification (with on-demand proof scripts, recommended)
view specification (without proof scripts)
Prosa v0.4 is the first release of the completely refactored “new Prosa”. The prior version is still available in the “classic” namespace, but it is deprecated and will not be developed any further. Eventually, the classic version will be removed.
Released on July 17, 2018. Tested with Coq 8.7.0 and mathcomp 1.6.4.
view specification (without proof scripts)
view specification (with proof scripts)
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.
Released on June 6, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.
view specification (without proof scripts)
view specification (with proof scripts)
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.
Released on May 5, 2016. Tested with Coq 8.5pl1 and ssreflect 1.6.
view specification (without proof scripts)
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.