Prosa v0.6: The aRSA Edition

Prosa v0.6 is the first release of Prosa with RTAs for non-ideal processor types, based on a novel abstract Restricted Supply Analysis (aRSA, developed by Sergey Bozhko).

Download

Download the release here: prosa-v0.6.tar.bz2

Reading Prosa

The v0.6 release of Prosa uses CoqdocJS to obtain a prettier spec.

Read the Prosa v0.6 specification and proofs.

Alternatively, there is also a plain coqdoc version without proofs (which is better suited for printing to PDF).

Read the Prosa v0.6 specification without proofs.

Organization

The directory and module structure is organized as follows. First, the main parts, of which there are currently six.

prosa.behavior: The behavior namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa’s trace-based semantics). There are no proofs here. This module is mandatory: all results in Prosa rely on the basic trace-based semantics defined in this module.
prosa.model: The model namespace collects all definitions and basic properties of various system models (e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple alternatives of the same concept (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected “pick and choose” whatever definitions and assumptions are appropriate.
prosa.analysis: The analysis namespace collects all definitions and proof libraries needed to establish system properties (e.g., schedulability, response time, etc.). This includes a substantial library of basic facts that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.
prosa.results: The results namespace contains all high-level analysis results.
prosa.implementation: Concrete implementations of some of the axiomatic models to which the results apply.
prosa.implementation.refinements: The refinements needed by POET to compute with large numbers, based on CoqEAL.

Installing Prosa

With OPAM

Prosa can be installed using the OPAM package manager (>= 2.0).

opam repo add rocq-released https://rocq-prover.org/opam/released
opam update
opam install "rocq-prosa>=0.6"

If you plan on using POET, also install the rocq-prosa-refinements package.

opam install "rocq-prosa-refinements>=0.6"

From Sources with `opam`

OPAM can also be used to install a local checkout. For example, this is done in the CI setup (see .gitlab-ci.yaml).

opam repo add rocq-released https://rocq-prover.org/opam/released
opam update
opam pin add -n -y -k path rocq-prosa .
opam pin add -n -y -k path rocq-prosa-refinements .
opam install rocq-prosa rocq-prosa-refinements

Manually From Sources

Dependencies

Besides on Coq itself, Prosa depends on

the ssreflect library of the Mathematical Components project,
the Micromega support for the Mathematical Components library provided by mczify, and
the The Coq Effective Algebra Library (optional, needed only for POET-related refinements).

Prosa v0.6 is known to work with Rocq 9.0.0, MathComp 2.4.0, mczify 1.5.0, and CoqEAL 2.1.0.

These dependencies can be easily installed with OPAM.

opam install -y rocq-mathcomp-ssreflect coq-mathcomp-zify coq-coqeal

Compiling Prosa

Assuming all dependencies are available (either via OPAM or compiled from source), compile Prosa simply via the provided Makefile:

make -j

To also compile the refinements needed by POET, run instead:

make -j all