Prosa v0.4: The new, Restructured Prosa

Prosa v0.4 is the first release of the new, completely restructured version of Prosa.

Organization

The directory and module structure is organized as follows. First, the main parts, of which there are currently four (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.
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.4 release of Prosa includes a new, prettier HTML specification thanks to integration of the CoqdocJS tool.

Read the Prosa v0.4 specification and proofs.

Compiling Prosa

Assuming ssreflect is available (either via OPAM or compiled from source, see the Prosa setup instructions), compiling Prosa consists of only two steps.

First, create an appropriate Makefile.

./create_makefile.sh

Second, compile the library.

make -j 4

Configuration Options

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.

./create_makefile.sh --without-classic

It’s also possible to only compile the “classic” Prosa by specifying the --only-classic option, but this is rarely needed.

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 (other than those introduced by the Mathematical Components library).

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

*Theory: Set is predicative
  
*Axioms:
    mathcomp.ssreflect.finset.Imset.imsetE
    mathcomp.ssreflect.finset.Imset.imset2
    mathcomp.ssreflect.finfun.FinfunDef.finfunE
    mathcomp.ssreflect.fintype.SubsetDef.subsetEdef
    mathcomp.ssreflect.generic_quotient.MPi.f
    mathcomp.ssreflect.generic_quotient.MPi.E
    mathcomp.ssreflect.fintype.Finite.EnumDef.enumDef
    mathcomp.ssreflect.generic_quotient.Repr.f
    mathcomp.ssreflect.generic_quotient.Repr.E
    mathcomp.ssreflect.finset.Imset.imset
    mathcomp.ssreflect.finset.Imset.imset2E
    mathcomp.ssreflect.finset.SetDef.pred_of_set
    mathcomp.ssreflect.finset.SetDef.finset
    mathcomp.ssreflect.tuple.FinTuple.enumP
    mathcomp.ssreflect.tuple.FinTuple.enum
    mathcomp.ssreflect.bigop.BigOp.bigopE
    mathcomp.ssreflect.tuple.FinTuple.size_enum
    mathcomp.ssreflect.finfun.FinfunDef.finfun
    mathcomp.ssreflect.fintype.CardDef.card
    mathcomp.ssreflect.fintype.CardDef.cardEdef
    mathcomp.ssreflect.finset.SetDef.pred_of_setE
    mathcomp.ssreflect.bigop.BigOp.bigop
    mathcomp.ssreflect.fintype.SubsetDef.subset
    mathcomp.ssreflect.generic_quotient.Pi.f
    mathcomp.ssreflect.generic_quotient.Pi.E
    mathcomp.ssreflect.fintype.Finite.EnumDef.enum
    mathcomp.ssreflect.finset.SetDef.finsetE