re-organize analysis module (!69) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Merged Björn Brandenburg requested to merge analysis-reorg into master 5 years ago

Dec 10, 2019
- define dynamic self-suspension model · d0d593ec
  Björn Brandenburg authored 5 years ago
  
  d0d593ec
- define readiness for jobs with self-suspensions · f4c8366a
  Björn Brandenburg authored 5 years ago
  
  ...and define a job's total suspension time.
  f4c8366a
- define notion of job progress / lack of progress · 0c43c153
  Björn Brandenburg authored 5 years ago
  
  0c43c153
- augment model with definitions of well-known priority policies · 2e447612
  Björn Brandenburg authored 5 years ago
  
  2e447612
- CI: compile classic and new Prosa separately · d0709163
  Björn Brandenburg authored 5 years ago
  
  For improved parallelism and nicer documentation.
  d0709163
- CI: enable spell checker for comments · 61b3b10e
  Björn Brandenburg authored 5 years ago
  
  61b3b10e
- address spell-checking issues in analysis · d1f8192c
  Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago
  
  d1f8192c
- address spell-checking issues in results · 54220d8c
  Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago
  
  54220d8c
- address spell-checking issues in util · 6cb786f2
  Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago
  
  6cb786f2
- address spell-checking issues in EDF optimality proof · fbcbb997
  Björn Brandenburg authored 5 years ago
  
  fbcbb997
- address spell-checking issues in model module · 22a76ba8
  Björn Brandenburg authored 5 years ago
  
  22a76ba8
- address spell-checker complaints in behavior module · ce01dfe1
  Björn Brandenburg authored 5 years ago
  
  ce01dfe1
- add tool for extracting comments and a word list · 085ea530
  Björn Brandenburg authored 5 years ago
  
  085ea530
- re-organization of the analysis module, part 1 · 064a1c75
  Björn Brandenburg authored 5 years ago
  
  This is not yet the final organization, but already an improvement. Move main high-level results to separate top-level `results` module. Rationale: Let's make it very clear where to find the main, high-level results in Prosa, and at the same time let's declutter the analysis namespace. Other notable change, apart from moving files around: - move two key analysis definitions to analysis.definitions - split RBF definition and facts into separate files - move facts about ideal schedule to ideal_schedule.v
  064a1c75

re-organize analysis module

Merge request reports

Activity