Skip to content
Snippets Groups Projects
Felipe Cerqueira's avatar
Felipe Cerqueira authored
- Removed unnecessary assumption in RTA about task precedence/no intra-task parallelism.
- Scheduler models and analyses are organized in separate modules/folders.
- Added RTA for FP and EDF for schedulers with release jitter.
- The scheduling invariants were split into more fine-grained assumptions:
  (a) scheduler is work-conserving
  (b) scheduler enforces FP/JLDP priority X
- New helper lemmas about counting, and sorted/uniq lists
- Inclusion of tactics feed and feed_n (see documentation).
- Added a Makefile generator
32126a75
History

RT-PROOFS

This repository contains the main Coq proof spec & proof development of the RT-PROOFS project.

Plan

For now, this is more or less just a "code dump" with a flat hierarchy to get things started.

Going forward, the goal is to both

  • restructure the repository as it grows in scope, and to

  • add significant documentation to make it easier to bring new collaborators who are not yet familiar with Coq into the project.

Commit and Development Rules

  1. Always follow the project coding and writing guidelines.

  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.

  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.

  4. It's usually a good idea to ask first on the mailing list before merging a substantial change.

  5. Pushing fixes, small improvements, etc. is always ok.

  6. Document the tactics that you use in the list of tactics.