Prosa v0.5: The POET Edition

Prosa v0.5 is the first release of Prosa to support POET.

Download

Download the release here: prosa_v05.zip

Organization

The directory and module structure is organized as follows. First, the main parts, of which there are currently five (plus the classic Prosa version).

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, mutually exclusive alternatives (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.
classic: This module contains the “classic” version of Prosa as first presented at ECRTS’16.
All results published prior to 2020 build on this “classic” version of Prosa.

Reading Prosa

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

Read the Prosa v0.5 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.5 specification without proofs.

We also provide HTML renderings of the classic (i.e., pre-2020) Prosa spec, which is no longer being developed:

Recommended: CoqdocJS-prettified (with proofs)
Alternative: plain coqdoc (without proofs):

Installing Prosa

With OPAM

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

opam repo add coq-released https://coq.inria.fr/opam/released
# or for the dev version (git master): https://coq.inria.fr/opam/extra-dev
opam update
opam install coq-prosa

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 coq-released https://coq.inria.fr/opam/released
opam update
opam pin add -n -y -k path coq-prosa .
opam install coq-prosa

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

These dependencies can be easily installed with OPAM.

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

Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect.

Compiling Prosa

Assuming all dependencies are available (either via OPAM or compiled from source), compiling Prosa consists of only two steps.

First, create an appropriate Makefile.

./create_makefile.sh

Alternatively, to avoid compiling the older “classic” Prosa, specify the --without-classic option. This can speed up compilation considerably and is a good idea during development. (It’s also possible to only compile the “classic” Prosa by specifying the --only-classic option, but this is rarely needed.)

./create_makefile.sh --without-classic

To avoid compiling the POET-related refinements (which require CoqEAL to be installed and inject a dependency on the proof irrelevance axiom), specify the switch --without-refinements. For example, to skip both “classic” Prosa and the refinements library, use the following command:

./create_makefile.sh --without-classic --without-refinements

Second, compile the library.

make -j

Depending on how powerful your machine is, this will take a few minutes.

Checking the Correctness of the Proofs

To check the correctness of all proofs, compile the code as described above and run make validate.

make validate

You should see the following output, confirming that all proofs in Prosa were mechanically checked and do not include any additional Axioms .

CONTEXT SUMMARY
===============

* Theory: Set is predicative
  
* Axioms:
    Coq.Logic.ProofIrrelevance.proof_irrelevance
  
* Constants/Inductives relying on type-in-type: <none>
  
* Constants/Inductives relying on unsafe (co)fixpoints: <none>
  
* Inductives whose positivity is assumed: <none>

The assumption of proof irrelevance is introduced by the CoqEAL library and can be avoided by running ./create_makefile.sh with the --without-refinements flag.