Commits · 5b509b250d61b2dc2c6d4ecc303760f3c73d753c · Pierre Roux / PROSA - Formally Proven Schedulability Analysis

04 Aug, 2020 4 commits
- update opam spec file · 5b509b25
  Björn Brandenburg authored Aug 04, 2020
  
  5b509b25
- CI: remove older versions no longer supported · 131f1998
  Björn Brandenburg authored Aug 04, 2020
  
  131f1998
- CI: add new jobs for mathcomp 1.11 and Coq 8.12 · e48ad1ec
  Björn Brandenburg authored Aug 04, 2020
  
  e48ad1ec
- CI: don't hardcode version multiple times · 7cd0103c
  Björn Brandenburg authored Aug 04, 2020
  
  7cd0103c
30 Jul, 2020 1 commit
- add ideal uniprocessor reference scheduler · e8c4edca
  Björn Brandenburg authored Apr 01, 2020
  
  e8c4edca
09 Jul, 2020 4 commits
- replace_at does not need decidable equality · ff55c0a7
  Björn Brandenburg authored Jul 09, 2020
  
  ff55c0a7
- add readiness properties and facts on backlogged · e1426920
  Björn Brandenburg authored Apr 01, 2020
```
add lemmas on consistency of backlogged jobs set

add notion of a non-clairvoyant readiness model
```
  e1426920
- add notion of a shared identical schedule prefix · e236efb1
  Björn Brandenburg authored Apr 02, 2020
  
  e236efb1
- additional minor lemmas on job arrivals · a77c7c71
  Björn Brandenburg authored Apr 01, 2020
  
  a77c7c71
08 Jul, 2020 5 commits
- add trivial replace_at definition rewriting lemma · 93b40629
  Björn Brandenburg authored Apr 02, 2020
  
  93b40629
- generalize notion of jobs_backlogged_at · 87f6ec3c
  Björn Brandenburg authored Mar 31, 2020
```
This is a general definition and not specific to a particular
implementation.
```
  87f6ec3c
- add function to generate uniprocessor schedules · 6739de4f
  Marco Perronet authored Mar 31, 2020 and Björn Brandenburg committed Jul 08, 2020
  
  6739de4f
- update ack config · 953b38b7
  Björn Brandenburg authored Apr 03, 2020
  
  953b38b7
- make --only-classic skip prosa.implementation module · 967c6d07
  Björn Brandenburg authored Mar 31, 2020
  
  967c6d07
30 Jun, 2020 1 commit
- guidelines: add a section about backward vs forward reasoning · 7d507ed0
  Marco Maida authored Jun 30, 2020 and Björn Brandenburg committed Jun 30, 2020
  
  7d507ed0
19 May, 2020 5 commits
- fix injection warnings in single-cost sustainability reduction · 3c00f057
  Björn Brandenburg authored May 19, 2020
  
  3c00f057
- prosa classic: move import out of section to fix warning · 030af432
  Björn Brandenburg authored May 19, 2020
  
  030af432
- fix some warnings in prosa.classic.util.tactics · 60286128
  Björn Brandenburg authored May 19, 2020
  
  60286128
- suppress warnings in prosa.util.seqset · 1c73b853
  Björn Brandenburg authored May 19, 2020
```
...by adding the -projection-no-head-constant flag to the build settings.
```
  1c73b853
- fix warnings in prosa.util.search_arg · 2da5f091
  Björn Brandenburg authored May 19, 2020
  
  2da5f091
11 May, 2020 1 commit
- resolve warnings related to eq_big_perm · 9bd265d8
  Vedant Chavda authored May 11, 2020 and Björn Brandenburg committed May 11, 2020
```
change it to perm_big
```
  9bd265d8
03 Apr, 2020 2 commits
- Added spell command to Makefile · b1459e3c
  Marco Maida authored Apr 03, 2020
  
  b1459e3c
- Removed verbatim text from spell-checker · 3709e9b3
  Marco Maida authored Apr 03, 2020
  
  3709e9b3
02 Apr, 2020 1 commit
- Improved guideline · 9ce7a967
  Marco Maida authored Apr 03, 2020
  
  9ce7a967
01 Apr, 2020 2 commits
- Added guideline · 08546417
  Marco Maida authored Apr 01, 2020
  
  08546417
- Fixed broken intervals · fa2f1873
  Marco Maida authored Apr 01, 2020
  
  fa2f1873
31 Mar, 2020 2 commits
- don't rename index.html to indexpage.html in coqdocjs target · f645d086
  Björn Brandenburg authored Mar 31, 2020
  
  f645d086
- add notion of hyperperiod for periodic tasks · 9fa2acb3
  Vedant Chavda authored Mar 26, 2020 and Björn Brandenburg committed Mar 31, 2020
  
  9fa2acb3
27 Mar, 2020 1 commit
- Delete duplications of search space · fedef925
  Sergey Bozhko authored Mar 11, 2020
  
  fedef925
10 Mar, 2020 1 commit
- Remove hardcoded ideal processor model from aRTA · aae570d0
  Sergey Bozhko authored Mar 10, 2020 and Sergey Bozhko committed Mar 10, 2020
  
  aae570d0
27 Feb, 2020 1 commit
- Fix CI · 041d30a2
  Pierre Roux authored Feb 27, 2020
  
  041d30a2
26 Feb, 2020 1 commit
- Add an Opam file · 979772bb
  Pierre Roux authored Jan 17, 2020
  
  979772bb
19 Feb, 2020 1 commit
- Work-conservation transformation and proof. · 57806e76
  Marco Maida authored Feb 10, 2020 and Marco Maida committed Feb 19, 2020
```
Added the proof of correctness of the work-conservation transformation for an ideal uniprocessor schedule.
```
  57806e76
11 Feb, 2020 1 commit
- Add LICENSE · c8cff9a3
  Björn Brandenburg authored Feb 11, 2020
  
  c8cff9a3
10 Feb, 2020 1 commit
- Restructure and document util.bigcat · 7dc8adcc
  Marco Maida authored Feb 10, 2020 and Björn Brandenburg committed Feb 10, 2020
  
  7dc8adcc
23 Jan, 2020 1 commit
- Compile with coq dev · 12f79735
  Pierre Roux authored Jan 23, 2020
  
  12f79735
21 Jan, 2020 1 commit
- Compile with mathcomp 1.10 · aae959e6
  Pierre Roux authored Jan 21, 2020
  
  aae959e6
21 Dec, 2019 1 commit
- Add periodic task model · ee05f255
  Björn Brandenburg authored Dec 21, 2019
  
  ee05f255
20 Dec, 2019 2 commits
- Improve readability of analysis · 49036f00
  Sergey Bozhko authored Dec 20, 2019
  
  49036f00
- Restructure facts.model · 5fc2e7dd
  Sergey Bozhko authored Dec 20, 2019
  
  5fc2e7dd