Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • classic-prosa
  • wip-hunspell
  • prepare_MC_PR
  • tutorial
  • fset
  • embed_arr_seq_uniq
  • v0.5
  • v0.4
  • v0.3
  • v0.2
  • v0.1
12 results
Compare
Felipe Cerqueira's avatar
Major Commit - Prosa v0.2
Felipe Cerqueira authored 
- Add definitions related to APA scheduling
- Prove correctness of reduction-based RTA for APA scheduling (FP and EDF)
- Add implementation of a weak APA scheduler
- Update definition of taskset to assume uniqueness
- Modify names and comments to improve readability
- Remove strong assumptions about priority order in FP scheduling
- Add tests with FP RTA for every model
- Add tests for RTA with parallel jobs
f7a79913
History
Felipe Cerqueira's avatar f7a79913
History
Name Last commit Last update
analysis
doc
implementation
model
util
.gitignore
Makefile
README.md
_CoqProject
create_makefile.sh
README.md

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.