diff --git a/README.md b/README.md index 3ff34257c5a45a9dd7700c1c1dc06a79efd6a79a..0c90f604ed00abaf0bfe9ddc9d1b8ea291f9b836 100644 --- a/README.md +++ b/README.md @@ -1,70 +1,81 @@ -# RT-PROOFS +# Prosa: Formally Proven Schedulability Analysis -This repository contains the main Coq proof spec & proof development of the RT-PROOFS project. +This repository contains the main Coq specification & proof development of the [Prosa open-source project](https://prosa.mpi-sws.org), which was launched in 2016. As of 2018, Prosa is primarily being developed in the context of the [RT-Proofs research project](https://rt-proofs.inria.fr/) (kindly funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively). -## Directory Structure +<center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center> -The Prosa directory is organized in a hierarchy: while generic, reusable foundations stay in -the upper levels, definitions for specific analyses should go deeper into the directory tree. +## Publications -### Base Directories +Please see the [list of publications](http://prosa.mpi-sws.org/documentation.html#publications) on the Prosa project's homepage. -Currently, Prosa contains the following base directories: +## Directory and Module Structure -- **model/:** Specification of task and scheduler models, as well as generic lemmas related to scheduling. - -- **analysis/:** Definition, proofs and implementation of schedulability analyses. +The directory and module structure is currently undergoing a fundamental reorganization. -- **implementation/:** Instantiation of each schedulability analysis with concrete task and scheduler implementations. - Testing the main theorems in an assumption free environment shows the absence of contradictions. +- [classic/](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. +- [util/](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa. +- [restructuring/](restructuring/): The new, refactored version of Prosa. Currently still under heavy development. This part of Prosa will soon move out of the `restructuring` namespace. +- [scripts/](scripts/): Scripts and supporting resources required for continuous integration and documentation generation. -### Internal Directories +## Dependencies -The major concepts in Prosa are specified in the *model/* folder. +Besides Coq itself, Prosa's only external dependency is the ssreflect library of the [Mathematical Components project](https://math-comp.github.io). -- **model/arrival:** Arrival sequences and arrival bounds -- **model/schedule:** Definitions and properties of schedules +Prosa always tracks the latest stable versions of Coq and ssreflect. We do not maintain compatibility with older versions of either Coq or ssreflect. -Inside *model/schedule*, you can find the different classes of schedulers. +## Compiling Prosa -- **model/schedule/uni:** Uniprocessor scheduling. -- **model/schedule/global:** Global scheduling. -- **model/schedule/partitioned:** Partitioned scheduling. -- **model/schedule/apa:** APA scheduling. +Assuming ssreflect is available (either via OPAM or compiled from source, see the [Prosa setup instructions](http://prosa.mpi-sws.org/setup-instructions.html)), compiling Prosa consists of only two steps. -### Extending Prosa +First, create an appropriate `Makefile`. -When adding a new model or analysis to Prosa, please extend the corresponding directory. -For example, the schedulability analysis for global scheduling with release jitter is organized as follows. +``` +./create_makefile.sh +``` -- **model/schedule/global/jitter:** Definitions and lemmas for global scheduling with release jitter. -- **analysis/global/jitter:** Analysis for global scheduling with release jitter. -- **implementation/global/jitter:** Implementation of the concrete scheduler with release jitter. +Second, compile the library. -## Generating HTML Documentation +``` +make -j +``` + +## Documentation + +Up-to-date documentation for all branches of the main Prosa repository is available at <https://prosa.mpi-sws.org/branches>. -The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with `Make`: -```$ make html -j 4``` *Documentation with proofs* +## Generating HTML Documentation + +The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with the provided `Makefile`: -```$ make gallinahtml -j 4``` *Documentation without proofs* +- `make htmlpretty -j` --- pretty documentation based on CoqdocJS (can hide/show proofs), +- `make gallinahtml -j` --- just the specification, without proofs, +- `make html -j` --- full specification with all proofs. -```$ make htmlpretty -j 4``` *Pretty documentation (can also hide/show proofs)* -Since Coqdoc requires object files as input, please make sure that the code is compilable. +Since Coqdoc requires object files (`*.vo`) as input, please make sure that the code is compilable. ## Commit and Development Rules +We very much welcome external contributions. Please don't hesitate to [get in touch](http://prosa.mpi-sws.org/get-in-touch.html)! + +To make things as smooth as possible, here are a couple of rules and guidelines that we seek to abide by. + 1. Always follow the project [coding and writing guidelines](doc/guidelines.md). -2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, but going forward we should strive to keep it working at all times. +2. Make sure the master branch "compiles" at each commit. This is not true for the early history of the repository, and during certain stretches of heavy refactoring, but going forward we should strive to keep it working at all times. + +3. It's ok (and even recommended) to develop in a (private) dirty branch, but clean up and rebase (i.e., `git-rebase -i`) on top of the current master branch before opening a merge request. + +4. Create merge requests liberally. No improvement is too small or too insignificant for a merge request. This applies to documentation fixes (e.g., typo fixes, grammar fixes, clarifications, etc.) as well. -3. It's ok to develop in a (private) dirty branch, but then clean up and `git-rebase -i` on top of the current master before merging your work into master. +5. If you are unsure whether a proposed change is even acceptable or the right way to go about things, create a work-in-progress (WIP) merge request as a basis for discussion. A WIP merge request is prefixed by "WIP:". -4. It's usually a good idea to ask first on the mailing list before merging a substantial change. +6. We strive to have only "fast-forward merges" without merge commits, so always rebase your branch to linearize the history before merging. (WIP branches do not need to be linear.) -5. Pushing fixes, small improvements, etc. is always ok. +7. Recommendation: Document the tactics that you use in the [list of tactics](doc/tactics.md), especially when introducing/using non-standard tactics. -6. Document the tactics that you use in the [list of tactics](doc/tactics.md). +8. If something seems confusing, please help with improving the documentation. :-) -7. Whenever you have time available, please help with extending the documentation. :-) \ No newline at end of file +9. If you don't know how to fix or improve something, or if you have an open-ended suggestion in need of discusion, please file a ticket. diff --git a/classic/README.md b/classic/README.md new file mode 100644 index 0000000000000000000000000000000000000000..11d51e6b3680a1ad973c9ba6fb90f4cf73c4c105 --- /dev/null +++ b/classic/README.md @@ -0,0 +1,48 @@ +# Classic Prosa + +This module contains the Coq specification & proof development of the Prosa project as presented in the ECRTS'16 paper by Cerqueira et al. + +- Felipe Cerqueira, Felix Stutz, and Björn Brandenburg, “[Prosa: A Case for Readable Mechanized Schedulability Analysis](https://www.mpi-sws.org/~bbb/papers/pdf/ecrts16f.pdf)â€, *Proceedings of the 28th Euromicro Conference on Real-Time Systems (ECRTS 2016)*, pp. 273–284, July 2016. + +This "classic" version of Prosa has since been superseded by a restructuring and refactoring effort that took place throughout most of 2019 in the context of the [RT-Proofs project](https://rt-proofs.inria.fr/) (kindly funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively). + +For the sake of historical completeness, and since not all "classic" proofs have (yet) been ported to the new Prosa base, "classic" Prosa is still included in the master branch of Prosa of the time being. + +## Directory Structure + +The Classic Prosa directory was intended to be organized in a hierarchy: while generic, reusable foundations stay in the upper levels, definitions for specific analyses may be found deeper in the directory tree. However, this organizational principle is not consistently followed due to historical developments. + +### Base Directories + +Classic Prosa contains the following base directories: + +- **classic/model/:** Specification of task and scheduler models, as well as generic lemmas related to scheduling. + +- **classic/analysis/:** Definition, proofs and implementation of schedulability analyses. + +- **classic/implementation/:** Instantiation of each schedulability analysis with concrete task and scheduler implementations. +Instantiating the main theorems in an assumption free environment shows the absence of contradictory assumptions in the proofs. + +### Internal Directories + +The major concepts in classic Prosa are specified in the *classic/model/* folder. + +- **classic/model/arrival:** Arrival sequences and arrival bounds +- **classic/model/schedule:** Definitions and properties of schedules + +Inside *classic/model/schedule*, one can find the different classes of schedulers. + +- **classic/model/schedule/uni:** Uniprocessor scheduling. +- **classic/model/schedule/global:** Global scheduling. +- **classic/model/schedule/partitioned:** Partitioned scheduling. +- **classic/model/schedule/apa:** APA scheduling. + +For example, the schedulability analysis for global scheduling with release jitter is organized as follows. + +- **classic/model/schedule/global/jitter:** Definitions and lemmas for global scheduling with release jitter. +- **classic/analysis/global/jitter:** Analysis for global scheduling with release jitter. +- **classic/implementation/global/jitter:** Implementation of the concrete scheduler with release jitter. + +## Extending Prosa + +Please do not extend this classic version of Prosa in ongoing or future work. As of 2019, all efforts should now be focused on the new, restructured base.