README.md 2.82 KB
Newer Older
1
2
3
4
# RT-PROOFS

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

5
## Directory Structure
6

7
8
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.
9

10
### Base Directories
11

12
Currently, Prosa contains the following base directories:
13

14
15
16
- **model/:** Specification of task and scheduler models, as well as generic lemmas related to scheduling.
	  
- **analysis/:** Definition, proofs and implementation of schedulability analyses.
17

18
19
- **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.
20

21
22
### Internal Directories

Felipe Cerqueira's avatar
Felipe Cerqueira committed
23
The major concepts in Prosa are specified in the *model/* folder.
24

Felipe Cerqueira's avatar
Felipe Cerqueira committed
25
26
27
28
29
30
31
32
33
- **model/arrival:** Arrival sequences and arrival bounds
- **model/schedule:** Definitions and properties of schedules

Inside *model/schedule*, you can find the different classes of schedulers.

- **model/schedule/uni:** Uniprocessor scheduling.
- **model/schedule/global:** Global scheduling.
- **model/schedule/partitioned:** Partitioned scheduling.
- **model/schedule/apa:** APA scheduling.
34
35
36
37
38
39

### Extending Prosa

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.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
40
- **model/schedule/global/jitter:** Definitions and lemmas for global scheduling with release jitter.
41
42
- **analysis/global/jitter:** Analysis for global scheduling with release jitter.
- **implementation/global/jitter:** Implementation of the concrete scheduler with release jitter. 
43

44
45
46
47
48
49
50
51
## Generating HTML Documentation

The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with `Make`:

```$ make gallinahtml -j4```

Since Coqdoc requires object files as input, please make sure that the code is compilable.

52
53
54
55
56
57
58
59
60
61
## Commit and Development Rules

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. 

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.

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

64
65
66
6. Document the tactics that you use in the [list of tactics](doc/tactics.md).

7. Whenever you have time available, please help with extending the documentation. :-)